Second

noncomputable def LO.Arith.Formalized.substNumeral {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (φ x : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Formalized.substNumeral φ x = ⌜ℒₒᵣ⌝.substs₁ (LO.Arith.Formalized.numeral x) φ

theorem LO.Arith.Formalized.substNumeral_app_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (σ : FirstOrder.Semisentence ℒₒᵣ 1) (n : ℕ) : substNumeral ⌜σ⌝ ↑n = ⌜σ/[↑n]⌝

theorem LO.Arith.Formalized.substNumeral_app_quote_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (σ π : FirstOrder.Semisentence ℒₒᵣ 1) : substNumeral ⌜σ⌝ ⌜π⌝ = ⌜σ/[⌜π⌝]⌝

noncomputable def LO.Arith.Formalized.substNumerals {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (φ : V) (v : Fin k → V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.Formalized.substNumerals φ v = ⌜ℒₒᵣ⌝.substs ⌜fun (i : Fin k) => LO.Arith.Formalized.numeral (v i)⌝ φ

theorem LO.Arith.Formalized.substNumerals_app_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (σ : FirstOrder.Semisentence ℒₒᵣ k) (v : Fin k → ℕ) : (substNumerals ⌜σ⌝ fun (x : Fin k) => ↑(v x)) = ⌜(FirstOrder.Rewriting.app (FirstOrder.Rew.substs fun (i : Fin k) => ↑(v i))) σ⌝

theorem LO.Arith.Formalized.substNumerals_app_quote_quote {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (σ : FirstOrder.Semisentence ℒₒᵣ k) (π : Fin k → FirstOrder.Semisentence ℒₒᵣ k) : (substNumerals ⌜σ⌝ fun (i : Fin k) => ⌜π i⌝) = ⌜(FirstOrder.Rewriting.app (FirstOrder.Rew.substs fun (i : Fin k) => ⌜π i⌝)) σ⌝

noncomputable def LO.FirstOrder.Arith.ssnum : Sg1.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Formalized.substNumeral_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg1-Function₂ substNumeral via FirstOrder.Arith.ssnum

@[simp]

theorem LO.Arith.Formalized.eval_ssnum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.ssnum) ↔ v 0 = substNumeral (v 1) (v 2)

theorem LO.Arith.Formalized.eval_ssnum_oring {V : Type u_2} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.ssnum) ↔ v 0 = substNumeral (v 1) (v 2)

noncomputable def LO.FirstOrder.Arith.ssnums {k : ℕ} : Sg1.Semisentence (k + 2)

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Formalized.substNumerals_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} : FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (k + 1) → V) => substNumerals (v 0) fun (x : Fin k) => v x.succ) FirstOrder.Arith.ssnums

@[simp]

theorem LO.Arith.Formalized.eval_ssnums {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {k : ℕ} (v : Fin (k + 2) → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.ssnums) ↔ v 0 = substNumerals (v 1) fun (i : Fin k) => v i.succ.succ

noncomputable def LO.FirstOrder.Arith.multidiag {k : ℕ} (θ : Semisentence ℒₒᵣ k) : Semisentence ℒₒᵣ k

$\mathrm{diag}_i(\vec{x}) := (\forall \vec{y})\left[ \left(\bigwedge_j \mathrm{ssnums}(y_j, x_j, \vec{x})\right) \to \theta_i(\vec{y}) \right]$

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LO.FirstOrder.Arith.multifixpoint {k : ℕ} (θ : Fin k → Semisentence ℒₒᵣ k) (i : Fin k) : Sentence ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.multifixpoint θ i = (LO.FirstOrder.Rewriting.app (LO.FirstOrder.Rew.substs fun (j : Fin k) => ⌜LO.FirstOrder.Arith.multidiag (θ j)⌝)) (LO.FirstOrder.Arith.multidiag (θ i))

theorem LO.FirstOrder.Arith.multidiagonal {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {k : ℕ} {i : Fin k} (θ : Fin k → Semisentence ℒₒᵣ k) : T ⊢!. multifixpoint θ i <=> (Rewriting.app (Rew.substs fun (j : Fin k) => ⌜multifixpoint θ j⌝)) (θ i)

noncomputable def LO.FirstOrder.Arith.diag (θ : Semisentence ℒₒᵣ 1) : Semisentence ℒₒᵣ 1

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.diag θ = LO.FirstOrder.Arith.multidiag θ

noncomputable def LO.FirstOrder.Arith.fixpoint (θ : Semisentence ℒₒᵣ 1) : Sentence ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.fixpoint θ = (LO.FirstOrder.Arith.diag θ)/[⌜LO.FirstOrder.Arith.diag θ⌝]

theorem LO.FirstOrder.Arith.diagonal {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] (θ : Semisentence ℒₒᵣ 1) : T ⊢!. fixpoint θ <=> θ/[⌜fixpoint θ⌝]

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Theory.bewₐ (U : Theory ℒₒᵣ) [U.Delta1Definable] (σ : Sentence ℒₒᵣ) : Sentence ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

• U.bewₐ σ = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val U.provableₐ)/[⌜σ⌝]

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Theory.consistentₐ (U : Theory ℒₒᵣ) [U.Delta1Definable] : Sentence ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

• U.consistentₐ = ∼U.bewₐ ⊥

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Consistentₐ (U : Theory ℒₒᵣ) [U.Delta1Definable] : Theory ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

• 𝐂𝐨𝐧[U] = {↑U.consistentₐ}

def LO.FirstOrder.Arith.«term𝐂𝐨𝐧[_]» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Inconsistentₐ (U : Theory ℒₒᵣ) [U.Delta1Definable] : Theory ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

• ¬𝐂𝐨𝐧[U] = {∼↑U.consistentₐ}

def LO.FirstOrder.Arith.«term¬𝐂𝐨𝐧[_]» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LO.FirstOrder.Theory.goedelₐ (U : Theory ℒₒᵣ) [U.Delta1Definable] : Sentence ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

• U.goedelₐ = LO.FirstOrder.Arith.fixpoint (∼LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val U.provableₐ)

theorem LO.FirstOrder.Arith.provableₐ_D1 {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] {σ : Sentence ℒₒᵣ} : U ⊢!. σ → T ⊢!. U.bewₐ σ

theorem LO.FirstOrder.Arith.provableₐ_D2 {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] {σ π : Sentence ℒₒᵣ} : T ⊢!. U.bewₐ (σ ==> π) ==> U.bewₐ σ ==> U.bewₐ π

theorem LO.FirstOrder.Arith.provableₐ_sigma₁_complete {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] {σ : Sentence ℒₒᵣ} (hσ : Hierarchy Sg 1 σ) : T ⊢!. σ ==> U.bewₐ σ

theorem LO.FirstOrder.Arith.provableₐ_D3 {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] {σ : Sentence ℒₒᵣ} : T ⊢!. U.bewₐ σ ==> U.bewₐ (U.bewₐ σ)

theorem LO.FirstOrder.Arith.goedel_iff_unprovable_goedel {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] : T ⊢!. U.goedelₐ <=> ∼U.bewₐ U.goedelₐ

theorem LO.FirstOrder.Arith.provableₐ_D2_context {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] {Γ : List (Sentence ℒₒᵣ)} {σ π : Sentence ℒₒᵣ} (hσπ : Γ ⊢[T.alt]! U.bewₐ (σ ==> π)) (hσ : Γ ⊢[T.alt]! U.bewₐ σ) : Γ ⊢[T.alt]! U.bewₐ π

theorem LO.FirstOrder.Arith.provableₐ_D3_context {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] {Γ : List (Sentence ℒₒᵣ)} {σ : Sentence ℒₒᵣ} (hσπ : Γ ⊢[T.alt]! U.bewₐ σ) : Γ ⊢[T.alt]! U.bewₐ (U.bewₐ σ)

theorem LO.FirstOrder.Arith.provableₐ_sound {T U : Theory ℒₒᵣ} [U.Delta1Definable] [ℕ ⊧ₘ* T] [𝐑₀ wkn U] {σ : Sentence ℒₒᵣ} : T ⊢!. U.bewₐ σ → U ⊢! ↑σ

theorem LO.FirstOrder.Arith.provableₐ_complete {T : Theory ℒₒᵣ} [𝐈Sg1 wkn T] {U : Theory ℒₒᵣ} [U.Delta1Definable] [ℕ ⊧ₘ* T] [𝐑₀ wkn U] {σ : Sentence ℒₒᵣ} : U ⊢! ↑σ ↔ T ⊢!. U.bewₐ σ

theorem LO.FirstOrder.Arith.goedel_unprovable (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [Entailment.Consistent T] : T ⊬ ↑T.goedelₐ

theorem LO.FirstOrder.Arith.not_goedel_unprovable (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : T ⊬ ∼↑T.goedelₐ

theorem LO.FirstOrder.Arith.consistent_iff_goedel (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] : T ⊢! ↑T.consistentₐ <=> ↑T.goedelₐ

theorem LO.FirstOrder.Arith.goedel_second_incompleteness (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [Entailment.Consistent T] : T ⊬ ↑T.consistentₐ

Gödel's Second Incompleteness Theorem

theorem LO.FirstOrder.Arith.inconsistent_unprovable (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : T ⊬ ∼↑T.consistentₐ

theorem LO.FirstOrder.Arith.inconsistent_undecidable (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : Entailment.Undecidable T ↑T.consistentₐ

instance LO.FirstOrder.Arith.instStrictlyWeakerThanSyntacticFormulaORingTheoryHAddConsistentₐOfConsistent (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [Entailment.Consistent T] : T swkn T + 𝐂𝐨𝐧[T]

instance LO.FirstOrder.Arith.instModelsTheoryNatConsistentₐOfConsistentSyntacticFormulaORingTheory (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [Entailment.Consistent T] : ℕ ⊧ₘ* 𝐂𝐨𝐧[T]

instance LO.FirstOrder.Arith.instModelsTheoryNatHAddTheoryORingConsistentₐ (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : ℕ ⊧ₘ* T + 𝐂𝐨𝐧[T]

instance LO.FirstOrder.Arith.instStrictlyWeakerThanSyntacticFormulaORingTheoryHAddInconsistentₐOfModelsTheoryNat (T : Theory ℒₒᵣ) [𝐈Sg1 wkn T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : T swkn T + ¬𝐂𝐨𝐧[T]