Strict arithmetical hierarchy #
StrictHierarchy Γ s φ singles out the prenex Γ-formulas of level s with a Δ₀ matrix
beneath alternating quantifier blocks.
References #
- [HP98]
inductive
FFL.FirstOrder.Arithmetic.StrictHierarchy
{L : Language}
[L.LT]
{ξ : Type u_1}
:
Polarity → ℕ → {n : ℕ} → Semiformula L ξ n → Prop
- zero {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {n : ℕ} {φ : Semiformula L ξ n} : Semiformula.Bounded BoundingOperator φ → StrictHierarchy Γ 0 φ
- ofAlt {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ n} : StrictHierarchy Γ.alt s φ → StrictHierarchy Γ (s + 1) φ
- exs {L : Language} [L.LT] {ξ : Type u_1} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : StrictHierarchy 𝚺 (s + 1) φ → StrictHierarchy 𝚺 (s + 1) (∃¹ φ)
- all {L : Language} [L.LT] {ξ : Type u_1} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : StrictHierarchy 𝚷 (s + 1) φ → StrictHierarchy 𝚷 (s + 1) (∀¹ φ)
Instances For
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.zero_iff_bounded
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{n : ℕ}
{φ : Semiformula L ξ n}
:
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.hierarchy
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ n}
:
StrictHierarchy Γ s φ → Hierarchy Γ s φ
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.neg
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ n}
:
StrictHierarchy Γ s φ → StrictHierarchy Γ.alt s (∼φ)
@[simp]
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.neg_iff
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ n}
:
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.rew
{L : Language}
[L.LT]
{Γ : Polarity}
{s n₁ n₂ : ℕ}
{ξ₁ : Type u_2}
{ξ₂ : Type u_3}
{φ : Semiformula L ξ₁ n₁}
(ω : Rew L ξ₁ n₁ ξ₂ n₂)
:
StrictHierarchy Γ s φ → StrictHierarchy Γ s ((Rewriting.app ω) φ)
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.of_rew
{L : Language}
[L.LT]
{Γ : Polarity}
{s n₂ : ℕ}
{ξ₂ : Type u_2}
{ψ : Semiformula L ξ₂ n₂}
:
StrictHierarchy Γ s ψ →
∀ {ξ₁ : Type u_3} {n₁ : ℕ} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁},
(Rewriting.app ω) φ = ψ → StrictHierarchy Γ s φ
@[simp]
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.rew_iff
{L : Language}
[L.LT]
{Γ : Polarity}
{s n₁ n₂ : ℕ}
{ξ₁ : Type u_2}
{ξ₂ : Type u_3}
{ω : Rew L ξ₁ n₁ ξ₂ n₂}
{φ : Semiformula L ξ₁ n₁}
:
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.toPrenex
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n j : ℕ}
{φ : Semiformula L ξ (n + s)}
(h : StrictHierarchy (Γ.altItr s) j φ)
:
StrictHierarchy Γ (j + s) (Semiformula.toPrenex Γ s φ)
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.toPrenex_of_deltaZero
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ (n + s)}
(h : Semiformula.Bounded BoundingOperator φ)
:
StrictHierarchy Γ s (Semiformula.toPrenex Γ s φ)
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.mono
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n s' : ℕ}
{φ : Semiformula L ξ n}
(h : StrictHierarchy Γ s φ)
(hs : s ≤ s')
:
StrictHierarchy Γ s' φ
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.strict_mono
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ n}
(h : StrictHierarchy Γ s φ)
(Γ' : Polarity)
{s' : ℕ}
(hs : s < s')
:
StrictHierarchy Γ' s' φ
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.of_deltaZero
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ n}
(h : Hierarchy 𝚺 0 φ)
:
StrictHierarchy Γ s φ
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.zero_iff
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{n : ℕ}
{φ : Semiformula L ξ n}
:
theorem
FFL.FirstOrder.Arithmetic.StrictHierarchy.allClosure
{L : Language}
[L.LT]
{ξ : Type u_1}
{s n : ℕ}
{φ : Semiformula L ξ n}
:
StrictHierarchy 𝚷 (s + 1) φ → StrictHierarchy 𝚷 (s + 1) (∀¹* φ)