Arithmetization.Definability.Hierarchy

source

structure LO.FirstOrder.Arith.HierarchySymbol :

Type

Γ : SigmaPiDelta
rank : ℕ

source

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

Lean.TrailingParserDescr

Equations

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.sigmaZero :

HierarchySymbol

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.piZero :

HierarchySymbol

Equations

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.deltaZero :

HierarchySymbol

Equations

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.sigmaOne :

HierarchySymbol

Equations

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

Instances For

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.piOne :

HierarchySymbol

Equations

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

source

@[reducible, inline]

abbrev LO.FirstOrder.Arith.HierarchySymbol.deltaOne :

HierarchySymbol

Equations

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

Instances For

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

Lean.ParserDescr

Equations

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

source

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

HierarchySymbol → Type u_1

mkSigma {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) : Hierarchy 𝚺 m φ → HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m }
mkPi {ξ : Type u_1} {n m : ℕ} (φ : Semiformula ℒₒᵣ ξ n) : Hierarchy 𝚷 m φ → 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

source

@[reducible, inline]

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

Type

Equations

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

Instances For

source

@[reducible, inline]

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

Type

Equations

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

source

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

HierarchySymbol.Semiformula ξ n Γ → Semiformula ℒₒᵣ ξ n

Equations

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

source

@[simp]

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

(mkSigma φ hp).val = φ

source

@[simp]

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

(mkPi φ hp).val = φ

source

@[simp]

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

(φ.mkDelta ψ).val = φ.val

source

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaZeroSemisentenceORing {n : ℕ} :

Coe (𝚺₀.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

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

source

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiZeroSemisentenceORing {n : ℕ} :

Coe (𝚷₀.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

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

source

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaZeroSemisentenceORing {n : ℕ} :

Coe (𝚫₀.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

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

source

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaOneSemisentenceORing {n : ℕ} :

Coe (𝚺₁.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

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

source

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiOneSemisentenceORing {n : ℕ} :

Coe (𝚷₁.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

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

source

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaOneSemisentenceORing {n : ℕ} :

Coe (𝚫₁.Semisentence n) (Semisentence ℒₒᵣ n)

Equations

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

source

@[simp]

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

Hierarchy 𝚺 m φ.val

source

@[simp]

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

Hierarchy 𝚷 m φ.val

source

@[simp]

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

Hierarchy Γ m φ.val

source

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

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

Equations

(φ.mkDelta a).sigma = φ

source

@[simp]

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

(φ.mkDelta ψ).sigma = φ

source

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

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

Equations

(φ.mkDelta a).pi = a

source

@[simp]

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

(φ.mkDelta ψ).pi = ψ

source

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

φ.sigma.val = φ.val

source

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

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

Equations

source

@[simp]

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

(mkPolarity φ Γ h).val = φ

source

@[simp]

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

Hierarchy 𝚺 m φ.val

source

@[simp]

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

Hierarchy 𝚷 m φ.val

source

@[simp]

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

Hierarchy Γ' m φ.val

source

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

Prop

Equations

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

source

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

Prop

Equations

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

source

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

Prop

Equations

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

source

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

M ⊧/e (sigma φ).val ↔ M ⊧/e (pi φ).val

source

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

(Semiformula.Evalm M e id) φ.sigma.val ↔ (Semiformula.Evalm M e id) φ.pi.val

source

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

M ⊧/e (pi φ).val ↔ M ⊧/e (val φ)

source

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

(Semiformula.Evalm M e id) φ.pi.val ↔ (Semiformula.Evalm M e id) φ.val

source

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

ProvablyProperOn φ T

source

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

ProperOn M φ

source

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

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

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

source

@[simp]

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

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

source

@[simp]

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

ProperOn M (Semiformula.rew ω φ)

source

@[simp]

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

ProperWithParamOn M (Semiformula.rew ω φ)

source

@[simp]

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

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

source

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

HierarchySymbol.Semiformula ξ n Γ → 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

source

@[simp]

theorem LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_emb {ξ : Type u_1} {n : ℕ} {Γ : HierarchySymbol} (φ : HierarchySymbol.Semiformula ξ n Γ) :

φ.emb.val = (Semiformula.lMap Language.oringEmb) φ.val

source

@[simp]

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

φ.emb.pi = φ.pi.emb

source

@[simp]

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

φ.emb.sigma = φ.sigma.emb

source

@[simp]

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

ProperOn M (emb φ) ↔ ProperOn M φ

source

@[simp]

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

ProperWithParamOn M φ.emb ↔ ProperWithParamOn M φ

source

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

HierarchySymbol.Semiformula ξ n Γ → 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

source

@[simp]

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

(Semiformula.Evalm M e ε) φ.extd.val ↔ (Semiformula.Evalm M e ε) φ.val

source

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

ProperOn M (Semiformula.extd φ)

source

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

ProperOn M (Semiformula.extd φ)

source

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

φ.extd.val = (Semiformula.lMap Language.oringEmb) φ.val

source

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

φ.extd.val = (Semiformula.lMap Language.oringEmb) φ.val

source

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

Hierarchy 𝚺 0 φ.val

source

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

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

source

def LO.FirstOrder.Arith.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.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 ⋯)

source

@[simp]

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

(φ.ofZero Γ).val = φ.val

source

@[simp]

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

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

source

@[simp]

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

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

source

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

HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → 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) ⋯)

source

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

HierarchySymbol.Semiformula ξ n Γ → HierarchySymbol.Semiformula ξ n Γ → 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) ⋯)

source

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

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

Equations

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

source

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

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

Equations

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

source

def LO.FirstOrder.Arith.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

source

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

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

Equations

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

source

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

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

Equations

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

source

def LO.FirstOrder.Arith.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.Arith.HierarchySymbol.Semiformula.mkPi (∀' φ.val) ⋯

source

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

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

Equations

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

source

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

Top (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

source

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

Bot (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

source

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

Wedge (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

source

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

Vee (HierarchySymbol.Semiformula ξ n Γ)

Equations

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

source

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

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

Equations

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

source

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

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

Equations

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

source

instance LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instExQuantifierMkSigmaSigmaPiDeltaHAddNatOfNat {ξ : Type u_1} {m : ℕ} :

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

Equations

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

source

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

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

Equations

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

source

def LO.FirstOrder.Arith.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.Arith.HierarchySymbol.Semiformula.rew (LO.FirstOrder.Rew.substs ![LO.FirstOrder.Semiterm.bvar 0]) φ).ex

source

@[simp]

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

⊤.val = ⊤

source

@[simp]

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

⊤.sigma = ⊤

source

@[simp]

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

⊤.pi = ⊤

source

@[simp]

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

⊥.val = ⊥

source

@[simp]

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

⊥.sigma = ⊥

source

@[simp]

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

⊥.pi = ⊥

source

@[simp]

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

(φ ⋏ ψ).val = φ.val ⋏ ψ.val

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(φ ⋎ ψ).val = φ.val ⋎ ψ.val

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

φ.negSigma.val = ∼φ.val

source

@[simp]

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

φ.negPi.val = ∼φ.val

source

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

(∼φ).val = ∼φ.pi.val

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(bex t φ).val = (“(∃[!!(Semiterm.bvar 0) < !!(Rew.bShift t)] !φ.val)”)

source

@[simp]

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

φ.ex.val = ∃' φ.val

source

@[simp]

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

φ.all.val = ∀' φ.val

source

@[simp]

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

ProperOn M ⊤

source

@[simp]

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

ProperOn M ⊥

source

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

ProperOn M (φ ⋏ ψ)

source

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

ProperOn M (φ ⋎ ψ)

source

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

ProperOn M (∼φ)

source

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

M ⊧/e (val (∼φ)) ↔ ¬M ⊧/e (val φ)

source

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

ProperOn M (Semiformula.ball t φ)

source

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

ProperOn M (Semiformula.bex t φ)

source

@[simp]

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

ProperWithParamOn M ⊤

source

@[simp]

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

ProperWithParamOn M ⊥

source

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

ProperWithParamOn M (φ ⋏ ψ)

source

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

ProperWithParamOn M (φ ⋎ ψ)

source

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

ProperWithParamOn M (∼φ)

source

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

(Semiformula.Evalm M e id) (∼φ).val ↔ ¬(Semiformula.Evalm M e id) φ.val

source

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

ProperWithParamOn M (Semiformula.ball t φ)

source

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

ProperWithParamOn M (Semiformula.bex t φ)

source

def LO.FirstOrder.Arith.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 }

source

@[simp]

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

φ.graphDelta.val = φ.val

Documentation

Arithmetization.Definability.Hierarchy

Arithmetical Formula Sorted by Arithmetical Hierarchy #