def LO.Arith.Formalized.substNumeral {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) (x : V) : V

Equations

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

theorem LO.Arith.Formalized.substNumeral_app_quote {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (σ : LO.FirstOrder.Semisentence ℒₒᵣ 1) (n : ℕ) : LO.Arith.Formalized.substNumeral ⌜σ⌝ ↑n = ⌜(LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)]).hom σ⌝

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

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

Equations

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

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

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

def LO.FirstOrder.Arith.ssnum : 𝚺₁.Semisentence 3

Equations

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

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

@[simp]

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

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

Equations

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

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

@[simp]

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

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

Equations

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

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

Equations

• LO.FirstOrder.Arith.fixpoint θ = (LO.FirstOrder.Rew.substs ![⌜LO.FirstOrder.Arith.diag θ⌝]).hom (LO.FirstOrder.Arith.diag θ)

theorem LO.FirstOrder.Arith.substs_diag (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) (σ : LO.FirstOrder.Semisentence ℒₒᵣ 1) : (LO.FirstOrder.Rew.substs ![⌜σ⌝]).hom (LO.FirstOrder.Arith.diag θ) = ∀' ((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0, ⌜σ⌝, ⌜σ⌝]).hom (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.ssnum) ➝ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom θ)

theorem LO.FirstOrder.Arith.fixpoint_eq (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) : LO.FirstOrder.Arith.fixpoint θ = ∀' ((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0, ⌜LO.FirstOrder.Arith.diag θ⌝, ⌜LO.FirstOrder.Arith.diag θ⌝]).hom (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.ssnum) ➝ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom θ)

theorem LO.FirstOrder.Arith.diagonal {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T] (θ : LO.FirstOrder.Semisentence ℒₒᵣ 1) : T ⊢!. LO.FirstOrder.Arith.fixpoint θ ⭤ (LO.FirstOrder.Rew.substs ![⌜LO.FirstOrder.Arith.fixpoint θ⌝]).hom θ

def LO.FirstOrder.Arith.multidiag {k : ℕ} (θ : LO.FirstOrder.Semisentence ℒₒᵣ k) : LO.FirstOrder.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.

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

Equations

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

theorem LO.FirstOrder.Arith.multidiagonal {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T] {k : ℕ} {i : Fin k} (θ : Fin k → LO.FirstOrder.Semisentence ℒₒᵣ k) : T ⊢!. LO.FirstOrder.Arith.multifixpoint θ i ⭤ (LO.FirstOrder.Rew.substs fun (j : Fin k) => ⌜LO.FirstOrder.Arith.multifixpoint θ j⌝).hom (θ i)

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

theorem LO.FirstOrder.Arith.provableₐ_D2 {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T] {U : LO.FirstOrder.Theory ℒₒᵣ} [U.Delta1Definable] {σ : LO.FirstOrder.Sentence ℒₒᵣ} {π : LO.FirstOrder.Sentence ℒₒᵣ} : T ⊢!. U.bewₐ (σ ➝ π) ➝ U.bewₐ σ ➝ U.bewₐ π

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

theorem LO.FirstOrder.Arith.provableₐ_D3 {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T] {U : LO.FirstOrder.Theory ℒₒᵣ} [U.Delta1Definable] {σ : LO.FirstOrder.Sentence ℒₒᵣ} : T ⊢!. U.bewₐ σ ➝ U.bewₐ (U.bewₐ σ)

theorem LO.FirstOrder.Arith.goedel_iff_unprovable_goedel {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T] {U : LO.FirstOrder.Theory ℒₒᵣ} [U.Delta1Definable] : T ⊢!. U.goedelₐ ⭤ ∼U.bewₐ U.goedelₐ

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

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

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

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

theorem LO.FirstOrder.Arith.goedel_unprovable (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [LO.System.Consistent T] : T ⊬ ↑T.goedelₐ

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

theorem LO.FirstOrder.Arith.consistent_iff_goedel (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : T ⊢! ↑T.consistentₐ ⭤ ↑T.goedelₐ

theorem LO.FirstOrder.Arith.goedel_second_incompleteness (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [LO.System.Consistent T] : T ⊬ ↑T.consistentₐ

Gödel's Second Incompleteness Theorem

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

theorem LO.FirstOrder.Arith.inconsistent_undecidable (T : LO.FirstOrder.Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : LO.System.Undecidable T ↑T.consistentₐ