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 aSemiformula ℒₒᵣ ξ n
which is𝚺-[m]
.𝚷-[m].Semiformula ξ n
is aSemiformula ℒₒᵣ ξ n
which is𝚷-[m]
.𝚫-[m].Semiformula ξ n
is a pair of𝚺-[m].Semiformula ξ n
and𝚷-[m].Semiformula ξ n
.ProperOn
:p.ProperOn M
iffp
's two elementp.sigma
andp.pi
are equivalent on modelM
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
@[reducible, inline]
Instances For
Equations
- LO.FirstOrder.Arith.«term𝚺₀» = Lean.ParserDescr.node `LO.FirstOrder.Arith.term𝚺₀ 1024 (Lean.ParserDescr.symbol "𝚺₀")
Instances For
Equations
- LO.FirstOrder.Arith.«term𝚷₀» = Lean.ParserDescr.node `LO.FirstOrder.Arith.term𝚷₀ 1024 (Lean.ParserDescr.symbol "𝚷₀")
Instances For
Equations
- LO.FirstOrder.Arith.«term𝚫₀» = Lean.ParserDescr.node `LO.FirstOrder.Arith.term𝚫₀ 1024 (Lean.ParserDescr.symbol "𝚫₀")
Instances For
Equations
- LO.FirstOrder.Arith.«term𝚺₁» = Lean.ParserDescr.node `LO.FirstOrder.Arith.term𝚺₁ 1024 (Lean.ParserDescr.symbol "𝚺₁")
Instances For
Equations
- LO.FirstOrder.Arith.«term𝚷₁» = Lean.ParserDescr.node `LO.FirstOrder.Arith.term𝚷₁ 1024 (Lean.ParserDescr.symbol "𝚷₁")
Instances For
Equations
- LO.FirstOrder.Arith.«term𝚫₁» = Lean.ParserDescr.node `LO.FirstOrder.Arith.term𝚫₁ 1024 (Lean.ParserDescr.symbol "𝚫₁")
Instances For
- 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
@[reducible, inline]
abbrev
LO.FirstOrder.Arith.HierarchySymbol.Semisentence
(Γ : LO.FirstOrder.Arith.HierarchySymbol)
(n : ℕ)
:
Equations
- Γ.Semisentence n = LO.FirstOrder.Arith.HierarchySymbol.Semiformula Empty n Γ
Instances For
@[reducible, inline]
Equations
- Γ.Sentence = LO.FirstOrder.Arith.HierarchySymbol.Semiformula Empty 0 Γ
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
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
Instances For
@[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
Instances For
@[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
Instances For
@[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.
Instances For
@[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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 })
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProvablyProperOn
{n : ℕ}
{m : ℕ}
(p : { Γ := 𝚫, rank := m }.Semisentence n)
(T : LO.FirstOrder.Theory ℒₒᵣ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
:
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)
:
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)
:
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]
:
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.rew
{ξ₁ : Type u_3}
{n₁ : ℕ}
{ξ₂ : Type u_4}
{n₂ : ℕ}
(ω : LO.FirstOrder.Rew ℒₒᵣ ξ₁ n₁ ξ₂ n₂)
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
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)
Instances For
@[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₂)
:
@[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₂)
:
@[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₂)
:
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.emb
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
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
Instances For
@[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)
:
@[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 })
:
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.extd
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
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
Instances For
@[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)
:
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)
:
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)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
@[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}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.falsum
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.and
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.or
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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) ⋯
Instances For
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) ⋯
Instances For
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
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ball
{ξ : Type u_1}
{n : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.bex
{ξ : Type u_1}
{n : ℕ}
(t : LO.FirstOrder.Semiterm ℒₒᵣ ξ n)
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
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) ⋯
Instances For
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) ⋯
Instances For
instance
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instTop
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
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}
:
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}
:
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}
:
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 }
instance
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.instUnivQuantifierMkPiSigmaPiDeltaHAddNatOfNat
{ξ : Type u_1}
{m : ℕ}
:
LO.UnivQuantifier fun (n : ℕ) => LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m + 1 }
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
Instances For
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_verum
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_falsum
{ξ : Type u_1}
{n : ℕ}
{Γ : LO.FirstOrder.Arith.HierarchySymbol}
:
@[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 Γ)
:
@[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 })
:
@[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 })
:
@[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 Γ)
:
@[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 })
:
@[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 })
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negSigma
{ξ : Type u_1}
{n : ℕ}
{m : ℕ}
(p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚺, rank := m })
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negPi
{ξ : Type u_1}
{n : ℕ}
{m : ℕ}
(p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚷, rank := m })
:
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val_negDelta
{ξ : Type u_1}
{n : ℕ}
{m : ℕ}
(p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m })
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_negDelta
{ξ : Type u_1}
{n : ℕ}
{m : ℕ}
(p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m })
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.sigma_negPi
{ξ : Type u_1}
{n : ℕ}
{m : ℕ}
(p : LO.FirstOrder.Arith.HierarchySymbol.Semiformula ξ n { Γ := 𝚫, rank := m })
:
@[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.ProperOn.verum
{M : Type u_2}
[LO.ORingStruc M]
{m : ℕ}
{k : ℕ}
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn.falsum
{M : Type u_2}
[LO.ORingStruc M]
{m : ℕ}
{k : ℕ}
:
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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.verum
{M : Type u_2}
[LO.ORingStruc M]
{m : ℕ}
{k : ℕ}
:
@[simp]
theorem
LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperWithParamOn.falsum
{M : Type u_2}
[LO.ORingStruc M]
{m : ℕ}
{k : ℕ}
:
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)
:
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)
:
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)
:
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)
:
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)
:
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.
Instances For
@[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