Editing Gödel's incompleteness theorems (section)

== Second incompleteness theorem<!--'Gödel's second incompleteness theorem' and 'Second incompleteness theorem' redirect here--> ==

For each formal system {{mvar|F}} containing basic arithmetic, it is possible to canonically define a formula Cons({{mvar|F}}) expressing the consistency of {{mvar|F}}. This formula expresses the property that "there does not exist a natural number coding a formal derivation within the system {{mvar|F}} whose conclusion is a syntactic contradiction." The syntactic contradiction is often taken to be "0=1", in which case Cons({{mvar|F}}) states "there is no natural number that codes a derivation of '0=1' from the axioms of {{mvar|F}}."

'''Gödel's second incompleteness theorem'''<!--boldface per WP:R#PLA--> shows that, under general assumptions, this canonical consistency statement Cons({{mvar|F}}) will not be provable in {{mvar|F}}. The theorem first appeared as "Theorem XI" in Gödel's 1931 paper "[[On Formally Undecidable Propositions in Principia Mathematica and Related Systems I]]". In the following statement, the term "formalized system" also includes an assumption that {{mvar|F}} is effectively axiomatized. This theorem states that for any consistent system ''F'' within which a certain amount of elementary arithmetic can be carried out, the consistency of ''F'' cannot be proved in ''F'' itself.<ref>{{harvnb|Raatikainen|2020}} : "Assume {{mvar|F}} is a consistent formalized system which contains elementary arithmetic. Then <math>F \not \vdash \text{Cons}(F)</math>."</ref> This theorem is stronger than the first incompleteness theorem because the statement constructed in the first incompleteness theorem does not directly express the consistency of the system. The proof of the second incompleteness theorem is obtained by formalizing the proof of the first incompleteness theorem within the system {{mvar|F}} itself.

=== Expressing consistency ===

There is a technical subtlety in the second incompleteness theorem regarding the method of expressing the consistency of {{mvar|F}} as a formula in the language of {{mvar|F}}. There are many ways to express the consistency of a system, and not all of them lead to the same result. The formula Cons({{mvar|F}}) from the second incompleteness theorem is a particular expression of consistency.

Other formalizations of the claim that {{mvar|F}} is consistent may be inequivalent in {{mvar|F}}, and some may even be provable. For example, first-order Peano arithmetic (PA) can prove that "the largest consistent [[subset]] of PA" is consistent. But, because PA is consistent, the largest consistent subset of PA is just PA, so in this sense PA "proves that it is consistent". What PA does not prove is that the largest consistent subset of PA is, in fact, the whole of PA. (The term "largest consistent subset of PA" is meant here to be the largest consistent initial segment of the axioms of PA under some particular effective enumeration.)

=== The Hilbert&ndash;Bernays conditions ===

The standard proof of the second incompleteness theorem assumes that the provability predicate {{math|''Prov''<sub>A</sub>(''P'')}} satisfies the [[Hilbert–Bernays provability conditions]]. Letting {{math|#(''P'')}} represent the Gödel number of a formula {{mvar|P}}, the provability conditions say:

# If {{mvar|F}} proves {{mvar|P}}, then {{mvar|F}} proves {{math|''Prov''<sub>A</sub>(#(''P''))}}.
# {{mvar|F}} proves 1.; that is, {{mvar|F}} proves {{math|''Prov''<sub>A</sub>(#(''P'')) → ''Prov''<sub>A</sub>(#(''Prov''<sub>A</sub>(#(''P''))))}}.
# {{mvar|F}} proves {{math|''Prov''<sub>A</sub>(#(''P'' → ''Q'')) ∧ ''Prov''<sub>A</sub>(#(''P'')) → ''Prov''<sub>A</sub>(#(''Q''))}} &nbsp; (analogue of [[modus ponens]]).

There are systems, such as Robinson arithmetic, which are strong enough to meet the assumptions of the first incompleteness theorem, but which do not prove the Hilbert&ndash;Bernays conditions. Peano arithmetic, however, is strong enough to verify these conditions, as are all theories stronger than Peano arithmetic.

=== 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.