Formalized $\Sigma_1$-Completeness #

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

inductive LO.FirstOrder.Theory.CobhamR0' :

LO.FirstOrder.Theory ℒₒᵣ

eq_refl: 𝐑₀' (“∀' !!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.bvar 0)”)
replace: ∀ (p : LO.FirstOrder.SyntacticSemiformula ℒₒᵣ 1), 𝐑₀' (“∀' ∀' (!!(LO.FirstOrder.Semiterm.bvar 1) = !!(LO.FirstOrder.Semiterm.bvar 0) → !((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 1]).hom p ➝ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom p))”)
Ω₁: ∀ (n m : ℕ), 𝐑₀' (“(!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) + !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ m))) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (n + m)))”)
Ω₂: ∀ (n m : ℕ), 𝐑₀' (“(!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) * !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ m))) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (n * m)))”)
Ω₃: ∀ (n m : ℕ), n ≠ m → 𝐑₀' (“¬!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ m))”)
Ω₄: ∀ (n : ℕ), 𝐑₀' (“∀' (!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) ↔ !(LO.disjLt (fun (i : ℕ) => “!!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ i))”) n))”)

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

@[reducible, inline]

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

LO.FirstOrder.Theory ℒₒᵣ

Equations

T.addCobhamR0' = T + 𝐑₀'

Instances For

source

noncomputable instance LO.FirstOrder.Arith.CobhamR0'.subtheoryOfCobhamR0 :

𝐑₀' ≼ 𝐑₀

Equations

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

source

theorem LO.FirstOrder.Arith.add_cobhamR0' {T : LO.FirstOrder.Theory ℒₒᵣ} [𝐑₀ ≼ T] {p : LO.FirstOrder.SyntacticFormula ℒₒᵣ} :

T ⊢! p ↔ T + 𝐑₀' ⊢! p

source

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

{p}.Delta1Definable

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.eqRefl :

{“∀' !!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.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)”)

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.replace :

LO.FirstOrder.Theory.Delta1Definable {x : LO.FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (p : LO.FirstOrder.SyntacticSemiformula ℒₒᵣ 1), (“∀' ∀' (!!(LO.FirstOrder.Semiterm.bvar 1) = !!(LO.FirstOrder.Semiterm.bvar 0) → !((LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 1]).hom p ➝ (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]).hom p))”) = x}

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₁ :

LO.FirstOrder.Theory.Delta1Definable {p : LO.FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ) (m : ℕ), p = (“(!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) + !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ m))) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (n + m)))”)}

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₂ :

LO.FirstOrder.Theory.Delta1Definable {p : LO.FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ) (m : ℕ), p = (“(!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) * !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ m))) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ (n * m)))”)}

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₃ :

LO.FirstOrder.Theory.Delta1Definable {p : LO.FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ) (m : ℕ), n ≠ m ∧ p = (“¬!!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ m))”)}

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₄ :

LO.FirstOrder.Theory.Delta1Definable {x : LO.FirstOrder.SyntacticFormula ℒₒᵣ | ∃ (n : ℕ), (“∀' (!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ n)) ↔ !(LO.disjLt (fun (i : ℕ) => “!!(LO.FirstOrder.Semiterm.bvar 0) = !!(LO.FirstOrder.Semiterm.Operator.const (LO.FirstOrder.Semiterm.Operator.numeral ℒₒᵣ i))”) n))”) = x}

Equations

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

Instances For

source

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

𝐑₀'.Delta1Definable

Equations

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

source

@[reducible, inline]

abbrev LO.Arith.Formalized.Theory.CobhamR0' {V : Type u_1} [LO.ORingStruc V] :

⌜ℒₒᵣ⌝.Theory

Equations

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

Instances For

source

@[reducible, inline]

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

⌜ℒₒᵣ⌝.TTheory

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.eqRefl.proof {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] :

⌜𝐑₀'⌝ ⊢ ((LO.Arith.bv 0 ⋯).equals (LO.Arith.bv 0 ⋯)).all

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.replace.proof {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) :

⌜𝐑₀'⌝ ⊢ ((LO.Arith.bv 1 ⋯).equals (LO.Arith.bv 0 ⋯) ➝ p^/[(LO.Arith.bv 1 ⋯).sing] ➝ p^/[(LO.Arith.bv 0 ⋯).sing]).all.all

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₁.proof {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) (m : V) :

⌜𝐑₀'⌝ ⊢ (LO.Arith.Formalized.typedNumeral 0 n + LO.Arith.Formalized.typedNumeral 0 m).equals (LO.Arith.Formalized.typedNumeral 0 (n + m))

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₂.proof {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) (m : V) :

⌜𝐑₀'⌝ ⊢ (LO.Arith.Formalized.typedNumeral 0 n * LO.Arith.Formalized.typedNumeral 0 m).equals (LO.Arith.Formalized.typedNumeral 0 (n * m))

Equations

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

Instances For

source

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

⌜𝐑₀'⌝ ⊢ (LO.Arith.Formalized.typedNumeral 0 n).notEquals (LO.Arith.Formalized.typedNumeral 0 m)

Equations

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

Instances For

source

def LO.Arith.Formalized.Theory.CobhamR0'.Ω₄.proof {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (n : V) :

⌜𝐑₀'⌝ ⊢ ((LO.Arith.bv 0 ⋯).lessThan (LO.Arith.Formalized.typedNumeral (0 + 1) n) ⭤ (LO.Arith.Formalized.tSubstItr (LO.Arith.bv 0 ⋯).sing ((LO.Arith.bv 1 ⋯).equals (LO.Arith.bv 0 ⋯)) n).disj).all

Equations

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

Instances For

source

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

(T + 𝐑₀').Delta1Definable

Equations

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

source

@[reducible, inline]

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

⌜ℒₒᵣ⌝.TTheory

Equations

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

Instances For

source

@[simp]

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

⌜𝐑₀'⌝ ⊆ T.AddR₀TTheory

source

@[simp]

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

LO.FirstOrder.Theory.tCodeIn V T ⊆ T.AddR₀TTheory

source

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

LO.Arith.Formalized.R₀Theory T.AddR₀TTheory

Equations

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

source

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

Prop

Provability predicate for arithmetic stronger than $\mathbf{R_0}$.

Equations

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

Instances For

source

theorem LO.Arith.provableₐ_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : LO.FirstOrder.Theory ℒₒᵣ} [T.Delta1Definable] {σ : LO.FirstOrder.Sentence ℒₒᵣ} :

T.Provableₐ ⌜σ⌝ ↔ LO.FirstOrder.Theory.tCodeIn V (T + 𝐑₀') ⊢! ⌜σ⌝

source

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

𝚺₁.Semisentence 1

Equations

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

Instances For

source

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

𝚺₁ -Predicate T.Provableₐ via T.provableₐ

source

@[simp]

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

V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val T.provableₐ) ↔ T.Provableₐ (v 0)

source

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

𝚺₁ -Predicate T.Provableₐ

Equations

⋯ = ⋯

source

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

{ Γ := 𝚺, rank := 0 + 1 }-Predicate T.Provableₐ

instance for definability tactic

Equations

⋯ = ⋯

Documentation

Incompleteness.Arith.Theory

Formalized $\Sigma_1$-Completeness #