Godel's Second Incompleteness Theorem

Gödel's Second Incompleteness Theorem is a theorem in meta-mathematics which asserts that an axiomatic theory $F$, which can prove anything that $PA$ can, cannot prove its own consistency iff it is consistent. It is closely related to Godel's First Incompleteness Theorem, being in fact a stronger form, and easily derived (as shown below).

Proof

Firstly, if $F$ is not consistent, then $F$ can prove any statement, including its own consistency, because ex falso quodlibet.

Now suppose that $F$ is consistent. Then, by Godel's First Incompleteness Theorem, there is a statement $G_F$, which is equivalent to the statement "$F$ cannot prove $G_F$", and $F$ cannot prove $G_F$. But the proof of Gödel's First Incompleteness Theorem is itself a proof in $F$, so that $F$ can prove the statement "If $F$ is consistent, then $G_F$ is equivalent to '$F$ cannot prove $G_F$'"; by modus tollens, $F$ can also prove "If $F$ is consistent, then $G_F$ is true." But if $F$ could prove its own consistency, then it could also prove $G_F$, contradicting Gödel's First Incompleteness Theorem, and we are done.

See also