How to prove $x=5$ using the Peano Axioms?

Question

This question relates to Proposition V of Gödel's 1931 Incompleteness theorem (and another one posted on math.stackexchange here ) which says:

For every recursive relation $ R(x_{1},...,x_{n})$ there is an n-ary "predicate" $r$ (with "free variables" $u_1,...,u_n$) such that, for all n-tuples of numbers $(x_1,...,x_n)$, we have:

$$R(x_1,...,x_n)\Longrightarrow Bew[Sb(r~_{Z(x_1)}^{u_1}\cdot\cdot\cdot~_{Z(x_n)}^{u_n})] $$

$$\overline{R}(x_1,...x_n)\Longrightarrow Bew[Neg~Sb(r~_{Z(x_1)}^{u_1}\cdot\cdot\cdot~_{Z(x_n)}^{u_n})]$$

So one example of $R$ (in 1 variable) be... $$R(x) =(x = 5)$$ Proposition V states that there is a corresponding proof (proof-schema?) $r$ in 1 variable (say ${u_1}$) that is true when $Z(5)$ is substituted for ${u_1}$.

My question is this: would does this r look like? In other words what are the specific steps of a proof that uses only Peano Axioms and proves that a variable ${u_1}$ is equal to 5?

For what its worth I've read and understood the common proof that '1+1 = 2' using nothing but Peano Axioms (and even come up with one of my own). However, I have no idea how you would perform this proof using a variable.

Answer 1

Let me rephrase this in a clearer way first (the original source isn't always the best way to learn a proof!):

For each recursive relation $R\subseteq\mathbb{N}^n$, there is some formula $\varphi(x_1,...,x_n)$ such that for each $a_1,...,a_n\in\mathbb{N}$ we have:

• If $R(a_1,...,a_n)$ holds then $T$ proves $\varphi(\underline{a_1},...,\underline{a_n})$, and

• If $R(a_1,...,a_n)$ fails then $T$ proves $\neg\varphi(\underline{a_1},...,\underline{a_n})$.

I'm using the more modern notation "$\underline{k}$" for the numeral $$S(S(...(S(0))))\quad\mbox{($k$ many $S$s)}$$ corresponding to $k$ - this is your "$Z(k)$" - and I'm suppressing the substitution notation. Also, my "$T$" is whatever appropriate theory we're using - e.g. first-order Peano arithmetic.

---

In any given example - such as your case $R=\{5\}$ (so $n=1$) - the first step is to find the appropriate $\varphi$; only then do we look for the appropriate proofs.

In this case the first step is basically trivial: we want to use $$\varphi(x):\quad x=S(S(S(S(S(0)))))$$ (suppressing the subscript on the variable for clarity).

OK, now let's talk about the proofs we hope exist. There are two cases to consider: when $R$ holds, and when $R$ fails. There's only one example of when $R$ holds (namely, $a=5$ - again suppressing the subscript for clarity), and all the failures of $R$ are going to behave identically so I'll just consider $a=3$.

• $a=5$: here we need to give a proof in $T$ of $\varphi(\underline{5})$. Unfolding both $\varphi$ and $\underline{5}$, this is just $$S(S(S(S(S(0)))))=S(S(S(S(S(0))))).$$ And this has a one-line proof (indeed, from the basic logical rules alone - $T$ isn't needed): for any term $t$, we can infer $t=t$ without any hypotheses.

• $a=3$: here we need to give a proof in $T$ of $\neg\varphi(\underline{3})$. Again unfolding everything, what we're trying to prove is $$\neg S(S(S(0)))=S(S(S(S(S(0))))).$$ While equally obvious this is a bit less trivial:

  • First, we prove $\neg 0=S(S(0))$.

  • Next, we prove $$\forall u,v[(\neg u=v)\implies(\neg S(u)=S(v))].$$ (Actually we only need to do this if this statement isn't already an axiom of $T$ - which it often will be.)

  • Now we repeatedly apply the second bulletpoint to the first bulletpoint (e.g. one application gets us from $\neg 0=S(S(0))$ to $\neg S(0)=S(S(S(0)))$). After three iterations, we wind up with $$\neg S(S(S(0)))=S(S(S(S(S(0))))).$$ But this is just $\neg\varphi(\underline{3})$, which is exactly what we wanted!