Arithmetical Formula Sorted by Arithmetical Hierarchy

This file defines the $\Sigma_n / \Pi_n / \Delta_n$ formulas of arithmetic of first-order logic.

• Sg-[m].Semiformula ξ n is a Semiformula ℒₒᵣ ξ n which is Sg-[m].
• Pg-[m].Semiformula ξ n is a Semiformula ℒₒᵣ ξ n which is Pg-[m].
• Dlt-[m].Semiformula ξ n is a pair of Sg-[m].Semiformula ξ n and Pg-[m].Semiformula ξ n.
• ProperOn : φ.ProperOn M iff φ's two element φ.sigma and φ.pi are equivalent on model M.

structure LO.FirstOrder.Arith.HierarchySymbol : Type

Imported declaration from the Incompleteness formalization.

• Γ : SigmaPiDelta

  Imported declaration from the Incompleteness formalization.

• rank : ℕ

  Imported declaration from the Incompleteness formalization.

def LO.FirstOrder.Arith.«term_-[_]» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.sigmaZero : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.sigmaZero = { Γ := Sg, rank := 0 }

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.piZero : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.piZero = { Γ := Pg, rank := 0 }

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.deltaZero : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.deltaZero = { Γ := Dlt, rank := 0 }

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.sigmaOne : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.sigmaOne = { Γ := Sg, rank := 1 }

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.piOne : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.piOne = { Γ := Pg, rank := 1 }

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.deltaOne : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.deltaOne = { Γ := Dlt, rank := 1 }

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Sg0 : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.Sg0 = LO.FirstOrder.Arith.HierarchySymbol.sigmaZero

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Pg0 : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.Pg0 = LO.FirstOrder.Arith.HierarchySymbol.piZero

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Dlt0 : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.Dlt0 = LO.FirstOrder.Arith.HierarchySymbol.deltaZero

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Sg1 : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.Sg1 = LO.FirstOrder.Arith.HierarchySymbol.sigmaOne

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Pg1 : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.Pg1 = LO.FirstOrder.Arith.HierarchySymbol.piOne

@[reducible, inline]

abbrev LO.FirstOrder.Arith.Dlt1 : HierarchySymbol

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.Dlt1 = LO.FirstOrder.Arith.HierarchySymbol.deltaOne

inductive LO.FirstOrder.Arith.HierarchySymbol.Semiformula (ξ : Type u_1) (n : ℕ) : HierarchySymbol → Type u_1

Imported declaration from the Incompleteness formalization.

• mkSigma {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) : Hierarchy Sg m φ → HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }
• mkPi {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) : Hierarchy Pg m φ → HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }
• mkDelta {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.Semisentence (Γ : HierarchySymbol) (n : ℕ) : Type

Imported declaration from the Incompleteness formalization.

Equations

• Γ.Semisentence n = LO.FirstOrder.Arith.HierarchySymbol.Semiformula Empty n Γ

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.Sentence (Γ : HierarchySymbol) : Type

Imported declaration from the Incompleteness formalization.

Equations

• Γ.Sentence = LO.FirstOrder.Arith.HierarchySymbol.Semiformula Empty 0 Γ

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → Semiformula ℒₒᵣ ξ n

Imported declaration from the Incompleteness formalization.

Equations

• (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma φ a).val = φ
• (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ a).val = φ
• (φ.mkDelta a).val = φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_mkSigma {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) (hp : Hierarchy Sg m φ) : (mkSigma φ hp).val = φ

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_mkPi {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) (hp : Hierarchy Pg m φ) : (mkPi φ hp).val = φ

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_mkDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : (φ.mkDelta ψ).val = φ.val

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSg0SemisentenceORing {n : ℕ} : Coe (Sg0.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSg0SemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePg0SemisentenceORing {n : ℕ} : Coe (Pg0.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePg0SemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDlt0SemisentenceORing {n : ℕ} : Coe (Dlt0.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDlt0SemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSg1SemisentenceORing {n : ℕ} : Coe (Sg1.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSg1SemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePg1SemisentenceORing {n : ℕ} : Coe (Pg1.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePg1SemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDlt1SemisentenceORing {n : ℕ} : Coe (Dlt1.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDlt1SemisentenceORing = { coe := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val }

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_prop {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) : Hierarchy Sg m φ.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_prop {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : Hierarchy Pg m φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.polarity_prop {ξ : Type u_1} {n m : ℕ} {Γ : Polarity} (φ : HierarchySymbol.Semiformula ξ n { Γ := Γ.coe, rank := m }) : Hierarchy Γ m φ.val

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }

Imported declaration from the Incompleteness formalization.

Equations

• (φ.mkDelta a).sigma = φ

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_mkDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : (φ.mkDelta ψ).sigma = φ

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }

Imported declaration from the Incompleteness formalization.

Equations

• (φ.mkDelta a).pi = a

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_mkDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : (φ.mkDelta ψ).pi = ψ

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_sigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : φ.sigma.val = φ.val

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPolarity {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) (Γ : Polarity) : Hierarchy Γ m φ → HierarchySymbol.Semiformula ξ n { Γ := Γ.coe, rank := m }

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPolarity φ LO.Polarity.sigma h = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma φ h
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPolarity φ LO.Polarity.pi h = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ h

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_mkPolarity {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) {Γ : Polarity} (h : Hierarchy Γ m φ) : (mkPolarity φ Γ h).val = φ

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.hierarchy_sigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) : Hierarchy Sg m φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.hierarchy_pi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : Hierarchy Pg m φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.hierarchy_zero {ξ : Type u_1} {n : ℕ} {Γ : SigmaPiDelta} {Γ' : Polarity} {m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Γ, rank := 0 }) : Hierarchy Γ' m φ.val

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn {n : ℕ} (M : Type u_2) [ORingStruc M] {m : ℕ} (φ : { Γ := Dlt, rank := m }.Semisentence n) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn {n : ℕ} (M : Type u_2) [ORingStruc M] {m : ℕ} (φ : HierarchySymbol.Semiformula M n { Γ := Dlt, rank := m }) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProvablyProperOn {n m : ℕ} (φ : { Γ := Dlt, rank := m }.Semisentence n) (T : Theory ℒₒᵣ) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.iff {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence n} (h : ProperOn M φ) (e : Fin n → M) : M ⊧/e (sigma φ).val ↔ M ⊧/e (pi φ).val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.iff {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} {φ : HierarchySymbol.Semiformula M n { Γ := Dlt, rank := m }} (h : ProperWithParamOn M φ) (e : Fin n → M) : (Semiformula.Evalm M e id) φ.sigma.val ↔ (Semiformula.Evalm M e id) φ.pi.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.iff' {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence n} (h : ProperOn M φ) (e : Fin n → M) : M ⊧/e (pi φ).val ↔ M ⊧/e (val φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.iff' {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} {φ : HierarchySymbol.Semiformula M n { Γ := Dlt, rank := m }} (h : ProperWithParamOn M φ) (e : Fin n → M) : (Semiformula.Evalm M e id) φ.pi.val ↔ (Semiformula.Evalm M e id) φ.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProvablyProperOn.ofProperOn {n : ℕ} (T : Theory ℒₒᵣ) {m : ℕ} [𝐄𝐐 wkn T] {φ : { Γ := Dlt, rank := m }.Semisentence n} (h : ∀ (M : Type w) [inst : ORingStruc M] [M ⊧ₘ* T], ProperOn M φ) : ProvablyProperOn φ T

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProvablyProperOn.properOn {n : ℕ} {T : Theory ℒₒᵣ} {m : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence n} (h : ProvablyProperOn φ T) (M : Type w) [ORingStruc M] [M ⊧ₘ* T] : ProperOn M φ

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew {ξ₁ : Type u_3} {n₁ : ℕ} {ξ₂ : Type u_4} {n₂ : ℕ} (ω : Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂) {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ₁ n₁ Γ → HierarchySymbol.Semiformula ξ₂ n₂ Γ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω (φ.mkDelta ψ) = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω φ).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω ψ)

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_rew {ξ₁ : Type u_3} {n₁ : ℕ} {ξ₂ : Type u_4} {n₂ : ℕ} (ω : Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂) {Γ : HierarchySymbol} (φ : HierarchySymbol.Semiformula ξ₁ n₁ Γ) : (rew ω φ).val = (Rewriting.app ω) φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.rew {M : Type u_2} [ORingStruc M] {m n₁ n₂ : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence n₁} (h : ProperOn M φ) (ω : Rew ℒₒᵣ Empty n₁ Empty n₂) : ProperOn M (Semiformula.rew ω φ)

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.rew' {M : Type u_2} [ORingStruc M] {m n₁ n₂ : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence n₁} (h : ProperOn M φ) (ω : Rew ℒₒᵣ Empty n₁ M n₂) : ProperWithParamOn M (Semiformula.rew ω φ)

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.rew {M : Type u_2} [ORingStruc M] {m n₁ n₂ : ℕ} {φ : HierarchySymbol.Semiformula M n₁ { Γ := Dlt, rank := m }} (h : ProperWithParamOn M φ) (f : Fin n₁ → Semiterm ℒₒᵣ M n₂) : ProperWithParamOn M (Semiformula.rew (Rew.substs f) φ)

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.emb {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ hp).emb = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi ((LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) φ) ⋯
• (φ.mkDelta ψ).emb = φ.emb.mkDelta ψ.emb

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_emb {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (φ : HierarchySymbol.Semiformula ξ n Γ) : φ.emb.val = (Semiformula.lMap Language.oringEmb) φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_emb {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : φ.emb.pi = φ.pi.emb

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_emb {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : φ.emb.sigma = φ.sigma.emb

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.emb_proper {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} (φ : { Γ := Dlt, rank := m }.Semisentence n) : ProperOn M (emb φ) ↔ ProperOn M φ

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.emb_properWithParam {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} (φ : HierarchySymbol.Semiformula M n { Γ := Dlt, rank := m }) : ProperWithParamOn M φ.emb ↔ ProperWithParamOn M φ

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.extd {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ a).extd = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi ((LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) φ) ⋯
• (φ.mkDelta a).extd = φ.extd.mkDelta a.extd

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.eval_extd_iff {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} {M : Type u_2} [ORingStruc M] {e : Fin n → M} {ε : ξ → M} {φ : HierarchySymbol.Semiformula ξ n Γ} : (Semiformula.Evalm M e ε) φ.extd.val ↔ (Semiformula.Evalm M e ε) φ.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.extd {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence n} (h : ProperOn M φ) : ProperOn M (Semiformula.extd φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.extd {n : ℕ} {M : Type u_2} [ORingStruc M] {m : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence n} (h : ProperOn M φ) : ProperOn M (Semiformula.extd φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_extd_val {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) : φ.extd.val = (Semiformula.lMap Language.oringEmb) φ.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_extd_val {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : φ.extd.val = (Semiformula.lMap Language.oringEmb) φ.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigmaZero {ξ : Type u_1} {k : ℕ} {Γ : SigmaPiDelta} (φ : HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := 0 }) : Hierarchy Sg 0 φ.val

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ofZero {ξ : Type u_1} {k : ℕ} {Γ' : SigmaPiDelta} (φ : HierarchySymbol.Semiformula ξ k { Γ := Γ', rank := 0 }) (Γ : HierarchySymbol) : HierarchySymbol.Semiformula ξ k Γ

Imported declaration from the Incompleteness formalization.

Equations

• φ.ofZero { Γ := LO.SigmaPiDelta.sigma, rank := rank } = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma φ.val ⋯
• φ.ofZero { Γ := LO.SigmaPiDelta.pi, rank := rank } = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ.val ⋯
• φ.ofZero { Γ := LO.SigmaPiDelta.delta, rank := rank } = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma φ.val ⋯).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ.val ⋯)

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ofDeltaOne {ξ : Type u_1} {k : ℕ} (φ : HierarchySymbol.Semiformula ξ k Dlt1) (Γ : SigmaPiDelta) (m : ℕ) : HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := m + 1 }

Imported declaration from the Incompleteness formalization.

Equations

• φ.ofDeltaOne LO.SigmaPiDelta.sigma x✝ = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma φ.sigma.val ⋯
• φ.ofDeltaOne LO.SigmaPiDelta.pi x✝ = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ.pi.val ⋯
• φ.ofDeltaOne LO.SigmaPiDelta.delta x✝ = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma φ.sigma.val ⋯).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi φ.pi.val ⋯)

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ofZero_val {ξ : Type u_1} {n : ℕ} {Γ' : SigmaPiDelta} (φ : HierarchySymbol.Semiformula ξ n { Γ := Γ', rank := 0 }) (Γ : HierarchySymbol) : (φ.ofZero Γ).val = φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.of_zero {M : Type u_2} [ORingStruc M] {Γ' : SigmaPiDelta} {k : ℕ} (φ : { Γ := Γ', rank := 0 }.Semisentence k) (m : ℕ) : ProperOn M (ofZero φ { Γ := Dlt, rank := m })

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.of_zero {M : Type u_2} [ORingStruc M] {Γ' : SigmaPiDelta} {k : ℕ} (φ : HierarchySymbol.Semiformula M k { Γ := Γ', rank := 0 }) (m : ℕ) : ProperWithParamOn M (φ.ofZero { Γ := Dlt, rank := m })

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.verum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.verum = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma ⊤ ⋯
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.verum = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi ⊤ ⋯
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.verum = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma ⊤ ⋯).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi ⊤ ⋯)

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.falsum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.falsum = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma ⊥ ⋯
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.falsum = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi ⊥ ⋯
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.falsum = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma ⊥ ⋯).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi ⊥ ⋯)

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.and {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• φ.and ψ = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (φ.val ⋏ ψ.val) ⋯
• φ.and ψ = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi (φ.val ⋏ ψ.val) ⋯
• φ.and ψ = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (φ.sigma.val ⋏ ψ.sigma.val) ⋯).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi (φ.pi.val ⋏ ψ.pi.val) ⋯)

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.or {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• φ.or ψ = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (φ.val ⋎ ψ.val) ⋯
• φ.or ψ = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi (φ.val ⋎ ψ.val) ⋯
• φ.or ψ = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (φ.sigma.val ⋎ ψ.sigma.val) ⋯).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi (φ.pi.val ⋎ ψ.pi.val) ⋯)

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.negSigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }

Imported declaration from the Incompleteness formalization.

Equations

• φ.negSigma = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi (∼φ.val) ⋯

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.negPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }

Imported declaration from the Incompleteness formalization.

Equations

• φ.negPi = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (∼φ.val) ⋯

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.negDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }

Imported declaration from the Incompleteness formalization.

Equations

• φ.negDelta = φ.pi.negPi.mkDelta φ.sigma.negSigma

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ball {ξ : Type u_1} {n : ℕ} (t : Semiterm ℒₒᵣ ξ n) {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.bex {ξ : Type u_1} {n : ℕ} (t : Semiterm ℒₒᵣ ξ n) {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.all {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := Pg, rank := m + 1 }) : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m + 1 }

Imported declaration from the Incompleteness formalization.

Equations

• φ.all = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi (∀' φ.val) ⋯

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ex {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := Sg, rank := m + 1 }) : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m + 1 }

Imported declaration from the Incompleteness formalization.

Equations

• φ.ex = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (∃' φ.val) ⋯

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTop {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Top (HierarchySymbol.Semiformula ξ n Γ)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTop = { top := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.verum }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instBot {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Bot (HierarchySymbol.Semiformula ξ n Γ)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instBot = { bot := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.falsum }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instWedge {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Wedge (HierarchySymbol.Semiformula ξ n Γ)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instWedge = { wedge := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.and }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instVee {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Vee (HierarchySymbol.Semiformula ξ n Γ)

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instVee = { vee := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.or }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta {ξ : Type u_1} {n m : ℕ} : Tilde (HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m })

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta = { tilde := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.negDelta }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instLogicalConnectiveMkDeltaSigmaPiDelta {ξ : Type u_1} {n m : ℕ} : LogicalConnective (HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m })

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instExQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} : ExQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m + 1 }

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instExQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat = { ex := fun {n : ℕ} => LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ex }

@[implicit_reducible]

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} : UnivQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m + 1 }

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat = { univ := fun {n : ℕ} => LO.FirstOrder.Arith.HierarchySymbol.Semiformula.all }

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.substSigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ 1 { Γ := Sg, rank := m + 1 }) (F : HierarchySymbol.Semiformula ξ (n + 1) { Γ := Sg, rank := m + 1 }) : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m + 1 }

Imported declaration from the Incompleteness formalization.

Equations

• φ.substSigma F = (F ⋏ LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]) φ).ex

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_verum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : ⊤.val = ⊤

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_verum {ξ : Type u_1} {n m : ℕ} : ⊤.sigma = ⊤

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_verum {ξ : Type u_1} {n m : ℕ} : ⊤.pi = ⊤

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_falsum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : ⊥.val = ⊥

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_falsum {ξ : Type u_1} {n m : ℕ} : ⊥.sigma = ⊥

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_falsum {ξ : Type u_1} {n m : ℕ} : ⊥.pi = ⊥

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_and {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (φ ψ : HierarchySymbol.Semiformula ξ n Γ) : (φ ⋏ ψ).val = φ.val ⋏ ψ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_and {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : (φ ⋏ ψ).sigma = φ.sigma ⋏ ψ.sigma

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_and {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : (φ ⋏ ψ).pi = φ.pi ⋏ ψ.pi

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_or {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (φ ψ : HierarchySymbol.Semiformula ξ n Γ) : (φ ⋎ ψ).val = φ.val ⋎ ψ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_or {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : (φ ⋎ ψ).sigma = φ.sigma ⋎ ψ.sigma

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi_or {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : (φ ⋎ ψ).pi = φ.pi ⋎ ψ.pi

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negSigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Sg, rank := m }) : φ.negSigma.val = ∼φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Pg, rank := m }) : φ.negPi.val = ∼φ.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : (∼φ).val = ∼φ.pi.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_negDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : (∼φ).sigma = φ.pi.negPi

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_negPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Dlt, rank := m }) : (∼φ).pi = φ.sigma.negSigma

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_ball {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (t : Semiterm ℒₒᵣ ξ n) (φ : HierarchySymbol.Semiformula ξ (n + 1) Γ) : (ball t φ).val = (“(∀[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ.val)”)

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_bex {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (t : Semiterm ℒₒᵣ ξ n) (φ : HierarchySymbol.Semiformula ξ (n + 1) Γ) : (bex t φ).val = (“(∃[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ.val)”)

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_exSigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := Sg, rank := m + 1 }) : φ.ex.val = ∃' φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_allPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := Pg, rank := m + 1 }) : φ.all.val = ∀' φ.val

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.verum {M : Type u_2} [ORingStruc M] {m k : ℕ} : ProperOn M ⊤

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.falsum {M : Type u_2} [ORingStruc M] {m k : ℕ} : ProperOn M ⊥

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.and {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ ψ : { Γ := Dlt, rank := m }.Semisentence k} (hp : ProperOn M φ) (hq : ProperOn M ψ) : ProperOn M (φ ⋏ ψ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.or {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ ψ : { Γ := Dlt, rank := m }.Semisentence k} (hp : ProperOn M φ) (hq : ProperOn M ψ) : ProperOn M (φ ⋎ ψ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.neg {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence k} (hp : ProperOn M φ) : ProperOn M (∼φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.eval_neg {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ : { Γ := Dlt, rank := m }.Semisentence k} (hp : ProperOn M φ) (e : Fin k → M) : M ⊧/e (val (∼φ)) ↔ ¬M ⊧/e (val φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.ball {M : Type u_2} [ORingStruc M] {m k : ℕ} {t : Semiterm ℒₒᵣ Empty k} {φ : { Γ := Dlt, rank := m + 1 }.Semisentence (k + 1)} (hp : ProperOn M φ) : ProperOn M (Semiformula.ball t φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.bex {M : Type u_2} [ORingStruc M] {m k : ℕ} {t : Semiterm ℒₒᵣ Empty k} {φ : { Γ := Dlt, rank := m + 1 }.Semisentence (k + 1)} (hp : ProperOn M φ) : ProperOn M (Semiformula.bex t φ)

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.verum {M : Type u_2} [ORingStruc M] {m k : ℕ} : ProperWithParamOn M ⊤

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.falsum {M : Type u_2} [ORingStruc M] {m k : ℕ} : ProperWithParamOn M ⊥

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.and {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ ψ : HierarchySymbol.Semiformula M k { Γ := Dlt, rank := m }} (hp : ProperWithParamOn M φ) (hq : ProperWithParamOn M ψ) : ProperWithParamOn M (φ ⋏ ψ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.or {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ ψ : HierarchySymbol.Semiformula M k { Γ := Dlt, rank := m }} (hp : ProperWithParamOn M φ) (hq : ProperWithParamOn M ψ) : ProperWithParamOn M (φ ⋎ ψ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.neg {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ : HierarchySymbol.Semiformula M k { Γ := Dlt, rank := m }} (hp : ProperWithParamOn M φ) : ProperWithParamOn M (∼φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.eval_neg {M : Type u_2} [ORingStruc M] {m k : ℕ} {φ : HierarchySymbol.Semiformula M k { Γ := Dlt, rank := m }} (hp : ProperWithParamOn M φ) (e : Fin k → M) : (Semiformula.Evalm M e id) (∼φ).val ↔ ¬(Semiformula.Evalm M e id) φ.val

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.ball {M : Type u_2} [ORingStruc M] {m k : ℕ} {t : Semiterm ℒₒᵣ M k} {φ : HierarchySymbol.Semiformula M (k + 1) { Γ := Dlt, rank := m }} (hp : ProperWithParamOn M φ) : ProperWithParamOn M (Semiformula.ball t φ)

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.bex {M : Type u_2} [ORingStruc M] {m k : ℕ} {t : Semiterm ℒₒᵣ M k} {φ : HierarchySymbol.Semiformula M (k + 1) { Γ := Dlt, rank := m }} (hp : ProperWithParamOn M φ) : ProperWithParamOn M (Semiformula.bex t φ)

def LO.FirstOrder.Arith.HierarchySymbol.Semiformula.graphDelta {ξ : Type u_1} {m k : ℕ} (φ : HierarchySymbol.Semiformula ξ (k + 1) { Γ := Sg, rank := m }) : HierarchySymbol.Semiformula ξ (k + 1) { Γ := Dlt, rank := m }

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• φ_2.graphDelta = φ_2.ofZero { Γ := Dlt, rank := 0 }

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.graphDelta_val {ξ : Type u_1} {m k : ℕ} (φ : HierarchySymbol.Semiformula ξ (k + 1) { Γ := Sg, rank := m }) : φ.graphDelta.val = φ.val