inductive
LO.FirstOrder.Arith.StrictHierarchy
{L : LO.FirstOrder.Language}
[L.LT]
{μ : Type u_2}
:
LO.Polarity → ℕ → {n : ℕ} → LO.FirstOrder.Semiformula L μ n → Prop
- zero: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {μ : Type u_2} {x s : ℕ} {Γ : LO.Polarity} {φ : LO.FirstOrder.Semiformula L μ x}, LO.FirstOrder.Arith.DeltaZero φ → LO.FirstOrder.Arith.StrictHierarchy Γ s φ
- sigma: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {μ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L μ (n + 1)}, LO.FirstOrder.Arith.StrictHierarchy 𝚷 s φ → LO.FirstOrder.Arith.StrictHierarchy 𝚺 (s + 1) (∃' φ)
- pi: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {μ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L μ (n + 1)}, LO.FirstOrder.Arith.StrictHierarchy 𝚺 s φ → LO.FirstOrder.Arith.StrictHierarchy 𝚷 (s + 1) (∀' φ)
- ex: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {μ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L μ (n + 1)}, LO.FirstOrder.Arith.StrictHierarchy 𝚺 (s + 1) φ → LO.FirstOrder.Arith.StrictHierarchy 𝚺 (s + 1) (∃' φ)
- all: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {μ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L μ (n + 1)}, LO.FirstOrder.Arith.StrictHierarchy 𝚷 (s + 1) φ → LO.FirstOrder.Arith.StrictHierarchy 𝚷 (s + 1) (∀' φ)
Instances For
theorem
LO.FirstOrder.Arith.DeltaZero.of_open
{L : LO.FirstOrder.Language}
[L.LT]
{μ : Type u_1}
{n : ℕ}
{φ : LO.FirstOrder.Semiformula L μ n}
:
φ.Open → LO.FirstOrder.Arith.DeltaZero φ
theorem
LO.FirstOrder.Arith.StrictHierarchy.rew
{L : LO.FirstOrder.Language}
[L.LT]
{μ₁ : Type u_1}
{n₁ : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{μ₂ : Type u_2}
{n₂ : ℕ}
{φ : LO.FirstOrder.Semiformula L μ₁ n₁}
(h : LO.FirstOrder.Arith.StrictHierarchy Γ s φ)
(ω : LO.FirstOrder.Rew L μ₁ n₁ μ₂ n₂)
:
theorem
LO.FirstOrder.Arith.StrictHierarchy.rew_iff
{L : LO.FirstOrder.Language}
[L.LT]
{μ₁ : Type u_1}
{n₁ : ℕ}
{μ₂ : Type u_2}
{n₂ : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{φ : LO.FirstOrder.Semiformula L μ₁ n₁}
(ω : LO.FirstOrder.Rew L μ₁ n₁ μ₂ n₂)
:
theorem
LO.FirstOrder.Arith.StrictHierarchy.succ
{L : LO.FirstOrder.Language}
[L.LT]
{μ₁ : Type u_1}
{n₁ s : ℕ}
{Γ : LO.Polarity}
{φ : LO.FirstOrder.Semiformula L μ₁ n₁}
(h : LO.FirstOrder.Arith.StrictHierarchy Γ s φ)
:
LO.FirstOrder.Arith.StrictHierarchy Γ (s + 1) φ
theorem
LO.FirstOrder.Arith.StrictHierarchy.zero_iff_delta_zero
{L : LO.FirstOrder.Language}
[L.LT]
{μ : Type u_1}
{n : ℕ}
{Γ : LO.Polarity}
{φ : LO.FirstOrder.Semiformula L μ n}
: