On What "Is" Is, Part 2

As is well-known, the Leibnizian definition of identity, using the defining formula $\forall X(Xx \rightarrow 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 $\forall X(Xx \rightarrow Xy)$ and to $\forall R(\forall zRzz \rightarrow 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 \vdash \forall x(x \approx x)$
(b) $T \vdash \forall x \forall y(x \approx y \rightarrow (\phi(z/x) \rightarrow \phi(z/y))$,

for any $L$-formula $\phi(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 \vdash \forall x \forall y(x \approx y \leftrightarrow \forall X(Xx \rightarrow Xy))$
(ii) $T \vdash \forall x \forall y(x \approx y \leftrightarrow \forall R(\forall z Rzz \rightarrow Rxy))$

Proof
Part (i) By comprehension, $\forall y \exists X \forall x(Xx \leftrightarrow x \approx y)$. Let $a$ be such that $\exists X \forall x(Xx \leftrightarrow x = a)$. Let $A$ be such that $\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 $\neg(a \approx b)$. By symmetry of $\approx$, $\neg(b \approx a)$. So, $\neg Ab $. So, $Aa \wedge \neg Ab$. Hence, $\neg (a \approx b) \rightarrow (Aa \wedge \neg Ab)$. So, $\neg(a \approx b) \rightarrow \exists X(Xa \wedge \neg Xb)$. Since $a$ and $b$ are arbitrary, $\forall x \forall y(\neg(x \approx y) \rightarrow \exists X(Xx \wedge \neg Xy)$. By contraposition, $\forall x \forall y(\forall X(Xx \rightarrow Xy) \rightarrow 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 \rightarrow Xb$. So, $\forall X(Xa \rightarrow Xb)$. So, $a \approx b \rightarrow \forall X(Xa \rightarrow Xb)$. So, $\forall x \forall y(x \approx y \rightarrow \forall X(Xx \rightarrow Xy)$, as required. (This requires substitutivity.) QED.

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

For the converse, suppose $a \approx b$ and $\forall z Rzz$. So, $Raa$. By substitutivity, $Rab$. So, $\forall z Rzz \rightarrow Rab$. So, $\forall R(\forall z Rzz \rightarrow Rab)$. So, $a \approx b \rightarrow \forall R(\forall z Rzz \rightarrow Rab)$. So, $\forall x \forall y(x \approx y \rightarrow \forall R(\forall z Rzz \rightarrow 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 \vdash \forall x \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 \rightarrow (x \equiv x \rightarrow x \equiv y)$. (Take $\phi(z)$ to be $x \equiv z$. Then $\phi(z/x)$ is $x \equiv x$ and $\phi(z/y)$ is $x \equiv y$.) So, $x \equiv x \rightarrow 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$).