Arithmetical Formula Sorted by Arithmetical Hierarchy

This file defines the ${\mathrm{\Sigma }}_n/{\mathrm{\Pi }}_n/{\mathrm{\Delta }}_n$ formulas of arithmetic of first-order logic.

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

structure LO.FirstOrder.Arith.HierarchySymbol : Type

• Γ : LO.SigmaPiDelta
• rank : ℕ

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

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Arith.Language.Defined.func_definable
• LO.Arith.Language.Defined.rel_definable
• LO.Arith.Nuon.ext_Definable
• LO.Arith.Nuon.nuonAux_definable
• LO.Arith.bexp_definable
• LO.Arith.bitSubset_definable
• LO.Arith.cons_definable
• LO.Arith.div_definable
• LO.Arith.domain_definable
• LO.Arith.exp_definable_deltaZero
• LO.Arith.exponential_definable
• LO.Arith.ext_definable
• LO.Arith.fbit_definable
• LO.Arith.fstIdx_definable
• LO.Arith.hash_definable
• LO.Arith.insert_definable
• LO.Arith.isMapping_definable
• LO.Arith.lenbit_definable
• LO.Arith.length_definable
• LO.Arith.lh_definable
• LO.Arith.log_definable
• LO.Arith.mem_definable
• LO.Arith.mkSeq₁_definable
• LO.Arith.mkVec₁_definable
• LO.Arith.nuon_definable
• LO.Arith.pair_definable
• LO.Arith.pi₁_definable
• LO.Arith.pi₂_definable
• LO.Arith.pow2_definable
• LO.Arith.ppow2_definable
• LO.Arith.product_definable
• LO.Arith.range_definable
• LO.Arith.rem_definable
• LO.Arith.sUnion_definable
• LO.Arith.seqCons_definable
• LO.Arith.seq_definable
• LO.Arith.sndIdx_definable
• LO.Arith.sqrt_definable
• LO.Arith.under_definable
• LO.Arith.union_definable
• LO.Arith.znth_definable

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Arith.Fixpoint.Construction.limSeq_definable
• LO.Arith.Formalized.numeral_definable
• LO.Arith.Formalized.substItr_definable
• LO.Arith.Language.TermRec.Construction.graph_definable
• LO.Arith.Language.Theory.derivable_definable
• LO.Arith.Language.Theory.provable_definable
• LO.Arith.Language.bv_definable
• LO.Arith.Language.free_definable
• LO.Arith.Language.iff_definable
• LO.Arith.Language.imp_definable
• LO.Arith.Language.neg_definable
• LO.Arith.Language.qVec_definable
• LO.Arith.Language.setShift_definable
• LO.Arith.Language.shift_definable
• LO.Arith.Language.substs_definable
• LO.Arith.Language.substs₁_definable
• LO.Arith.Language.termBShiftVec_definable
• LO.Arith.Language.termBShift_definable
• LO.Arith.Language.termBVVec_definable
• LO.Arith.Language.termBV_definable
• LO.Arith.Language.termShiftVec_definable
• LO.Arith.Language.termShift_definable
• LO.Arith.Language.termSubstVec_definable
• LO.Arith.Language.termSubst_definable
• LO.Arith.Nth.graph_definable
• LO.Arith.PR.Construction.result_definable
• LO.Arith.VecRec.Construction.graph_definable
• LO.Arith.VecRec.Construction.graph_definable'
• LO.Arith.VecRec.Construction.result_definable
• LO.Arith.concat_definable
• LO.Arith.len_definable
• LO.Arith.listMax_definable
• LO.Arith.mkSeq₂_definable
• LO.Arith.mkVec₂_definable
• LO.Arith.nth_definable
• LO.Arith.provableₐ_definable
• LO.Arith.qqConj_definable
• LO.Arith.qqDisj_definable
• LO.Arith.qqVerums_definable
• LO.Arith.repeatVec_definable
• LO.Arith.takeLast_definable
• LO.Arith.vecToSet_definable

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

Instances For

• LO.Arith.Language.Theory.derivationOf_definable
• LO.Arith.Language.Theory.derivation_definable
• LO.Arith.Language.Theory.mem_definable
• LO.Arith.Language.isFormulaSet_definable
• LO.Arith.Language.isSemiformula_definable
• LO.Arith.Language.isSemitermVec_definable
• LO.Arith.Language.isSemiterm_definable
• LO.Arith.Language.isUFormulaDef_definable
• LO.Arith.Language.isUTermVecDef_definable
• LO.Arith.Language.isUTerm_definable
• LO.Arith.PR.Construction.result_definable_delta₁
• LO.Arith.memVec_definable
• LO.Arith.subsetVec_definable

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Instances For

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instBot
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instLogicalConnectiveMkDeltaSigmaPiDelta
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTildeMkDeltaSigmaPiDelta
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTop
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instVee
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instWedge

@[reducible, inline]

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

Equations

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

Instances For

• LO.Arith.Fixpoint.Blueprint.instCoeSemisentenceDeltaOneHAddNatOfNat
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaOneSemisentenceORing
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceDeltaZeroSemisentenceORing
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiOneSemisentenceORing
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentencePiZeroSemisentenceORing
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaOneSemisentenceORing
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instCoeSemisentenceSigmaZeroSemisentenceORing

@[reducible, inline]

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• x.sigma = match x with | p.mkDelta a => p

@[simp]

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

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

Equations

• x.pi = match x with | a.mkDelta p => p

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

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

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

Equations

• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma p hp) = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkSigma (ω.hom p) ⋯
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi p hp) = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.mkPi (ω.hom p) ⋯
• LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω (p.mkDelta q) = (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω p).mkDelta (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew ω q)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

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

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

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

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

Equations

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

@[simp]

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