Supporting results for pointwise provable equality.
Strict arithmetical hierarchy #
StrictHierarchy Γ s φ singles out the prenex Γ-formulas of level s with a Δ₀ matrix
beneath alternating quantifier blocks.
References #
- [HP98]
inductive
PointwiseComposition.FFL.FirstOrder.Arithmetic.StrictHierarchy
{L : Language}
[L.LT]
{ξ : Type u_1}
:
Polarity → ℕ → {n : ℕ} → Semiformula L ξ n → Prop
The strict arithmetical hierarchy with explicit quantifier alternations.
- zero {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {n : ℕ} {φ : Semiformula L ξ n} : Hierarchy Σ 0 φ → 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
PointwiseComposition.FFL.FirstOrder.Arithmetic.StrictHierarchy.hierarchy
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ n}
:
StrictHierarchy Γ s φ → Hierarchy Γ s φ
theorem
PointwiseComposition.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
PointwiseComposition.FFL.FirstOrder.Arithmetic.StrictHierarchy.neg_iff
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ n}
:
theorem
PointwiseComposition.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
PointwiseComposition.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
PointwiseComposition.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
PointwiseComposition.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
PointwiseComposition.FFL.FirstOrder.Arithmetic.StrictHierarchy.toPrenex_of_deltaZero
{L : Language}
[L.LT]
{ξ : Type u_1}
{Γ : Polarity}
{s n : ℕ}
{φ : Semiformula L ξ (n + s)}
(h : Hierarchy Σ 0 φ)
:
StrictHierarchy Γ s (Semiformula.toPrenex Γ s φ)
theorem
PointwiseComposition.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
PointwiseComposition.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' φ