Documentation

Foundation.FirstOrder.Arith.StrictHierarchy

inductive LO.FirstOrder.Arith.StrictHierarchy {L : Language} [L.LT] {μ : Type u_2} :
Polarity{n : } → Semiformula L μ nProp
Instances For
    theorem LO.FirstOrder.Arith.DeltaZero.of_open {L : Language} [L.LT] {μ : Type u_1} {n : } {φ : Semiformula L μ n} :
    φ.OpenDeltaZero φ
    theorem LO.FirstOrder.Arith.StrictHierarchy.rew {L : Language} [L.LT] {μ₁ : Type u_1} {n₁ : } {Γ : Polarity} {s : } {μ₂ : Type u_2} {n₂ : } {φ : Semiformula L μ₁ n₁} (h : StrictHierarchy Γ s φ) (ω : Rew L μ₁ n₁ μ₂ n₂) :
    theorem LO.FirstOrder.Arith.StrictHierarchy.rew_iff {L : Language} [L.LT] {μ₁ : Type u_1} {n₁ : } {μ₂ : Type u_2} {n₂ : } {Γ : Polarity} {s : } {φ : Semiformula L μ₁ n₁} (ω : Rew L μ₁ n₁ μ₂ n₂) :
    theorem LO.FirstOrder.Arith.StrictHierarchy.succ {L : Language} [L.LT] {μ₁ : Type u_1} {n₁ s : } {Γ : Polarity} {φ : Semiformula L μ₁ n₁} (h : StrictHierarchy Γ s φ) :
    StrictHierarchy Γ (s + 1) φ