Theory

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

Imported declaration from the Incompleteness formalization.

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 ξ

Imported declaration from the Incompleteness formalization.

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 ξ

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• 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))”)

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.addZero {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.addZero = (“(!!(LO.FirstOrder.Semiterm.fvar 0) + !!↑0) = !!(LO.FirstOrder.Semiterm.fvar 0)”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.addAssoc {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.addComm {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.addComm = (“(!!(LO.FirstOrder.Semiterm.fvar 0) + !!(LO.FirstOrder.Semiterm.fvar 1)) = (!!(LO.FirstOrder.Semiterm.fvar 1) + !!(LO.FirstOrder.Semiterm.fvar 0))”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.addEqOfLt {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.zeroLe {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.zeroLe = (“!!↑0 ≤ !!(LO.FirstOrder.Semiterm.fvar 0)”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.zeroLtOne {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.zeroLtOne = (“!!↑0 < !!↑1”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.oneLeOfZeroLt {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.oneLeOfZeroLt = (“(!!↑0 < !!(LO.FirstOrder.Semiterm.fvar 0) → !!↑1 ≤ !!(LO.FirstOrder.Semiterm.fvar 0))”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.addLtAdd {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.mulZero {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.mulZero = (“(!!(LO.FirstOrder.Semiterm.fvar 0) * !!↑0) = !!↑0”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.mulOne {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.mulOne = (“(!!(LO.FirstOrder.Semiterm.fvar 0) * !!↑1) = !!(LO.FirstOrder.Semiterm.fvar 0)”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.mulAssoc {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.mulComm {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.mulComm = (“(!!(LO.FirstOrder.Semiterm.fvar 0) * !!(LO.FirstOrder.Semiterm.fvar 1)) = (!!(LO.FirstOrder.Semiterm.fvar 1) * !!(LO.FirstOrder.Semiterm.fvar 0))”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.mulLtMul {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.distr {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.ltIrrefl {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Arith.ltIrrefl = (“¬!!(LO.FirstOrder.Semiterm.fvar 0) < !!(LO.FirstOrder.Semiterm.fvar 0)”)

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.ltTrans {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Theory.Arith.ltTri {L : Language} [L.ORing] : SyntacticFormula L

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• equal (φ : SyntacticFormula ℒₒᵣ) : φ ∈ 𝐄𝐐 → 𝐏𝐀⁻ φ
• addZero : 𝐏𝐀⁻ Arith.addZero
• addAssoc : 𝐏𝐀⁻ Arith.addAssoc
• addComm : 𝐏𝐀⁻ Arith.addComm
• addEqOfLt : 𝐏𝐀⁻ Arith.addEqOfLt
• zeroLe : 𝐏𝐀⁻ Arith.zeroLe
• zeroLtOne : 𝐏𝐀⁻ Arith.zeroLtOne
• oneLeOfZeroLt : 𝐏𝐀⁻ Arith.oneLeOfZeroLt
• addLtAdd : 𝐏𝐀⁻ Arith.addLtAdd
• mulZero : 𝐏𝐀⁻ Arith.mulZero
• mulOne : 𝐏𝐀⁻ Arith.mulOne
• mulAssoc : 𝐏𝐀⁻ Arith.mulAssoc
• mulComm : 𝐏𝐀⁻ Arith.mulComm
• mulLtMul : 𝐏𝐀⁻ Arith.mulLtMul
• distr : 𝐏𝐀⁻ Arith.distr
• ltIrrefl : 𝐏𝐀⁻ Arith.ltIrrefl
• ltTrans : 𝐏𝐀⁻ Arith.ltTrans
• ltTri : 𝐏𝐀⁻ Arith.ltTri

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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 ℒₒᵣ

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• 𝐈Sgk = 𝐈𝐍𝐃Sg k

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• 𝐈Pgk = 𝐈𝐍𝐃Pg k

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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 Γ ν)

theorem LO.FirstOrder.Theory.indScheme_subset {C C' : Semiformula ℒₒᵣ ℕ 1 → Prop} (h : ∀ {φ : Semiformula ℒₒᵣ ℕ 1}, C φ → C' φ) : indScheme ℒₒᵣ C ⊆ indScheme ℒₒᵣ C'

theorem LO.FirstOrder.Theory.iSigma_subset_mono {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝐈Sgs₁ ⊆ 𝐈Sgs₂

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingPeanoMinusIndH {Γ : Polarity} {n : ℕ} : 𝐏𝐀⁻ wkn 𝐈𝐍𝐃Γ n

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingEqAxiomCobhamR0 : 𝐄𝐐 wkn 𝐑₀

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingEqAxiomPeanoMinus : 𝐄𝐐 wkn 𝐏𝐀⁻

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingEqAxiomIndH {Γ : Polarity} {n : ℕ} : 𝐄𝐐 wkn 𝐈𝐍𝐃Γ n

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingEqAxiomIOpen : 𝐄𝐐 wkn 𝐈open

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingIOpenISigma (i : ℕ) : 𝐈open wkn 𝐈Sgi

theorem LO.FirstOrder.Theory.iSigma_weakerThan_of_le {s₁ s₂ : ℕ} (h : s₁ ≤ s₂) : 𝐈Sgs₁ wkn 𝐈Sgs₂

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingISigmaOfNatNat : 𝐈Sg0 wkn 𝐈Sg1

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaORingISigmaPeano (i : ℕ) : 𝐈Sgi wkn 𝐏𝐀

@[simp]

theorem LO.FirstOrder.Theory.PeanoMinus.finite : Set.Finite 𝐏𝐀⁻