Formalized ${\mathrm{\Sigma }}_1$-Completeness

def LO.FirstOrder.«first_order_formulaLet_:=__;_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.«first_order_formulaLet'_:=__;_» : Lean.ParserDescr

Equations

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

inductive LO.FirstOrder.Theory.CobhamR0' : Theory ℒₒᵣ

• eq_refl : 𝐑₀' (“∀' !!(Semiterm.bvar 0) = !!(Semiterm.bvar 0)”)
• replace (φ : SyntacticSemiformula ℒₒᵣ 1) : 𝐑₀' (“∀' ∀' (!!(Semiterm.bvar 1) = !!(Semiterm.bvar 0) → !(φ/[Semiterm.bvar 1] ➝ φ/[Semiterm.bvar 0]))”)
• Ω₁ (n m : ℕ) : 𝐑₀' (“(!!↑n + !!↑m) = !!↑(n + m)”)
• Ω₂ (n m : ℕ) : 𝐑₀' (“(!!↑n * !!↑m) = !!↑(n * m)”)
• Ω₃ (n m : ℕ) : n ≠ m → 𝐑₀' (“¬!!↑n = !!↑m”)
• Ω₄ (n : ℕ) : 𝐑₀' (“∀' (!!(Semiterm.bvar 0) < !!↑n ↔ !(disjLt (fun (i : ℕ) => “!!(Semiterm.bvar 0) = !!↑i”) n))”)

Instances For

• LO.Arith.Formalized.Theory.CobhamR0'Delta1Definable
• LO.FirstOrder.Arith.CobhamR0'.subtheoryOfCobhamR0

def LO.FirstOrder.Theory.«term𝐑₀'» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐑₀'» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐑₀'» 1024 (Lean.ParserDescr.symbol "𝐑₀'")

@[reducible, inline]

abbrev LO.FirstOrder.Theory.addCobhamR0' (T : Theory ℒₒᵣ) : Theory ℒₒᵣ

Equations

• T.addCobhamR0' = T + 𝐑₀'

noncomputable instance LO.FirstOrder.Arith.CobhamR0'.subtheoryOfCobhamR0 : 𝐑₀' ≼ 𝐑₀

Equations

• LO.FirstOrder.Arith.CobhamR0'.subtheoryOfCobhamR0 = LO.System.Subtheory.ofAxm! @LO.FirstOrder.Arith.CobhamR0'.subtheoryOfCobhamR0.proof_2

theorem LO.FirstOrder.Arith.add_cobhamR0' {T : Theory ℒₒᵣ} [𝐑₀ ≼ T] {φ : SyntacticFormula ℒₒᵣ} : T ⊢! φ ↔ T + 𝐑₀' ⊢! φ

def LO.Arith.singleton {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] (φ : FirstOrder.SyntacticFormula L) : {φ}.Delta1Definable

Equations

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

@[simp]

theorem LO.Arith.singleton_toTDef_ch_val {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] (φ : FirstOrder.SyntacticFormula L) : FirstOrder.Arith.HierarchySymbol.Semiformula.val (FirstOrder.Theory.Delta1Definable.toTDef {φ}).ch = (“!!(FirstOrder.Semiterm.bvar 0) = !!↑⌜φ⌝”)

def LO.Arith.Formalized.Theory.CobhamR0'.eqRefl : {“∀' !!(FirstOrder.Semiterm.bvar 0) = !!(FirstOrder.Semiterm.bvar 0)”}.Delta1Definable

Equations

• LO.Arith.Formalized.Theory.CobhamR0'.eqRefl = LO.Arith.singleton (“∀' !!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.bvar 0)”)

def LO.Arith.Formalized.Theory.CobhamR0'.replace : FirstOrder.Theory.Delta1Definable {x : FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (φ : FirstOrder.SyntacticSemiformula ℒₒᵣ 1), (“∀' ∀' (!!(FirstOrder.Semiterm.bvar 1) = !!(FirstOrder.Semiterm.bvar 0) → !(φ/[FirstOrder.Semiterm.bvar 1] ➝ φ/[FirstOrder.Semiterm.bvar 0]))”) = x}

Equations

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

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₁ : FirstOrder.Theory.Delta1Definable {φ : FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ) (m : ℕ), φ = (“(!!↑n + !!↑m) = !!↑(n + m)”)}

Equations

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

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₂ : FirstOrder.Theory.Delta1Definable {φ : FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ) (m : ℕ), φ = (“(!!↑n * !!↑m) = !!↑(n * m)”)}

Equations

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

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₃ : FirstOrder.Theory.Delta1Definable {φ : FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ) (m : ℕ), n ≠ m ∧ φ = (“¬!!↑n = !!↑m”)}

Equations

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

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₄ : FirstOrder.Theory.Delta1Definable {x : FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ), (“∀' (!!(FirstOrder.Semiterm.bvar 0) < !!↑n ↔ !(disjLt (fun (i : ℕ) => “!!(FirstOrder.Semiterm.bvar 0) = !!↑i”) n))”) = x}

Equations

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

instance LO.Arith.Formalized.Theory.CobhamR0'Delta1Definable : 𝐑₀'.Delta1Definable

Equations

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

@[reducible, inline]

abbrev LO.Arith.Formalized.Theory.CobhamR0' {V : Type u_1} [ORingStruc V] : ⌜ℒₒᵣ⌝.Theory

Equations

• LO.Arith.Formalized.Theory.CobhamR0' = LO.FirstOrder.Theory.codeIn V 𝐑₀'

@[reducible, inline]

abbrev LO.Arith.Formalized.TTheory.CobhamR0' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜ℒₒᵣ⌝.TTheory

Equations

• ⌜𝐑₀'⌝ = LO.FirstOrder.Theory.tCodeIn V 𝐑₀'

def LO.Arith.Formalized.«term⌜𝐑₀'⌝» : Lean.ParserDescr

Equations

• LO.Arith.Formalized.«term⌜𝐑₀'⌝» = Lean.ParserDescr.node `LO.Arith.Formalized.«term⌜𝐑₀'⌝» 1024 (Lean.ParserDescr.symbol "⌜𝐑₀'⌝")

def LO.Arith.Formalized.«term⌜𝐑₀'⌝[_]» : Lean.ParserDescr

Equations

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

def LO.Arith.Formalized.Theory.CobhamR0'.eqRefl.proof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : ⌜𝐑₀'⌝ ⊢ ((bv 0 ⋯).equals (bv 0 ⋯)).all

Equations

• LO.Arith.Formalized.Theory.CobhamR0'.eqRefl.proof = LO.Arith.Language.Theory.TProof.byAxm ⋯

def LO.Arith.Formalized.Theory.CobhamR0'.replace.proof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) : ⌜𝐑₀'⌝ ⊢ ((bv 1 ⋯).equals (bv 0 ⋯) ➝ φ^/[(bv 1 ⋯).sing] ➝ φ^/[(bv 0 ⋯).sing]).all.all

Equations

• LO.Arith.Formalized.Theory.CobhamR0'.replace.proof φ = LO.Arith.Language.Theory.TProof.byAxm ⋯

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₁.proof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n m : V) : ⌜𝐑₀'⌝ ⊢ (typedNumeral 0 n + typedNumeral 0 m).equals (typedNumeral 0 (n + m))

Equations

• LO.Arith.Formalized.Theory.CobhamR0'.Ω₁.proof n m = LO.Arith.Language.Theory.TProof.byAxm ⋯

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₂.proof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n m : V) : ⌜𝐑₀'⌝ ⊢ (typedNumeral 0 n * typedNumeral 0 m).equals (typedNumeral 0 (n * m))

Equations

• LO.Arith.Formalized.Theory.CobhamR0'.Ω₂.proof n m = LO.Arith.Language.Theory.TProof.byAxm ⋯

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₃.proof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {n m : V} (ne : n ≠ m) : ⌜𝐑₀'⌝ ⊢ (typedNumeral 0 n).notEquals (typedNumeral 0 m)

Equations

• LO.Arith.Formalized.Theory.CobhamR0'.Ω₃.proof ne = LO.Arith.Language.Theory.TProof.byAxm ⋯

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₄.proof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) : ⌜𝐑₀'⌝ ⊢ ((bv 0 ⋯).lessThan (typedNumeral (0 + 1) n) ⭤ (tSubstItr (bv 0 ⋯).sing ((bv 1 ⋯).equals (bv 0 ⋯)) n).disj).all

Equations

• LO.Arith.Formalized.Theory.CobhamR0'.Ω₄.proof n = LO.Arith.Language.Theory.TProof.byAxm ⋯

instance LO.Arith.Formalized.Theory.addCobhamR0'Delta1Definable (T : FirstOrder.Theory ℒₒᵣ) [d : T.Delta1Definable] : (T + 𝐑₀').Delta1Definable

Equations

• LO.Arith.Formalized.Theory.addCobhamR0'Delta1Definable T = d.add LO.Arith.Formalized.Theory.CobhamR0'Delta1Definable

@[reducible, inline]

abbrev LO.FirstOrder.Theory.AddR₀TTheory {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : Theory ℒₒᵣ) [T.Delta1Definable] : ⌜ℒₒᵣ⌝.TTheory

Equations

• T.AddR₀TTheory = LO.FirstOrder.Theory.tCodeIn V (T + 𝐑₀')

Instances For

• LO.Arith.Formalized.instR₀TheoryAddR₀TTheory

@[simp]

theorem LO.Arith.Formalized.R₀'_subset_AddR₀ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] : ⌜𝐑₀'⌝ ⊆ T.AddR₀TTheory

@[simp]

theorem LO.Arith.Formalized.theory_subset_AddR₀ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] : FirstOrder.Theory.tCodeIn V T ⊆ T.AddR₀TTheory

instance LO.Arith.Formalized.instR₀TheoryAddR₀TTheory {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] : R₀Theory T.AddR₀TTheory

Equations

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

def LO.FirstOrder.Theory.Provableₐ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : Theory ℒₒᵣ) [T.Delta1Definable] (φ : V) : Prop

Provability predicate for arithmetic stronger than ${\mathbf{R}}_{\mathbf{0}}$.

Equations

• T.Provableₐ φ = (LO.FirstOrder.Theory.codeIn V (T + 𝐑₀')).Provable φ

Instances For

• LO.Arith.provableₐ_definable
• LO.Arith.provableₐ_definable'

theorem LO.Arith.provableₐ_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] {σ : FirstOrder.Sentence ℒₒᵣ} : T.Provableₐ ⌜σ⌝ ↔ FirstOrder.Theory.tCodeIn V (T + 𝐑₀') ⊢! ⌜σ⌝

def LO.FirstOrder.Theory.provableₐ (T : Theory ℒₒᵣ) [T.Delta1Definable] : 𝚺₁.Semisentence 1

Equations

• T.provableₐ = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma ((LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val (T + 𝐑₀').tDef.prv)/[LO.FirstOrder.Semiterm.bvar 0]) ⋯

theorem LO.Arith.provableₐ_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] : 𝚺₁-Predicate T.Provableₐ via T.provableₐ

@[simp]

theorem LO.Arith.eval_provableₐ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] (v : Fin 1 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val T.provableₐ) ↔ T.Provableₐ (v 0)

instance LO.Arith.provableₐ_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] : 𝚺₁-Predicate T.Provableₐ

instance LO.Arith.provableₐ_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : FirstOrder.Theory ℒₒᵣ) [T.Delta1Definable] : { Γ := 𝚺, rank := 0 + 1 }-Predicate T.Provableₐ

instance for definability tactic