inductive LO.FirstOrder.Arith.Hierarchy {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_2} : LO.Polarity → ℕ → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n → Prop

• verum: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} (Γ : LO.Polarity) (s n : ℕ), LO.FirstOrder.Arith.Hierarchy Γ s ⊤
• falsum: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} (Γ : LO.Polarity) (s n : ℕ), LO.FirstOrder.Arith.Hierarchy Γ s ⊥
• rel: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {x : ℕ} (Γ : LO.Polarity) (s : ℕ) {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ x), LO.FirstOrder.Arith.Hierarchy Γ s (LO.FirstOrder.Semiformula.rel r v)
• nrel: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {x : ℕ} (Γ : LO.Polarity) (s : ℕ) {k : ℕ} (r : L.Rel k) (v : Fin k → LO.FirstOrder.Semiterm L ξ x), LO.FirstOrder.Arith.Hierarchy Γ s (LO.FirstOrder.Semiformula.nrel r v)
• and: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {Γ : LO.Polarity} {s n : ℕ} {φ ψ : LO.FirstOrder.Semiformula L ξ n}, LO.FirstOrder.Arith.Hierarchy Γ s φ → LO.FirstOrder.Arith.Hierarchy Γ s ψ → LO.FirstOrder.Arith.Hierarchy Γ s (φ ⋏ ψ)
• or: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {Γ : LO.Polarity} {s n : ℕ} {φ ψ : LO.FirstOrder.Semiformula L ξ n}, LO.FirstOrder.Arith.Hierarchy Γ s φ → LO.FirstOrder.Arith.Hierarchy Γ s ψ → LO.FirstOrder.Arith.Hierarchy Γ s (φ ⋎ ψ)
• ball: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {Γ : LO.Polarity} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)}, t.Positive → LO.FirstOrder.Arith.Hierarchy Γ s φ → LO.FirstOrder.Arith.Hierarchy Γ s (“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!t] !φ)”)
• bex: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {Γ : LO.Polarity} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)}, t.Positive → LO.FirstOrder.Arith.Hierarchy Γ s φ → LO.FirstOrder.Arith.Hierarchy Γ s (“(∃[!!(LO.FirstOrder.Semiterm.bvar 0) < !!t] !φ)”)
• ex: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) φ → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃' φ)
• all: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) φ → LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀' φ)
• sigma: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚷 s φ → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃' φ)
• pi: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚺 s φ → LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀' φ)
• dummy_sigma: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) φ → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1 + 1) (∀' φ)
• dummy_pi: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type u_2} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) φ → LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1 + 1) (∃' φ)

def LO.FirstOrder.Arith.DeltaZero {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_2} {n : ℕ} (φ : LO.FirstOrder.Semiformula L ξ n) : Prop

Equations

• LO.FirstOrder.Arith.DeltaZero φ = LO.FirstOrder.Arith.Hierarchy 𝚺 0 φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.and_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ ψ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (φ ⋏ ψ) ↔ LO.FirstOrder.Arith.Hierarchy Γ s φ ∧ LO.FirstOrder.Arith.Hierarchy Γ s ψ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.or_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ ψ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (φ ⋎ ψ) ↔ LO.FirstOrder.Arith.Hierarchy Γ s φ ∧ LO.FirstOrder.Arith.Hierarchy Γ s ψ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.conj_iff {L : LO.FirstOrder.Language} [L.LT] {m : ℕ} {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ : Fin m → LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (Matrix.conj φ) ↔ ∀ (i : Fin m), LO.FirstOrder.Arith.Hierarchy Γ s (φ i)

theorem LO.FirstOrder.Arith.Hierarchy.zero_eq_alt {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ 0 φ → LO.FirstOrder.Arith.Hierarchy Γ.alt 0 φ

theorem LO.FirstOrder.Arith.Hierarchy.pi_zero_iff_sigma_zero {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy 𝚷 0 φ ↔ LO.FirstOrder.Arith.Hierarchy 𝚺 0 φ

theorem LO.FirstOrder.Arith.Hierarchy.zero_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ Γ' : LO.Polarity} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ 0 φ ↔ LO.FirstOrder.Arith.Hierarchy Γ' 0 φ

theorem LO.FirstOrder.Arith.Hierarchy.zero_iff_delta_zero {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ 0 φ ↔ LO.FirstOrder.Arith.DeltaZero φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.alt_zero_iff_zero {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ.alt 0 φ ↔ LO.FirstOrder.Arith.Hierarchy Γ 0 φ

theorem LO.FirstOrder.Arith.Hierarchy.accum {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s φ → ∀ (Γ' : LO.Polarity), LO.FirstOrder.Arith.Hierarchy Γ' (s + 1) φ

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

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

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

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.equal {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} [L.Eq] [L.LT] {t u : LO.FirstOrder.Semiterm L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (“!!t = !!u”)

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.lt {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} [L.LT] {t u : LO.FirstOrder.Semiterm L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (“!!t < !!u”)

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.le {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} [L.Eq] [L.LT] {t u : LO.FirstOrder.Semiterm L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (“!!t ≤ !!u”)

theorem LO.FirstOrder.Arith.Hierarchy.neg {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s φ → LO.FirstOrder.Arith.Hierarchy Γ.alt s (∼φ)

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.neg_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (∼φ) ↔ LO.FirstOrder.Arith.Hierarchy Γ.alt s φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.imp_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ ψ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (φ ➝ ψ) ↔ LO.FirstOrder.Arith.Hierarchy Γ.alt s φ ∧ LO.FirstOrder.Arith.Hierarchy Γ s ψ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.ball_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {Γ : LO.Polarity} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)} (ht : t.Positive) : LO.FirstOrder.Arith.Hierarchy Γ s (“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!t] !φ)”) ↔ LO.FirstOrder.Arith.Hierarchy Γ s φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.bex_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {Γ : LO.Polarity} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)} (ht : t.Positive) : LO.FirstOrder.Arith.Hierarchy Γ s (“(∃[!!(LO.FirstOrder.Semiterm.bvar 0) < !!t] !φ)”) ↔ LO.FirstOrder.Arith.Hierarchy Γ s φ

@[simp]

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

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.bexLT_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {Γ : LO.Polarity} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (LO.FirstOrder.Semiformula.bexLT t φ) ↔ LO.FirstOrder.Arith.Hierarchy Γ s φ

@[simp]

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

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.bexLTSucc_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} [L.Zero] [L.One] [L.Add] {Γ : LO.Polarity} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s (LO.FirstOrder.Semiformula.bexLTSucc t φ) ↔ LO.FirstOrder.Arith.Hierarchy Γ s φ

theorem LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} : LO.FirstOrder.Arith.Hierarchy 𝚷 s (∀' φ) → LO.FirstOrder.Arith.Hierarchy 𝚷 s φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.all_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} : LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀' φ) ↔ LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) φ

theorem LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} : LO.FirstOrder.Arith.Hierarchy 𝚺 s (∃' φ) → LO.FirstOrder.Arith.Hierarchy 𝚺 s φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.sigma_iff {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} : LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃' φ) ↔ LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) φ

theorem LO.FirstOrder.Arith.Hierarchy.rew {L : LO.FirstOrder.Language} [L.LT] {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {Γ : LO.Polarity} {s : ℕ} (ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂) {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} : LO.FirstOrder.Arith.Hierarchy Γ s φ → LO.FirstOrder.Arith.Hierarchy Γ s ((LO.FirstOrder.Rewriting.app ω) φ)

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.rew_iff {L : LO.FirstOrder.Language} [L.LT] {ξ₁ : Type u_1} {n₁ : ℕ} {ξ₂ : Type u_2} {n₂ : ℕ} {Γ : LO.Polarity} {s : ℕ} {ω : LO.FirstOrder.Rew L ξ₁ n₁ ξ₂ n₂} {φ : LO.FirstOrder.Semiformula L ξ₁ n₁} : LO.FirstOrder.Arith.Hierarchy Γ s ((LO.FirstOrder.Rewriting.app ω) φ) ↔ LO.FirstOrder.Arith.Hierarchy Γ s φ

theorem LO.FirstOrder.Arith.Hierarchy.exClosure {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {s n : ℕ} {φ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) φ → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃* φ)

instance LO.FirstOrder.Arith.Hierarchy.instAndOrClosedSemiformula {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {k : ℕ} {Γ : LO.Polarity} {s : ℕ} : LO.LogicalConnective.AndOrClosed (LO.FirstOrder.Arith.Hierarchy Γ s)

Equations

• ⋯ = ⋯

instance LO.FirstOrder.Arith.Hierarchy.instClosedSemiformulaOfNatNat {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {k : ℕ} {Γ : LO.Polarity} : LO.LogicalConnective.Closed (LO.FirstOrder.Arith.Hierarchy Γ 0)

Equations

• ⋯ = ⋯

theorem LO.FirstOrder.Arith.Hierarchy.of_open {L : LO.FirstOrder.Language} [L.LT] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ n} : φ.Open → LO.FirstOrder.Arith.Hierarchy Γ s φ

theorem LO.FirstOrder.Arith.Hierarchy.oringEmb {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {Γ : LO.Polarity} {s : ℕ} {φ : LO.FirstOrder.Semiformula ℒₒᵣ ξ n} : LO.FirstOrder.Arith.Hierarchy Γ s φ → LO.FirstOrder.Arith.Hierarchy Γ s ((LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) φ)

theorem LO.FirstOrder.Arith.Hierarchy.iff_iff {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : LO.Polarity} {s : ℕ} {φ ψ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy b s (φ ⭤ ψ) ↔ LO.FirstOrder.Arith.Hierarchy b s φ ∧ LO.FirstOrder.Arith.Hierarchy b.alt s φ ∧ LO.FirstOrder.Arith.Hierarchy b s ψ ∧ LO.FirstOrder.Arith.Hierarchy b.alt s ψ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.iff_iff₀ {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : LO.Polarity} {φ ψ : LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy b 0 (φ ⭤ ψ) ↔ LO.FirstOrder.Arith.Hierarchy b 0 φ ∧ LO.FirstOrder.Arith.Hierarchy b 0 ψ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.matrix_conj_iff {L : LO.FirstOrder.Language} [L.ORing] {m : ℕ} {ξ : Type u_1} {b : LO.Polarity} {s n : ℕ} {φ : Fin m → LO.FirstOrder.Semiformula L ξ n} : LO.FirstOrder.Arith.Hierarchy b s (Matrix.conj fun (j : Fin m) => φ j) ↔ ∀ (j : Fin m), LO.FirstOrder.Arith.Hierarchy b s (φ j)

theorem LO.FirstOrder.Arith.Hierarchy.remove_forall {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : LO.Polarity} {s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} : LO.FirstOrder.Arith.Hierarchy b s (∀' φ) → LO.FirstOrder.Arith.Hierarchy b s φ

theorem LO.FirstOrder.Arith.Hierarchy.remove_exists {L : LO.FirstOrder.Language} [L.ORing] {ξ : Type u_1} {n : ℕ} {b : LO.Polarity} {s : ℕ} {φ : LO.FirstOrder.Semiformula L ξ (n + 1)} : LO.FirstOrder.Arith.Hierarchy b s (∃' φ) → LO.FirstOrder.Arith.Hierarchy b s φ

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Sigma1Sound {L : LO.FirstOrder.Language} [L.LT] [LO.FirstOrder.Structure L ℕ] (T : LO.FirstOrder.Theory L) : Prop

Equations

• LO.FirstOrder.Arith.Sigma1Sound T = LO.FirstOrder.Arith.SoundOn T (LO.FirstOrder.Arith.Hierarchy 𝚺 1)

theorem LO.FirstOrder.Arith.consistent_of_sigma1Sound {L : LO.FirstOrder.Language} [L.LT] [LO.FirstOrder.Structure L ℕ] (T : LO.FirstOrder.Theory L) [LO.FirstOrder.Arith.Sigma1Sound T] : LO.System.Consistent T

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

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