inductive
LO.FirstOrder.Arith.StrictHierarchy
{L : Language}
[L.LT]
{μ : Type u_2}
:
Polarity → ℕ → {n : ℕ} → Semiformula L μ n → Prop
- zero {L : Language} [L.LT] {μ : Type u_2} {x✝ s : ℕ} {Γ : Polarity} {φ : Semiformula L μ x✝} : DeltaZero φ → StrictHierarchy Γ s φ
- sigma {L : Language} [L.LT] {μ : Type u_2} {s n : ℕ} {φ : Semiformula L μ (n + 1)} : StrictHierarchy 𝚷 s φ → StrictHierarchy 𝚺 (s + 1) (∃' φ)
- pi {L : Language} [L.LT] {μ : Type u_2} {s n : ℕ} {φ : Semiformula L μ (n + 1)} : StrictHierarchy 𝚺 s φ → StrictHierarchy 𝚷 (s + 1) (∀' φ)
- ex {L : Language} [L.LT] {μ : Type u_2} {s n : ℕ} {φ : Semiformula L μ (n + 1)} : StrictHierarchy 𝚺 (s + 1) φ → StrictHierarchy 𝚺 (s + 1) (∃' φ)
- all {L : Language} [L.LT] {μ : Type u_2} {s n : ℕ} {φ : Semiformula L μ (n + 1)} : StrictHierarchy 𝚷 (s + 1) φ → StrictHierarchy 𝚷 (s + 1) (∀' φ)
theorem
LO.FirstOrder.Arith.DeltaZero.of_open
{L : Language}
[L.LT]
{μ : Type u_1}
{n : ℕ}
{φ : Semiformula L μ n}
:
φ.Open → DeltaZero φ
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₂)
:
StrictHierarchy Γ s ((Rewriting.app ω) φ)
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₂)
:
StrictHierarchy Γ s ((Rewriting.app ω) φ) ↔ StrictHierarchy Γ s φ
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) φ
theorem
LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero
{L : Language}
[L.LT]
{μ : Type u_1}
{n : ℕ}
{Γ : Polarity}
{φ : Semiformula L μ n}
:
StrictHierarchy Γ 0 φ ↔ DeltaZero φ