12:25
@Amr I think the connection there is pretty tenuous. The inability of PA to prove its own consistency is ultimately derived from the diagonal lemma, which allows sentences to make claims "about themselves" in some sense. We can construct a sentence S which basically says "I am unprovable", and it turns out that S is true if and only if PA is consistent, so the truth of S is equivalent to the unprovability of S which is also equivalent to the consistency of PA.
Basically, if S were provable then it's false ("S is provable" is exactly "not S"), and more strongly if S is provable then it's provably provable, and therefore provably false. Hence, if S is provable then it's also disprovable and therefore PA is inconsistent. Conversely if S is unprovable then it must be true (since "S is unprovable" is exactly S), and moreover PA must be consistent (since inconsistent theories prove everything). Hence, S is unprovable iff S is true iff PA is consistent.
The diagonal lemma basically does all the work here, in allowing us to construct S with this self-referential property. There is a small amount of work being done by the "if S is provable then it's provably provable", but this is a much more obvious observation. If S is provable, then you can prove it's provable by simply locating a specific proof for S and verifying that it does actually prove S.
The diagonal lemma is pretty non-obvious by comparison, I'd say. That mere statements about string concatenation are powerful enough to make self-referential statements (in the sense of the diagonal lemma) is honestly rather shocking. That the theory of computation can do this is much less shocking; recursively defined computer programs are bog standard. It's not hard to see why proof verification is computable, so of course any theory that reasons about computation can do such things.
I suppose, the non-obvious component of the diagonal lemma is just that some particular theory can reason about computer programs. If we merge arithmetic with a theory of finite symbol sequences (i.e. strings), then obviously we can reason about computer programs, since computation is just a sequence of arithmetic operations. It's much less obvious that arithmetic alone is enough to do this, and even less obvious that string concatenation alone is sufficient.
Perhaps it's worth noting that formalizing and expressing the notion of "provability" is tantamount to just expressing computation outright. The relation "theory T proves the sentence S" can be directly converted into a definition for computation, as "the turing machine M halts on input x and outputs y" is true if and only if "PA proves M halts on input x and outputs y".
Whether a given theory can actually prove that equivalence is a matter of strength, but incompleteness is automatic for any sufficiently expressive theory.
