Foundation.FirstOrder.Arithmetic.Basic.Hierarchy

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.rec {L : Language} [L.LT] {ξ : Type u_2} {motive : (a : Polarity) → (a_1 : ℕ) → {n : ℕ} → (a_2 : Semiformula L ξ n) → BoundingHierarchy BoundingOperator a a_1 a_2 → Prop} (bounded : ∀ (Γ : Polarity) (s n : ℕ) {φ : Semiformula L ξ n} (a : Semiformula.Bounded BoundingOperator φ), motive Γ s φ ⋯) (and : ∀ {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} (a : BoundingHierarchy BoundingOperator Γ s φ) (a_1 : BoundingHierarchy BoundingOperator Γ s ψ), motive Γ s φ a → motive Γ s ψ a_1 → motive Γ s (φ ⋏ ψ) ⋯) (or : ∀ {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} (a : BoundingHierarchy BoundingOperator Γ s φ) (a_1 : BoundingHierarchy BoundingOperator Γ s ψ), motive Γ s φ a → motive Γ s ψ a_1 → motive Γ s (φ ⋎ ψ) ⋯) (ball : ∀ {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (a : t.Positive) (a_1 : BoundingHierarchy BoundingOperator Γ s φ), motive Γ s φ a_1 → motive Γ s (∀¹[BoundingOperator.operator ![Semiterm.bvar 0, t]] φ) ⋯) (bexs : ∀ {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (a : t.Positive) (a_1 : BoundingHierarchy BoundingOperator Γ s φ), motive Γ s φ a_1 → motive Γ s (∃¹[BoundingOperator.operator ![Semiterm.bvar 0, t]] φ) ⋯) (exs : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 (s + 1) φ), motive 𝚺 (s + 1) φ a → motive 𝚺 (s + 1) (∃¹ φ) ⋯) (all : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 (s + 1) φ), motive 𝚷 (s + 1) φ a → motive 𝚷 (s + 1) (∀¹ φ) ⋯) (sigma : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 s φ), motive 𝚷 s φ a → motive 𝚺 (s + 1) (∃¹ φ) ⋯) (pi : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 s φ), motive 𝚺 s φ a → motive 𝚷 (s + 1) (∀¹ φ) ⋯) (dummy_sigma : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 (s + 1) φ), motive 𝚷 (s + 1) φ a → motive 𝚺 (s + 1 + 1) (∀¹ φ) ⋯) (dummy_pi : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 (s + 1) φ), motive 𝚺 (s + 1) φ a → motive 𝚷 (s + 1 + 1) (∃¹ φ) ⋯) {a✝ : Polarity} {a✝¹ n : ℕ} {a✝² : Semiformula L ξ n} (t : BoundingHierarchy BoundingOperator a✝ a✝¹ a✝²) :

motive a✝ a✝¹ a✝² t

Equations

⋯ = ⋯

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.recOn {L : Language} [L.LT] {ξ : Type u_2} {motive : (a : Polarity) → (a_1 : ℕ) → {n : ℕ} → (a_2 : Semiformula L ξ n) → BoundingHierarchy BoundingOperator a a_1 a_2 → Prop} {a✝ : Polarity} {a✝¹ n : ℕ} {a✝² : Semiformula L ξ n} (t : BoundingHierarchy BoundingOperator a✝ a✝¹ a✝²) (bounded : ∀ (Γ : Polarity) (s n : ℕ) {φ : Semiformula L ξ n} (a : Semiformula.Bounded BoundingOperator φ), motive Γ s φ ⋯) (and : ∀ {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} (a : BoundingHierarchy BoundingOperator Γ s φ) (a_1 : BoundingHierarchy BoundingOperator Γ s ψ), motive Γ s φ a → motive Γ s ψ a_1 → motive Γ s (φ ⋏ ψ) ⋯) (or : ∀ {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} (a : BoundingHierarchy BoundingOperator Γ s φ) (a_1 : BoundingHierarchy BoundingOperator Γ s ψ), motive Γ s φ a → motive Γ s ψ a_1 → motive Γ s (φ ⋎ ψ) ⋯) (ball : ∀ {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (a : t.Positive) (a_1 : BoundingHierarchy BoundingOperator Γ s φ), motive Γ s φ a_1 → motive Γ s (∀¹[BoundingOperator.operator ![Semiterm.bvar 0, t]] φ) ⋯) (bexs : ∀ {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (a : t.Positive) (a_1 : BoundingHierarchy BoundingOperator Γ s φ), motive Γ s φ a_1 → motive Γ s (∃¹[BoundingOperator.operator ![Semiterm.bvar 0, t]] φ) ⋯) (exs : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 (s + 1) φ), motive 𝚺 (s + 1) φ a → motive 𝚺 (s + 1) (∃¹ φ) ⋯) (all : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 (s + 1) φ), motive 𝚷 (s + 1) φ a → motive 𝚷 (s + 1) (∀¹ φ) ⋯) (sigma : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 s φ), motive 𝚷 s φ a → motive 𝚺 (s + 1) (∃¹ φ) ⋯) (pi : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 s φ), motive 𝚺 s φ a → motive 𝚷 (s + 1) (∀¹ φ) ⋯) (dummy_sigma : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 (s + 1) φ), motive 𝚷 (s + 1) φ a → motive 𝚺 (s + 1 + 1) (∀¹ φ) ⋯) (dummy_pi : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 (s + 1) φ), motive 𝚺 (s + 1) φ a → motive 𝚷 (s + 1 + 1) (∃¹ φ) ⋯) :

motive a✝ a✝¹ a✝² t

Equations

⋯ = ⋯

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.casesOn {L : Language} [L.LT] {ξ : Type u_2} {motive : (a : Polarity) → (a_1 : ℕ) → {n : ℕ} → (a_2 : Semiformula L ξ n) → BoundingHierarchy BoundingOperator a a_1 a_2 → Prop} {a✝ : Polarity} {a✝¹ n : ℕ} {a✝² : Semiformula L ξ n} (t : BoundingHierarchy BoundingOperator a✝ a✝¹ a✝²) (bounded : ∀ (Γ : Polarity) (s n : ℕ) {φ : Semiformula L ξ n} (a : Semiformula.Bounded BoundingOperator φ), motive Γ s φ ⋯) (and : ∀ {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} (a : BoundingHierarchy BoundingOperator Γ s φ) (a_1 : BoundingHierarchy BoundingOperator Γ s ψ), motive Γ s (φ ⋏ ψ) ⋯) (or : ∀ {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} (a : BoundingHierarchy BoundingOperator Γ s φ) (a_1 : BoundingHierarchy BoundingOperator Γ s ψ), motive Γ s (φ ⋎ ψ) ⋯) (ball : ∀ {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (a : t.Positive) (a_1 : BoundingHierarchy BoundingOperator Γ s φ), motive Γ s (∀¹[BoundingOperator.operator ![Semiterm.bvar 0, t]] φ) ⋯) (bexs : ∀ {Γ : Polarity} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} {t : Semiterm L ξ (n + 1)} (a : t.Positive) (a_1 : BoundingHierarchy BoundingOperator Γ s φ), motive Γ s (∃¹[BoundingOperator.operator ![Semiterm.bvar 0, t]] φ) ⋯) (exs : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 (s + 1) φ), motive 𝚺 (s + 1) (∃¹ φ) ⋯) (all : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 (s + 1) φ), motive 𝚷 (s + 1) (∀¹ φ) ⋯) (sigma : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 s φ), motive 𝚺 (s + 1) (∃¹ φ) ⋯) (pi : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 s φ), motive 𝚷 (s + 1) (∀¹ φ) ⋯) (dummy_sigma : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚷 (s + 1) φ), motive 𝚺 (s + 1 + 1) (∀¹ φ) ⋯) (dummy_pi : ∀ {s n : ℕ} {φ : Semiformula L ξ (n + 1)} (a : BoundingHierarchy BoundingOperator 𝚺 (s + 1) φ), motive 𝚷 (s + 1 + 1) (∃¹ φ) ⋯) :

motive a✝ a✝¹ a✝² t

Equations

⋯ = ⋯

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.below {L : Language} [L.LT] {ξ : Type u_2} {motive : (a : Polarity) → (a_1 : ℕ) → {n : ℕ} → (a_2 : Semiformula L ξ n) → BoundingHierarchy BoundingOperator a a_1 a_2 → Prop} {a✝ : Polarity} {a✝¹ n : ℕ} {a✝² : Semiformula L ξ n} (t : BoundingHierarchy BoundingOperator a✝ a✝¹ a✝²) :

Prop

Equations

@FFL.FirstOrder.Arithmetic.Hierarchy.below L inst✝ = @FFL.FirstOrder.BoundingHierarchy.below L FFL.FirstOrder.Arithmetic.BoundingOperator

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.brecOn {L : Language} [L.LT] {ξ : Type u_2} {motive : (a : Polarity) → (a_1 : ℕ) → {n : ℕ} → (a_2 : Semiformula L ξ n) → BoundingHierarchy BoundingOperator a a_1 a_2 → Prop} {a✝ : Polarity} {a✝¹ n : ℕ} {a✝² : Semiformula L ξ n} (t : BoundingHierarchy BoundingOperator a✝ a✝¹ a✝²) (F_1 : ∀ (a : Polarity) (a_1 : ℕ) {n : ℕ} (a_2 : Semiformula L ξ n) (t : BoundingHierarchy BoundingOperator a a_1 a_2), BoundingHierarchy.below t → motive a a_1 a_2 t) :

motive a✝ a✝¹ a✝² t

Equations

⋯ = ⋯

Instances For

source

@[reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.bounded {L : Language} [L.LT] {ξ : Type v} (Γ : Polarity) (s n : ℕ) {φ : Semiformula L ξ n} :

Semiformula.Bounded BoundingOperator φ → Hierarchy Γ s φ

Equations

⋯ = ⋯

Instances For

source

@[simp, reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.verum {L : Language} [L.LT] {ξ : Type v} (Γ : Polarity) (s n : ℕ) :

Hierarchy Γ s ⊤

Equations

⋯ = ⋯

Instances For

source

@[simp, reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.falsum {L : Language} [L.LT] {ξ : Type v} (Γ : Polarity) (s n : ℕ) :

Hierarchy Γ s ⊥

Equations

⋯ = ⋯

Instances For

source

@[simp, reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.rel {L : Language} [L.LT] {ξ : Type v} {x : ℕ} (Γ : Polarity) (s : ℕ) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ x) :

Hierarchy Γ s (Semiformula.rel r v)

Equations

⋯ = ⋯

Instances For

source

@[simp, reducible, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.nrel {L : Language} [L.LT] {ξ : Type v} {x : ℕ} (Γ : Polarity) (s : ℕ) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ξ x) :

Hierarchy Γ s (Semiformula.nrel r v)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.and {L : Language} [L.LT] {ξ : Type v} {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} :

Hierarchy Γ s φ → Hierarchy Γ s ψ → Hierarchy Γ s (φ ⋏ ψ)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.or {L : Language} [L.LT] {ξ : Type v} {Γ : Polarity} {s n : ℕ} {φ ψ : Semiformula L ξ n} :

Hierarchy Γ s φ → Hierarchy Γ s ψ → Hierarchy Γ s (φ ⋎ ψ)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

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

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

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

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

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

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.exs {L : Language} [L.LT] {ξ : Type v} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚺 (s + 1) φ → Hierarchy 𝚺 (s + 1) (∃¹ φ)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.all {L : Language} [L.LT] {ξ : Type v} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚷 (s + 1) φ → Hierarchy 𝚷 (s + 1) (∀¹ φ)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.sigma {L : Language} [L.LT] {ξ : Type v} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚷 s φ → Hierarchy 𝚺 (s + 1) (∃¹ φ)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.pi {L : Language} [L.LT] {ξ : Type v} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚺 s φ → Hierarchy 𝚷 (s + 1) (∀¹ φ)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.dummy_sigma {L : Language} [L.LT] {ξ : Type v} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚷 (s + 1) φ → Hierarchy 𝚺 (s + 1 + 1) (∀¹ φ)

Equations

⋯ = ⋯

Instances For

source

@[reducible, match_pattern, inline]

abbrev FFL.FirstOrder.Arithmetic.Hierarchy.dummy_pi {L : Language} [L.LT] {ξ : Type v} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚺 (s + 1) φ → Hierarchy 𝚷 (s + 1 + 1) (∃¹ φ)

Equations

⋯ = ⋯

Instances For

source

@[simp]

theorem 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 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 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 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 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 FFL.FirstOrder.Arithmetic.Hierarchy.zero_iff {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ Γ' : Polarity} {φ : Semiformula L ξ n} :

Hierarchy Γ 0 φ ↔ Hierarchy Γ' 0 φ

source

theorem 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 FFL.FirstOrder.Arithmetic.Hierarchy.exsClosure {L : Language} [L.LT] {ξ : Type u_1} {s n : ℕ} {φ : Semiformula L ξ n} :

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

source

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

φ.Open → Hierarchy Γ s φ

source

theorem FFL.FirstOrder.Arithmetic.Hierarchy.zero_induction {L : Language} [L.LT] {ξ : Type u_1} {Γ : Polarity} {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), Hierarchy Γ 0 φ → Hierarchy Γ 0 ψ → P n φ → P n ψ → P n (φ ⋏ ψ)) (hOr : ∀ (n : ℕ) (φ ψ : Semiformula L ξ n), Hierarchy Γ 0 φ → Hierarchy Γ 0 ψ → P n φ → P n ψ → P n (φ ⋎ ψ)) (hBall : ∀ (n : ℕ) (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)), Hierarchy Γ 0 φ → P (n + 1) φ → P n (“(∀¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (hBexs : ∀ (n : ℕ) (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)), Hierarchy Γ 0 φ → P (n + 1) φ → P n (“(∃¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (n : ℕ) (φ : Semiformula L ξ n) :

Hierarchy Γ 0 φ → P n φ

source

theorem FFL.FirstOrder.Arithmetic.Hierarchy.sigma_succ_induction {L : Language} [L.LT] {ξ : Type u_1} {s : ℕ} {P : (n : ℕ) → Semiformula L ξ n → Prop} (hPi : ∀ (n : ℕ) (φ : Semiformula L ξ n), Hierarchy 𝚷 s φ → P n φ) (hAnd : ∀ (n : ℕ) (φ ψ : Semiformula L ξ n), Hierarchy 𝚺 (s + 1) φ → Hierarchy 𝚺 (s + 1) ψ → P n φ → P n ψ → P n (φ ⋏ ψ)) (hOr : ∀ (n : ℕ) (φ ψ : Semiformula L ξ n), Hierarchy 𝚺 (s + 1) φ → Hierarchy 𝚺 (s + 1) ψ → P n φ → P n ψ → P n (φ ⋎ ψ)) (hBall : ∀ (n : ℕ) (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)), Hierarchy 𝚺 (s + 1) φ → P (n + 1) φ → P n (“(∀¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (hBexs : ∀ (n : ℕ) (t : Semiterm L ξ n) (φ : Semiformula L ξ (n + 1)), Hierarchy 𝚺 (s + 1) φ → P (n + 1) φ → P n (“(∃¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (hExs : ∀ (n : ℕ) (φ : Semiformula L ξ (n + 1)), Hierarchy 𝚺 (s + 1) φ → P (n + 1) φ → P n (∃¹ φ)) (n : ℕ) (φ : Semiformula L ξ n) :

Hierarchy 𝚺 (s + 1) φ → P n φ

source

theorem FFL.FirstOrder.Arithmetic.Hierarchy.iff_iff {L : Language} [L.LT] {ξ : 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 FFL.FirstOrder.Arithmetic.Hierarchy.iff_iff₀ {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {b : Polarity} {φ ψ : Semiformula L ξ n} :

Hierarchy b 0 (φ 🡘 ψ) ↔ Hierarchy b 0 φ ∧ Hierarchy b 0 ψ

source

@[simp]

theorem FFL.FirstOrder.Arithmetic.Hierarchy.matrix_conj_iff {L : Language} [L.LT] {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 FFL.FirstOrder.Arithmetic.Hierarchy.remove_forall {L : Language} [L.LT] {ξ : Type u_1} {n : ℕ} {b : Polarity} {s : ℕ} {φ : Semiformula L ξ (n + 1)} :

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

source

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

Hierarchy Γ s (List.conj' φ l) ↔ ∀ i ∈ l, Hierarchy Γ s (φ i)

source

@[simp]

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

Hierarchy Γ s (List.disj' φ l) ↔ ∀ i ∈ l, Hierarchy Γ s (φ i)

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

theorem 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 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 FFL.FirstOrder.ArithmeticTheory.SoundOnHierarchy (T : ArithmeticTheory) (Γ : Polarity) (k : ℕ) :

Prop

Equations

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

Instances For

source

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

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

source

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

Entailment.Consistent T

source

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

Entailment.Consistent T