LeanPool.PointwiseComposition.Foundation.FirstOrder.Arithmetic.Basic.Hierarchy

Supporting results for pointwise provable equality.

inductive PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy {L : Language} [L.LT] {ξ : Type u_2} :

Polarity → ℕ → {n : ℕ} → Semiformula L ξ n → Prop

The arithmetical hierarchy, starting with bounded formulas at level zero.

verum {L : Language} [L.LT] {ξ : Type u_2} (Γ : Polarity) (s n : ℕ) : Hierarchy Γ s ⊤
falsum {L : Language} [L.LT] {ξ : Type u_2} (Γ : Polarity) (s n : ℕ) : Hierarchy Γ s ⊥
rel {L : Language} [L.LT] {ξ : Type u_2} {x✝ : ℕ} (Γ : Polarity) (s : ℕ) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ x✝) : Hierarchy Γ s (Semiformula.rel r v)
nrel {L : Language} [L.LT] {ξ : Type u_2} {x✝ : ℕ} (Γ : Polarity) (s : ℕ) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ x✝) : Hierarchy Γ s (Semiformula.nrel r v)
and {L : Language} [L.LT] {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} : Hierarchy Γ s φ → Hierarchy Γ s ψ → Hierarchy Γ s (φ ⋏ ψ)
or {L : Language} [L.LT] {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} : Hierarchy Γ s φ → Hierarchy Γ s ψ → Hierarchy Γ s (φ ⋎ ψ)
ball {L : Language} [L.LT] {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} : t.Positive → Hierarchy Γ s φ → Hierarchy Γ s (“(∀¹[!!(Semiterm.bvar 0) < !!t] !φ)”)
bexs {L : Language} [L.LT] {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} : t.Positive → Hierarchy Γ s φ → Hierarchy Γ s (“(∃¹[!!(Semiterm.bvar 0) < !!t] !φ)”)
exs {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Σ (s + 1) φ → Hierarchy Σ (s + 1) (∃¹ φ)
all {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Π (s + 1) φ → Hierarchy Π (s + 1) (∀¹ φ)
sigma {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Π s φ → Hierarchy Σ (s + 1) (∃¹ φ)
pi {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Σ s φ → Hierarchy Π (s + 1) (∀¹ φ)
dummy_sigma {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Π (s + 1) φ → Hierarchy Σ (s + 1 + 1) (∀¹ φ)
dummy_pi {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Σ (s + 1) φ → Hierarchy Π (s + 1 + 1) (∃¹ φ)

Instances For

def PointwiseComposition.FFL.FirstOrder.Arithmetic.DeltaZero {L : Language} [L.LT] {ξ : Type u_2} {n : ℕ} (φ : Semiformula L ξ n) :

Prop

The Delta Zero construction in FFL.FirstOrder.Arithmetic.

Equations

PointwiseComposition.FFL.FirstOrder.Arithmetic.DeltaZero φ = PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy Σ 0 φ

Instances For

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.and_iff {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} :

Hierarchy Γ s (φ ⋏ ψ) ↔ Hierarchy Γ s φ ∧ Hierarchy Γ s ψ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.or_iff {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} :

Hierarchy Γ s (φ ⋎ ψ) ↔ Hierarchy Γ s φ ∧ Hierarchy Γ s ψ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.conj_iff {L : Language} [L.LT] {m : ℕ} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Fin m → Semiformula L ξ n} :

Hierarchy Γ s (Matrix.conj φ) ↔ ∀ (i : Fin m), Hierarchy Γ s (φ i)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.zero_eq_alt {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ : Semiformula L ξ n} :

Hierarchy Γ 0 φ → Hierarchy Γ.alt 0 φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.pi_zero_iff_sigma_zero {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {φ : Semiformula L ξ n} :

Hierarchy Π 0 φ ↔ Hierarchy Σ 0 φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.zero_iff {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ Γ' : Polarity} {φ : Semiformula L ξ n} :

Hierarchy Γ 0 φ ↔ Hierarchy Γ' 0 φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.zero_iff_delta_zero {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ : Semiformula L ξ n} :

Hierarchy Γ 0 φ ↔ DeltaZero φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.alt_zero_iff_zero {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {φ : Semiformula L ξ n} :

Hierarchy Γ.alt 0 φ ↔ Hierarchy Γ 0 φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.accum {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} :

Hierarchy Γ s φ → ∀ (Γ' : Polarity), Hierarchy Γ' (s + 1) φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.strict_mono {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} (hp : Hierarchy Γ s φ) (Γ' : Polarity) {s' : ℕ} (h : s < s') :

Hierarchy Γ' s' φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.mono {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s s' : ℕ} {φ : Semiformula L ξ n} (hp : Hierarchy Γ s φ) (h : s ≤ s') :

Hierarchy Γ s' φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.of_zero {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {b b' : Polarity} {s : ℕ} {φ : Semiformula L ξ n} (hp : Hierarchy b 0 φ) :

Hierarchy b' s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.equal {L : Language} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} [L.Eq] [L.LT] {t u : Semiterm L ξ n} :

Hierarchy Γ s (“!!t = !!u”)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.lt {L : Language} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} [L.LT] {t u : Semiterm L ξ n} :

Hierarchy Γ s (“!!t < !!u”)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.le {L : Language} {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} [L.Eq] [L.LT] {t u : Semiterm L ξ n} :

Hierarchy Γ s (“!!t ≤ !!u”)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.neg {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} :

Hierarchy Γ s φ → Hierarchy Γ.alt s (∼φ)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.neg_iff {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} :

Hierarchy Γ s (∼φ) ↔ Hierarchy Γ.alt s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.imp_iff {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} :

Hierarchy Γ s (φ ⇒ₗ ψ) ↔ Hierarchy Γ.alt s φ ∧ Hierarchy Γ s ψ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.ball_iff {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) :

Hierarchy Γ s (“(∀¹[!!(Semiterm.bvar 0) < !!t] !φ)”) ↔ Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.bexs_iff {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (ht : t.Positive) :

Hierarchy Γ s (“(∃¹[!!(Semiterm.bvar 0) < !!t] !φ)”) ↔ Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.ballLT_iff {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} :

Hierarchy Γ s (Semiformula.ballLT t φ) ↔ Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.bexsLT_iff {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} :

Hierarchy Γ s (Semiformula.bexsLT t φ) ↔ Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.ballLTSucc_iff {L : Language} [L.LT] {ξ : Type u_1} [L.Zero] [L.One] [L.Add] {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} :

Hierarchy Γ s (Semiformula.ballLTSucc t φ) ↔ Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.bexsLTSucc_iff {L : Language} [L.LT] {ξ : Type u_1} [L.Zero] [L.One] [L.Add] {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ n} :

Hierarchy Γ s (Semiformula.bexsLTSucc t φ) ↔ Hierarchy Γ s φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.pi_of_pi_all {L : Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy Π s (∀¹ φ) → Hierarchy Π s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.all_iff {L : Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy Π (s + 1) (∀¹ φ) ↔ Hierarchy Π (s + 1) φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.allItr_iff {L : Language} [L.LT] {ξ : Type u_1} {n k s : ℕ} {φ : Semiformula L ξ (n + k)} :

Hierarchy Π (s + 1) (∀¹^[k] φ) ↔ Hierarchy Π (s + 1) φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.sigma_of_sigma_ex {L : Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy Σ s (∃¹ φ) → Hierarchy Σ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.sigma_iff {L : Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy Σ (s + 1) (∃¹ φ) ↔ Hierarchy Σ (s + 1) φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.exsItr_iff {L : Language} [L.LT] {ξ : Type u_1} {n k s : ℕ} {φ : Semiformula L ξ (n + k)} :

Hierarchy Σ (s + 1) (∃¹^[k] φ) ↔ Hierarchy Σ (s + 1) φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.rew {L : Language} [L.LT] {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {Γ : Polarity} {s : ℕ} (ω : Rew L ξ₁ n₁ ξ₂ n₂) {φ : Semiformula L ξ₁ n₁} :

Hierarchy Γ s φ → Hierarchy Γ s ((Rewriting.app ω) φ)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.rew_iff {L : Language} [L.LT] {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {Γ : Polarity} {s : ℕ} {ω : Rew L ξ₁ n₁ ξ₂ n₂} {φ : Semiformula L ξ₁ n₁} :

Hierarchy Γ s ((Rewriting.app ω) φ) ↔ Hierarchy Γ s φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.exsClosure {L : Language} [L.LT] {ξ : Type u_1} {s n : ℕ} {φ : Semiformula L ξ n} :

Hierarchy Σ (s + 1) φ → Hierarchy Σ (s + 1) (∃¹* φ)

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.instAndOrClosedSemiformula {L : Language} [L.LT] {ξ : Type u_1} {k : ℕ} {Γ : Polarity} {s : ℕ} :

LogicalConnective.AndOrClosed (Hierarchy Γ s)

source

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.instClosedSemiformulaOfNatNat {L : Language} [L.LT] {ξ : Type u_1} {k : ℕ} {Γ : Polarity} :

LogicalConnective.Closed (Hierarchy Γ 0)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.of_open {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : Polarity} {s : ℕ} {φ : Semiformula L ξ n} :

φ.Open → Hierarchy Γ s φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.iff_iff {L : Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : Polarity} {s : ℕ} {φ ψ : Semiformula L ξ n} :

Hierarchy b s (φ ⇔ₗ ψ) ↔ Hierarchy b s φ ∧ Hierarchy b.alt s φ ∧ Hierarchy b s ψ ∧ Hierarchy b.alt s ψ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.iff_iff₀ {L : Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : Polarity} {φ ψ : Semiformula L ξ n} :

Hierarchy b 0 (φ ⇔ₗ ψ) ↔ Hierarchy b 0 φ ∧ Hierarchy b 0 ψ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.matrix_conj_iff {L : Language} [L.ORing] {m : ℕ} {ξ : Type u_1} {b : Polarity} {s n : ℕ} {φ : Fin m → Semiformula L ξ n} :

Hierarchy b s (Matrix.conj fun (j : Fin m) => φ j) ↔ ∀ (j : Fin m), Hierarchy b s (φ j)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.remove_forall {L : Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : Polarity} {s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy b s (∀¹ φ) → Hierarchy b s φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.remove_exists {L : Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : Polarity} {s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy b s (∃¹ φ) → Hierarchy b s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.padding_iff {L : Language} [L.ORing] {ξ : Type u_1} {k : ℕ} {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ n} :

Hierarchy Γ s (φ.padding k) ↔ Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.list_conj₂_iff {L : Language} [L.ORing] {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {l : List (Semiformula L ξ n)} :

Hierarchy Γ s (⋀l) ↔ ∀ φ ∈ l, Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.list_disj₂_iff {L : Language} [L.ORing] {ξ : Type u_1} {Γ : Polarity} {s n : ℕ} {l : List (Semiformula L ξ n)} :

Hierarchy Γ s (⋁l) ↔ ∀ φ ∈ l, Hierarchy Γ s φ

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.list_conj'_iff {L : Language} [L.ORing] {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {l : List ι} {φ : ι → Semiformula L ξ n} :

Hierarchy Γ s ((fun (x : ι → Semiformula L ξ n) => List.conj' x l) φ) ↔ ∀ i ∈ l, Hierarchy Γ s (φ i)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.list_disj'_iff {L : Language} [L.ORing] {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {l : List ι} {φ : ι → Semiformula L ξ n} :

Hierarchy Γ s ((fun (x : ι → Semiformula L ξ n) => List.disj' x l) φ) ↔ ∀ i ∈ l, Hierarchy Γ s (φ i)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.finset_conj'_iff {L : Language} [L.ORing] {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {t : Finset ι} {φ : ι → Semiformula L ξ n} :

Hierarchy Γ s (Finset.conj' t φ) ↔ ∀ i ∈ t, Hierarchy Γ s (φ i)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.finset_disj'_iff {L : Language} [L.ORing] {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} {t : Finset ι} {φ : ι → Semiformula L ξ n} :

Hierarchy Γ s (Finset.disj' t φ) ↔ ∀ i ∈ t, Hierarchy Γ s (φ i)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.finset_uconj_iff {L : Language} [L.ORing] {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} [Fintype ι] {φ : ι → Semiformula L ξ n} :

Hierarchy Γ s (Finset.uconj φ) ↔ ∀ (i : ι), Hierarchy Γ s (φ i)

source

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.finset_udisj_iff {L : Language} [L.ORing] {ι : Type u_1} {ξ : Type u_2} {Γ : Polarity} {s n : ℕ} [Fintype ι] {φ : ι → Semiformula L ξ n} :

Hierarchy Γ s (Finset.udisj φ) ↔ ∀ (i : ι), Hierarchy Γ s (φ i)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy.toPrenex {L : Language} [L.ORing] {ξ : Type u_1} {n s j : ℕ} {Γ : Polarity} {φ : Semiformula L ξ (n + s)} (h : Hierarchy (Γ.altItr s) j φ) :

Hierarchy Γ (j + s) (Semiformula.toPrenex Γ s φ)

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma₁_induction {ξ : Type u_1} {P : (n : ℕ) → ArithmeticSemiformula ξ n → Prop} (hVerum : ∀ (n : ℕ), P n ⊤) (hFalsum : ∀ (n : ℕ), P n ⊥) (hEQ : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.rel op(=) ![t₁, t₂])) (hNEQ : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.nrel op(=) ![t₁, t₂])) (hLT : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.rel op(<) ![t₁, t₂])) (hNLT : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.nrel op(<) ![t₁, t₂])) (hAnd : ∀ (n : ℕ) (φ ψ : Semiformula ℒₒᵣ ξ n), Hierarchy Σ 1 φ → Hierarchy Σ 1 ψ → P n φ → P n ψ → P n (φ ⋏ ψ)) (hOr : ∀ (n : ℕ) (φ ψ : Semiformula ℒₒᵣ ξ n), Hierarchy Σ 1 φ → Hierarchy Σ 1 ψ → P n φ → P n ψ → P n (φ ⋎ ψ)) (hBall : ∀ (n : ℕ) (t : Semiterm ℒₒᵣ ξ n) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Σ 1 φ → P (n + 1) φ → P n (“(∀¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (hExs : ∀ (n : ℕ) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Σ 1 φ → P (n + 1) φ → P n (∃¹ φ)) (n : ℕ) (φ : Semiformula ℒₒᵣ ξ n) :

Hierarchy Σ 1 φ → P n φ

source

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.sigma₁_induction' {ξ : Type u_1} {n : ℕ} {φ : Semiformula ℒₒᵣ ξ n} (hp : Hierarchy Σ 1 φ) {P : (n : ℕ) → ArithmeticSemiformula ξ n → Prop} (hVerum : ∀ (n : ℕ), P n ⊤) (hFalsum : ∀ (n : ℕ), P n ⊥) (hEQ : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.rel op(=) ![t₁, t₂])) (hNEQ : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.nrel op(=) ![t₁, t₂])) (hLT : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.rel op(<) ![t₁, t₂])) (hNLT : ∀ (n : ℕ) (t₁ t₂ : Semiterm ℒₒᵣ ξ n), P n (Semiformula.nrel op(<) ![t₁, t₂])) (hAnd : ∀ (n : ℕ) (φ ψ : Semiformula ℒₒᵣ ξ n), Hierarchy Σ 1 φ → Hierarchy Σ 1 ψ → P n φ → P n ψ → P n (φ ⋏ ψ)) (hOr : ∀ (n : ℕ) (φ ψ : Semiformula ℒₒᵣ ξ n), Hierarchy Σ 1 φ → Hierarchy Σ 1 ψ → P n φ → P n ψ → P n (φ ⋎ ψ)) (hBall : ∀ (n : ℕ) (t : Semiterm ℒₒᵣ ξ n) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Σ 1 φ → P (n + 1) φ → P n (“(∀¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (hExs : ∀ (n : ℕ) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Σ 1 φ → P (n + 1) φ → P n (∃¹ φ)) :

P n φ

source

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.ArithmeticTheory.SoundOnHierarchy (T : ArithmeticTheory) (Γ : Polarity) (k : ℕ) :

Prop

The Sound On Hierarchy construction in FFL.FirstOrder.ArithmeticTheory.

Equations

T.SoundOnHierarchy Γ k = T.SoundOn (PointwiseComposition.FFL.FirstOrder.Arithmetic.Hierarchy Γ k)

Instances For

source

theorem PointwiseComposition.FFL.FirstOrder.ArithmeticTheory.soundOnHierarchy {σ : Sentence ℒₒᵣ} (T : ArithmeticTheory) (Γ : Polarity) (k : ℕ) [T.SoundOnHierarchy Γ k] :

T ⊢ σ → Arithmetic.Hierarchy Γ k σ → ℕ ↓[ℒₒᵣ ] ⊧ σ

source

instance PointwiseComposition.FFL.FirstOrder.instConsistentSentenceORingArithmeticTheoryOfSoundOnHierarchySigmaPolarityOfNatNat (T : ArithmeticTheory) [T.SoundOnHierarchy Σ 1] :

Entailment.Consistent T

source

instance PointwiseComposition.FFL.FirstOrder.instConsistentSentenceORingArithmeticTheoryOfSoundOnHierarchyPiPolarityOfNatNat (T : ArithmeticTheory) [T.SoundOnHierarchy Π 2] :

Entailment.Consistent T