inductive FFL.FirstOrder.BoundingHierarchy {L : Language} (R : Semiformula.Operator L 2) {ξ : Type u_2} : Polarity → ℕ → {n : ℕ} → Semiformula L ξ n → Prop

This formalization generalizes the syntactic arithmetical hierarchy using R for bounds.

• bounded {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} (Γ : Polarity) (s n : ℕ) {φ : Semiformula L ξ n} : Semiformula.Bounded R φ → BoundingHierarchy R Γ s φ
• and {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} : BoundingHierarchy R Γ s φ → BoundingHierarchy R Γ s ψ → BoundingHierarchy R Γ s (φ ⋏ ψ)
• or {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} : BoundingHierarchy R Γ s φ → BoundingHierarchy R Γ s ψ → BoundingHierarchy R Γ s (φ ⋎ ψ)
• ball {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} : t.Positive → BoundingHierarchy R Γ s φ → BoundingHierarchy R Γ s (∀¹[R.operator ![Semiterm.bvar 0, t]] φ)
• bexs {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} : t.Positive → BoundingHierarchy R Γ s φ → BoundingHierarchy R Γ s (∃¹[R.operator ![Semiterm.bvar 0, t]] φ)
• exs {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚺 (s + 1) φ → BoundingHierarchy R 𝚺 (s + 1) (∃¹ φ)
• all {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚷 (s + 1) φ → BoundingHierarchy R 𝚷 (s + 1) (∀¹ φ)
• sigma {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚷 s φ → BoundingHierarchy R 𝚺 (s + 1) (∃¹ φ)
• pi {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚺 s φ → BoundingHierarchy R 𝚷 (s + 1) (∀¹ φ)
• dummy_sigma {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚷 (s + 1) φ → BoundingHierarchy R 𝚺 (s + 1 + 1) (∀¹ φ)
• dummy_pi {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚺 (s + 1) φ → BoundingHierarchy R 𝚷 (s + 1 + 1) (∃¹ φ)

@[reducible, inline]

abbrev FFL.FirstOrder.BoundingHierarchy.DeltaZero {L : Language} (R : Semiformula.Operator L 2) {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ n) : Prop

Equations

• FFL.FirstOrder.BoundingHierarchy.DeltaZero R φ = FFL.FirstOrder.Semiformula.Bounded R φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.verum {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} (Γ : Polarity) (s n : ℕ) : BoundingHierarchy R Γ s ⊤

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.falsum {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} (Γ : Polarity) (s n : ℕ) : BoundingHierarchy R Γ s ⊥

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.rel {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} (Γ : Polarity) (s : ℕ) {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : BoundingHierarchy R Γ s (Semiformula.rel r v)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.nrel {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} (Γ : Polarity) (s : ℕ) {n k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ n) : BoundingHierarchy R Γ s (Semiformula.nrel r v)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.and_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} : BoundingHierarchy R Γ s (φ ⋏ ψ) ↔ BoundingHierarchy R Γ s φ ∧ BoundingHierarchy R Γ s ψ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.or_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} : BoundingHierarchy R Γ s (φ ⋎ ψ) ↔ BoundingHierarchy R Γ s φ ∧ BoundingHierarchy R Γ s ψ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.conj_iff {L : Language} {R : Semiformula.Operator L 2} {m : ℕ} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Fin m → Semiformula L ξ n} : BoundingHierarchy R Γ s (Matrix.conj φ) ↔ ∀ (i : Fin m), BoundingHierarchy R Γ s (φ i)

theorem FFL.FirstOrder.BoundingHierarchy.zero_eq_alt {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ 0 φ → BoundingHierarchy R Γ.alt 0 φ

theorem FFL.FirstOrder.BoundingHierarchy.pi_zero_iff_sigma_zero {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} : BoundingHierarchy R 𝚷 0 φ ↔ BoundingHierarchy R 𝚺 0 φ

theorem FFL.FirstOrder.BoundingHierarchy.zero_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ Γ' : Polarity} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ 0 φ ↔ BoundingHierarchy R Γ' 0 φ

theorem FFL.FirstOrder.BoundingHierarchy.zero_iff_bounded {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ 0 φ ↔ Semiformula.Bounded R φ

theorem FFL.FirstOrder.BoundingHierarchy.zero_iff_delta_zero {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ 0 φ ↔ DeltaZero R φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.alt_zero_iff_zero {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ.alt 0 φ ↔ BoundingHierarchy R Γ 0 φ

theorem FFL.FirstOrder.BoundingHierarchy.accum {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ s φ → ∀ (Γ' : Polarity), BoundingHierarchy R Γ' (s + 1) φ

theorem FFL.FirstOrder.BoundingHierarchy.strict_mono {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} (hp : BoundingHierarchy R Γ s φ) (Γ' : Polarity) {s' : ℕ} (h : s < s') : BoundingHierarchy R Γ' s' φ

theorem FFL.FirstOrder.BoundingHierarchy.mono {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s s' : ℕ} {φ : Semiformula L ξ n} (hp : BoundingHierarchy R Γ s φ) (h : s ≤ s') : BoundingHierarchy R Γ s' φ

theorem FFL.FirstOrder.BoundingHierarchy.of_zero {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ Γ' : Polarity} {s : ℕ} {φ : Semiformula L ξ n} (hp : BoundingHierarchy R Γ 0 φ) : BoundingHierarchy R Γ' s φ

theorem FFL.FirstOrder.BoundingHierarchy.neg {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ s φ → BoundingHierarchy R Γ.alt s (∼φ)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.neg_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ s (∼φ) ↔ BoundingHierarchy R Γ.alt s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.imp_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} : BoundingHierarchy R Γ s (φ 🡒 ψ) ↔ BoundingHierarchy R Γ.alt s φ ∧ BoundingHierarchy R Γ s ψ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.ball_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) : BoundingHierarchy R Γ s (∀¹[R.operator ![Semiterm.bvar 0, t]] φ) ↔ BoundingHierarchy R Γ s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.bexs_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) : BoundingHierarchy R Γ s (∃¹[R.operator ![Semiterm.bvar 0, t]] φ) ↔ BoundingHierarchy R Γ s φ

class FFL.FirstOrder.BoundingHierarchy.Small {L : Language} (R : Semiformula.Operator L 2) (ξ : Type u_1) : Prop

An auxiliary condition here requiring every application of R to lie in every hierarchy level.

• operator {n : ℕ} {Γ : Polarity} {s : ℕ} (v : Fin 2 → Semiterm L ξ n) : BoundingHierarchy R Γ s (R.operator v)

instance FFL.FirstOrder.BoundingHierarchy.smallEq {L : Language} [L.Eq] (ξ : Type u_1) : Small op(=) ξ

instance FFL.FirstOrder.BoundingHierarchy.smallLT {L : Language} [L.LT] (ξ : Type u_1) : Small op(<) ξ

instance FFL.FirstOrder.BoundingHierarchy.smallMem {L : Language} [L.Mem] (ξ : Type u_1) : Small op(∈) ξ

theorem FFL.FirstOrder.BoundingHierarchy.pi_of_pi_all {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚷 s (∀¹ φ) → BoundingHierarchy R 𝚷 s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.all_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚷 (s + 1) (∀¹ φ) ↔ BoundingHierarchy R 𝚷 (s + 1) φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.allItr_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n k s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + k)} : BoundingHierarchy R 𝚷 (s + 1) (∀¹^[k] φ) ↔ BoundingHierarchy R 𝚷 (s + 1) φ

theorem FFL.FirstOrder.BoundingHierarchy.sigma_of_sigma_ex {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚺 s (∃¹ φ) → BoundingHierarchy R 𝚺 s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.sigma_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R 𝚺 (s + 1) (∃¹ φ) ↔ BoundingHierarchy R 𝚺 (s + 1) φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.exsItr_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n k s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + k)} : BoundingHierarchy R 𝚺 (s + 1) (∃¹^[k] φ) ↔ BoundingHierarchy R 𝚺 (s + 1) φ

theorem FFL.FirstOrder.BoundingHierarchy.rew {L : Language} {R : Semiformula.Operator L 2} {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {Γ : Polarity} {s : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} : BoundingHierarchy R Γ s φ → BoundingHierarchy R Γ s ((Rewriting.app ω) φ)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.rew_iff {L : Language} {R : Semiformula.Operator L 2} {ξ₁ : Type u_1} {ξ₂ : Type u_2} {n₁ n₂ : ℕ} {Γ : Polarity} {s : ℕ} [R.SymbolLike ξ₁ ξ₂] {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} : BoundingHierarchy R Γ s ((Rewriting.app ω) φ) ↔ BoundingHierarchy R Γ s φ

theorem FFL.FirstOrder.BoundingHierarchy.exsClosure {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {s n : ℕ} {φ : Semiformula L ξ n} : BoundingHierarchy R 𝚺 (s + 1) φ → BoundingHierarchy R 𝚺 (s + 1) (∃¹* φ)

instance FFL.FirstOrder.BoundingHierarchy.instAndOrClosedSemiformula {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {k : ℕ} {Γ : Polarity} {s : ℕ} : LogicalConnective.AndOrClosed (BoundingHierarchy R Γ s)

instance FFL.FirstOrder.BoundingHierarchy.instClosedSemiformulaOfNatNat {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {k : ℕ} {Γ : Polarity} : LogicalConnective.Closed (BoundingHierarchy R Γ 0)

theorem FFL.FirstOrder.BoundingHierarchy.of_open {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} : φ.Open → BoundingHierarchy R Γ s φ

theorem FFL.FirstOrder.BoundingHierarchy.iff_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} : BoundingHierarchy R Γ s (φ 🡘 ψ) ↔ BoundingHierarchy R Γ s φ ∧ BoundingHierarchy R Γ.alt s φ ∧ BoundingHierarchy R Γ s ψ ∧ BoundingHierarchy R Γ.alt s ψ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.iff_iff₀ {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ ψ : Semiformula L ξ n} : BoundingHierarchy R Γ 0 (φ 🡘 ψ) ↔ BoundingHierarchy R Γ 0 φ ∧ BoundingHierarchy R Γ 0 ψ

theorem FFL.FirstOrder.BoundingHierarchy.remove_forall {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R Γ s (∀¹ φ) → BoundingHierarchy R Γ s φ

theorem FFL.FirstOrder.BoundingHierarchy.remove_exists {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} [Small R ξ] {φ : Semiformula L ξ (n + 1)} : BoundingHierarchy R Γ s (∃¹ φ) → BoundingHierarchy R Γ s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.padding_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {k : ℕ} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ n} : BoundingHierarchy R Γ s (φ.padding k) ↔ BoundingHierarchy R Γ s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.list_conj₂_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {l : List (Semiformula L ξ n)} : BoundingHierarchy R Γ s (⋀l) ↔ ∀ φ ∈ l, BoundingHierarchy R Γ s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.list_disj₂_iff {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {l : List (Semiformula L ξ n)} : BoundingHierarchy R Γ s (⋁l) ↔ ∀ φ ∈ l, BoundingHierarchy R Γ s φ

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.list_conj'_iff {L : Language} {R : Semiformula.Operator L 2} {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {l : List ι} {φ : ι → Semiformula L ξ n} : BoundingHierarchy R Γ s (List.conj' φ l) ↔ ∀ i ∈ l, BoundingHierarchy R Γ s (φ i)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.list_disj'_iff {L : Language} {R : Semiformula.Operator L 2} {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {l : List ι} {φ : ι → Semiformula L ξ n} : BoundingHierarchy R Γ s (List.disj' φ l) ↔ ∀ i ∈ l, BoundingHierarchy R Γ s (φ i)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.finset_conj'_iff {L : Language} {R : Semiformula.Operator L 2} {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {t : Finset ι} {φ : ι → Semiformula L ξ n} : BoundingHierarchy R Γ s (t.conj' φ) ↔ ∀ i ∈ t, BoundingHierarchy R Γ s (φ i)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.finset_disj'_iff {L : Language} {R : Semiformula.Operator L 2} {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {t : Finset ι} {φ : ι → Semiformula L ξ n} : BoundingHierarchy R Γ s (t.disj' φ) ↔ ∀ i ∈ t, BoundingHierarchy R Γ s (φ i)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.finset_uconj_iff {L : Language} {R : Semiformula.Operator L 2} {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} [Fintype ι] {φ : ι → Semiformula L ξ n} : BoundingHierarchy R Γ s (Finset.uconj φ) ↔ ∀ (i : ι), BoundingHierarchy R Γ s (φ i)

@[simp]

theorem FFL.FirstOrder.BoundingHierarchy.finset_udisj_iff {L : Language} {R : Semiformula.Operator L 2} {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} [Fintype ι] {φ : ι → Semiformula L ξ n} : BoundingHierarchy R Γ s (Finset.udisj φ) ↔ ∀ (i : ι), BoundingHierarchy R Γ s (φ i)

theorem FFL.FirstOrder.BoundingHierarchy.sigma₁_induction {L : Language} {R : Semiformula.Operator L 2} {ξ : Type u_1} [Small R ξ] {P : (n : ℕ) → Semiformula L ξ n → Prop} (hVerum : ∀ (n : ℕ), P n ⊤) (hFalsum : ∀ (n : ℕ), P n ⊥) (hRel : ∀ (n k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n), P n (Semiformula.rel r v)) (hNRel : ∀ (n k : ℕ) (r : L.Rel k) (v : Fin k → Semiterm L ξ n), P n (Semiformula.nrel r v)) (hAnd : ∀ (n : ℕ) (φ ψ : Semiformula L ξ n), BoundingHierarchy R 𝚺 1 φ → BoundingHierarchy R 𝚺 1 ψ → P n φ → P n ψ → P n (φ ⋏ ψ)) (hOr : ∀ (n : ℕ) (φ ψ : Semiformula L ξ n), BoundingHierarchy R 𝚺 1 φ → BoundingHierarchy R 𝚺 1 ψ → P n φ → P n ψ → P n (φ ⋎ ψ)) (hBall : ∀ (n : ℕ) (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)), BoundingHierarchy R 𝚺 1 φ → P (n + 1) φ → P n (∀¹[R.operator ![Semiterm.bvar 0, Rew.bShift t]] φ)) (hExs : ∀ (n : ℕ) (φ : Semiformula L ξ (n + 1)), BoundingHierarchy R 𝚺 1 φ → P (n + 1) φ → P n (∃¹ φ)) (hOperator : ∀ (n : ℕ) (t : Semiterm L ξ n), P (n + 1) (R.operator ![Semiterm.bvar 0, Rew.bShift t])) (n : ℕ) (φ : Semiformula L ξ n) : BoundingHierarchy R 𝚺 1 φ → P n φ