Arithmetical Formula Sorted by Arithmetical Hierarchy

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

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

structure LO.FirstOrder.Arith.HierarchySymbol : Type

• Γ : LO.SigmaPiDelta
• rank : ℕ

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

Equations

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

@[reducible, inline]

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

Equations

• 𝚺₀ = { Γ := 𝚺, rank := 0 }

@[reducible, inline]

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

Equations

• 𝚷₀ = { Γ := 𝚷, rank := 0 }

@[reducible, inline]

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

Equations

• 𝚫₀ = { Γ := 𝚫, rank := 0 }

@[reducible, inline]

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

Equations

• 𝚺₁ = { Γ := 𝚺, rank := 1 }

@[reducible, inline]

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

Equations

• 𝚷₁ = { Γ := 𝚷, rank := 1 }

@[reducible, inline]

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

Equations

• 𝚫₁ = { Γ := 𝚫, rank := 1 }

def LO.FirstOrder.Arith.«term𝚺₀» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arith.«term𝚺₀» = Lean.ParserDescr.node `LO.FirstOrder.Arith.«term𝚺₀» 1024 (Lean.ParserDescr.symbol "𝚺₀")

def LO.FirstOrder.Arith.«term𝚷₀» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arith.«term𝚷₀» = Lean.ParserDescr.node `LO.FirstOrder.Arith.«term𝚷₀» 1024 (Lean.ParserDescr.symbol "𝚷₀")

def LO.FirstOrder.Arith.«term𝚫₀» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arith.«term𝚫₀» = Lean.ParserDescr.node `LO.FirstOrder.Arith.«term𝚫₀» 1024 (Lean.ParserDescr.symbol "𝚫₀")

def LO.FirstOrder.Arith.«term𝚺₁» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arith.«term𝚺₁» = Lean.ParserDescr.node `LO.FirstOrder.Arith.«term𝚺₁» 1024 (Lean.ParserDescr.symbol "𝚺₁")

def LO.FirstOrder.Arith.«term𝚷₁» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arith.«term𝚷₁» = Lean.ParserDescr.node `LO.FirstOrder.Arith.«term𝚷₁» 1024 (Lean.ParserDescr.symbol "𝚷₁")

def LO.FirstOrder.Arith.«term𝚫₁» : Lean.ParserDescr

Equations

• LO.FirstOrder.Arith.«term𝚫₁» = Lean.ParserDescr.node `LO.FirstOrder.Arith.«term𝚫₁» 1024 (Lean.ParserDescr.symbol "𝚫₁")

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

• mkSigma: {ξ : Type u_1} → {n m : ℕ} → (φ : LO.FirstOrder.Semiformula ℒₒᵣ ξ n) → LO.FirstOrder.Arith.Hierarchy 𝚺 m φ → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }
• mkPi: {ξ : Type u_1} → {n m : ℕ} → (φ : LO.FirstOrder.Semiformula ℒₒᵣ ξ n) → LO.FirstOrder.Arith.Hierarchy 𝚷 m φ → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }
• mkDelta: {ξ : Type u_1} → {n m : ℕ} → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m } → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m } → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

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 : ℕ} (φ : LO.FirstOrder.Semiformula ℒₒᵣ ξ n) (hp : LO.FirstOrder.Arith.Hierarchy 𝚺 m φ) : (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma φ hp).val = φ

@[simp]

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

@[simp]

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

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaZeroSemisentenceORing {n : ℕ} : Coe (𝚺₀.Semisentence n) (LO.FirstOrder.Semisentence ℒₒᵣ n)

Equations

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

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiZeroSemisentenceORing {n : ℕ} : Coe (𝚷₀.Semisentence n) (LO.FirstOrder.Semisentence ℒₒᵣ n)

Equations

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

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaZeroSemisentenceORing {n : ℕ} : Coe (𝚫₀.Semisentence n) (LO.FirstOrder.Semisentence ℒₒᵣ n)

Equations

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

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaOneSemisentenceORing {n : ℕ} : Coe (𝚺₁.Semisentence n) (LO.FirstOrder.Semisentence ℒₒᵣ n)

Equations

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

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiOneSemisentenceORing {n : ℕ} : Coe (𝚷₁.Semisentence n) (LO.FirstOrder.Semisentence ℒₒᵣ n)

Equations

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

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaOneSemisentenceORing {n : ℕ} : Coe (𝚫₁.Semisentence n) (LO.FirstOrder.Semisentence ℒₒᵣ n)

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• (φ.mkDelta a).sigma = φ

@[simp]

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

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

Equations

• (φ.mkDelta a).pi = a

@[simp]

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

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

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

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 : ℕ} (φ : LO.FirstOrder.Semiformula ℒₒᵣ ξ n) {Γ : LO.Polarity} (h : LO.FirstOrder.Arith.Hierarchy Γ m φ) : (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPolarity φ Γ h).val = φ

@[simp]

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

@[simp]

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

@[simp]

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

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

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) [LO.ORingStruc M] {m : ℕ} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula M n { Γ := 𝚫, rank := m }) : Prop

Equations

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

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

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} [LO.ORingStruc M] {m : ℕ} {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn M φ) (e : Fin n → M) : M ⊧/e (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma φ).val ↔ M ⊧/e (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.pi φ).val

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

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

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

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

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

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

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₂ : ℕ} (ω : LO.FirstOrder.Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂) {Γ : LO.FirstOrder.Arith.HierarchySymbol} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ₁ n₁ Γ) : (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω φ).val = (LO.FirstOrder.Rewriting.app ω) φ.val

@[simp]

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

@[simp]

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

@[simp]

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

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

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 : ℕ} {Γ : LO.FirstOrder.Arith.HierarchySymbol} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ) : φ.emb.val = (LO.FirstOrder.Semiformula.lMap LO.FirstOrder.Language.oringEmb) φ.val

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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 : ℕ} {Γ : LO.FirstOrder.Arith.HierarchySymbol} {M : Type u_2} [LO.ORingStruc M] {e : Fin n → M} {ε : ξ → M} {φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ} : (LO.FirstOrder.Semiformula.Evalm M e ε) φ.extd.val ↔ (LO.FirstOrder.Semiformula.Evalm M e ε) φ.val

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

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

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

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

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

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

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 : ℕ} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ k 𝚫₁) (Γ : LO.SigmaPiDelta) (m : ℕ) : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := m + 1 }

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 : ℕ} {Γ' : LO.SigmaPiDelta} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := Γ', rank := 0 }) (Γ : LO.FirstOrder.Arith.HierarchySymbol) : (φ.ofZero Γ).val = φ.val

@[simp]

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

@[simp]

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

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

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 : ℕ} {Γ : LO.FirstOrder.Arith.HierarchySymbol} : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ

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 : ℕ} {Γ : LO.FirstOrder.Arith.HierarchySymbol} : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ

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 : ℕ} {Γ : LO.FirstOrder.Arith.HierarchySymbol} : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ

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 : ℕ} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }) : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }

Equations

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

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

Equations

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

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

Equations

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

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

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 : LO.FirstOrder.Semiterm ℒₒᵣ ξ n) {Γ : LO.FirstOrder.Arith.HierarchySymbol} : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ (n + 1) Γ → LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ

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 : ℕ} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚷, rank := m + 1 }) : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m + 1 }

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instLogicalConnectiveMkDeltaSigmaPiDelta = LO.LogicalConnective.mk

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

Equations

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

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} : LO.UnivQuantifier fun (n : ℕ) => LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, 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 : ℕ} (φ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ 1 { Γ := 𝚺, rank := m + 1 }) (F : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ (n + 1) { Γ := 𝚺, rank := m + 1 }) : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m + 1 }

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 : ℕ} {Γ : LO.FirstOrder.Arith.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 : ℕ} {Γ : LO.FirstOrder.Arith.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 : ℕ} {Γ : LO.FirstOrder.Arith.HierarchySymbol} (φ ψ : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n Γ) : (φ ⋏ ψ).val = φ.val ⋏ ψ.val

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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