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

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 ⊧ₘ* 𝐈𝚺₁] (σ : FirstOrder.Semisentence ℒₒᵣ 1) (n : ℕ) : substNumeral ⌜σ⌝ ↑n = ⌜σ/[↑n]⌝

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

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

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 ⊧ₘ* 𝐈𝚺₁] {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 ⊧ₘ* 𝐈𝚺₁] {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⌝)) σ⌝

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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₂ substNumeral via FirstOrder.Arith.ssnum

@[simp]

theorem LO.Arith.Formalized.eval_ssnum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.ssnum) ↔ v 0 = 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {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 ⊧ₘ* 𝐈𝚺₁] {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

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

Equations

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

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

Equations

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

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

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

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

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

${\mathrm{diag}}_i(\overrightarrow{x}):=(\mathrm{\forall }\overrightarrow{y})[(\underset{j}{\bigwedge }\mathrm{ssnums}(y_j,x_j,\overrightarrow{x}))\to {\theta }_i(\overrightarrow{y})]$

Equations

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

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

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 ℒₒᵣ} [𝐈𝚺₁ ≼ T] {k : ℕ} {i : Fin k} (θ : Fin k → Semisentence ℒₒᵣ k) : T ⊢!. multifixpoint θ i ⭤ (Rewriting.app (Rew.substs fun (j : Fin k) => ⌜multifixpoint θ j⌝)) (θ i)

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

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

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

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

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

theorem LO.FirstOrder.Arith.provableₐ_D2_context {T : Theory ℒₒᵣ} [𝐈𝚺₁ ≼ 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 ℒₒᵣ} [𝐈𝚺₁ ≼ 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] [𝐑₀ ≼ U] {σ : Sentence ℒₒᵣ} : T ⊢!. U.bewₐ σ → U ⊢! ↑σ

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

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

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

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

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

Gödel's Second Incompleteness Theorem

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

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