Hierarchy

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

Imported declaration from the Incompleteness formalization.

• 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] !φ)”)
• bex {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] !φ)”)
• ex {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Sg (s + 1) φ → Hierarchy Sg (s + 1) (∃' φ)
• all {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Pg (s + 1) φ → Hierarchy Pg (s + 1) (∀' φ)
• sigma {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Pg s φ → Hierarchy Sg (s + 1) (∃' φ)
• pi {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Sg s φ → Hierarchy Pg (s + 1) (∀' φ)
• dummy_sigma {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Pg (s + 1) φ → Hierarchy Sg (s + 1 + 1) (∀' φ)
• dummy_pi {L : Language} [L.LT] {ξ : Type u_2} {s n : ℕ} {φ : Semiformula L ξ (n + 1)} : Hierarchy Sg (s + 1) φ → Hierarchy Pg (s + 1 + 1) (∃' φ)

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

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

theorem LO.FirstOrder.Arith.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' φ

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

theorem LO.FirstOrder.Arith.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 φ

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Arith.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 φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.bex_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 φ

@[simp]

theorem LO.FirstOrder.Arith.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 φ

@[simp]

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

@[simp]

theorem LO.FirstOrder.Arith.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 φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.bexLTSucc_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.bexLTSucc t φ) ↔ Hierarchy Γ s φ

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

@[simp]

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

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

@[simp]

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

theorem LO.FirstOrder.Arith.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 ω) φ)

@[simp]

theorem LO.FirstOrder.Arith.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 φ

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

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

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

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

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

theorem LO.FirstOrder.Arith.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 ψ

@[simp]

theorem LO.FirstOrder.Arith.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 ψ

@[simp]

theorem LO.FirstOrder.Arith.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.conjVec fun (j : Fin m) => φ j) ↔ ∀ (j : Fin m), Hierarchy b s (φ j)

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

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

theorem LO.FirstOrder.Arith.sigma₁_induction {ξ : Type u_1} {P : (n : ℕ) → Semiformula ℒₒᵣ ξ 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 Sg 1 φ → Hierarchy Sg 1 ψ → P n φ → P n ψ → P n (φ ⋏ ψ)) (hOr : ∀ (n : ℕ) (φ ψ : Semiformula ℒₒᵣ ξ n), Hierarchy Sg 1 φ → Hierarchy Sg 1 ψ → P n φ → P n ψ → P n (φ ⋎ ψ)) (hBall : ∀ (n : ℕ) (t : Semiterm ℒₒᵣ ξ n) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Sg 1 φ → P (n + 1) φ → P n (“(∀[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (hEx : ∀ (n : ℕ) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Sg 1 φ → P (n + 1) φ → P n (∃' φ)) (n : ℕ) (φ : Semiformula ℒₒᵣ ξ n) : Hierarchy Sg 1 φ → P n φ

theorem LO.FirstOrder.Arith.sigma₁_induction' {ξ : Type u_1} {n : ℕ} {φ : Semiformula ℒₒᵣ ξ n} (hp : Hierarchy Sg 1 φ) {P : (n : ℕ) → Semiformula ℒₒᵣ ξ 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 Sg 1 φ → Hierarchy Sg 1 ψ → P n φ → P n ψ → P n (φ ⋏ ψ)) (hOr : ∀ (n : ℕ) (φ ψ : Semiformula ℒₒᵣ ξ n), Hierarchy Sg 1 φ → Hierarchy Sg 1 ψ → P n φ → P n ψ → P n (φ ⋎ ψ)) (hBall : ∀ (n : ℕ) (t : Semiterm ℒₒᵣ ξ n) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Sg 1 φ → P (n + 1) φ → P n (“(∀[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ)”)) (hEx : ∀ (n : ℕ) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy Sg 1 φ → P (n + 1) φ → P n (∃' φ)) : P n φ