First-order logic and Peano Arithmetic paradox

Question

I'm working through the Stanford Introduction to Logic course, and seem to have proved that all natural numbers are equal to zero: Ax.(x = 0). Obviously, this is incorrect, but I can't see how. My proof is by induction:

• Base case: 0 = 0 by premise
• Inductive case: Ax.((x = 0) -> (s(x) = 0))
  • If we assume that all natural numbers equal zero: x = 0
  • Then, since all natural numbers equal zero, the successor of any natural number also equals zero: s(x) = 0 by simple substitution
• Conclusion: Ax.(x = 0)

I worked this up formally in Stanford's Fitch editor as well:

Can anyone explain my error? Thank you.

Answer 1

David C. Ullrich had the most useful answer, which I'll repeat here: The Universal Introduction on line 3 is invalid because x is free in the active assumption x = 0. Thank you for finding the error!

Answer 2

When you write “If we assume that all natural numbers equal zero”, you are assuming the thing that you want to prove.

A proof by induction would be as follows:

• first you prove that the assertion holds when $x=0$ (as you did);
• then you prove that if the statement holds for $x$, then it also holds for $s(x)$.

And it's here where the problem lies, because one of the Peano axioms states that $0$ is never of the form $s(x)$.

Answer 3

The informal version is just not how induction works. In proving $\forall x.x=0$ you're allowed to assume $x=0$, then you're required to prove $s(x)=0$. You're certainly not allowed to assume $\forall x.x=0$. Proofs by induction look sorta like they assume what they want to prove, but they don't, because of the difference between $x=0$ and $\forall x.x=0$.

That's if you're trying to prove $\forall x.x=0$. When Carlos pointed this out you mentioned something about Implication Introduction. But you didn't discharge the assumption!! As pointed out, you're allowed to assume $\forall x.x=0$ if you're trying to prove $\forall x.x=0\implies \forall x.x=0$.

The error, or at least one error, in the formal version is an invalid application of UI: The first UI is invalid because $X$ is free in an active assumption. (An informal version of that UI thing, as used by actual people in actual proofs: To prove $\forall xp(x)$, prove $p(x)$ without assuming anything about $x$.)