Formalized Formal Logic

2.3. Gödel's First Incompleteness Theorem🔗

A deduction system \mathcal{S} is complete iff it can prove or refute every sentence \sigma. Otherwise, \mathcal{S} is incomplete.

🔗type class
LO.Entailment.Incomplete.{u_1, u_2, u_5} {F : Type u_1} {S : Type u_2}
  [Entailment F S] [LogicalConnective F] (𝓢 : S) : Prop
LO.Entailment.Incomplete.{u_1, u_2, u_5}
  {F : Type u_1} {S : Type u_2}
  [Entailment F S] [LogicalConnective F]
  (𝓢 : S) : Prop

A proof system is incomplete if and only if there exists a formula that is both unprovable and irrefutable.

Instance Constructor

LO.Entailment.Incomplete.mk.{u_1, u_2, u_5}

Methods

indep : ∃ φ, Independent 𝓢 φ

Let T be a \Delta_1-definable arithmetic theory, stronger than \mathsf{R}_0 and \Sigma_1-sound.

variable (T : ArithmeticTheory) [T.Δ₁] [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1]

2.3.1. Representeation Theorem

Let P be a r.e. set. There exists a formula \varphi_P(x) such that n \in P \iff T \vdash \varphi_P(\overline{n}) for all n \in \mathbb{N}.

🔗theorem
LO.FirstOrder.Arithmetic.re_complete {T : ArithmeticTheory} [𝗥₀ ⪯ T]
  [T.SoundOnHierarchy 𝚺 1] {A : ℕ → Prop} (hp : REPred A) {x : ℕ} :
  A x ↔ T ⊢ (codeOfREPred A)/[↑x]
LO.FirstOrder.Arithmetic.re_complete
  {T : ArithmeticTheory} [𝗥₀ ⪯ T]
  [T.SoundOnHierarchy 𝚺 1] {A : ℕ → Prop}
  (hp : REPred A) {x : ℕ} :
  A x ↔ T ⊢ (codeOfREPred A)/[↑x]

Weak representation of a r.e. predicate

2.3.2. First Incompleteness Theorem

Define a set D_T, which satisfies \ulcorner\phi\urcorner \in D_T \iff T \vdash \lnot\phi(\ulcorner\phi\urcorner). D_T is a r.e. set, since the provability predicate of T is \Sigma_1-definable, and the substitution function is \Delta_1-definable.

def D : ℕ → Prop := fun φ : ℕ ↦ IsSemiformula ℒₒᵣ 1 φ ∧ T.Provable (neg ℒₒᵣ <| subst ℒₒᵣ ?[numeral φ] φ) lemma D_spec (φ : Semisentence ℒₒᵣ 1) : D T ⌜φ⌝ ↔ T ⊢ ∼φ/[⌜φ⌝] := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1φ:Semisentence ℒₒᵣ 1⊢ D T ⌜φ⌝ ↔ T ⊢ ∼φ/[⌜φ⌝] All goals completed! 🐙 lemma D_re : REPred (D T) := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1⊢ REPred (D T) have : 𝚺₁-Predicate fun φ : ℕ ↦ IsSemiformula ℒₒᵣ 1 φ ∧ T.Provable (neg ℒₒᵣ <| subst ℒₒᵣ ?[numeral φ] φ) := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1⊢ REPred (D T) All goals completed! 🐙 All goals completed! 🐙

By the representeation theorem, there exists a \Sigma-sentence \delta_T(x), such that n \in D_T \iff T \vdash \delta_T(n) for all n \in \mathbb{N}.

noncomputable def δ : Semisentence ℒₒᵣ 1 := codeOfREPred (D T) lemma δ_spec (n : ℕ) : D T n ↔ T ⊢ (δ T)/[↑n] := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1n:ℕ⊢ D T n ↔ T ⊢ (δ T)/[↑n] All goals completed! 🐙

Define sentence \pi_T, defined as \delta_T(\ulcorner\delta_T\urcorner)

noncomputable def π : Sentence ℒₒᵣ := (δ T)/[⌜δ T⌝]

By a simple inference, it can be shown that the provability of \pi_T and the provability of its negation are equivalent.

lemma paradoxical : T ⊢ π T ↔ T ⊢ ∼π T := calc T ⊢ π T ↔ T ⊢ (δ T)/[⌜δ T⌝] := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1⊢ T ⊢ π T ↔ T ⊢ (δ T)/[⌜δ T⌝] All goals completed! 🐙 _ ↔ D T ⌜δ T⌝ := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1⊢ T ⊢ (δ T)/[⌜δ T⌝] ↔ D T ⌜δ T⌝ All goals completed! 🐙 _ ↔ T ⊢ ∼(δ T)/[⌜δ T⌝] := D_spec T (δ T) _ ↔ T ⊢ ∼π T := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1⊢ T ⊢ ∼(δ T)/[⌜δ T⌝] ↔ T ⊢ ∼π T All goals completed! 🐙

Hence, \pi_T and its negation are both unprovable from T, since T is consistent.

theorem unprovable : T ⊬ π T := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1⊢ T ⊬ π T T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1h:T ⊢ π T⊢ False T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1h:T ⊢ π Tthis:_fvar.2 ⊢ ∼π _fvar.2 := (paradoxical _fvar.2).mp _fvar.178⊢ False T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1h:T ⊢ π Tthis✝:_fvar.2 ⊢ ∼π _fvar.2 := (paradoxical _fvar.2).mp _fvar.178this:Inconsistent _fvar.2 := inconsistent_of_provable_of_unprovable _fvar.178 _fvar.894⊢ False All goals completed! 🐙 theorem irrefutable : T ⊬ ∼π T := T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1⊢ T ⊬ ∼π T T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1h:T ⊢ ∼π T⊢ False T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1h:T ⊢ ∼π Tthis:_fvar.1523 ⊢ π _fvar.1523 := (paradoxical _fvar.1523).mpr _fvar.2353⊢ False T:ArithmeticTheoryinst✝²:Theory.Δ₁ Tinst✝¹:𝗥₀ ⪯ Tinst✝:T.SoundOnHierarchy 𝚺 1h:T ⊢ ∼π Tthis✝:_fvar.1523 ⊢ π _fvar.1523 := (paradoxical _fvar.1523).mpr _fvar.2353this:Inconsistent _fvar.1523 := inconsistent_of_provable_of_unprovable _fvar.2415 _fvar.2353⊢ False All goals completed! 🐙

Therefore, we obtain the Gödel's first incompleteness theorem for \Delta_1-theory stronger than \mathsf{R_0} and \Sigma_1-sound.

🔗theorem
LO.FirstOrder.Arithmetic.incomplete (T : ArithmeticTheory) [Theory.Δ₁ T]
  [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : Incomplete T
LO.FirstOrder.Arithmetic.incomplete
  (T : ArithmeticTheory) [Theory.Δ₁ T]
  [𝗥₀ ⪯ T] [T.SoundOnHierarchy 𝚺 1] :
  Incomplete T

Gödel's first incompleteness theorem