Documentation

Foundation.FirstOrder.Arith.Hierarchy

inductive LO.FirstOrder.Arith.Hierarchy {L : LO.FirstOrder.Language} [L.LT] {ξ : Type v} :
LO.Polarity{n : } → LO.FirstOrder.Semiformula L ξ nProp
Instances For
    @[simp]
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.equal {ξ : Type v} {L : LO.FirstOrder.Language} [L.Eq] [L.LT] {n : } {Γ : LO.Polarity} {s : } {t : LO.FirstOrder.Semiterm L ξ n} {u : LO.FirstOrder.Semiterm L ξ n} :
    LO.FirstOrder.Arith.Hierarchy Γ s (“!!t = !!u)
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.lt {ξ : Type v} {L : LO.FirstOrder.Language} [L.LT] {n : } {Γ : LO.Polarity} {s : } {t : LO.FirstOrder.Semiterm L ξ n} {u : LO.FirstOrder.Semiterm L ξ n} :
    LO.FirstOrder.Arith.Hierarchy Γ s (“!!t < !!u)
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.le {ξ : Type v} {L : LO.FirstOrder.Language} [L.Eq] [L.LT] {n : } {Γ : LO.Polarity} {s : } {t : LO.FirstOrder.Semiterm L ξ n} {u : LO.FirstOrder.Semiterm L ξ n} :
    LO.FirstOrder.Arith.Hierarchy Γ s (“!!t ≤ !!u)
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.ball_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type v} {Γ : LO.Polarity} {s : } {n : } {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)} (ht : t.Positive) :
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.bex_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type v} {Γ : LO.Polarity} {s : } {n : } {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)} (ht : t.Positive) :
    theorem LO.FirstOrder.Arith.Hierarchy.rew {L : LO.FirstOrder.Language} [L.LT] {ξ₁ : Type u_1} {n₁ : } {ξ₂ : Type u_2} {n₂ : } {Γ : LO.Polarity} {s : } (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {p : LO.FirstOrder.Semiformula L ξ₁ n₁} :
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.rew_iff {L : LO.FirstOrder.Language} [L.LT] {ξ₁ : Type u_1} {n₁ : } {ξ₂ : Type u_2} {n₂ : } {Γ : LO.Polarity} {s : } {ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {p : LO.FirstOrder.Semiformula L ξ₁ n₁} :
    Equations
    • LO.FirstOrder.Arith.Hierarchy.instAndOrClosedSemiformula = { verum := , falsum := , and := , or := }
    Equations
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.matrix_conj_iff {ξ : Type v} {L : LO.FirstOrder.Language} [L.ORing] {m : } {b : LO.Polarity} {s : } {n : } {p : Fin mLO.FirstOrder.Semiformula L ξ n} :
    LO.FirstOrder.Arith.Hierarchy b s (Matrix.conj fun (j : Fin m) => p j) ∀ (j : Fin m), LO.FirstOrder.Arith.Hierarchy b s (p j)
    theorem LO.FirstOrder.Arith.sigma₁_induction {ξ : Type v} {P : (n : ) → LO.FirstOrder.Semiformula ℒₒᵣ ξ nProp} (hVerum : ∀ (n : ), P n ) (hFalsum : ∀ (n : ), P n ) (hEQ : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.rel op(=) ![t₁, t₂])) (hNEQ : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.nrel op(=) ![t₁, t₂])) (hLT : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.rel op(<) ![t₁, t₂])) (hNLT : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.nrel op(<) ![t₁, t₂])) (hAnd : ∀ (n : ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pLO.FirstOrder.Arith.Hierarchy 𝚺 1 qP n pP n qP n (p q)) (hOr : ∀ (n : ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pLO.FirstOrder.Arith.Hierarchy 𝚺 1 qP n pP n qP n (p q)) (hBall : ∀ (n : ) (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pP (n + 1) pP n (“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Rew.bShift t)] !p)”)) (hEx : ∀ (n : ) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pP (n + 1) pP n (∃' p)) (n : ) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ n) :
    theorem LO.FirstOrder.Arith.sigma₁_induction' {ξ : Type v} {n : } {p : LO.FirstOrder.Semiformula ℒₒᵣ ξ n} (hp : LO.FirstOrder.Arith.Hierarchy 𝚺 1 p) {P : (n : ) → LO.FirstOrder.Semiformula ℒₒᵣ ξ nProp} (hVerum : ∀ (n : ), P n ) (hFalsum : ∀ (n : ), P n ) (hEQ : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.rel op(=) ![t₁, t₂])) (hNEQ : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.nrel op(=) ![t₁, t₂])) (hLT : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.rel op(<) ![t₁, t₂])) (hNLT : ∀ (n : ) (t₁ t₂ : LO.FirstOrder.Semiterm ℒₒᵣ ξ n), P n (LO.FirstOrder.Semiformula.nrel op(<) ![t₁, t₂])) (hAnd : ∀ (n : ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pLO.FirstOrder.Arith.Hierarchy 𝚺 1 qP n pP n qP n (p q)) (hOr : ∀ (n : ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pLO.FirstOrder.Arith.Hierarchy 𝚺 1 qP n pP n qP n (p q)) (hBall : ∀ (n : ) (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pP (n + 1) pP n (“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Rew.bShift t)] !p)”)) (hEx : ∀ (n : ) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)), LO.FirstOrder.Arith.Hierarchy 𝚺 1 pP (n + 1) pP n (∃' p)) :
    P n p