Editing Gödel's incompleteness theorems (section)

== Proof sketch for the second theorem ==
{{See also|Hilbert–Bernays provability conditions}}

The main difficulty in proving the second incompleteness theorem is to show that various facts about provability used in the proof of the first incompleteness theorem can be formalized within a system {{mvar|S}} using a formal predicate {{mvar|''P''}} for provability. Once this is done, the second incompleteness theorem follows by formalizing the entire proof of the first incompleteness theorem within the system {{mvar|S}} itself.

Let {{mvar|p}} stand for the undecidable sentence constructed above, and assume for purposes of obtaining a contradiction that the consistency of the system {{mvar|S}} can be proved from within the system {{mvar|S}} itself. This is equivalent to proving the statement "System {{mvar|S}} is consistent". 
Now consider the statement {{mvar|c}}, where {{mvar|c}} = "If the system {{mvar|S}} is consistent, then {{mvar|p}} is not provable". The proof of sentence {{mvar|c}} can be formalized within the system {{mvar|S}}, and therefore the statement {{mvar|c}}, "{{mvar|p}} is not provable", (or identically, "not {{math|''P''(''p'')}}") can be proved in the system {{mvar|S}}.

Observe then, that if we can prove that the system {{mvar|S}} is consistent (ie. the statement in the hypothesis of {{mvar|c}}), then we have proved that {{mvar|p}} is not provable. But this is a contradiction since by the 1st Incompleteness Theorem, this sentence (ie. what is implied in the sentence {{mvar|c}}, ""{{mvar|p}}" is not provable") is what we construct to be unprovable. Notice that this is why we require formalizing the first Incompleteness Theorem in {{mvar|S}}: to prove the 2nd Incompleteness Theorem, we obtain a contradiction with the 1st Incompleteness Theorem which can do only by showing that the theorem holds in {{mvar|S}}. So we cannot prove that the system {{mvar|S}} is consistent. And the 2nd Incompleteness Theorem statement follows.