On What "Is" Is, Part 2

As is well-known, the Leibnizian definition of identity, using the defining formula $\mathrm{\forall }X(Xx\to Xy)$, is second-order. It quantifies over properties. One can get further information about this kind of definition of identity by seeing how it can be proved in a theory in which identity is already definable. In fact, one can consider any formula which behaves "like identity" in a given (second-order) theory, and then show that this formula is provably equivalent to both $\mathrm{\forall }X(Xx\to Xy)$ and to $\mathrm{\forall }R(\mathrm{\forall }zRzz\to Rxy)$.

Suppose that $L$ is a second-order language, where we do not assume $=$ is a primitive. Let $T$ be an $L$-theory containing Comprehension for all arities (we just need unary and binary below).

Definition: An $L$-formula $x\approx y$ is a Leibniz formula in $T$ just in case both the following hold:

(a) $T⊢\mathrm{\forall }x(x\approx x)$
(b) $T⊢\mathrm{\forall }x\mathrm{\forall }y(x\approx y\to (\varphi (z/x)\to \varphi (z/y))$,

for any $L$-formula $\varphi (z)$.

Clearly, these conditions (a) and (b) are the formal syntactic properties of $=$. That is, reflexivity and substitutivity.

Lemma 1: Let $x\approx y$ be a Leibniz formula in $T$. Then:

(i) $T⊢\mathrm{\forall }x\mathrm{\forall }y(x\approx y\leftrightarrow \mathrm{\forall }X(Xx\to Xy))$
(ii) $T⊢\mathrm{\forall }x\mathrm{\forall }y(x\approx y\leftrightarrow \mathrm{\forall }R(\mathrm{\forall }zRzz\to Rxy))$

Proof
Part (i) By comprehension, $\mathrm{\forall }y\mathrm{\exists }X\mathrm{\forall }x(Xx\leftrightarrow x\approx y)$. Let $a$ be such that $\mathrm{\exists }X\mathrm{\forall }x(Xx\leftrightarrow x=a)$. Let $A$ be such that $\mathrm{\forall }x(Ax\leftrightarrow x\approx a)$. Thus, $Aa\leftrightarrow a\approx a$. Since $a\approx a$, we have $Aa$. Let $b$ be such that $\mathrm{\neg }(a\approx b)$. By symmetry of $\approx$, $\mathrm{\neg }(b\approx a)$. So, $\mathrm{\neg }Ab$. So, $Aa\wedge \mathrm{\neg }Ab$. Hence, $\mathrm{\neg }(a\approx b)\to (Aa\wedge \mathrm{\neg }Ab)$. So, $\mathrm{\neg }(a\approx b)\to \mathrm{\exists }X(Xa\wedge \mathrm{\neg }Xb)$. Since $a$ and $b$ are arbitrary, $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\neg }(x\approx y)\to \mathrm{\exists }X(Xx\wedge \mathrm{\neg }Xy)$. By contraposition, $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }X(Xx\to Xy)\to x\approx y)$, as required. (Notice that this requires simply that $\approx$ be reflexive and symmetric.)

For the converse, suppose $a\approx b$ and $Xa$. By substitutivity, $Xb$. So, $Xa\to Xb$. So, $\mathrm{\forall }X(Xa\to Xb)$. So, $a\approx b\to \mathrm{\forall }X(Xa\to Xb)$. So, $\mathrm{\forall }x\mathrm{\forall }y(x\approx y\to \mathrm{\forall }X(Xx\to Xy)$, as required. (This requires substitutivity.) QED.

Part (ii). First, we have $\mathrm{\forall }z(z\approx z)$. Suppose that $\mathrm{\forall }R(\mathrm{\forall }zRzz\to Rab)$. By comprehension, $\mathrm{\exists }R\mathrm{\forall }x\mathrm{\forall }y(Rxy\leftrightarrow x\approx y)$. So, $\mathrm{\forall }z(z\approx z)\to a\approx b$. So, $a\approx b$. So, $\mathrm{\forall }R(\mathrm{\forall }zRzz\to Rxy)\to a\approx b$. So, $\mathrm{\forall }x\mathrm{\forall }y(\mathrm{\forall }R(\mathrm{\forall }zRzz\to Rxy)\to x\approx y)$, as required. (Notice that this requires merely that $\approx$ be reflexive.)

For the converse, suppose $a\approx b$ and $\mathrm{\forall }zRzz$. So, $Raa$. By substitutivity, $Rab$. So, $\mathrm{\forall }zRzz\to Rab$. So, $\mathrm{\forall }R(\mathrm{\forall }zRzz\to Rab)$. So, $a\approx b\to \mathrm{\forall }R(\mathrm{\forall }zRzz\to Rab)$. So, $\mathrm{\forall }x\mathrm{\forall }y(x\approx y\to \mathrm{\forall }R(\mathrm{\forall }zRzz\to Rxy)$, as required. (This requires substitutivity.) QED.

There is a sense in which the notion of being a Leibniz formula is unique. For:

Lemma 2: Let $x\approx y$ and $x\equiv y$ be Leibniz formulas in $T$. Then:

$T⊢\mathrm{\forall }x\mathrm{\forall }y(x\approx y\leftrightarrow x\equiv y)$

Proof. By symmetry, it is no loss of generality to prove just one direction. Suppose $x\approx y$. An instance of substititivity is $x\approx y\to (x\equiv x\to x\equiv y)$. (Take $\varphi (z)$ to be $x\equiv z$. Then $\varphi (z/x)$ is $x\equiv x$ and $\varphi (z/y)$ is $x\equiv y$.) So, $x\equiv x\to x\equiv y$. But, we already have $x\equiv x$. So, $x\equiv y$, as required. QED.

Thus, any two Leibniz formulas (in $T$) are provably equivalent (in $T$).