Gödel's incompleteness theorems - Second Incompleteness Theorem

The Second Incompleteness Theorem Understanding the Main Result The Second Incompleteness Theorem is a fundamental result in mathematical logic that reveals a surprising limitation: no consistent formal system capable of expressing basic arithmetic can prove its own consistency. This is a powerful statement. It means that if you have a formal system $F$ that is strong enough to do arithmetic (like Peano arithmetic), and if that system is consistent (never produces contradictions), then $F$ itself cannot demonstrate this fact. You cannot prove the consistency of the system from within the system itself. This theorem builds directly on the First Incompleteness Theorem. In fact, understanding the second theorem requires you to already be comfortable with how the first one works. Formalizing Consistency: The Statement $Cons(F)$ To state and prove the Second Incompleteness Theorem precisely, we need a formal way to express what it means for a system to be consistent. For a formal system $F$, we define the consistency formula $Cons(F)$ as follows: $$Cons(F) \equiv \neg\exists n: \text{Proof}F(n, \ulcorner 0=1 \urcorner)$$ Let's break this down carefully. The formula $Cons(F)$ asserts that there does not exist a natural number $n$ that codes a derivation of the contradiction $0=1$ from the axioms of $F$. The notation $\ulcorner 0=1 \urcorner$ represents the Gödel number—a natural number that encodes the statement "$0=1$". Similarly, $ProofF(n, \ulcorner 0=1 \urcorner)$ is a formula that says "$n$ codes a valid proof of $0=1$ in system $F$." So $Cons(F)$ is saying: "There is no proof of a contradiction in $F$," which is exactly what we mean when we say a system is consistent. The remarkable content of the Second Incompleteness Theorem is that if $F$ is actually consistent, then $F$ cannot prove $Cons(F)$. Why the Theorem Works: The Proof Sketch The proof of the Second Incompleteness Theorem uses a clever self-referential argument. Here's the essential idea: Step 1: Formalizing the First Theorem Inside $F$ Recall that the First Incompleteness Theorem essentially argues: "If $F$ is consistent, then the Gödel sentence $p$ is not provable in $F$." This argument can be formalized inside the system $F$ itself, as long as $F$ is strong enough to express arithmetic. In other words, $F$ can contain a proof of the statement: $$Cons(F) \to \neg\text{Proof}F(\ulcorner p \urcorner)$$ This says: "If $F$ is consistent, then $p$ is not provable in $F$." Step 2: The Contradiction Argument Now suppose, for the sake of contradiction, that $F$ can prove its own consistency—that is, suppose $F \vdash Cons(F)$. If $F$ proves $Cons(F)$, and $F$ can prove "$Cons(F) \to \neg\text{Proof}F(\ulcorner p \urcorner)$" (from Step 1), then by modus ponens, $F$ can prove $\neg\text{Proof}F(\ulcorner p \urcorner)$. This means $F$ proves that $p$ is not provable in $F$. But here's the problem: The First Incompleteness Theorem tells us that if $F$ is consistent, then $F$ cannot actually prove that $p$ is unprovable. We have derived a contradiction. Step 3: The Conclusion The only way to avoid this contradiction is to conclude that our initial assumption was wrong: $F$ cannot prove $Cons(F)$. Key Consequences for Mathematics and Logic The Second Incompleteness Theorem has several important implications that you should understand clearly. No System Can Prove Its Own Consistency Any formal system meeting basic requirements (specifically, the Hilbert–Bernays conditions, which ensure the system can express arithmetic reasonably) cannot prove its own consistency if it is consistent. This rules out a natural approach to addressing the First Incompleteness Theorem: you can't escape incompleteness by strengthening the system with a self-consistency proof. Hierarchy of Consistency Strength Here's a crucial practical consequence: suppose system $F$ can prove that system $G$ is consistent. Then we know immediately that $F$ must be strictly stronger than $G$. Why? Because if $G$ could prove $Cons(F)$, then by the Second Incompleteness Theorem, $G$ would have to be inconsistent (since the Second Theorem tells us only systems that can already express certain strength can fail to prove consistency of stronger systems). The Case of Peano Arithmetic A concrete example makes this clear. Primitive recursive arithmetic (PRA) is a finitistic formal system—it only uses methods that are constructively verifiable. First-order Peano arithmetic (PA) is stronger; it includes full induction over all first-order formulas. It turns out that PA can prove its own consistency (though this requires a stronger metatheory, not PA itself). However, PRA cannot prove the consistency of PA. This is a direct consequence of the Second Incompleteness Theorem: since PRA is weaker than PA, and PA can prove (externally) that it's consistent, PRA cannot do so. This tells us something deep: the consistency of PA requires going beyond the finitistic methods allowed in PRA. <extrainfo> The Hilbert–Bernays conditions are technical requirements for formal systems related to how they represent provability. Specifically, they require the system to be able to formalize certain basic logical operations on proofs. Most natural systems like PA and ZFC satisfy these conditions. </extrainfo>