3
$\begingroup$

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?

$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$ Feb 25, 2019 at 4:56
  • $\begingroup$ 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. $\endgroup$
    – mjtsquared
    Feb 25, 2019 at 5:06
  • $\begingroup$ 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. $\endgroup$ Feb 25, 2019 at 5:10

1 Answer 1

6
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thanks, I guess my problem was that I did not look up what an axiom schema really was. You highlighted it for me. $\endgroup$
    – mjtsquared
    Feb 25, 2019 at 7:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .