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

Equations

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

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

Equations

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

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

Equations

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

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

• equal: ∀ p ∈ 𝐄𝐐, 𝐑₀ 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

• 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 : LO.FirstOrder.Theory ℒₒᵣ

• equal: ∀ p ∈ 𝐄𝐐, 𝐏𝐀⁻ p
• addZero: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) + 0) = !!(LO.FirstOrder.Semiterm.fvar 0)”)
• addAssoc: 𝐏𝐀⁻ (“((!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.fvar 1)) + !!(LO.FirstOrder.Semiterm.fvar 2)) = (!!(LO.FirstOrder.Semiterm.fvar 0) + (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 2)))”)
• addComm: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.fvar 1)) = (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 0))”)
• addEqOfLt: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) → ∃' (!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.bvar 0)) = !!(LO.FirstOrder.Semiterm.fvar 1))”)
• zeroLe: 𝐏𝐀⁻ (“0 ≤ !!(LO.FirstOrder.Semiterm.fvar 0)”)
• zeroLtOne: 𝐏𝐀⁻ (“0 < 1”)
• oneLeOfZeroLt: 𝐏𝐀⁻ (“(0 < !!(LO.FirstOrder.Semiterm.fvar 0) → 1 ≤ !!(LO.FirstOrder.Semiterm.fvar 0))”)
• addLtAdd: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) → (!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.fvar 2)) < (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 2)))”)
• mulZero: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) * 0) = 0”)
• mulOne: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) * 1) = !!(LO.FirstOrder.Semiterm.fvar 0)”)
• mulAssoc: 𝐏𝐀⁻ (“((!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 1)) * !!(LO.FirstOrder.Semiterm.fvar 2)) = (!!(LO.FirstOrder.Semiterm.fvar 0) * (!!(LO.FirstOrder.Semiterm.fvar 1) * !!(LO.FirstOrder.Semiterm.fvar 2)))”)
• mulComm: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 1)) = (!!(LO.FirstOrder.Semiterm.fvar 1) * !!(LO.FirstOrder.Semiterm.fvar 0))”)
• mulLtMul: 𝐏𝐀⁻ (“((!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) ∧ 0 < !!(LO.FirstOrder.Semiterm.fvar 2)) → (!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 2)) < (!!(LO.FirstOrder.Semiterm.fvar 1) * !!(LO.FirstOrder.Semiterm.fvar 2)))”)
• distr: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) * (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 2))) = ((!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 1)) + (!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 2)))”)
• ltIrrefl: 𝐏𝐀⁻ (“¬!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 0)”)
• ltTrans: 𝐏𝐀⁻ (“((!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) ∧ !!(LO.FirstOrder.Semiterm.fvar 1) < !!(LO.FirstOrder.Semiterm.fvar 2)) → !!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 2))”)
• ltTri: 𝐏𝐀⁻ (“(!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 1) ∨ (!!(LO.FirstOrder.Semiterm.fvar 0) = !!(LO.FirstOrder.Semiterm.fvar 1) ∨ !!(LO.FirstOrder.Semiterm.fvar 1) < !!(LO.FirstOrder.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 : LO.FirstOrder.Language) [L.ORing] (Γ : LO.FirstOrder.Semiformula L ℕ 1 → Prop) : LO.FirstOrder.Theory L

Equations

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

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 : LO.FirstOrder.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 (Γ : LO.Polarity) (k : ℕ) : LO.FirstOrder.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

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.iSigma (k : ℕ) : LO.FirstOrder.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 : ℕ) : LO.FirstOrder.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 : LO.FirstOrder.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 : LO.FirstOrder.Language} [L.ORing] {Γ : LO.Polarity} {ν : ℕ} : ⇑(LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) '' LO.FirstOrder.Theory.indScheme ℒₒᵣ (LO.FirstOrder.Arith.Hierarchy Γ ν) ⊆ LO.FirstOrder.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Γ ν)

instance LO.FirstOrder.Theory.PAMinus.subtheoryOfIndH {Γ : LO.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 {Γ : LO.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