How can equality be defined in first-order logic?

Question

This Wikipedia page about first-order logic mentions Leibniz's law as one of the axiom schemas of equality. But Leibniz's law states that $\forall x\forall y(\forall P(P(x)\leftrightarrow P(y))\leftrightarrow x=y)$. There has been a quantification over predicates which is not allowed in first-order logic. Could someone please point out what I could've gotten wrong? Is the definition of equality formulated in a different manner?

Answer 1

Specifically, what we want is $\forall P.P(x)\land (x = y) \to P(y)$. Note that this is equivalent to: $(x=y)\to(\forall P.P(x)\to P(y))$. Given this, it is easy to show that $(x=y) \to (\forall P.P(x)\leftrightarrow P(y))$. $(\forall P.P(x)\leftrightarrow P(y))\to (x=y)$ is trivial to show simply by instantiating $P$ as $P(z)=(x=z)\land(z=y)$. (Reflexivity, i.e. $\forall x.x=x$ is also taken as an axiom usually and does not follow from the above.)

The benefit of $\forall P.P(x)\land (x=y)\to P(y)$ is that we can commute the $\forall$ with the $\forall$s I've left implicit for $x$ and $y$, i.e. we have $\forall P.\forall x,y.P(x)\land (x=y)\to P(y)$. Now there's still the problem that you've pointed out. Quantifying over predicates, i.e. the $\forall P$ is not allowed in first-order logic. It is allowed in second-order logic, but that is not the logical system that is usually used. Instead, in a fairly common move (e.g. the induction rule in first-order Peano arithmetic), we move the quantification over predicates to the meta-level. What we say instead is that for every formula (i.e. piece of syntax in the first-order language) $\varphi$, $\forall x,y.\varphi(x)\land (x=y)\to \varphi(x)$ is an axiom. This produces an axiom schema, or, alternatively it is often presented as a rule of inference. This is strictly weaker than the second-order axiom (with respect to full semantics at least). The second-order axiom pins equality down to being equality in the semantics. This first-order axiom schema only pins equality down to being an equivalence relation that respects every formula we can state in the first-order language.

As far as provability is concerned, there isn't really any difference between the second-order quantification or the axiom schema. Syntactically, we can only talk about things we can write down anyway. Semantically, we could add equality to the logical framework itself rather than just provide an axiom schema. We can then state that by definition the equality operator in the logic gets interpreted as equality semantically. This is safe because we could always just quotient any model by the equivalence relation that is the interpretation of the equality operator and have a suitably equivalent model where the equality operator is interpreted as equality in the semantics. In other words, making this choice doesn't lose completeness.