Equations
- LO.Arith.qqRel k r v = ⟪0, ⟪k, ⟪r, v⟫⟫⟫ + 1
Instances For
Equations
- LO.Arith.qqNRel k r v = ⟪1, ⟪k, ⟪r, v⟫⟫⟫ + 1
Instances For
Instances For
Instances For
Equations
- LO.Arith.qqAnd p q = ⟪4, ⟪p, q⟫⟫ + 1
Instances For
Equations
- LO.Arith.qqOr p q = ⟪5, ⟪p, q⟫⟫ + 1
Instances For
Equations
- LO.Arith.qqAll p = ⟪6, p⟫ + 1
Instances For
Equations
- LO.Arith.qqEx p = ⟪7, p⟫ + 1
Instances For
Equations
- LO.Arith.«term^rel_» = Lean.ParserDescr.node `LO.Arith.term^rel_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^rel ") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- LO.Arith.«term^nrel_» = Lean.ParserDescr.node `LO.Arith.term^nrel_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^nrel ") (Lean.ParserDescr.cat `term 1024))
Instances For
Equations
- LO.Arith.«term^⊤» = Lean.ParserDescr.node `LO.Arith.term^⊤ 1024 (Lean.ParserDescr.symbol "^⊤")
Instances For
Equations
- LO.Arith.«term^⊥» = Lean.ParserDescr.node `LO.Arith.term^⊥ 1024 (Lean.ParserDescr.symbol "^⊥")
Instances For
Equations
- LO.Arith.«term_^⋏_» = Lean.ParserDescr.trailingNode `LO.Arith.term_^⋏_ 1022 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^⋏ ") (Lean.ParserDescr.cat `term 70))
Instances For
Equations
- LO.Arith.«term_^⋎_» = Lean.ParserDescr.trailingNode `LO.Arith.term_^⋎_ 1022 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^⋎ ") (Lean.ParserDescr.cat `term 69))
Instances For
Equations
- LO.Arith.«term^∀_» = Lean.ParserDescr.node `LO.Arith.term^∀_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^∀ ") (Lean.ParserDescr.cat `term 64))
Instances For
Equations
- LO.Arith.«term^∃_» = Lean.ParserDescr.node `LO.Arith.term^∃_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^∃ ") (Lean.ParserDescr.cat `term 64))
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.qqRel_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₃ LO.Arith.qqRel via LO.FirstOrder.Arith.qqRelDef
theorem
LO.Arith.qqNRel_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₃ LO.Arith.qqNRel via LO.FirstOrder.Arith.qqNRelDef
theorem
LO.Arith.qqVerum_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₀ LO.Arith.qqVerum via LO.FirstOrder.Arith.qqVerumDef
theorem
LO.Arith.qqFalsum_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₀ LO.Arith.qqFalsum via LO.FirstOrder.Arith.qqFalsumDef
theorem
LO.Arith.qqAnd_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.qqAnd via LO.FirstOrder.Arith.qqAndDef
theorem
LO.Arith.qqOr_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.qqOr via LO.FirstOrder.Arith.qqOrDef
theorem
LO.Arith.qqForall_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.qqAll via LO.FirstOrder.Arith.qqAllDef
theorem
LO.Arith.qqExists_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.qqEx via LO.FirstOrder.Arith.qqExDef
@[simp]
theorem
LO.Arith.eval_qqRelDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 4 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqRelDef) ↔ v 0 = LO.Arith.qqRel (v 1) (v 2) (v 3)
@[simp]
theorem
LO.Arith.eval_qqNRelDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 4 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqNRelDef) ↔ v 0 = LO.Arith.qqNRel (v 1) (v 2) (v 3)
@[simp]
theorem
LO.Arith.eval_qqVerumDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 1 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqVerumDef) ↔ v 0 = LO.Arith.qqVerum
@[simp]
theorem
LO.Arith.eval_qqFalsumDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 1 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqFalsumDef) ↔ v 0 = LO.Arith.qqFalsum
@[simp]
theorem
LO.Arith.eval_qqAndDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqAndDef) ↔ v 0 = LO.Arith.qqAnd (v 1) (v 2)
@[simp]
theorem
LO.Arith.eval_qqOrDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqOrDef) ↔ v 0 = LO.Arith.qqOr (v 1) (v 2)
@[simp]
@[simp]
instance
LO.Arith.instBoldfaceFunction₃QqRel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₃ LO.Arith.qqRel
Equations
- ⋯ = ⋯
instance
LO.Arith.instBoldfaceFunction₃QqNRel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₃ LO.Arith.qqNRel
Equations
- ⋯ = ⋯
instance
LO.Arith.instBoldfaceFunction₂QqAnd
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₂ LO.Arith.qqAnd
Equations
- ⋯ = ⋯
instance
LO.Arith.instBoldfaceFunction₂QqOr
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₂ LO.Arith.qqOr
Equations
- ⋯ = ⋯
instance
LO.Arith.instBoldfaceFunction₁QqAll
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₁ LO.Arith.qqAll
Equations
- ⋯ = ⋯
instance
LO.Arith.instBoldfaceFunction₁QqEx
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(ℌ : LO.FirstOrder.Arith.HierarchySymbol)
:
ℌ-Function₁ LO.Arith.qqEx
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.qqRel_inj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k₁ : V)
(r₁ : V)
(v₁ : V)
(k₂ : V)
(r₂ : V)
(v₂ : V)
:
LO.Arith.qqRel k₁ r₁ v₁ = LO.Arith.qqRel k₂ r₂ v₂ ↔ k₁ = k₂ ∧ r₁ = r₂ ∧ v₁ = v₂
@[simp]
theorem
LO.Arith.qqNRel_inj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k₁ : V)
(r₁ : V)
(v₁ : V)
(k₂ : V)
(r₂ : V)
(v₂ : V)
:
LO.Arith.qqNRel k₁ r₁ v₁ = LO.Arith.qqNRel k₂ r₂ v₂ ↔ k₁ = k₂ ∧ r₁ = r₂ ∧ v₁ = v₂
@[simp]
theorem
LO.Arith.qqAnd_inj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p₁ : V)
(q₁ : V)
(p₂ : V)
(q₂ : V)
:
LO.Arith.qqAnd p₁ q₁ = LO.Arith.qqAnd p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
@[simp]
theorem
LO.Arith.qqOr_inj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p₁ : V)
(q₁ : V)
(p₂ : V)
(q₂ : V)
:
LO.Arith.qqOr p₁ q₁ = LO.Arith.qqOr p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂
@[simp]
theorem
LO.Arith.qqAll_inj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p₁ : V)
(p₂ : V)
:
LO.Arith.qqAll p₁ = LO.Arith.qqAll p₂ ↔ p₁ = p₂
@[simp]
theorem
LO.Arith.qqEx_inj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p₁ : V)
(p₂ : V)
:
LO.Arith.qqEx p₁ = LO.Arith.qqEx p₂ ↔ p₁ = p₂
@[simp]
theorem
LO.Arith.arity_lt_rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k : V)
(r : V)
(v : V)
:
k < LO.Arith.qqRel k r v
@[simp]
theorem
LO.Arith.r_lt_rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k : V)
(r : V)
(v : V)
:
r < LO.Arith.qqRel k r v
@[simp]
theorem
LO.Arith.v_lt_rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k : V)
(r : V)
(v : V)
:
v < LO.Arith.qqRel k r v
@[simp]
theorem
LO.Arith.arity_lt_nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k : V)
(r : V)
(v : V)
:
k < LO.Arith.qqNRel k r v
@[simp]
theorem
LO.Arith.r_lt_nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k : V)
(r : V)
(v : V)
:
r < LO.Arith.qqNRel k r v
@[simp]
theorem
LO.Arith.v_lt_nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(k : V)
(r : V)
(v : V)
:
v < LO.Arith.qqNRel k r v
theorem
LO.Arith.nth_lt_qqRel_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{k : V}
{r : V}
{v : V}
(hi : i < LO.Arith.len v)
:
LO.Arith.nth v i < LO.Arith.qqRel k r v
theorem
LO.Arith.nth_lt_qqNRel_of_lt
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{i : V}
{k : V}
{r : V}
{v : V}
(hi : i < LO.Arith.len v)
:
LO.Arith.nth v i < LO.Arith.qqNRel k r v
@[simp]
theorem
LO.Arith.lt_and_left
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
(q : V)
:
p < LO.Arith.qqAnd p q
@[simp]
theorem
LO.Arith.lt_and_right
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
(q : V)
:
q < LO.Arith.qqAnd p q
@[simp]
theorem
LO.Arith.lt_or_left
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
(q : V)
:
p < LO.Arith.qqOr p q
@[simp]
theorem
LO.Arith.lt_or_right
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
(q : V)
:
q < LO.Arith.qqOr p q
@[simp]
theorem
LO.Arith.lt_forall
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
:
p < LO.Arith.qqAll p
@[simp]
theorem
LO.Arith.lt_exists
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(p : V)
:
p < LO.Arith.qqEx p
def
LO.Arith.FormalizedFormula.Phi
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(C : Set V)
(p : V)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.FormalizedFormula.construction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Equations
- LO.Arith.FormalizedFormula.construction L = { Φ := fun (x : Fin 0 → V) => LO.Arith.FormalizedFormula.Phi L, defined := ⋯, monotone := ⋯ }
Instances For
instance
LO.Arith.FormalizedFormula.instStrongFiniteConstruction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Equations
- LO.Arith.FormalizedFormula.instStrongFiniteConstruction L = { strong_finite := ⋯ }
def
LO.Arith.Language.IsUFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
V → Prop
Equations
- L.IsUFormula = (LO.Arith.FormalizedFormula.construction L).Fixpoint ![]
Instances For
Equations
- pL.isUFormulaDef = (LO.Arith.FormalizedFormula.blueprint pL).fixpointDefΔ₁
Instances For
theorem
LO.Arith.Language.isUFormula_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚫₁-Predicate L.IsUFormula via pL.isUFormulaDef
instance
LO.Arith.Language.isUFormulaDef_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚫₁-Predicate L.IsUFormula
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.isUFormulaDef_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Predicate L.IsUFormula
Equations
- ⋯ = ⋯
theorem
LO.Arith.Language.IsUFormula.case_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula p ↔ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqEx p₁
theorem
LO.Arith.Language.IsUFormula.mk
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
((∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqEx p₁) →
L.IsUFormula p
Alias of the reverse direction of LO.Arith.Language.IsUFormula.case_iff
.
theorem
LO.Arith.Language.IsUFormula.case
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula p →
(∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqEx p₁
Alias of the forward direction of LO.Arith.Language.IsUFormula.case_iff
.
@[simp]
theorem
LO.Arith.Language.IsUFormula.rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{r : V}
{v : V}
:
L.IsUFormula (LO.Arith.qqRel k r v) ↔ L.Rel k r ∧ L.IsUTermVec k v
@[simp]
theorem
LO.Arith.Language.IsUFormula.nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{r : V}
{v : V}
:
L.IsUFormula (LO.Arith.qqNRel k r v) ↔ L.Rel k r ∧ L.IsUTermVec k v
@[simp]
theorem
LO.Arith.Language.IsUFormula.verum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.IsUFormula LO.Arith.qqVerum
@[simp]
theorem
LO.Arith.Language.IsUFormula.falsum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.IsUFormula LO.Arith.qqFalsum
@[simp]
theorem
LO.Arith.Language.IsUFormula.and
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
:
L.IsUFormula (LO.Arith.qqAnd p q) ↔ L.IsUFormula p ∧ L.IsUFormula q
@[simp]
theorem
LO.Arith.Language.IsUFormula.or
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
:
L.IsUFormula (LO.Arith.qqOr p q) ↔ L.IsUFormula p ∧ L.IsUFormula q
@[simp]
theorem
LO.Arith.Language.IsUFormula.all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula (LO.Arith.qqAll p) ↔ L.IsUFormula p
@[simp]
theorem
LO.Arith.Language.IsUFormula.ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsUFormula (LO.Arith.qqEx p) ↔ L.IsUFormula p
theorem
LO.Arith.Language.IsUFormula.pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(h : L.IsUFormula p)
:
0 < p
@[simp]
theorem
LO.Arith.Language.IsUFormula.not_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
¬L.IsUFormula 0
theorem
LO.Arith.Language.IsUFormula.induction1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(Γ : LO.SigmaPiDelta)
{P : V → Prop}
(hP : { Γ := Γ, rank := 1 }-Predicate P)
(hrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqRel k r v))
(hnrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqNRel k r v))
(hverum : P LO.Arith.qqVerum)
(hfalsum : P LO.Arith.qqFalsum)
(hand : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqAnd p q))
(hor : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqOr p q))
(hall : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqAll p))
(hex : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqEx p))
(p : V)
:
L.IsUFormula p → P p
theorem
LO.Arith.Language.IsUFormula.induction_sigma1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{P : V → Prop}
(hP : 𝚺₁-Predicate P)
(hrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqRel k r v))
(hnrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqNRel k r v))
(hverum : P LO.Arith.qqVerum)
(hfalsum : P LO.Arith.qqFalsum)
(hand : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqAnd p q))
(hor : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqOr p q))
(hall : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqAll p))
(hex : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqEx p))
(p : V)
:
L.IsUFormula p → P p
theorem
LO.Arith.Language.IsUFormula.induction_pi1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{P : V → Prop}
(hP : 𝚷₁-Predicate P)
(hrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqRel k r v))
(hnrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqNRel k r v))
(hverum : P LO.Arith.qqVerum)
(hfalsum : P LO.Arith.qqFalsum)
(hand : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqAnd p q))
(hor : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqOr p q))
(hall : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqAll p))
(hex : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqEx p))
(p : V)
:
L.IsUFormula p → P p
def
LO.Arith.Language.UformulaRec1.Blueprint.blueprint
{pL : LO.FirstOrder.Arith.LDef}
(β : LO.Arith.Language.UformulaRec1.Blueprint pL)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.UformulaRec1.Blueprint.graph
{pL : LO.FirstOrder.Arith.LDef}
(β : LO.Arith.Language.UformulaRec1.Blueprint pL)
:
𝚺₁.Semisentence 3
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.UformulaRec1.Blueprint.result
{pL : LO.FirstOrder.Arith.LDef}
(β : LO.Arith.Language.UformulaRec1.Blueprint pL)
:
𝚺₁.Semisentence 3
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
LO.Arith.Language.UformulaRec1.Construction
(V : Type u_1)
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
(L : LO.Arith.Language V)
(φ : LO.Arith.Language.UformulaRec1.Blueprint pL)
:
Type u_1
- rel : V → V → V → V → V
- nrel : V → V → V → V → V
- verum : V → V
- falsum : V → V
- and : V → V → V → V → V → V
- or : V → V → V → V → V → V
- all : V → V → V → V
- ex : V → V → V → V
- allChanges : V → V
- exChanges : V → V
- rel_defined : 𝚺₁-Function₄ self.rel via φ.rel
- nrel_defined : 𝚺₁-Function₄ self.nrel via φ.nrel
- verum_defined : 𝚺₁-Function₁ self.verum via φ.verum
- falsum_defined : 𝚺₁-Function₁ self.falsum via φ.falsum
- and_defined : 𝚺₁-Function₅ self.and via φ.and
- or_defined : 𝚺₁-Function₅ self.or via φ.or
- all_defined : 𝚺₁-Function₃ self.all via φ.all
- ex_defined : 𝚺₁-Function₃ self.ex via φ.ex
- allChanges_defined : 𝚺₁-Function₁ self.allChanges via φ.allChanges
- exChanges_defined : 𝚺₁-Function₁ self.exChanges via φ.exChanges
Instances For
theorem
LO.Arith.Language.UformulaRec1.Construction.rel_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₄ self.rel via φ.rel
theorem
LO.Arith.Language.UformulaRec1.Construction.nrel_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₄ self.nrel via φ.nrel
theorem
LO.Arith.Language.UformulaRec1.Construction.verum_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₁ self.verum via φ.verum
theorem
LO.Arith.Language.UformulaRec1.Construction.falsum_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₁ self.falsum via φ.falsum
theorem
LO.Arith.Language.UformulaRec1.Construction.and_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₅ self.and via φ.and
theorem
LO.Arith.Language.UformulaRec1.Construction.or_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₅ self.or via φ.or
theorem
LO.Arith.Language.UformulaRec1.Construction.all_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₃ self.all via φ.all
theorem
LO.Arith.Language.UformulaRec1.Construction.ex_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₃ self.ex via φ.ex
theorem
LO.Arith.Language.UformulaRec1.Construction.allChanges_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₁ self.allChanges via φ.allChanges
theorem
LO.Arith.Language.UformulaRec1.Construction.exChanges_defined
{V : Type u_1}
[LO.ORingStruc V]
{pL : LO.FirstOrder.Arith.LDef}
{L : LO.Arith.Language V}
{φ : LO.Arith.Language.UformulaRec1.Blueprint pL}
(self : LO.Arith.Language.UformulaRec1.Construction V L φ)
:
𝚺₁-Function₁ self.exChanges via φ.exChanges
def
LO.Arith.Language.UformulaRec1.Construction.Phi
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(C : Set V)
(pr : V)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.UformulaRec1.Construction.construction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
:
LO.Arith.Fixpoint.Construction V β.blueprint
Instances For
instance
LO.Arith.Language.UformulaRec1.Construction.instFiniteConstruction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
:
LO.Arith.Fixpoint.Construction.Finite V c.construction
Equations
- c.instFiniteConstruction = { finite := ⋯ }
def
LO.Arith.Language.UformulaRec1.Construction.Graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(param : V)
(x : V)
(y : V)
:
Equations
- c.Graph param x y = c.construction.Fixpoint ![] ⟪param, ⟪x, y⟫⟫
Instances For
theorem
LO.Arith.Language.UformulaRec1.Construction.Graph.case_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
{c : LO.Arith.Language.UformulaRec1.Construction V L β}
{param : V}
{p : V}
{y : V}
:
c.Graph param p y ↔ L.IsUFormula p ∧ ((∃ (k : V) (R : V) (v : V), p = LO.Arith.qqRel k R v ∧ y = c.rel param k R v) ∨ (∃ (k : V) (R : V) (v : V), p = LO.Arith.qqNRel k R v ∧ y = c.nrel param k R v) ∨ p = LO.Arith.qqVerum ∧ y = c.verum param ∨ p = LO.Arith.qqFalsum ∧ y = c.falsum param ∨ (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V),
c.Graph param p₁ y₁ ∧ c.Graph param p₂ y₂ ∧ p = LO.Arith.qqAnd p₁ p₂ ∧ y = c.and param p₁ p₂ y₁ y₂) ∨ (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V),
c.Graph param p₁ y₁ ∧ c.Graph param p₂ y₂ ∧ p = LO.Arith.qqOr p₁ p₂ ∧ y = c.or param p₁ p₂ y₁ y₂) ∨ (∃ (p₁ : V) (y₁ : V),
c.Graph (c.allChanges param) p₁ y₁ ∧ p = LO.Arith.qqAll p₁ ∧ y = c.all param p₁ y₁) ∨ ∃ (p₁ : V) (y₁ : V), c.Graph (c.exChanges param) p₁ y₁ ∧ p = LO.Arith.qqEx p₁ ∧ y = c.ex param p₁ y₁)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(β : LO.Arith.Language.UformulaRec1.Blueprint pL)
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
:
𝚺₁-Relation₃ c.Graph via β.graph
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.eval_graphDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(β : LO.Arith.Language.UformulaRec1.Blueprint pL)
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.graph) ↔ c.Graph (v 0) (v 1) (v 2)
instance
LO.Arith.Language.UformulaRec1.Construction.graph_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(β : LO.Arith.Language.UformulaRec1.Blueprint pL)
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
:
{ Γ := 𝚺, rank := 0 + 1 }-Relation₃ c.Graph
Equations
- ⋯ = ⋯
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_dom_uformula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p : V}
{r : V}
:
c.Graph param p r → L.IsUFormula p
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_rel_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{k : V}
{r : V}
{v : V}
{y : V}
(hkr : L.Rel k r)
(hv : L.IsUTermVec k v)
:
c.Graph param (LO.Arith.qqRel k r v) y ↔ y = c.rel param k r v
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_nrel_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{k : V}
{r : V}
{v : V}
{y : V}
(hkr : L.Rel k r)
(hv : L.IsUTermVec k v)
:
c.Graph param (LO.Arith.qqNRel k r v) y ↔ y = c.nrel param k r v
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_verum_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{y : V}
:
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_falsum_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{y : V}
:
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{k : V}
{r : V}
{v : V}
(hkr : L.Rel k r)
(hv : L.IsUTermVec k v)
:
c.Graph param (LO.Arith.qqRel k r v) (c.rel param k r v)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{k : V}
{r : V}
{v : V}
(hkr : L.Rel k r)
(hv : L.IsUTermVec k v)
:
c.Graph param (LO.Arith.qqNRel k r v) (c.nrel param k r v)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_verum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
:
c.Graph param LO.Arith.qqVerum (c.verum param)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_falsum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
:
c.Graph param LO.Arith.qqFalsum (c.falsum param)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_and
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{p₂ : V}
{r₁ : V}
{r₂ : V}
(hp₁ : L.IsUFormula p₁)
(hp₂ : L.IsUFormula p₂)
(h₁ : c.Graph param p₁ r₁)
(h₂ : c.Graph param p₂ r₂)
:
c.Graph param (LO.Arith.qqAnd p₁ p₂) (c.and param p₁ p₂ r₁ r₂)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_and_inv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{p₂ : V}
{r : V}
:
c.Graph param (LO.Arith.qqAnd p₁ p₂) r →
∃ (r₁ : V) (r₂ : V), c.Graph param p₁ r₁ ∧ c.Graph param p₂ r₂ ∧ r = c.and param p₁ p₂ r₁ r₂
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_or
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{p₂ : V}
{r₁ : V}
{r₂ : V}
(hp₁ : L.IsUFormula p₁)
(hp₂ : L.IsUFormula p₂)
(h₁ : c.Graph param p₁ r₁)
(h₂ : c.Graph param p₂ r₂)
:
c.Graph param (LO.Arith.qqOr p₁ p₂) (c.or param p₁ p₂ r₁ r₂)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_or_inv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{p₂ : V}
{r : V}
:
c.Graph param (LO.Arith.qqOr p₁ p₂) r →
∃ (r₁ : V) (r₂ : V), c.Graph param p₁ r₁ ∧ c.Graph param p₂ r₂ ∧ r = c.or param p₁ p₂ r₁ r₂
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{r₁ : V}
(hp₁ : L.IsUFormula p₁)
(h₁ : c.Graph (c.allChanges param) p₁ r₁)
:
c.Graph param (LO.Arith.qqAll p₁) (c.all param p₁ r₁)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_all_inv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{r : V}
:
c.Graph param (LO.Arith.qqAll p₁) r → ∃ (r₁ : V), c.Graph (c.allChanges param) p₁ r₁ ∧ r = c.all param p₁ r₁
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{r₁ : V}
(hp₁ : L.IsUFormula p₁)
(h₁ : c.Graph (c.exChanges param) p₁ r₁)
:
c.Graph param (LO.Arith.qqEx p₁) (c.ex param p₁ r₁)
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_ex_inv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p₁ : V}
{r : V}
:
c.Graph param (LO.Arith.qqEx p₁) r → ∃ (r₁ : V), c.Graph (c.exChanges param) p₁ r₁ ∧ r = c.ex param p₁ r₁
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_exists
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(param : V)
{p : V}
:
L.IsUFormula p → ∃ (y : V), c.Graph param p y
theorem
LO.Arith.Language.UformulaRec1.Construction.graph_unique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{p : V}
:
L.IsUFormula p → ∀ {param r r' : V}, c.Graph param p r → c.Graph param p r' → r = r'
theorem
LO.Arith.Language.UformulaRec1.Construction.exists_unique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(param : V)
{p : V}
(hp : L.IsUFormula p)
:
∃! r : V, c.Graph param p r
theorem
LO.Arith.Language.UformulaRec1.Construction.exists_unique_all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(param : V)
(p : V)
:
def
LO.Arith.Language.UformulaRec1.Construction.result
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(param : V)
(p : V)
:
V
Equations
- c.result param p = Classical.choose! ⋯
Instances For
theorem
LO.Arith.Language.UformulaRec1.Construction.result_prop
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(param : V)
{p : V}
(hp : L.IsUFormula p)
:
c.Graph param p (c.result param p)
theorem
LO.Arith.Language.UformulaRec1.Construction.result_prop_not
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
(param : V)
{p : V}
(hp : ¬L.IsUFormula p)
:
c.result param p = 0
theorem
LO.Arith.Language.UformulaRec1.Construction.result_eq_of_graph
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p : V}
{r : V}
(h : c.Graph param p r)
:
c.result param p = r
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
c.result param (LO.Arith.qqRel k R v) = c.rel param k R v
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
c.result param (LO.Arith.qqNRel k R v) = c.nrel param k R v
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_verum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
:
c.result param LO.Arith.qqVerum = c.verum param
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_falsum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
:
c.result param LO.Arith.qqFalsum = c.falsum param
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_and
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
c.result param (LO.Arith.qqAnd p q) = c.and param p q (c.result param p) (c.result param q)
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_or
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
c.result param (LO.Arith.qqOr p q) = c.or param p q (c.result param p) (c.result param q)
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p : V}
(hp : L.IsUFormula p)
:
c.result param (LO.Arith.qqAll p) = c.all param p (c.result (c.allChanges param) p)
@[simp]
theorem
LO.Arith.Language.UformulaRec1.Construction.result_ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{param : V}
{p : V}
(hp : L.IsUFormula p)
:
c.result param (LO.Arith.qqEx p) = c.ex param p (c.result (c.exChanges param) p)
theorem
LO.Arith.Language.UformulaRec1.Construction.result_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
:
𝚺₁-Function₂ c.result via β.result
instance
LO.Arith.Language.UformulaRec1.Construction.result_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
:
{ Γ := 𝚺, rank := 0 + 1 }-Function₂ c.result
Equations
- ⋯ = ⋯
theorem
LO.Arith.Language.UformulaRec1.Construction.uformula_result_induction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
(c : LO.Arith.Language.UformulaRec1.Construction V L β)
{P : V → V → V → Prop}
(hP : 𝚺₁-Relation₃ P)
(hRel : ∀ (param k R v : V), L.Rel k R → L.IsUTermVec k v → P param (LO.Arith.qqRel k R v) (c.rel param k R v))
(hNRel : ∀ (param k R v : V), L.Rel k R → L.IsUTermVec k v → P param (LO.Arith.qqNRel k R v) (c.nrel param k R v))
(hverum : ∀ (param : V), P param LO.Arith.qqVerum (c.verum param))
(hfalsum : ∀ (param : V), P param LO.Arith.qqFalsum (c.falsum param))
(hand : ∀ (param p q : V),
L.IsUFormula p →
L.IsUFormula q →
P param p (c.result param p) →
P param q (c.result param q) →
P param (LO.Arith.qqAnd p q) (c.and param p q (c.result param p) (c.result param q)))
(hor : ∀ (param p q : V),
L.IsUFormula p →
L.IsUFormula q →
P param p (c.result param p) →
P param q (c.result param q) →
P param (LO.Arith.qqOr p q) (c.or param p q (c.result param p) (c.result param q)))
(hall : ∀ (param p : V),
L.IsUFormula p →
P (c.allChanges param) p (c.result (c.allChanges param) p) →
P param (LO.Arith.qqAll p) (c.all param p (c.result (c.allChanges param) p)))
(hex : ∀ (param p : V),
L.IsUFormula p →
P (c.exChanges param) p (c.result (c.exChanges param) p) →
P param (LO.Arith.qqEx p) (c.ex param p (c.result (c.exChanges param) p)))
{param : V}
{p : V}
:
L.IsUFormula p → P param p (c.result param p)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.BV.construction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.bv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
:
V
Equations
- L.bv p = (LO.Arith.BV.construction L).result 0 p
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.bv_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.bv via pL.bvDef
instance
LO.Arith.Language.bv_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.bv
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.bv_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{m : ℕ}
(Γ : LO.SigmaPiDelta)
:
{ Γ := Γ, rank := m + 1 }-Function₁ L.bv
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.bv_rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.bv (LO.Arith.qqRel k R v) = LO.Arith.listMax (L.termBVVec k v)
@[simp]
theorem
LO.Arith.bv_nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{k : V}
{R : V}
{v : V}
(hR : L.Rel k R)
(hv : L.IsUTermVec k v)
:
L.bv (LO.Arith.qqNRel k R v) = LO.Arith.listMax (L.termBVVec k v)
@[simp]
theorem
LO.Arith.bv_verum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.bv LO.Arith.qqVerum = 0
@[simp]
theorem
LO.Arith.bv_falsum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.bv LO.Arith.qqFalsum = 0
@[simp]
theorem
LO.Arith.bv_and
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.bv (LO.Arith.qqAnd p q) = max (L.bv p) (L.bv q)
@[simp]
theorem
LO.Arith.bv_or
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{q : V}
(hp : L.IsUFormula p)
(hq : L.IsUFormula q)
:
L.bv (LO.Arith.qqOr p q) = max (L.bv p) (L.bv q)
@[simp]
theorem
LO.Arith.bv_all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsUFormula p)
:
L.bv (LO.Arith.qqAll p) = L.bv p - 1
@[simp]
theorem
LO.Arith.bv_ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(hp : L.IsUFormula p)
:
L.bv (LO.Arith.qqEx p) = L.bv p - 1
theorem
LO.Arith.bv_eq_of_not_isUFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(h : ¬L.IsUFormula p)
:
L.bv p = 0
structure
LO.Arith.Language.IsSemiformula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(n : V)
(p : V)
:
- isUFormula : L.IsUFormula p
- bv : L.bv p ≤ n
Instances For
theorem
LO.Arith.Language.IsSemiformula.isUFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
(self : L.IsSemiformula n p)
:
L.IsUFormula p
theorem
LO.Arith.Language.IsSemiformula.bv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
(self : L.IsSemiformula n p)
:
L.bv p ≤ n
@[reducible, inline]
abbrev
LO.Arith.Language.IsFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : V)
:
Equations
- L.IsFormula p = L.IsSemiformula 0 p
Instances For
theorem
LO.Arith.Language.isSemiformula_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.isSemiformula_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
instance
LO.Arith.Language.isSemiformula_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.isSemiformulaDef_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.Language.IsUFormula.isSemiformula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
(h : L.IsUFormula p)
:
L.IsSemiformula (L.bv p) p
@[simp]
theorem
LO.Arith.Language.IsSemiformula.rel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
{r : V}
{v : V}
:
L.IsSemiformula n (LO.Arith.qqRel k r v) ↔ L.Rel k r ∧ L.IsSemitermVec k n v
@[simp]
theorem
LO.Arith.Language.IsSemiformula.nrel
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{k : V}
{r : V}
{v : V}
:
L.IsSemiformula n (LO.Arith.qqNRel k r v) ↔ L.Rel k r ∧ L.IsSemitermVec k n v
@[simp]
theorem
LO.Arith.Language.IsSemiformula.verum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
:
L.IsSemiformula n LO.Arith.qqVerum
@[simp]
theorem
LO.Arith.Language.IsSemiformula.falsum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
:
L.IsSemiformula n LO.Arith.qqFalsum
@[simp]
theorem
LO.Arith.Language.IsSemiformula.and
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
{q : V}
:
L.IsSemiformula n (LO.Arith.qqAnd p q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q
@[simp]
theorem
LO.Arith.Language.IsSemiformula.or
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
{q : V}
:
L.IsSemiformula n (LO.Arith.qqOr p q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q
@[simp]
theorem
LO.Arith.Language.IsSemiformula.all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n (LO.Arith.qqAll p) ↔ L.IsSemiformula (n + 1) p
@[simp]
theorem
LO.Arith.Language.IsSemiformula.ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n (LO.Arith.qqEx p) ↔ L.IsSemiformula (n + 1) p
theorem
LO.Arith.Language.IsSemiformula.case_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
:
L.IsSemiformula n p ↔ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsSemitermVec k n v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsSemitermVec k n v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ ∧ L.IsSemiformula n p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ ∧ L.IsSemiformula n p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ ∧ p = LO.Arith.qqEx p₁
theorem
LO.Arith.Language.IsSemiformula.case
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{P : V → V → Prop}
{n : V}
{p : V}
(hp : L.IsSemiformula n p)
(hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v))
(hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v))
(hverum : ∀ (n : V), P n LO.Arith.qqVerum)
(hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum)
(hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n (LO.Arith.qqAnd p q))
(hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n (LO.Arith.qqOr p q))
(hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P n (LO.Arith.qqAll p))
(hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P n (LO.Arith.qqEx p))
:
P n p
theorem
LO.Arith.Language.IsSemiformula.induction_sigma1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{P : V → V → Prop}
(hP : 𝚺₁-Relation P)
(hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v))
(hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v))
(hverum : ∀ (n : V), P n LO.Arith.qqVerum)
(hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum)
(hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqAnd p q))
(hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqOr p q))
(hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqAll p))
(hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqEx p))
{n : V}
{p : V}
:
L.IsSemiformula n p → P n p
theorem
LO.Arith.Language.IsSemiformula.induction_pi1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{P : V → V → Prop}
(hP : 𝚷₁-Relation P)
(hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v))
(hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v))
(hverum : ∀ (n : V), P n LO.Arith.qqVerum)
(hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum)
(hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqAnd p q))
(hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqOr p q))
(hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqAll p))
(hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqEx p))
{n : V}
{p : V}
:
L.IsSemiformula n p → P n p
theorem
LO.Arith.Language.IsSemiformula.induction1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(Γ : LO.SigmaPiDelta)
{P : V → V → Prop}
(hP : { Γ := Γ, rank := 1 }-Relation P)
(hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v))
(hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v))
(hverum : ∀ (n : V), P n LO.Arith.qqVerum)
(hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum)
(hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqAnd p q))
(hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqOr p q))
(hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqAll p))
(hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqEx p))
{n : V}
{p : V}
:
L.IsSemiformula n p → P n p
theorem
LO.Arith.Language.IsSemiformula.pos
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{n : V}
{p : V}
(h : L.IsSemiformula n p)
:
0 < p
@[simp]
theorem
LO.Arith.Language.IsSemiformula.not_zero
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(m : V)
:
¬L.IsSemiformula m 0
theorem
LO.Arith.Language.UformulaRec1.Construction.semiformula_result_induction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{β : LO.Arith.Language.UformulaRec1.Blueprint pL}
{c : LO.Arith.Language.UformulaRec1.Construction V L β}
{P : V → V → V → V → Prop}
(hP : 𝚺₁-Relation₄ P)
(hRel : ∀ (n param k R v : V), L.Rel k R → L.IsSemitermVec k n v → P param n (LO.Arith.qqRel k R v) (c.rel param k R v))
(hNRel : ∀ (n param k R v : V), L.Rel k R → L.IsSemitermVec k n v → P param n (LO.Arith.qqNRel k R v) (c.nrel param k R v))
(hverum : ∀ (n param : V), P param n LO.Arith.qqVerum (c.verum param))
(hfalsum : ∀ (n param : V), P param n LO.Arith.qqFalsum (c.falsum param))
(hand : ∀ (n param p q : V),
L.IsSemiformula n p →
L.IsSemiformula n q →
P param n p (c.result param p) →
P param n q (c.result param q) →
P param n (LO.Arith.qqAnd p q) (c.and param p q (c.result param p) (c.result param q)))
(hor : ∀ (n param p q : V),
L.IsSemiformula n p →
L.IsSemiformula n q →
P param n p (c.result param p) →
P param n q (c.result param q) →
P param n (LO.Arith.qqOr p q) (c.or param p q (c.result param p) (c.result param q)))
(hall : ∀ (n param p : V),
L.IsSemiformula (n + 1) p →
P (c.allChanges param) (n + 1) p (c.result (c.allChanges param) p) →
P param n (LO.Arith.qqAll p) (c.all param p (c.result (c.allChanges param) p)))
(hex : ∀ (n param p : V),
L.IsSemiformula (n + 1) p →
P (c.exChanges param) (n + 1) p (c.result (c.exChanges param) p) →
P param n (LO.Arith.qqEx p) (c.ex param p (c.result (c.exChanges param) p)))
{param : V}
{n : V}
{p : V}
:
L.IsSemiformula n p → P param n p (c.result param p)