Knowledge out of nowhere: a note on Löb's theorem

Löb's theorem states that for any extension of Peano arithmetic, any “reasonable” intra-system definition of the term ‘provable’ and any statement \(P\):

If \(PA \vdash (Provable(P) \rightarrow P)\) (“\(PA\) proves that (a proof of \(P\) implies the truth of \(P\))...”), then \(PA \vdash P\) (“\(PA\) proves \(P\)”).

Example. Let \(P\) be “\(0 = 1\)”. Assume \(PA \vdash \lnot Provable(0 = 1)\) (i.e. PA proves that there is no proof of \(0 = 1\), or: \(PA\) proves its own consistency.)

Then by explosion, \(PA \vdash (Provable(0 = 1) \rightarrow 0 = 1)\), and by Löb's theorem, \(PA \vdash 0 = 1\) (i.e. \(PA\) is inconsistent). This result is Gödel's second incompleteness theorem.

There’s a stronger consequence at play from this strategy here — a consistent extension of \(PA\) can’t prove the unprovability of anything within it, even what looks like blindingly obvious examples.

Consider the example of \(PA_x\), which is exactly Peano arithmetic with the introduction of an additional named constant, \(x\). Notably, \(x\) does not appear in any of the axioms. \(PA_x\) implies nothing about \(x\) that it doesn’t already imply about other numbers.

Then by the same reasoning, if \(PA_x \vdash \lnot Provable(x = 0)\), then \(PA_x \vdash x = 0\). This conclusion is ridiculous, since from the “outside view” we can see that there should be no proof of \(x = 0\) within the system. Given a model of \(PA\) (such as the natural numbers), we can easily construct a model of \(PA_x\) where \(x \neq 0\).

Assuming the consistency of \(PA_x\) (which trivially follows from the consistency of \(PA\)), this implies that \(PA_x \not \vdash \lnot Provable(x = 0)\). But why can’t \(PA_x\) prove the unprovability of the statement?

Credit: Geometry Daily

Firstly, our “outside view” intuition is a little faulty here — as usual, with many of these paradoxes, we are thinking about the natural numbers as a model for \(PA_x\). But indeed there are necessarily other models of \(PA_x\) where \(Provable(x = 0)\), namely because once we step into degenerate models, whatever neat definition of “provability” we had (e.g. statements about finite chains of proof steps) turns degenerate as well.

More importantly, once we accept that a model-theoretic “\(x = 1\) is possible” view of the situation is not a statement about provability, and try to prove that there is no proof of \(x = 0\) from the axioms, this turns out to be a little harder than it first looks.

For example, we might attempt an inductive proof that statements of the form “\(x = \Phi\)”, where the formula \(\Phi\) doesn't contain \(x\), cannot be proven from the axioms. But then the inductive step (prove that statements of this form cannot follow from statements not of this form) fails here, since “\(x + 1 = 1 \vdash x = 0\)”. (And this isn’t even counting statements with logical operators, such as “\(3 + 2 = 5 \land x = 0\)”.)

Trying to inductively prove that “statements containing \(x\) never follow from the axioms” is futile, since “\(x \neq x + 1\)” follows from the axioms. Indeed, by universal instantiation, so is any statement “\(\Phi(x)\)” where \(PA \vdash \forall z \cdot \Phi(z)\) — and it’s not difficult to prove (by induction over proofs) the reverse: if \(PA \vdash \Phi(x)\), then \(PA \vdash \forall z \cdot \Phi(z)\).

This points to the source of our difficulty: proving \(\lnot Provable(x = 0)\) is as difficult as proving \(\lnot Provable(\forall z \cdot z = 0)\). And the latter statement is logically equivalent to “\(\lnot Provable(0 = 1)\)” (proof omitted).

So proving that we don’t know anything about the unreferenced constant \(x\) is just as hard as proving that \(PA_x\) is consistent.