Gödel's Second Incompleteness Theorem

[SOberhoff]

I see that you have Gödel's Second Incompleteness Theorem weaseled away under "The Gödel statement (optional)". I find the exposition of the second incompleteness theorem given there quite confusing. There is a much better and arguably more computer-sciency proof available. The following is a corrected and cleaned up version of an argument given in Scott Aaronson's Quantum Computing since Democritus:

Given formal system F consider the Turing machine given by the following pseudocode:

P(M) {
  for all proofs p ∈ proofs(F) {
    if p proves that M(M) doesn't halt {
      halt;
    }
  }
}

Claim: If F is consistent, then P(P) doesn't halt.

Proof (by contradiction): Suppose P(P) halts. Then, on the one hand, it must've found a proof in F that P(P) doesn't halt. On the other hand, given that P(P) halts, one can prove this in F by writing out a trace of the computation of P(P) and pointing out that it leads to a terminal state. So both "P(P) halts" and "P(P) doesn't halt" are provable in F, making it inconsistent. ⚡

What's more, there's nothing here that one couldn't arrive at within F itself. Hence "F is consistent ⟹ P(P) doesn't halt" is actually a theorem in F. We can now see that, as long as F is consistent, F's consistency can't be provable in F. For if it was, then by modus ponens "P(P) doesn't halt" would be provable. But then P would eventually find this proof and halt. And as we've just seen that would imply F being inconsistent. ◻

Note that this proof carefully avoids the pitfall of supposing that F's soundness can be formalized. We're only ever using consistency, which is an easily formalized syntactic property.

[SOberhoff]

I've significantly expanded on this idea in an essay that went up on Scott Aaronson's blog: https://www.scottaaronson.com/incompleteness.pdf

[boazbk]

Thanks!! I will take a look at this. I do like to actually show the full on Godel's Theorem with statements about integers, as it provides an important lesson that computation can arise in surprising places.

I am less worried about the difference between consistency and soundness, especially since for students (as opposed to logicians) it is soundness that is the most natural quality. Nonetheless, if I can work this argument simply into the book then I will do it. (I also like the idea of deriving Godel's Theorem in a black box way from an uncomputability result, which allows to obtain the integer version by simply plugging in a different unocomputable funciton, so would want to keep this invariant.)

It does seem to still assume some kind of soundness - that a finite proof that a Turing Machine halts (i.e., by a sequence of configurations) is in fact a valid proof in the system.

That is of course necessary because otherwise you could have a formal system that applies to statements like "Machine M halts on input x" but actually ignores their semantic content and pretend they are statements in some decidable theory such as first order logic. Such a system can still be consistent.

Happy new year!

[SOberhoff]

Unfortunately soundness can't be formalized which creates dire problems for the Second Incompleteness Theorem. You need consistency for that one.

And no, soundness is completely immaterial for the Rosser proofs and the proofs of the Second Incompleteness Theorem.

[boazbk]

Thanks, closing for now. Am planning to go over this chapter in a couple of months and will then have to decide if talking about Rosser and second incompleteness is worth it or not.