Editing Gödel's incompleteness theorems (section)

=== Implications for consistency proofs ===

Gödel's second incompleteness theorem also implies that a system {{math|''F''<sub>1</sub>}} satisfying the technical conditions outlined above cannot prove the consistency of any system {{math|''F''<sub>2</sub>}} that proves the consistency of {{math|''F''<sub>1</sub>}}. This is because such a system {{math|''F''<sub>1</sub>}} can prove that if {{math|''F''<sub>2</sub>}} proves the consistency of {{math|''F''<sub>1</sub>}}, then {{math|''F''<sub>1</sub>}} is in fact consistent. For the claim that {{math|''F''<sub>1</sub>}} is consistent has form "for all numbers {{mvar|n}}, {{mvar|n}} has the decidable property of not being a code for a proof of contradiction in {{math|''F''<sub>1</sub>}}". If {{math|''F''<sub>1</sub>}} were in fact inconsistent, then {{math|''F''<sub>2</sub>}} would prove for some {{mvar|n}} that {{mvar|n}} is the code of a contradiction in {{math|''F''<sub>1</sub>}}. But if {{math|''F''<sub>2</sub>}} also proved that {{math|''F''<sub>1</sub>}} is consistent (that is, that there is no such {{mvar|n}}), then it would itself be inconsistent. This reasoning can be formalized in {{math|''F''<sub>1</sub>}} to show that if {{math|''F''<sub>2</sub>}} is consistent, then {{math|''F''<sub>1</sub>}} is consistent. Since, by second incompleteness theorem, {{math|''F''<sub>1</sub>}} does not prove its consistency, it cannot prove the consistency of {{math|''F''<sub>2</sub>}} either.

This corollary of the second incompleteness theorem shows that there is no hope of proving, for example, the consistency of Peano arithmetic using any finitistic means that can be formalized in a system the consistency of which is provable in Peano arithmetic (PA). For example, the system of [[primitive recursive arithmetic]] (PRA), which is widely accepted as an accurate formalization of finitistic mathematics, is provably consistent in PA. Thus PRA cannot prove the consistency of PA. This fact is generally seen to imply that [[Hilbert's program]], which aimed to justify the use of "ideal" (infinitistic) mathematical principles in the proofs of "real" (finitistic) mathematical statements by giving a finitistic proof that the ideal principles are consistent, cannot be carried out.{{sfn|Franzén|2005|p=106}}

The corollary also indicates the epistemological relevance of the second incompleteness theorem. It would provide no interesting information if a system {{mvar|F}} proved its consistency. This is because inconsistent theories prove everything, including their consistency. Thus a consistency proof of {{mvar|F}} in {{mvar|F}} would give us no clue as to whether {{mvar|F}} is consistent; no doubts about the consistency of {{mvar|F}} would be resolved by such a consistency proof. The interest in consistency proofs lies in the possibility of proving the consistency of a system {{mvar|F}} in some system {{mvar|F'}} that is in some sense less doubtful than {{mvar|F}} itself, for example, weaker than {{mvar|F}}. For many naturally occurring theories {{mvar|F}} and {{mvar|F'}}, such as {{mvar|F}} = Zermelo–Fraenkel set theory and {{mvar|F'}} = primitive recursive arithmetic, the consistency of {{mvar|F'}} is provable in {{mvar|F}}, and thus {{mvar|F'}} cannot prove the consistency of {{mvar|F}} by the above corollary of the second incompleteness theorem.

The second incompleteness theorem does not rule out altogether the possibility of proving the consistency of a different system with different axioms. For example, [[Gerhard Gentzen]] proved the consistency of Peano arithmetic in a different system that includes an axiom asserting that the [[Ordinal number|ordinal]] called {{math|''ε''<sub>0</sub>}} is [[wellfounded]]; see [[Gentzen's consistency proof]].  Gentzen's theorem spurred the development of [[ordinal analysis]] in proof theory.