def LO.FirstOrder.succInd {L : Language} [L.ORing] {ξ : Type u_3} (φ : Semiformula L ξ 1) : Formula L ξ

Equations

• LO.FirstOrder.succInd φ = φ/[↑0] ➝ ∀' (φ/[LO.FirstOrder.Semiterm.bvar 0] ➝ φ/[‘(!!(LO.FirstOrder.Semiterm.bvar 0) + !!↑1)’]) ➝ ∀' φ/[LO.FirstOrder.Semiterm.bvar 0]

def LO.FirstOrder.orderInd {L : Language} [L.ORing] {ξ : Type u_3} (φ : Semiformula L ξ 1) : Formula L ξ

Equations

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

def LO.FirstOrder.leastNumber {L : Language} [L.ORing] {ξ : Type u_3} (φ : Semiformula L ξ 1) : Formula L ξ

Equations

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

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

• equal (φ : SyntacticFormula ℒₒᵣ) : φ ∈ 𝐄𝐐 → 𝐑₀ φ
• Ω₁ (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.FirstOrder.Arith.CobhamR0'.subtheoryOfCobhamR0
• LO.FirstOrder.Arith.CobhamR0.subTheoryPAMinus
• LO.FirstOrder.Arith.Standard.models_CobhamR0
• LO.FirstOrder.Arith.instModelsTheoryCobhamR0_arithmetization
• LO.FirstOrder.Arith.instSubtheorySyntacticFormulaORingTheoryCobhamR0_arithmetization
• LO.FirstOrder.Theory.CobhamR0.consistent
• LO.FirstOrder.Theory.EQ.subtheoryOfCobhamR0

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

Equations

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

inductive LO.FirstOrder.Theory.PAMinus : Theory ℒₒᵣ

• equal (φ : SyntacticFormula ℒₒᵣ) : φ ∈ 𝐄𝐐 → 𝐏𝐀⁻ φ
• addZero : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) + !!↑0) = !!(Semiterm.fvar 0)”)
• addAssoc : 𝐏𝐀⁻ (“((!!(Semiterm.fvar 0) + !!(Semiterm.fvar 1)) + !!(Semiterm.fvar 2)) = (!!(Semiterm.fvar 0) + (!!(Semiterm.fvar 1) + !!(Semiterm.fvar 2)))”)
• addComm : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) + !!(Semiterm.fvar 1)) = (!!(Semiterm.fvar 1) + !!(Semiterm.fvar 0))”)
• addEqOfLt : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) < !!(Semiterm.fvar 1) → ∃' (!!(Semiterm.fvar 0) + !!(Semiterm.bvar 0)) = !!(Semiterm.fvar 1))”)
• zeroLe : 𝐏𝐀⁻ (“!!↑0 ≤ !!(Semiterm.fvar 0)”)
• zeroLtOne : 𝐏𝐀⁻ (“!!↑0 < !!↑1”)
• oneLeOfZeroLt : 𝐏𝐀⁻ (“(!!↑0 < !!(Semiterm.fvar 0) → !!↑1 ≤ !!(Semiterm.fvar 0))”)
• addLtAdd : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) < !!(Semiterm.fvar 1) → (!!(Semiterm.fvar 0) + !!(Semiterm.fvar 2)) < (!!(Semiterm.fvar 1) + !!(Semiterm.fvar 2)))”)
• mulZero : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) * !!↑0) = !!↑0”)
• mulOne : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) * !!↑1) = !!(Semiterm.fvar 0)”)
• mulAssoc : 𝐏𝐀⁻ (“((!!(Semiterm.fvar 0) * !!(Semiterm.fvar 1)) * !!(Semiterm.fvar 2)) = (!!(Semiterm.fvar 0) * (!!(Semiterm.fvar 1) * !!(Semiterm.fvar 2)))”)
• mulComm : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) * !!(Semiterm.fvar 1)) = (!!(Semiterm.fvar 1) * !!(Semiterm.fvar 0))”)
• mulLtMul : 𝐏𝐀⁻ (“((!!(Semiterm.fvar 0) < !!(Semiterm.fvar 1) ∧ !!↑0 < !!(Semiterm.fvar 2)) → (!!(Semiterm.fvar 0) * !!(Semiterm.fvar 2)) < (!!(Semiterm.fvar 1) * !!(Semiterm.fvar 2)))”)
• distr : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) * (!!(Semiterm.fvar 1) + !!(Semiterm.fvar 2))) = ((!!(Semiterm.fvar 0) * !!(Semiterm.fvar 1)) + (!!(Semiterm.fvar 0) * !!(Semiterm.fvar 2)))”)
• ltIrrefl : 𝐏𝐀⁻ (“¬!!(Semiterm.fvar 0) < !!(Semiterm.fvar 0)”)
• ltTrans : 𝐏𝐀⁻ (“((!!(Semiterm.fvar 0) < !!(Semiterm.fvar 1) ∧ !!(Semiterm.fvar 1) < !!(Semiterm.fvar 2)) → !!(Semiterm.fvar 0) < !!(Semiterm.fvar 2))”)
• ltTri : 𝐏𝐀⁻ (“(!!(Semiterm.fvar 0) < !!(Semiterm.fvar 1) ∨ (!!(Semiterm.fvar 0) = !!(Semiterm.fvar 1) ∨ !!(Semiterm.fvar 1) < !!(Semiterm.fvar 0)))”)

Instances For

• LO.Arith.instModelsTheoryPAMinusOfIOpen_arithmetization
• LO.FirstOrder.Arith.CobhamR0.subTheoryPAMinus
• LO.FirstOrder.Arith.Nonstandard.instModelsTheoryPAMinus
• LO.FirstOrder.Arith.Standard.models_PAMinus
• LO.FirstOrder.Arith.instModelsTheoryPAMinusOfIOpen
• LO.FirstOrder.Arith.models_PAMinus_of_models_peano
• LO.FirstOrder.Theory.EQ.subtheoryOfPAMinus
• LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH

def LO.FirstOrder.Theory.«term𝐏𝐀⁻» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐏𝐀⁻» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐏𝐀⁻» 1024 (Lean.ParserDescr.symbol "𝐏𝐀⁻")

def LO.FirstOrder.Theory.indScheme (L : Language) [L.ORing] (Γ : Semiformula L ℕ 1 → Prop) : Theory L

Equations

• LO.FirstOrder.Theory.indScheme L Γ = {ψ : LO.FirstOrder.SyntacticFormula L | ∃ (φ : LO.FirstOrder.Semiformula L ℕ 1), Γ φ ∧ ψ = LO.FirstOrder.succInd φ}

Instances For

• LO.Arith.instModelsTheoryIndSchemeORingHierarchyNatAlt_arithmetization
• LO.Arith.instModelsTheoryIndSchemeORingHierarchyNatOfSigmaPolarity_arithmetization
• LO.FirstOrder.Arith.indScheme_of_indH
• LO.FirstOrder.Arith.instModelsTheoryIndSchemeORingOpenNatOfIOpen

@[reducible, inline]

abbrev LO.FirstOrder.Theory.iOpen : Theory ℒₒᵣ

Equations

• 𝐈open = 𝐏𝐀⁻ + LO.FirstOrder.Theory.indScheme ℒₒᵣ LO.FirstOrder.Semiformula.Open

Instances For

• LO.Arith.instModelsTheoryIOpenOfISigmaOfNatNat_arithmetization
• LO.FirstOrder.Theory.EQ.subtheoryOfIOpen

def LO.FirstOrder.Theory.«term𝐈open» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐈open» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐈open» 1024 (Lean.ParserDescr.symbol "𝐈open")

@[reducible, inline]

abbrev LO.FirstOrder.Theory.indH (Γ : Polarity) (k : ℕ) : Theory ℒₒᵣ

Equations

• 𝐈𝐍𝐃Γ k = 𝐏𝐀⁻ + LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ k)

Instances For

• LO.Arith.instModelsTheoryIndHOfISigma_arithmetization
• LO.FirstOrder.Arith.Standard.models_iSigma
• LO.FirstOrder.Theory.EQ.subtheoryOfIndH
• LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH

def LO.FirstOrder.Theory.«term𝐈𝐍𝐃_» : Lean.ParserDescr

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.iSigma (k : ℕ) : Theory ℒₒᵣ

Equations

• 𝐈𝚺k = 𝐈𝐍𝐃𝚺 k

Instances For

• LO.Arith.instModelsTheoryISigmaOfIPi_arithmetization
• LO.Arith.instModelsTheoryISigmaOfNatNat_arithmetization
• LO.Arith.instModelsTheoryISigmaOfNatNat_arithmetization_1
• LO.FirstOrder.Arith.Standard.models_iSigmaOne
• LO.FirstOrder.Arith.Standard.models_iSigmaZero

def LO.FirstOrder.Theory.«term𝐈𝚺_» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐈𝚺_» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐈𝚺_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝐈𝚺") (Lean.ParserDescr.cat `term 1024))

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.iPi (k : ℕ) : Theory ℒₒᵣ

Equations

• 𝐈𝚷k = 𝐈𝐍𝐃𝚷 k

Instances For

• LO.Arith.instModelsTheoryIPiOfISigma_arithmetization

def LO.FirstOrder.Theory.«term𝐈𝚷_» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐈𝚷_» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐈𝚷_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝐈𝚷") (Lean.ParserDescr.cat `term 1024))

def LO.FirstOrder.Theory.«term𝐈𝚷₀» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Theory.«term𝐈𝚺₁» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐈𝚺₁» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐈𝚺₁» 1024 (Lean.ParserDescr.symbol "𝐈𝚺₁")

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.peano : Theory ℒₒᵣ

Equations

• 𝐏𝐀 = 𝐏𝐀⁻ + LO.FirstOrder.Theory.indScheme ℒₒᵣ Set.univ

Instances For

• LO.FirstOrder.Arith.Standard.models_peano
• LO.FirstOrder.Theory.Peano.consistent

def LO.FirstOrder.Theory.«term𝐏𝐀» : Lean.ParserDescr

Equations

• LO.FirstOrder.Theory.«term𝐏𝐀» = Lean.ParserDescr.node `LO.FirstOrder.Theory.«term𝐏𝐀» 1024 (Lean.ParserDescr.symbol "𝐏𝐀")

theorem LO.FirstOrder.Theory.coe_indH_subset_indH {L : Language} [L.ORing] {Γ : Polarity} {ν : ℕ} : ⇑(Semiformula.lMap Language.oringEmb) '' indScheme ℒₒᵣ (Arith.Hierarchy Γ ν) ⊆ indScheme L (Arith.Hierarchy Γ ν)

instance LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH {Γ : Polarity} {n : ℕ} : 𝐏𝐀⁻ ≼ 𝐈𝐍𝐃Γ n

Equations

• LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH = LO.System.Subtheory.ofSubset ⋯

instance LO.FirstOrder.Theory.EQ.subtheoryOfCobhamR0 : 𝐄𝐐 ≼ 𝐑₀

Equations

• LO.FirstOrder.Theory.EQ.subtheoryOfCobhamR0 = LO.System.Subtheory.ofSubset ⋯

instance LO.FirstOrder.Theory.EQ.subtheoryOfPAMinus : 𝐄𝐐 ≼ 𝐏𝐀⁻

Equations

• LO.FirstOrder.Theory.EQ.subtheoryOfPAMinus = LO.System.Subtheory.ofSubset ⋯

instance LO.FirstOrder.Theory.EQ.subtheoryOfIndH {Γ : Polarity} {n : ℕ} : 𝐄𝐐 ≼ 𝐈𝐍𝐃Γ n

Equations

• LO.FirstOrder.Theory.EQ.subtheoryOfIndH = LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH.comp LO.FirstOrder.Theory.EQ.subtheoryOfPAMinus

instance LO.FirstOrder.Theory.EQ.subtheoryOfIOpen : 𝐄𝐐 ≼ 𝐈open

Equations

• LO.FirstOrder.Theory.EQ.subtheoryOfIOpen = inferInstance.comp LO.FirstOrder.Theory.EQ.subtheoryOfPAMinus