Supporting results for pointwise provable equality.

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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol : Type

Data and laws for Hierarchy Symbol in FFL.FirstOrder.Arithmetic.

• Γ : SigmaPiDelta

  The Γ construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.

• rank : ℕ

  The rank construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term_-[_]» : Lean.TrailingParserDescr

The «term -[ ]» construction in FFL.FirstOrder.Arithmetic.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.sigmaZero : HierarchySymbol

The Σ₀ construction in Σ₀.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.piZero : HierarchySymbol

The Π₀ construction in Π₀.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.deltaZero : HierarchySymbol

The ∆₀ construction in ∆₀.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.sigmaOne : HierarchySymbol

The Σ₁ construction in Σ₁.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.piOne : HierarchySymbol

The Π₁ construction in Π₁.

Equations

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

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.deltaOne : HierarchySymbol

The ∆₁ construction in ∆₁.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΣ₀» : Lean.ParserDescr

The «termΣ₀» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΣ₀» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΣ₀» 1024 (Lean.ParserDescr.symbol "Σ₀")

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΠ₀» : Lean.ParserDescr

The «termΠ₀» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΠ₀» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΠ₀» 1024 (Lean.ParserDescr.symbol "Π₀")

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term∆₀» : Lean.ParserDescr

The «term∆₀» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term∆₀» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term∆₀» 1024 (Lean.ParserDescr.symbol "∆₀")

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΣ₁» : Lean.ParserDescr

The «termΣ₁» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΣ₁» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΣ₁» 1024 (Lean.ParserDescr.symbol "Σ₁")

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΠ₁» : Lean.ParserDescr

The «termΠ₁» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΠ₁» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«termΠ₁» 1024 (Lean.ParserDescr.symbol "Π₁")

def PointwiseComposition.FFL.FirstOrder.Arithmetic.«term∆₁» : Lean.ParserDescr

The «term∆₁» construction in FFL.FirstOrder.Arithmetic.

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.«term∆₁» = Lean.ParserDescr.node `PointwiseComposition.FFL.FirstOrder.Arithmetic.«term∆₁» 1024 (Lean.ParserDescr.symbol "∆₁")

inductive PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula (ξ : Type u_1) (n : ℕ) : HierarchySymbol → Type u_1

First-order formulas with separate bound and free variables.

• 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 }

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semisentence (Γ : HierarchySymbol) (n : ℕ) : Type

The Semisentence construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.

Equations

• Γ.Semisentence n = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula Empty n Γ

@[reducible, inline]

abbrev PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Sentence (Γ : HierarchySymbol) : Type

The Sentence construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.

Equations

• Γ.Sentence = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula Empty 0 Γ

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ → ArithmeticSemiformula ξ n

The val construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• ↑(PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma φ hφ) = φ
• ↑(PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi φ hφ) = φ
• ↑(φ.mkDelta a) = ↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_mkSigma {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (hp : Hierarchy Σ m φ) : ↑(mkSigma φ hp) = φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_mkPi {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (hp : Hierarchy Π m φ) : ↑(mkPi φ hp) = φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_mkDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }) : ↑(φ.mkDelta ψ) = ↑φ

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaZeroArithmeticSemisentence {n : ℕ} : Coe (Σ₀.Semisentence n) (ArithmeticSemisentence n)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentencePiZeroArithmeticSemisentence {n : ℕ} : Coe (Π₀.Semisentence n) (ArithmeticSemisentence n)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaZeroArithmeticSemisentence {n : ℕ} : Coe (∆₀.Semisentence n) (ArithmeticSemisentence n)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaOneArithmeticSemisentence {n : ℕ} : Coe (Σ₁.Semisentence n) (ArithmeticSemisentence n)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentencePiOneArithmeticSemisentence {n : ℕ} : Coe (Π₁.Semisentence n) (ArithmeticSemisentence n)

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaOneArithmeticSemisentence {n : ℕ} : Coe (∆₁.Semisentence n) (ArithmeticSemisentence n)

Equations

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_prop {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }) : Hierarchy Σ m ↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_prop {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }) : Hierarchy Π m ↑φ

@[simp]

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }

The sigma construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• (φ.mkDelta a).sigma = φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_mkDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }) : (φ.mkDelta ψ).sigma = φ

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi {ξ : Type u_1} {n m : ℕ} : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m } → HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }

The pi construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• (φ.mkDelta a).pi = a

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_mkDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }) (ψ : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }) : (φ.mkDelta ψ).pi = ψ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_sigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : ↑φ.sigma = ↑φ

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPolarity {ξ : Type u_1} {n m : ℕ} (φ : ArithmeticSemiformula ξ n) (Γ : Polarity) : Hierarchy Γ m φ → HierarchySymbol.Semiformula ξ n { Γ := Γ.coe, rank := m }

The mk Polarity construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.hierarchy_sigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }) : Hierarchy Σ m ↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.hierarchy_pi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }) : Hierarchy Π m ↑φ

@[simp]

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

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

The Proper On construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

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

The Proper With Param On construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn {n m : ℕ} (φ : { Γ := ∆, rank := m }.Semisentence n) (T : ArithmeticTheory) : Prop

The Provably Proper On construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn' {n : ℕ} (T : ArithmeticTheory) {Γ : HierarchySymbol} {n✝ : ℕ} (φ : Γ.Semisentence n✝) : Prop

Data and laws for Provably Proper On' in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProvablyProperOn.properOn {n : ℕ} {T : ArithmeticTheory} {m : ℕ} {φ : { Γ := ∆, rank := m }.Semisentence n} (h : ProvablyProperOn φ T) (M : Type w) [ORingStructure M] [M↓[ℒₒᵣ] ⊧* T] : ProperOn M φ

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

The rew construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigmaZero {ξ : Type u_1} {k : ℕ} {Γ : SigmaPiDelta} (φ : HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := 0 }) : Hierarchy Σ 0 ↑φ

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

The of Zero construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ofDeltaOne {ξ : Type u_1} {k : ℕ} (φ : HierarchySymbol.Semiformula ξ k ∆₁) (Γ : SigmaPiDelta) (m : ℕ) : HierarchySymbol.Semiformula ξ k { Γ := Γ, rank := m + 1 }

The of Delta One construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• One or more equations did not get rendered due to their size.
• φ.ofDeltaOne PointwiseComposition.FFL.SigmaPiDelta.sigma x✝ = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma ↑φ.sigma ⋯
• φ.ofDeltaOne PointwiseComposition.FFL.SigmaPiDelta.pi x✝ = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi ↑φ.pi ⋯

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.verum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ n Γ

The verum construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

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

The falsum construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

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

The and construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• One or more equations did not get rendered due to their size.
• φ.and ψ = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑φ ⋏ ↑ψ) ⋯
• φ.and ψ = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (↑φ ⋏ ↑ψ) ⋯

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

The or construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• One or more equations did not get rendered due to their size.
• φ.or ψ = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑φ ⋎ ↑ψ) ⋯
• φ.or ψ = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (↑φ ⋎ ↑ψ) ⋯

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.negSigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }

The neg Sigma construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• φ.negSigma = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (∼↑φ) ⋯

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.negPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }) : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }

The neg Pi construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• φ.negPi = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (∼↑φ) ⋯

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

The neg Delta construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ball {ξ : Type u_1} {n : ℕ} (t : ArithmeticSemiterm ξ n) {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

The ball construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.bexs {ξ : Type u_1} {n : ℕ} (t : ArithmeticSemiterm ξ n) {Γ : HierarchySymbol} : HierarchySymbol.Semiformula ξ (n + 1) Γ → HierarchySymbol.Semiformula ξ n Γ

The bexs construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

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

The all construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• φ.all = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkPi (∀¹ ↑φ) ⋯

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

The exs construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

• φ.exs = PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (∃¹ ↑φ) ⋯

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instTop {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Top (HierarchySymbol.Semiformula ξ n Γ)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instTop = { top := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.verum }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instBot {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Bot (HierarchySymbol.Semiformula ξ n Γ)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instBot = { bot := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.falsum }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instWedge {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Wedge (HierarchySymbol.Semiformula ξ n Γ)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instWedge = { wedge := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.and }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instVee {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : Vee (HierarchySymbol.Semiformula ξ n Γ)

Equations

• PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instVee = { vee := PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.or }

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta {ξ : Type u_1} {n m : ℕ} : Tilde (HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m })

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.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.

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instExsQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} : ExsQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m + 1 }

Equations

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

@[instance_reducible]

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} : UnivQuantifier fun (n : ℕ) => HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m + 1 }

Equations

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

def PointwiseComposition.FFL.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 }

The subst Sigma construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_verum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : ↑⊤ = ⊤

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_verum {ξ : Type u_1} {n m : ℕ} : ⊤.sigma = ⊤

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_verum {ξ : Type u_1} {n m : ℕ} : ⊤.pi = ⊤

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_falsum {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} : ↑⊥ = ⊥

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_falsum {ξ : Type u_1} {n m : ℕ} : ⊥.sigma = ⊥

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_falsum {ξ : Type u_1} {n m : ℕ} : ⊥.pi = ⊥

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_and {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (φ ψ : HierarchySymbol.Semiformula ξ n Γ) : ↑(φ ⋏ ψ) = ↑φ ⋏ ↑ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_and {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : (φ ⋏ ψ).sigma = φ.sigma ⋏ ψ.sigma

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_and {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : (φ ⋏ ψ).pi = φ.pi ⋏ ψ.pi

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_or {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (φ ψ : HierarchySymbol.Semiformula ξ n Γ) : ↑(φ ⋎ ψ) = ↑φ ⋎ ↑ψ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_or {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : (φ ⋎ ψ).sigma = φ.sigma ⋎ ψ.sigma

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.pi_or {ξ : Type u_1} {n m : ℕ} (φ ψ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : (φ ⋎ ψ).pi = φ.pi ⋎ ψ.pi

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_negSigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Σ, rank := m }) : ↑φ.negSigma = ∼↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_negPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := Π, rank := m }) : ↑φ.negPi = ∼↑φ

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_negDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : ↑(∼φ) = ∼↑φ.pi

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_negDelta {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : (∼φ).sigma = φ.pi.negPi

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.sigma_negPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ n { Γ := ∆, rank := m }) : (∼φ).pi = φ.sigma.negSigma

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_exsSigma {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := Σ, rank := m + 1 }) : ↑φ.exs = ∃¹ ↑φ

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.val_allPi {ξ : Type u_1} {n m : ℕ} (φ : HierarchySymbol.Semiformula ξ (n + 1) { Γ := Π, rank := m + 1 }) : ↑φ.all = ∀¹ ↑φ

@[simp]

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

@[simp]

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperOn.neg {M : Type u_2} [ORingStructure M] {m k : ℕ} {φ : { Γ := ∆, rank := m }.Semisentence k} (hp : ProperOn M φ) : ProperOn M (∼φ)

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.ProperWithParamOn.verum {M : Type u_2} [ORingStructure M] {m k : ℕ} : ProperWithParamOn M ⊤

@[simp]

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

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.graphDelta {ξ : Type u_1} {m k : ℕ} (φ : HierarchySymbol.Semiformula ξ (k + 1) { Γ := Σ, rank := m }) : HierarchySymbol.Semiformula ξ (k + 1) { Γ := ∆, rank := m }

The graph Delta construction in FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.graphDelta_val {ξ : Type u_1} {m k : ℕ} (φ : HierarchySymbol.Semiformula ξ (k + 1) { Γ := Σ, rank := m }) : ↑φ.graphDelta = ↑φ