# How can equality be defined in first-order logic?

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?

• Do they state it that way in the very wikipedia page you link? As usual, a naturally second-order idea becomes a schema when expressed in a first order context. Feb 25, 2019 at 4:56
• Not exactly, but it started with "for any variable $x$ and $y$ and formula $\varphi$" which (correct me if I'm wrong) is a quantification even if it wasn't explicitly shown in notation. Feb 25, 2019 at 5:06
• First off, this is quantifying over formulas, not properties. But the main thing is that this quantification occurs in the metatheory: we are saying "for any formula $\phi$, the following is an axiom" not "'for all properties P, blah blah' is an axiom". This is called a schema and they occur all over the place. Note it is technically an infinite number of axioms, whereas the second order version would be a single axiom. Feb 25, 2019 at 5:10

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.