Gödel's Second Incompleteness Theorem

Recall that inside $I Σ_{1}$ we can do basic set theory and primitive recursion. Many inductive notions and functions on them are defined in $Δ_{1}$ or $Σ_{1}$ using the fixpoint construction.

We work inside an arbitrary model $V$ of $I Σ_{1}$ .

$u \in T_{C} ⟺ (\exists z) [u = # z] \lor (\exists x) [u = & x] \lor (\exists k, f, v) [Func_{k} (f) \land Seq (v) \land k = lh (v) \land (\forall i, z) [⟨ i, z ⟩ \in v \to z \in C] \land u = f^{k} (v)]$

$∙$ is a quasi-quotation. $bounded variable: free variable: function: # z & x f^{k} (v) : = ⟨ 0, z ⟩ + 1 : = ⟨ 1, x ⟩ + 1 : = ⟨ 2, f, k, v ⟩ + 1$

$T_{C}$ is $Δ_{1}$ (if $C$ is a finite set) and monotone. Let $UTerm (t)$ be a fixpoint of $T_{C}$ . It is $Δ_{1}$ since $T_{C}$ satisfies strong finiteness. Define the function $termBV (t)$ inductively on $UTerm$ meaning the largest bounded variable $+ 1$ that appears in the term. Define $Semiterm (n, t) := UTerm (t) \land termBV (t) \leq n$ .

Formula

Similarly, Define $F_{C}$ :

$u \in F_{C} ⟺ (\exists k, R, v) [Rel_{k} (R) \land v is a list of UTerm of length k \land u = R^{k} (v)] \lor (\exists k, R, v) [Rel_{k} (R) \land v is a list of UTerm of length k \land u = \neg R^{k} (v)] \lor [u = ⊤] \lor [u = ⊥] \lor (\exists p \in C, q \in C) [u = p \land q] \lor (\exists p \in C, q \in C) [u = p \lor q] \lor (\exists p \in C) [u = \forall p] \lor (\exists p \in C) [u = \exists p]$

$R^{k} (v) \neg R^{k} (v) ⊤ ⊥ p \land q p \lor q \forall p \exists p : = ⟨ 0, R, k, v ⟩ + 1 : = ⟨ 1, R, k, v ⟩ + 1 : = ⟨ 2, 0 ⟩ + 1 : = ⟨ 3, 0 ⟩ + 1 : = ⟨ 4, p, q ⟩ + 1 : = ⟨ 5, p, q ⟩ + 1 : = ⟨ 6, p ⟩ + 1 : = ⟨ 7, p ⟩ + 1$

$F_{C}$ is $Δ_{1}$ and monotone. Let $UFormula (p)$ be a fixpoint of $F_{C}$ and define

$Semiformula (n, p) ⟺ UFormula (p) \land bv (p) \leq n$

The function $bv (p)$ is defined inductively on $UFormula$ meaning the largest bounded variable $+ 1$ that appears in the formula.

$UFormula (p)$ and $Semiormula (n, p)$ are again $Δ_{1}$ since $F_{C}$ satisfies strong finiteness.

Formalized Provability

Let $T$ be $Δ_{1}$ -definable theory. Define $D_{C}$ :

$d \in D_{C} ⟺ [(\forall p \in sqt (d)) [Semiformula (0, p)] \land (\exists s, p) [d = AXL (s, p) \land p \in s \land \overset{\neg}{^} p \in s] \lor (\exists s) [d = ⊤ -INTRO (s) \land ⊤ \in s] \lor (\exists s, p, q) (\exists d_{p}, d_{q} \in C) [d = \land -INTRO (s, p, q, d_{p}, d_{q}) \land p \land q \in s \land sqt (d_{p}) = s \cup {p} \land sqt (d_{q}) = s \cup {q}] \lor (\exists s, p, q) (\exists d \in C) [d = \lor -INTRO (s, p, q, d) \land p \lor q \in s \land sqt (d) = s \cup {p, q}] \lor (\exists s, p) (\exists d \in C) [d = \forall -INTRO (s, p, d) \land \forall p \in s \land sqt (d) = s^{+} \cup {p^{+} [&0]}] \lor (\exists s, p, t) (\exists d \in C) [d = \exists -INTRO (s, p, t, d) \land \exists p \in s \land sqt (d) = s \cup {p (t)}] \lor (\exists s) (\exists d^{'} \in C) [d = WK (s, d^{'}) \land s \supseteq sqt (d^{'})] (\exists s) (\exists d^{'} \in C) [d = SHIFT (s, d^{'}) \land s = sqt (d^{'})^{+}] (\exists s, p) (\exists d_{1}, d_{2} \in C) [d = CUT (s, p, d_{1}, d_{2}) \land sqt (d_{1}) = s \cup {p} \land sqt (d_{2}) = s \cup {\neg p}] (\exists s, p) [d = ROOT (s, p) \land p \in s \land p \in T]]$

$AXL (s, p) ⊤ -INTRO (s) \land -INTRO (s, p, q, d_{p}, d_{q}) \lor -INTRO (s, p, q, d) \forall -INTRO (s, p, d) \exists -INTRO (s, p, t, d) WK (s, d) SHIFT (s, d) CUT (s, p, d_{1}, d_{2}) ROOT (s, p) sqt (d) : = ⟨ s, 0, p ⟩ + 1 : = ⟨ s, 1, 0 ⟩ + 1 : = ⟨ s, 2, p, q, d_{p}, d_{q} ⟩ + 1 : = ⟨ s, 3, p, q, d ⟩ + 1 : = ⟨ s, 4, p, d ⟩ + 1 : = ⟨ s, 5, p, t, d ⟩ + 1 : = ⟨ s, 6, d ⟩ + 1 : = ⟨ s, 7, d ⟩ + 1 : = ⟨ s, 8, p, d_{1}, d_{2} ⟩ + 1 : = ⟨ s, 9, p ⟩ + 1 : = π_{1} (d - 1)$

$p^{+}$ is a shift of a formula $p$ . $s^{+}$ is a image of shift of $s$ . Take fixpoint $Derivation_{T} (d)$ .

$Derivable_{T} (Γ) Bew_{T} (p) : = (\exists d) [Derivation_{T} (d) \land sqt (d) = Γ] : = Derivable_{T} ({p})$

Following holds for all formula (not coded one) $φ$ and finite set $Γ$ .

Sound:

N ⊨ Bew_{T} (┌ φ ┐) ⟹ T ⊢ φ

lemma LO.Arith.Language.Theory.Provable.sound :
    (T.codeIn ℕ).Provable ⌜p⌝ → T ⊢! p

LO.Arith.Language.Theory.Provable.sound

D1:

T ⊢ φ ⟹ V ⊨ Bew_{T} (┌ φ ┐)

theorem LO.Arith.provable_of_provable :
    T ⊢! p → (T.codeIn V).Provable ⌜p⌝

LO.Arith.provable_of_provable

D2: $Bew_{T} (┌ φ \to ψ ┐) & Bew_{T} (┌ φ ┐) ⟹ Bew_{T} (┌ ψ ┐)$

Formalized $Σ_{1}$ -completeness: Let

σ

be a

Σ_{1}

-sentence.

V ⊨ σ ⟹ V ⊨ Bew_{T + R_{0}} (┌ σ ┐)

theorem LO.Arith.sigma₁_complete (hσ : Hierarchy 𝚺 1 σ) :
    V ⊧ₘ₀ σ → T.Provableₐ (⌜σ⌝ : V)

LO.Arith.sigma₁_complete

Now assume that $U$ is a theory of arithmetic stronger than $R_{0}$ and $T$ be a theory of arithmetic stronger than $I Σ_{1}$ . The following holds, thanks to the completeness theorem.

$U ⊢ σ ⟺ T ⊢ Bew_{U} (┌ σ ┐)$
- LO.FirstOrder.Arith.provableₐ_complete
$T ⊢ Bew_{U} (┌ σ \to π ┐) \to Bew_{U} (┌ σ ┐) \to Bew_{U} (┌ π ┐)$
- LO.FirstOrder.Arith.provableₐ_D2
$T ⊢ Bew_{U} (┌ σ ┐) \to Bew_{U} (┌ Bew_{U} (┌ σ ┐) ┐)$
- LO.FirstOrder.Arith.provableₐ_D3

Second Incompleteness Theorem

Assume that $T$ is $Δ_{1}$ -definable and stronger than $I Σ_{1}$ .

Fixpoint Lemma

Since the substitution is $Σ_{1}$ , There is a formula $ssnum (y, p, x)$ such that, for all formula $φ$ with only one variable and $x, y \in V$ ,

$ssnum (y, ┌ φ ┐, x) ⟺ y = ┌ φ (\overline{x}) ┐$

holds. (overline $\overline{∙}$ denotes the (formalized) numeral of $x$ )

Define a sentence $fixpoint_{θ}$ for formula (with one variable) $θ$ as follows.

$fixpoint_{θ} diag_{θ} (x) : = diag_{θ} (\overline{┌ diag_{θ} ┐}) : = (\forall y) [ssnum (y, x, x) \to θ (y)]$

Lemma: $T ⊢ fixpoint_{θ} \leftrightarrow θ (┌ fixpoint_{θ} ┐)$

Proof. $fixpoint_{θ} \equiv (\forall x) [ssnum (x, ┌ diag_{θ} ┐, ┌ diag_{θ} ┐) \to θ (x)] \leftrightarrow θ (┌ diag_{θ} (\overline{┌ diag_{θ} ┐}) ┐) \equiv θ (┌ fixpoint_{θ} ┐)$ ∎

theorem LO.FirstOrder.Arith.diagonal (θ : Semisentence ℒₒᵣ 1) :
    T ⊢!. fixpoint θ ⭤ θ/[⌜fixpoint θ⌝]

LO.FirstOrder.Arith.diagonal

Main Theorem

Define Gödel sentence $G_{T}$ : $G_{T} : = fixpoint_{\neg Bew_{T} (x)}$

Lemma: Gödel sentence is undecidable, i.e., $T ⊬ G$ if $T$ is consistent, and $T ⊬ \neg G$ if $N ⊨ T$ .

lemma goedel_unprovable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
    T ⊬ ↑𝗚

lemma not_goedel_unprovable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
    T ⊬ ∼↑𝗚

Define formalized incompleteness sentence $Con_{T}$ : $Con_{T} : = \neg Bew_{T} (┌ ⊥ ┐)$

Lemma: $T ⊢ Con_{T} \leftrightarrow G_{T}$

lemma consistent_iff_goedel
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] :
    T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚

consistent_iff_goedel

Theorem: $T$ cannot prove its own consistency, i.e., $T ⊬ Con_{T}$ if $T$ is consistent. Moreover, $Con_{T}$ is undecidable from $T$ if $N ⊨ T$ .

theorem goedel_second_incompleteness
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
    T ⊬ ↑𝗖𝗼𝗻 

theorem inconsistent_undecidable
    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
    System.Undecidable T ↑𝗖𝗼𝗻

Logic Formalization in Lean 4