Documentation

Foundation.FirstOrder.Arithmetic.Definability.Hierarchy

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 ArithmeticSemiformula ξ n which is 𝚺-[m].
𝚷-[m].Semiformula ξ n is a ArithmeticSemiformula ξ 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.Arithmetic.HierarchySymbol :

Γ : SigmaPiDelta
rank : ℕ

Instances For

def LO.FirstOrder.Arithmetic.«term_-[_]» :

Lean.TrailingParserDescr

Equations

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

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.sigmaZero :

HierarchySymbol

Equations

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

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.piZero :

HierarchySymbol

Equations

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

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.deltaZero :

HierarchySymbol

Equations

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

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.sigmaOne :

HierarchySymbol

Equations

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

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.piOne :

HierarchySymbol

Equations

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

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.deltaOne :

HierarchySymbol

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.«term𝚺₀» :

Lean.ParserDescr

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.«term𝚷₀» :

Lean.ParserDescr

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.«term𝚫₀» :

Lean.ParserDescr

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.«term𝚺₁» :

Lean.ParserDescr

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.«term𝚷₁» :

Lean.ParserDescr

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.«term𝚫₁» :

Lean.ParserDescr

Equations

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

Instances For

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

HierarchySymbol → Type u_1

mkSigma {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (hφ : Hierarchy 𝚺 m φ := by simp) : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }
mkPi {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (hφ : Hierarchy 𝚷 m φ := by simp) : HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }
mkDelta {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }

Instances For

@[reducible, inline]

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

Equations

Γ.Semisentence n = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula Empty n Γ

Instances For

@[reducible, inline]

abbrev LO.FirstOrder.Arithmetic.HierarchySymbol.Sentence (Γ : HierarchySymbol) :

Equations

Γ.Sentence = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula Empty 0 Γ

Instances For

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} :

HierarchySymbol.Semiformula ξ n Γ → ArithmeticSemiformula ξ n

Equations

↑(LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma φ hφ) = φ
↑(LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi φ hφ) = φ
↑(φ.mkDelta a) = ↑φ

Instances For

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_mkSigma {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (hp : Hierarchy 𝚺 m φ) :

↑(mkSigma φ hp) = φ

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_mkPi {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (hp : Hierarchy 𝚷 m φ) :

↑(mkPi φ hp) = φ

@[simp]

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

↑(φ.mkDelta ψ) = ↑φ

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaZeroArithmeticSemisentence {n : ℕ} :

Coe (𝚺₀.Semisentence n) (ArithmeticSemisentence n)

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaZeroArithmeticSemisentence = { coe := LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentencePiZeroArithmeticSemisentence {n : ℕ} :

Coe (𝚷₀.Semisentence n) (ArithmeticSemisentence n)

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentencePiZeroArithmeticSemisentence = { coe := LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaZeroArithmeticSemisentence {n : ℕ} :

Coe (𝚫₀.Semisentence n) (ArithmeticSemisentence n)

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaZeroArithmeticSemisentence = { coe := LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaOneArithmeticSemisentence {n : ℕ} :

Coe (𝚺₁.Semisentence n) (ArithmeticSemisentence n)

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaOneArithmeticSemisentence = { coe := LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentencePiOneArithmeticSemisentence {n : ℕ} :

Coe (𝚷₁.Semisentence n) (ArithmeticSemisentence n)

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentencePiOneArithmeticSemisentence = { coe := LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaOneArithmeticSemisentence {n : ℕ} :

Coe (𝚫₁.Semisentence n) (ArithmeticSemisentence n)

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaOneArithmeticSemisentence = { coe := LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val }

@[simp]

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

Hierarchy 𝚺 m ↑φ

@[simp]

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

Hierarchy 𝚷 m ↑φ

@[simp]

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

Hierarchy Γ m ↑φ

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma {ξ : Type u_1} {n m : ℕ} :

HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }

Equations

(φ.mkDelta a).sigma = φ

Instances For

@[simp]

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

(φ.mkDelta ψ).sigma = φ

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi {ξ : Type u_1} {n m : ℕ} :

HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }

Equations

(φ.mkDelta a).pi = a

Instances For

@[simp]

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

(φ.mkDelta ψ).pi = ψ

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

↑φ.sigma = ↑φ

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPolarity {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (Γ : Polarity) :

Hierarchy Γ m φ → HierarchySymbol.Semiformula ξ n { Γ := Γ.coe, rank := m }

Equations

Instances For

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_mkPolarity {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) {Γ : Polarity} (h : Hierarchy Γ m φ) :

↑(mkPolarity φ Γ h) = φ

@[simp]

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

Hierarchy 𝚺 m ↑φ

@[simp]

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

Hierarchy 𝚷 m ↑φ

@[simp]

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

Hierarchy Γ' m ↑φ

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

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn {n : ℕ} (M : Type u_2) [ORingStructure M] {m : ℕ} (φ : HierarchySymbol.Semiformula M n { Γ := 𝚫, rank := m }) :

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn M φ = ∀ (e : Fin n → M), (LO.FirstOrder.Semiformula.Eval e id) ↑φ.sigma ↔ (LO.FirstOrder.Semiformula.Eval e id) ↑φ.pi

Instances For

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn {n m : ℕ} (φ : { Γ := 𝚫, rank := m }.Semisentence n) (T : ArithmeticTheory) :

Equations

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

Instances For

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.iff {n : ℕ} {M : Type u_2} [ORingStructure M] {m : ℕ} {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : ProperOn M φ) (e : Fin n → M) :

(Semiformula.Evalb e) ↑(sigma φ) ↔ (Semiformula.Evalb e) ↑(pi φ)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.iff {n : ℕ} {M : Type u_2} [ORingStructure M] {m : ℕ} {φ : HierarchySymbol.Semiformula M n { Γ := 𝚫, rank := m }} (h : ProperWithParamOn M φ) (e : Fin n → M) :

(Semiformula.Eval e id) ↑φ.sigma ↔ (Semiformula.Eval e id) ↑φ.pi

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.iff' {n : ℕ} {M : Type u_2} [ORingStructure M] {m : ℕ} {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : ProperOn M φ) (e : Fin n → M) :

(Semiformula.Evalb e) ↑(pi φ) ↔ (Semiformula.Evalb e) ↑φ

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.iff' {n : ℕ} {M : Type u_2} [ORingStructure M] {m : ℕ} {φ : HierarchySymbol.Semiformula M n { Γ := 𝚫, rank := m }} (h : ProperWithParamOn M φ) (e : Fin n → M) :

(Semiformula.Eval e id) ↑φ.pi ↔ (Semiformula.Eval e id) ↑φ

inductive LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn' {n : ℕ} (T : ArithmeticTheory) {Γ : HierarchySymbol} {n✝ : ℕ} (φ : Γ.Semisentence n✝) :

sigma {n : ℕ} {T : ArithmeticTheory} {m : ℕ} (φ : { Γ := 𝚺, rank := m }.Semisentence n) : ProvablyProperOn' T φ
pi {n : ℕ} {T : ArithmeticTheory} {m : ℕ} (φ : { Γ := 𝚷, rank := m }.Semisentence n) : ProvablyProperOn' T φ
delta {n : ℕ} {T : ArithmeticTheory} {m : ℕ} (φ : { Γ := 𝚫, rank := m }.Semisentence n) : ProvablyProperOn φ T → ProvablyProperOn' T φ

Instances For

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn.ofProperOn {n : ℕ} (T : ArithmeticTheory) {m : ℕ} [𝗘𝗤 ℒₒᵣ ⪯ T] {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : ∀ (M : Type w) [inst : ORingStructure M] [M↓[ℒₒᵣ ] ⊧* T], ProperOn M φ) :

ProvablyProperOn φ T

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn.properOn {n : ℕ} {T : ArithmeticTheory} {m : ℕ} {φ : { Γ := 𝚫, rank := m }.Semisentence n} (h : ProvablyProperOn φ T) (M : Type w) [ORingStructure M] [M↓[ℒₒᵣ ] ⊧* T] :

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

HierarchySymbol.Semiformula ξ₁ n₁ Γ → HierarchySymbol.Semiformula ξ₂ n₂ Γ

Equations

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

Instances For

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_rew {ξ₁ : Type u_3} {n₁ : ℕ} {ξ₂ : Type u_4} {n₂ : ℕ} (ω : Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂) {Γ : HierarchySymbol} (φ : HierarchySymbol.Semiformula ξ₁ n₁ Γ) :

↑(rew ω φ) = (Rewriting.app ω) ↑φ

@[simp]

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

ProperOn M (Semiformula.rew ω φ)

@[simp]

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

ProperWithParamOn M (Semiformula.rew ω φ)

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.rew {M : Type u_2} [ORingStructure M] {m n₁ n₂ : ℕ} {φ : HierarchySymbol.Semiformula M n₁ { Γ := 𝚫, rank := m }} (h : ProperWithParamOn M φ) (f : Fin n₁ → ArithmeticSemiterm M n₂) :

ProperWithParamOn M (Semiformula.rew (Rew.subst f) φ)

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

Hierarchy 𝚺 0 ↑φ

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

HierarchySymbol.Semiformula ξ k Γ

Equations

One or more equations did not get rendered due to their size.
φ.ofZero { Γ := LO.SigmaPiDelta.sigma, rank := rank } = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma ↑φ ⋯
φ.ofZero { Γ := LO.SigmaPiDelta.pi, rank := rank } = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi ↑φ ⋯

Instances For

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ofDeltaOne {ξ : Type u_1} {k : ℕ} (φ : HierarchySymbol.Semiformula ξ k 𝚫₁) (Γ : SigmaPiDelta) (m : ℕ) :

HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := m + 1 }

Equations

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

Instances For

@[simp]

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

↑(φ.ofZero Γ) = ↑φ

@[simp]

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

ProperOn M (ofZero φ { Γ := 𝚫, rank := m })

@[simp]

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

ProperWithParamOn M (φ.ofZero { Γ := 𝚫, rank := m })

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

HierarchySymbol.Semiformula ξ n Γ

Equations

One or more equations did not get rendered due to their size.
LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.verum = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma ⊤ ⋯
LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.verum = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi ⊤ ⋯

Instances For

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

HierarchySymbol.Semiformula ξ n Γ

Equations

One or more equations did not get rendered due to their size.
LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.falsum = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma ⊥ ⋯
LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.falsum = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi ⊥ ⋯

Instances For

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

HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

φ.and ψ = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑φ ⋏ ↑ψ) ⋯
φ.and ψ = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (↑φ ⋏ ↑ψ) ⋯
φ.and ψ = (LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑φ.sigma ⋏ ↑ψ.sigma) ⋯).mkDelta (LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (↑φ.pi ⋏ ↑ψ.pi) ⋯)

Instances For

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

HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

φ.or ψ = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑φ ⋎ ↑ψ) ⋯
φ.or ψ = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (↑φ ⋎ ↑ψ) ⋯
φ.or ψ = (LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑φ.sigma ⋎ ↑ψ.sigma) ⋯).mkDelta (LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (↑φ.pi ⋎ ↑ψ.pi) ⋯)

Instances For

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

HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m }

Equations

φ.negSigma = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (∼↑φ) ⋯

Instances For

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

HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }

Equations

φ.negPi = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (∼↑φ) ⋯

Instances For

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

HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m }

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ball {ξ : Type u_1} {n : ℕ} (t : ArithmeticSemiterm ξ n) {Γ : HierarchySymbol} :

HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

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

Instances For

def LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.bexs {ξ : Type u_1} {n : ℕ} (t : ArithmeticSemiterm ξ n) {Γ : HierarchySymbol} :

HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

Equations

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

Instances For

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

HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m + 1 }

Equations

φ.all = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (∀¹ ↑φ) ⋯

Instances For

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

HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m + 1 }

Equations

φ.exs = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (∃¹ ↑φ) ⋯

Instances For

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instTop {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} :

Top (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instBot {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} :

Bot (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instWedge {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} :

Wedge (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instVee {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} :

Vee (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta {ξ : Type u_1} {n m : ℕ} :

Tilde (HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m })

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instLogicalConnectiveMkDeltaSigmaPiDelta {ξ : Type u_1} {n m : ℕ} :

LogicalConnective (HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m })

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instExsQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} :

ExsQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m + 1 }

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instExsQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat = { exs := fun {n : ℕ} => LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.exs }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} :

UnivQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m + 1 }

Equations

LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat = { all := fun {n : ℕ} => LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.all }

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

HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m + 1 }

Equations

φ.substSigma F = (F ⋏ LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.rew (LO.FirstOrder.Rew.subst ![LO.FirstOrder.Semiterm.bvar 0]) φ).exs

Instances For

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_verum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} :

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_verum {ξ : Type u_1} {n m : ℕ} :

⊤.sigma = ⊤

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_verum {ξ : Type u_1} {n m : ℕ} :

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_falsum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} :

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_falsum {ξ : Type u_1} {n m : ℕ} :

⊥.sigma = ⊥

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_falsum {ξ : Type u_1} {n m : ℕ} :

@[simp]

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

↑(φ ⋏ ψ) = ↑φ ⋏ ↑ψ

@[simp]

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

(φ ⋏ ψ).sigma = φ.sigma ⋏ ψ.sigma

@[simp]

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

(φ ⋏ ψ).pi = φ.pi ⋏ ψ.pi

@[simp]

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

↑(φ ⋎ ψ) = ↑φ ⋎ ↑ψ

@[simp]

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

(φ ⋎ ψ).sigma = φ.sigma ⋎ ψ.sigma

@[simp]

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

(φ ⋎ ψ).pi = φ.pi ⋎ ψ.pi

@[simp]

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

↑φ.negSigma = ∼↑φ

@[simp]

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

↑φ.negPi = ∼↑φ

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

↑(∼φ) = ∼↑φ.pi

@[simp]

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

(∼φ).sigma = φ.pi.negPi

@[simp]

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

(∼φ).pi = φ.sigma.negSigma

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_ball {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (t : ArithmeticSemiterm ξ n) (φ : HierarchySymbol.Semiformula ξ (n + 1) Γ) :

↑(ball t φ) = (“(∀¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !↑φ)”)

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_bexs {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (t : ArithmeticSemiterm ξ n) (φ : HierarchySymbol.Semiformula ξ (n + 1) Γ) :

↑(bexs t φ) = (“(∃¹[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !↑φ)”)

@[simp]

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

↑φ.exs = ∃¹ ↑φ

@[simp]

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

↑φ.all = ∀¹ ↑φ

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.verum {M : Type u_2} [ORingStructure M] {m k : ℕ} :

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.falsum {M : Type u_2} [ORingStructure M] {m k : ℕ} :

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

ProperOn M (φ ⋏ ψ)

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

ProperOn M (φ ⋎ ψ)

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

ProperOn M (∼φ)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.eval_neg {M : Type u_2} [ORingStructure M] {m k : ℕ} {φ : { Γ := 𝚫, rank := m }.Semisentence k} (hp : ProperOn M φ) (e : Fin k → M) :

(Semiformula.Evalb e) ↑(∼φ) ↔ ¬(Semiformula.Evalb e) ↑φ

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.ball {M : Type u_2} [ORingStructure M] {m k : ℕ} {t : ArithmeticSemiterm Empty k} {φ : { Γ := 𝚫, rank := m + 1 }.Semisentence (k + 1)} (hp : ProperOn M φ) :

ProperOn M (Semiformula.ball t φ)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.bexs {M : Type u_2} [ORingStructure M] {m k : ℕ} {t : ArithmeticSemiterm Empty k} {φ : { Γ := 𝚫, rank := m + 1 }.Semisentence (k + 1)} (hp : ProperOn M φ) :

ProperOn M (Semiformula.bexs t φ)

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.verum {M : Type u_2} [ORingStructure M] {m k : ℕ} :

ProperWithParamOn M ⊤

@[simp]

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.falsum {M : Type u_2} [ORingStructure M] {m k : ℕ} :

ProperWithParamOn M ⊥

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

ProperWithParamOn M (φ ⋏ ψ)

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

ProperWithParamOn M (φ ⋎ ψ)

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

ProperWithParamOn M (∼φ)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.eval_neg {M : Type u_2} [ORingStructure M] {m k : ℕ} {φ : HierarchySymbol.Semiformula M k { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) (e : Fin k → M) :

(Semiformula.Eval e id) ↑(∼φ) ↔ ¬(Semiformula.Eval e id) ↑φ

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.ball {M : Type u_2} [ORingStructure M] {m k : ℕ} {t : ArithmeticSemiterm M k} {φ : HierarchySymbol.Semiformula M (k + 1) { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) :

ProperWithParamOn M (Semiformula.ball t φ)

theorem LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.bexs {M : Type u_2} [ORingStructure M] {m k : ℕ} {t : ArithmeticSemiterm M k} {φ : HierarchySymbol.Semiformula M (k + 1) { Γ := 𝚫, rank := m }} (hp : ProperWithParamOn M φ) :

ProperWithParamOn M (Semiformula.bexs t φ)

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

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 }

Instances For

@[simp]

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

↑φ.graphDelta = ↑φ