A principle formulated by philosopher and mathematician Gottfried Wilhelm Leibniz (1646–1716). The principle states that if two objects are indiscernible in the sense that they instantiate precisely the same properties, then the two objects are one and the same, i.e., are identical, whence Leibniz’ law is known as the identity of indiscernibles. Formally, with quantifiers ranging over properties $P$, the principle can be described as:

• • $\forall P\left(Px\leftrightarrow Py\right)\to x=y$

Leibniz’ law is sometimes phrased as not only the principle of identity of indiscernibles, but as the conjunction of this principle with its converse, the indiscernibility of identicals, that if two elements are identical, then they are indiscernible, that is, share precisely the same properties. The indiscernibility of identicals can be represented as:

• • $x=y\to \forall P\left(Px\leftrightarrow Py\right)$

or in first-order logic, by the scheme,

• • $x=y\to \left(\phi \left(x\right)\leftrightarrow \phi \left(y\right)\right)$