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