inductive
LO.FirstOrder.Arith.Hierarchy
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
:
LO.Polarity → ℕ → {n : ℕ} → LO.FirstOrder.Semiformula L ξ n → Prop
- verum: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} (Γ : LO.Polarity) (s n : ℕ), LO.FirstOrder.Arith.Hierarchy Γ s ⊤
- falsum: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} (Γ : LO.Polarity) (s n : ℕ), LO.FirstOrder.Arith.Hierarchy Γ s ⊥
- rel: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {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 v} {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 v} {Γ : LO.Polarity} {s n : ℕ} {p q : LO.FirstOrder.Semiformula L ξ n}, LO.FirstOrder.Arith.Hierarchy Γ s p → LO.FirstOrder.Arith.Hierarchy Γ s q → LO.FirstOrder.Arith.Hierarchy Γ s (p ⋏ q)
- or: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {Γ : LO.Polarity} {s n : ℕ} {p q : LO.FirstOrder.Semiformula L ξ n}, LO.FirstOrder.Arith.Hierarchy Γ s p → LO.FirstOrder.Arith.Hierarchy Γ s q → LO.FirstOrder.Arith.Hierarchy Γ s (p ⋎ q)
- ball: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {Γ : LO.Polarity} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)}, t.Positive → LO.FirstOrder.Arith.Hierarchy Γ s p → LO.FirstOrder.Arith.Hierarchy Γ s (“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!t] !p)”)
- bex: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {Γ : LO.Polarity} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)} {t : LO.FirstOrder.Semiterm L ξ (n + 1)}, t.Positive → LO.FirstOrder.Arith.Hierarchy Γ s p → LO.FirstOrder.Arith.Hierarchy Γ s (“(∃[!!(LO.FirstOrder.Semiterm.bvar 0) < !!t] !p)”)
- ex: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) p → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃' p)
- all: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) p → LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀' p)
- sigma: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚷 s p → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃' p)
- pi: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚺 s p → LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀' p)
- dummy_sigma: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) p → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1 + 1) (∀' p)
- dummy_pi: ∀ {L : LO.FirstOrder.Language} [inst : L.LT] {ξ : Type v} {s n : ℕ} {p : LO.FirstOrder.Semiformula L ξ (n + 1)}, LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) p → LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1 + 1) (∃' p)
Instances For
def
LO.FirstOrder.Arith.DeltaZero
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
(p : LO.FirstOrder.Semiformula L ξ n)
:
Equations
Instances For
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.and_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
{q : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s (p ⋏ q) ↔ LO.FirstOrder.Arith.Hierarchy Γ s p ∧ LO.FirstOrder.Arith.Hierarchy Γ s q
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.or_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
{q : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s (p ⋎ q) ↔ LO.FirstOrder.Arith.Hierarchy Γ s p ∧ LO.FirstOrder.Arith.Hierarchy Γ s q
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.conj_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{m : ℕ}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : Fin m → LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s (Matrix.conj p) ↔ ∀ (i : Fin m), LO.FirstOrder.Arith.Hierarchy Γ s (p i)
theorem
LO.FirstOrder.Arith.Hierarchy.zero_eq_alt
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{p : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ 0 p → LO.FirstOrder.Arith.Hierarchy Γ.alt 0 p
theorem
LO.FirstOrder.Arith.Hierarchy.pi_zero_iff_sigma_zero
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
:
theorem
LO.FirstOrder.Arith.Hierarchy.zero_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{Γ' : LO.Polarity}
{p : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ 0 p ↔ LO.FirstOrder.Arith.Hierarchy Γ' 0 p
theorem
LO.FirstOrder.Arith.Hierarchy.zero_iff_delta_zero
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{p : LO.FirstOrder.Semiformula L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.alt_zero_iff_zero
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{p : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ.alt 0 p ↔ LO.FirstOrder.Arith.Hierarchy Γ 0 p
theorem
LO.FirstOrder.Arith.Hierarchy.accum
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s p → ∀ (Γ' : LO.Polarity), LO.FirstOrder.Arith.Hierarchy Γ' (s + 1) p
theorem
LO.FirstOrder.Arith.Hierarchy.strict_mono
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
(hp : LO.FirstOrder.Arith.Hierarchy Γ s p)
(Γ' : LO.Polarity)
{s' : ℕ}
(h : s < s')
:
LO.FirstOrder.Arith.Hierarchy Γ' s' p
theorem
LO.FirstOrder.Arith.Hierarchy.mono
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{s' : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
(hp : LO.FirstOrder.Arith.Hierarchy Γ s p)
(h : s ≤ s')
:
theorem
LO.FirstOrder.Arith.Hierarchy.of_zero
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{b : LO.Polarity}
{b' : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
(hp : LO.FirstOrder.Arith.Hierarchy b 0 p)
:
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.equal
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.Eq]
[L.LT]
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{t : LO.FirstOrder.Semiterm L ξ n}
{u : LO.FirstOrder.Semiterm L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s (“!!t = !!u”)
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.lt
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.LT]
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{t : LO.FirstOrder.Semiterm L ξ n}
{u : LO.FirstOrder.Semiterm L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s (“!!t < !!u”)
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.le
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.Eq]
[L.LT]
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{t : LO.FirstOrder.Semiterm L ξ n}
{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 v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s p → LO.FirstOrder.Arith.Hierarchy Γ.alt s (∼p)
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.neg_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s (∼p) ↔ LO.FirstOrder.Arith.Hierarchy Γ.alt s p
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.imp_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
{q : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s (p ➝ q) ↔ LO.FirstOrder.Arith.Hierarchy Γ.alt s p ∧ LO.FirstOrder.Arith.Hierarchy Γ s q
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.ball_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{Γ : LO.Polarity}
{s : ℕ}
{n : ℕ}
{p : 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] !p)”) ↔ LO.FirstOrder.Arith.Hierarchy Γ s p
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.bex_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{Γ : LO.Polarity}
{s : ℕ}
{n : ℕ}
{p : 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] !p)”) ↔ LO.FirstOrder.Arith.Hierarchy Γ s p
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.ballLT_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{Γ : LO.Polarity}
{s : ℕ}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
{t : LO.FirstOrder.Semiterm L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.bexLT_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{Γ : LO.Polarity}
{s : ℕ}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
{t : LO.FirstOrder.Semiterm L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.ballLTSucc_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
[L.Zero]
[L.One]
[L.Add]
{Γ : LO.Polarity}
{s : ℕ}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
{t : LO.FirstOrder.Semiterm L ξ n}
:
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.bexLTSucc_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
[L.Zero]
[L.One]
[L.Add]
{Γ : LO.Polarity}
{s : ℕ}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
{t : LO.FirstOrder.Semiterm L ξ n}
:
theorem
LO.FirstOrder.Arith.Hierarchy.pi_of_pi_all
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
LO.FirstOrder.Arith.Hierarchy 𝚷 s (∀' p) → LO.FirstOrder.Arith.Hierarchy 𝚷 s p
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.all_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) (∀' p) ↔ LO.FirstOrder.Arith.Hierarchy 𝚷 (s + 1) p
theorem
LO.FirstOrder.Arith.Hierarchy.sigma_of_sigma_ex
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
LO.FirstOrder.Arith.Hierarchy 𝚺 s (∃' p) → LO.FirstOrder.Arith.Hierarchy 𝚺 s p
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.sigma_iff
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃' p) ↔ LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) p
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₂)
{p : LO.FirstOrder.Semiformula L ξ₁ n₁}
:
LO.FirstOrder.Arith.Hierarchy Γ s p → LO.FirstOrder.Arith.Hierarchy Γ s (ω.hom p)
@[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₂}
{p : LO.FirstOrder.Semiformula L ξ₁ n₁}
:
LO.FirstOrder.Arith.Hierarchy Γ s (ω.hom p) ↔ LO.FirstOrder.Arith.Hierarchy Γ s p
theorem
LO.FirstOrder.Arith.Hierarchy.exClosure
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{s : ℕ}
{n : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) p → LO.FirstOrder.Arith.Hierarchy 𝚺 (s + 1) (∃* p)
instance
LO.FirstOrder.Arith.Hierarchy.instAndOrClosedSemiformula
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{k : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
:
Equations
- LO.FirstOrder.Arith.Hierarchy.instAndOrClosedSemiformula = { verum := ⋯, falsum := ⋯, and := ⋯, or := ⋯ }
instance
LO.FirstOrder.Arith.Hierarchy.instClosedSemiformulaOfNatNat
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{k : ℕ}
{Γ : LO.Polarity}
:
Equations
- LO.FirstOrder.Arith.Hierarchy.instClosedSemiformulaOfNatNat = LO.LogicalConnective.Closed.mk ⋯ ⋯
theorem
LO.FirstOrder.Arith.Hierarchy.of_open
{L : LO.FirstOrder.Language}
[L.LT]
{ξ : Type v}
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
:
p.Open → LO.FirstOrder.Arith.Hierarchy Γ s p
theorem
LO.FirstOrder.Arith.Hierarchy.oringEmb
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.ORing]
{n : ℕ}
{Γ : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula ℒₒᵣ ξ n}
:
LO.FirstOrder.Arith.Hierarchy Γ s p →
LO.FirstOrder.Arith.Hierarchy Γ s ((LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) p)
theorem
LO.FirstOrder.Arith.Hierarchy.iff_iff
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.ORing]
{n : ℕ}
{b : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ n}
{q : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy b s (p ⭤ q) ↔ LO.FirstOrder.Arith.Hierarchy b s p ∧ LO.FirstOrder.Arith.Hierarchy b.alt s p ∧ LO.FirstOrder.Arith.Hierarchy b s q ∧ LO.FirstOrder.Arith.Hierarchy b.alt s q
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.iff_iff₀
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.ORing]
{n : ℕ}
{b : LO.Polarity}
{p : LO.FirstOrder.Semiformula L ξ n}
{q : LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy b 0 (p ⭤ q) ↔ LO.FirstOrder.Arith.Hierarchy b 0 p ∧ LO.FirstOrder.Arith.Hierarchy b 0 q
@[simp]
theorem
LO.FirstOrder.Arith.Hierarchy.matrix_conj_iff
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.ORing]
{m : ℕ}
{b : LO.Polarity}
{s : ℕ}
{n : ℕ}
{p : Fin m → LO.FirstOrder.Semiformula L ξ n}
:
LO.FirstOrder.Arith.Hierarchy b s (Matrix.conj fun (j : Fin m) => p j) ↔ ∀ (j : Fin m), LO.FirstOrder.Arith.Hierarchy b s (p j)
theorem
LO.FirstOrder.Arith.Hierarchy.remove_forall
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.ORing]
{n : ℕ}
{b : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
LO.FirstOrder.Arith.Hierarchy b s (∀' p) → LO.FirstOrder.Arith.Hierarchy b s p
theorem
LO.FirstOrder.Arith.Hierarchy.remove_exists
{ξ : Type v}
{L : LO.FirstOrder.Language}
[L.ORing]
{n : ℕ}
{b : LO.Polarity}
{s : ℕ}
{p : LO.FirstOrder.Semiformula L ξ (n + 1)}
:
LO.FirstOrder.Arith.Hierarchy b s (∃' p) → LO.FirstOrder.Arith.Hierarchy b s p
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.Sigma1Sound
{L : LO.FirstOrder.Language}
[L.LT]
[LO.FirstOrder.Structure L ℕ]
(T : LO.FirstOrder.Theory L)
:
Equations
Instances For
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]
:
theorem
LO.FirstOrder.Arith.sigma₁_induction
{ξ : Type v}
{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 : ℕ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n),
LO.FirstOrder.Arith.Hierarchy 𝚺 1 p → LO.FirstOrder.Arith.Hierarchy 𝚺 1 q → P n p → P n q → P n (p ⋏ q))
(hOr : ∀ (n : ℕ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n),
LO.FirstOrder.Arith.Hierarchy 𝚺 1 p → LO.FirstOrder.Arith.Hierarchy 𝚺 1 q → P n p → P n q → P n (p ⋎ q))
(hBall : ∀ (n : ℕ) (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)),
LO.FirstOrder.Arith.Hierarchy 𝚺 1 p →
P (n + 1) p → P n (“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Rew.bShift t)] !p)”))
(hEx : ∀ (n : ℕ) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)), LO.FirstOrder.Arith.Hierarchy 𝚺 1 p → P (n + 1) p → P n (∃' p))
(n : ℕ)
(p : LO.FirstOrder.Semiformula ℒₒᵣ ξ n)
:
LO.FirstOrder.Arith.Hierarchy 𝚺 1 p → P n p
theorem
LO.FirstOrder.Arith.sigma₁_induction'
{ξ : Type v}
{n : ℕ}
{p : LO.FirstOrder.Semiformula ℒₒᵣ ξ n}
(hp : LO.FirstOrder.Arith.Hierarchy 𝚺 1 p)
{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 : ℕ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n),
LO.FirstOrder.Arith.Hierarchy 𝚺 1 p → LO.FirstOrder.Arith.Hierarchy 𝚺 1 q → P n p → P n q → P n (p ⋏ q))
(hOr : ∀ (n : ℕ) (p q : LO.FirstOrder.Semiformula ℒₒᵣ ξ n),
LO.FirstOrder.Arith.Hierarchy 𝚺 1 p → LO.FirstOrder.Arith.Hierarchy 𝚺 1 q → P n p → P n q → P n (p ⋎ q))
(hBall : ∀ (n : ℕ) (t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)),
LO.FirstOrder.Arith.Hierarchy 𝚺 1 p →
P (n + 1) p → P n (“(∀[!!(LO.FirstOrder.Semiterm.bvar 0) < !!(LO.FirstOrder.Rew.bShift t)] !p)”))
(hEx : ∀ (n : ℕ) (p : LO.FirstOrder.Semiformula ℒₒᵣ ξ (n + 1)), LO.FirstOrder.Arith.Hierarchy 𝚺 1 p → P (n + 1) p → P n (∃' p))
:
P n p