Foundation.FirstOrder.Arith.Hierarchy

source

inductive LO.FirstOrder.Arith.Hierarchy {L : Language} [L.LT] {ξ : Type u_2} :

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

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 𝚺 (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

source

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

Prop

Equations

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

source

@[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 ψ

source

@[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 ψ

source

@[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.conj φ) ↔ ∀ (i : Fin m), Hierarchy Γ s (φ i)

source

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 φ

source

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

Hierarchy 𝚷 0 φ ↔ Hierarchy 𝚺 0 φ

source

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

Hierarchy Γ 0 φ ↔ Hierarchy Γ' 0 φ

source

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

Hierarchy Γ 0 φ ↔ DeltaZero φ

source

@[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 φ

source

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) φ

source

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' φ

source

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' φ

source

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 φ

source

@[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”)

source

@[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”)

source

@[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”)

source

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

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

source

@[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 φ

source

@[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 ψ

source

@[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 φ

source

@[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 φ

source

@[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 φ

source

@[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 φ

source

@[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 φ

source

@[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 φ

source

theorem LO.FirstOrder.Arith.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 LO.FirstOrder.Arith.Hierarchy.all_iff {L : Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚷 (s + 1) (∀' φ) ↔ Hierarchy 𝚷 (s + 1) φ

source

theorem LO.FirstOrder.Arith.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 LO.FirstOrder.Arith.Hierarchy.sigma_iff {L : Language} [L.LT] {ξ : Type u_1} {n s : ℕ} {φ : Semiformula L ξ (n + 1)} :

Hierarchy 𝚺 (s + 1) (∃' φ) ↔ Hierarchy 𝚺 (s + 1) φ

source

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 ω) φ)

source

@[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 φ

source

theorem LO.FirstOrder.Arith.Hierarchy.exClosure {L : Language} [L.LT] {ξ : Type u_1} {s n : ℕ} {φ : Semiformula L ξ n} :

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

source

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

LogicalConnective.AndOrClosed (Hierarchy Γ s)

source

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

LogicalConnective.Closed (Hierarchy Γ 0)

source

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

φ.Open → Hierarchy Γ s φ

source

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) φ)

source

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 ψ

source

@[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 ψ

source

@[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.conj fun (j : Fin m) => φ j) ↔ ∀ (j : Fin m), Hierarchy b s (φ j)

source

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 φ

source

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 φ

source

@[reducible, inline]

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

Prop

Equations

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

source

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

System.Consistent T

source

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 𝚺 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)] !φ)”)) (hEx : ∀ (n : ℕ) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy 𝚺 1 φ → P (n + 1) φ → P n (∃' φ)) (n : ℕ) (φ : Semiformula ℒₒᵣ ξ n) :

Hierarchy 𝚺 1 φ → P n φ

source

theorem LO.FirstOrder.Arith.sigma₁_induction' {ξ : Type u_1} {n : ℕ} {φ : Semiformula ℒₒᵣ ξ n} (hp : Hierarchy 𝚺 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 𝚺 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)] !φ)”)) (hEx : ∀ (n : ℕ) (φ : Semiformula ℒₒᵣ ξ (n + 1)), Hierarchy 𝚺 1 φ → P (n + 1) φ → P n (∃' φ)) :

P n φ