def
LO.Arith.Language.IsFormulaSet
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(s : V)
:
Equations
- L.IsFormulaSet s = ∀ p ∈ s, L.IsFormula p
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.isFormulaSet_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚫₁-Predicate L.IsFormulaSet via pL.isFormulaSetDef
instance
LO.Arith.Language.isFormulaSet_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚫₁-Predicate L.IsFormulaSet
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.isFormulaSet_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.IsFormulaSet
Equations
- ⋯ = ⋯
@[simp]
theorem
LO.Arith.Language.IsFormulaSet.empty
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
L.IsFormulaSet ∅
@[simp]
theorem
LO.Arith.Language.IsFormulaSet.singleton
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
:
L.IsFormulaSet {p} ↔ L.IsFormula p
@[simp]
theorem
LO.Arith.Language.IsFormulaSet.insert_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{s : V}
:
theorem
LO.Arith.Language.IsFormulaSet.insert
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{s : V}
:
Alias of the forward direction of LO.Arith.Language.IsFormulaSet.insert_iff
.
@[simp]
theorem
LO.Arith.Language.IsFormulaSet.union
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{s₁ : V}
{s₂ : V}
:
theorem
LO.Arith.setShift_existsUnique
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(s : V)
:
def
LO.Arith.Language.setShift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(s : V)
:
V
Equations
- L.setShift s = Classical.choose! ⋯
Instances For
theorem
LO.Arith.mem_setShift_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{s : V}
{y : V}
:
theorem
LO.Arith.Language.IsFormulaSet.setShift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{s : V}
(h : L.IsFormulaSet s)
:
L.IsFormulaSet (L.setShift s)
theorem
LO.Arith.shift_mem_setShift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : V}
{s : V}
(h : p ∈ s)
:
L.shift p ∈ L.setShift s
@[simp]
theorem
LO.Arith.Language.IsFormulaSet.setShift_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{s : V}
:
L.IsFormulaSet (L.setShift s) ↔ L.IsFormulaSet s
@[simp]
theorem
LO.Arith.mem_setShift_union
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{s : V}
{t : V}
:
@[simp]
theorem
LO.Arith.mem_setShift_insert
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{x : V}
{s : V}
:
@[simp]
theorem
LO.Arith.setShift_empty
{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
theorem
LO.Arith.Language.setShift_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.setShift via pL.setShiftDef
instance
LO.Arith.Language.setShift_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
𝚺₁-Function₁ L.setShift
Equations
- ⋯ = ⋯
Equations
- LO.Arith.axL s p = ⟪s, ⟪0, p⟫⟫ + 1
Instances For
Equations
- LO.Arith.verumIntro s = ⟪s, ⟪1, 0⟫⟫ + 1
Instances For
def
LO.Arith.andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dp : V)
(dq : V)
:
V
Equations
- LO.Arith.andIntro s p q dp dq = ⟪s, ⟪2, ⟪p, ⟪q, ⟪dp, dq⟫⟫⟫⟫⟫ + 1
Instances For
def
LO.Arith.orIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(d : V)
:
V
Equations
- LO.Arith.orIntro s p q d = ⟪s, ⟪3, ⟪p, ⟪q, d⟫⟫⟫⟫ + 1
Instances For
Equations
- LO.Arith.allIntro s p d = ⟪s, ⟪4, ⟪p, d⟫⟫⟫ + 1
Instances For
def
LO.Arith.exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(t : V)
(d : V)
:
V
Equations
- LO.Arith.exIntro s p t d = ⟪s, ⟪5, ⟪p, ⟪t, d⟫⟫⟫⟫ + 1
Instances For
Equations
- LO.Arith.wkRule s d = ⟪s, ⟪6, d⟫⟫ + 1
Instances For
Equations
- LO.Arith.shiftRule s d = ⟪s, ⟪7, d⟫⟫ + 1
Instances For
def
LO.Arith.cutRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d₁ : V)
(d₂ : V)
:
V
Equations
- LO.Arith.cutRule s p d₁ d₂ = ⟪s, ⟪8, ⟪p, ⟪d₁, d₂⟫⟫⟫⟫ + 1
Instances For
Equations
- LO.Arith.root s p = ⟪s, ⟪9, p⟫⟫ + 1
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.axL_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.axL via LO.FirstOrder.Arith.axLDef
@[simp]
theorem
LO.Arith.eval_axLDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.axLDef) ↔ v 0 = LO.Arith.axL (v 1) (v 2)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.verumIntro_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₁ LO.Arith.verumIntro via LO.FirstOrder.Arith.verumIntroDef
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.andIntro_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₅ LO.Arith.andIntro via LO.FirstOrder.Arith.andIntroDef
@[simp]
theorem
LO.Arith.eval_andIntroDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 6 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.andIntroDef) ↔ v 0 = LO.Arith.andIntro (v 1) (v 2) (v 3) (v 4) (v 5)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.orIntro_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₄ LO.Arith.orIntro via LO.FirstOrder.Arith.orIntroDef
@[simp]
theorem
LO.Arith.eval_orIntroDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 5 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.orIntroDef) ↔ v 0 = LO.Arith.orIntro (v 1) (v 2) (v 3) (v 4)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.allIntro_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₃ LO.Arith.allIntro via LO.FirstOrder.Arith.allIntroDef
@[simp]
theorem
LO.Arith.eval_allIntroDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 4 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.allIntroDef) ↔ v 0 = LO.Arith.allIntro (v 1) (v 2) (v 3)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.exIntro_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₄ LO.Arith.exIntro via LO.FirstOrder.Arith.exIntroDef
@[simp]
theorem
LO.Arith.eval_exIntroDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 5 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.exIntroDef) ↔ v 0 = LO.Arith.exIntro (v 1) (v 2) (v 3) (v 4)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.wkRule_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.wkRule via LO.FirstOrder.Arith.wkRuleDef
@[simp]
theorem
LO.Arith.eval_wkRuleDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.wkRuleDef) ↔ v 0 = LO.Arith.wkRule (v 1) (v 2)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.shiftRule_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.shiftRule via LO.FirstOrder.Arith.shiftRuleDef
@[simp]
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.cutRule_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₄ LO.Arith.cutRule via LO.FirstOrder.Arith.cutRuleDef
@[simp]
theorem
LO.Arith.eval_cutRuleDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 5 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.cutRuleDef) ↔ v 0 = LO.Arith.cutRule (v 1) (v 2) (v 3) (v 4)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.root_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
:
𝚺₀-Function₂ LO.Arith.root via LO.FirstOrder.Arith.rootDef
@[simp]
theorem
LO.Arith.eval_rootDef
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(v : Fin 3 → V)
:
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.rootDef) ↔ v 0 = LO.Arith.root (v 1) (v 2)
@[simp]
theorem
LO.Arith.seq_lt_axL
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
:
s < LO.Arith.axL s p
@[simp]
theorem
LO.Arith.arity_lt_axL
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
:
p < LO.Arith.axL s p
@[simp]
theorem
LO.Arith.seq_lt_verumIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
:
s < LO.Arith.verumIntro s
@[simp]
theorem
LO.Arith.seq_lt_andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dp : V)
(dq : V)
:
s < LO.Arith.andIntro s p q dp dq
@[simp]
theorem
LO.Arith.p_lt_andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dp : V)
(dq : V)
:
p < LO.Arith.andIntro s p q dp dq
@[simp]
theorem
LO.Arith.q_lt_andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dp : V)
(dq : V)
:
q < LO.Arith.andIntro s p q dp dq
@[simp]
theorem
LO.Arith.dp_lt_andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dp : V)
(dq : V)
:
dp < LO.Arith.andIntro s p q dp dq
@[simp]
theorem
LO.Arith.dq_lt_andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dp : V)
(dq : V)
:
dq < LO.Arith.andIntro s p q dp dq
@[simp]
theorem
LO.Arith.seq_lt_orIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(d : V)
:
s < LO.Arith.orIntro s p q d
@[simp]
theorem
LO.Arith.p_lt_orIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(d : V)
:
p < LO.Arith.orIntro s p q d
@[simp]
theorem
LO.Arith.q_lt_orIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(d : V)
:
q < LO.Arith.orIntro s p q d
@[simp]
theorem
LO.Arith.d_lt_orIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(d : V)
:
d < LO.Arith.orIntro s p q d
@[simp]
theorem
LO.Arith.seq_lt_allIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d : V)
:
s < LO.Arith.allIntro s p d
@[simp]
theorem
LO.Arith.p_lt_allIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d : V)
:
p < LO.Arith.allIntro s p d
@[simp]
theorem
LO.Arith.s_lt_allIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d : V)
:
d < LO.Arith.allIntro s p d
@[simp]
theorem
LO.Arith.seq_lt_exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(t : V)
(d : V)
:
s < LO.Arith.exIntro s p t d
@[simp]
theorem
LO.Arith.p_lt_exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(t : V)
(d : V)
:
p < LO.Arith.exIntro s p t d
@[simp]
theorem
LO.Arith.t_lt_exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(t : V)
(d : V)
:
t < LO.Arith.exIntro s p t d
@[simp]
theorem
LO.Arith.d_lt_exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(t : V)
(d : V)
:
d < LO.Arith.exIntro s p t d
@[simp]
theorem
LO.Arith.seq_lt_wkRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(d : V)
:
s < LO.Arith.wkRule s d
@[simp]
theorem
LO.Arith.d_lt_wkRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(d : V)
:
d < LO.Arith.wkRule s d
@[simp]
theorem
LO.Arith.seq_lt_shiftRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(d : V)
:
s < LO.Arith.shiftRule s d
@[simp]
theorem
LO.Arith.d_lt_shiftRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(d : V)
:
d < LO.Arith.shiftRule s d
@[simp]
theorem
LO.Arith.seq_lt_cutRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d₁ : V)
(d₂ : V)
:
s < LO.Arith.cutRule s p d₁ d₂
@[simp]
theorem
LO.Arith.p_lt_cutRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d₁ : V)
(d₂ : V)
:
p < LO.Arith.cutRule s p d₁ d₂
@[simp]
theorem
LO.Arith.d₁_lt_cutRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d₁ : V)
(d₂ : V)
:
d₁ < LO.Arith.cutRule s p d₁ d₂
@[simp]
theorem
LO.Arith.d₂_lt_cutRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d₁ : V)
(d₂ : V)
:
d₂ < LO.Arith.cutRule s p d₁ d₂
@[simp]
theorem
LO.Arith.seq_lt_root
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
:
s < LO.Arith.root s p
@[simp]
theorem
LO.Arith.p_lt_root
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
:
p < LO.Arith.root s p
@[simp]
theorem
LO.Arith.fstIdx_axL
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
:
LO.Arith.fstIdx (LO.Arith.axL s p) = s
@[simp]
@[simp]
theorem
LO.Arith.fstIdx_andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dp : V)
(dq : V)
:
LO.Arith.fstIdx (LO.Arith.andIntro s p q dp dq) = s
@[simp]
theorem
LO.Arith.fstIdx_orIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(q : V)
(dpq : V)
:
LO.Arith.fstIdx (LO.Arith.orIntro s p q dpq) = s
@[simp]
theorem
LO.Arith.fstIdx_allIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d : V)
:
LO.Arith.fstIdx (LO.Arith.allIntro s p d) = s
@[simp]
theorem
LO.Arith.fstIdx_exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(t : V)
(d : V)
:
LO.Arith.fstIdx (LO.Arith.exIntro s p t d) = s
@[simp]
theorem
LO.Arith.fstIdx_wkRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(d : V)
:
LO.Arith.fstIdx (LO.Arith.wkRule s d) = s
@[simp]
theorem
LO.Arith.fstIdx_shiftRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(d : V)
:
LO.Arith.fstIdx (LO.Arith.shiftRule s d) = s
@[simp]
theorem
LO.Arith.fstIdx_cutRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
(d₁ : V)
(d₂ : V)
:
LO.Arith.fstIdx (LO.Arith.cutRule s p d₁ d₂) = s
@[simp]
theorem
LO.Arith.fstIdx_root
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(s : V)
(p : V)
:
LO.Arith.fstIdx (LO.Arith.root s p) = s
@[reducible, inline]
Equations
Instances For
def
LO.Arith.Derivation.Phi
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
(C : Set V)
(d : 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
def
LO.Arith.Derivation.construction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
Equations
- LO.Arith.Derivation.construction T = { Φ := fun (x : Fin 0 → V) => LO.Arith.Derivation.Phi T, defined := ⋯, monotone := ⋯ }
Instances For
instance
LO.Arith.Derivation.instStrongFiniteConstruction
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
Equations
- LO.Arith.Derivation.instStrongFiniteConstruction T = { strong_finite := ⋯ }
def
LO.Arith.Language.Theory.Derivation
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
V → Prop
Equations
- T.Derivation = (LO.Arith.Derivation.construction T).Fixpoint ![]
Instances For
def
LO.Arith.Language.Theory.DerivationOf
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
(d : V)
(s : V)
:
Equations
- T.DerivationOf d s = (LO.Arith.fstIdx d = s ∧ T.Derivation d)
Instances For
def
LO.Arith.Language.Theory.Derivable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
(s : V)
:
Equations
- T.Derivable s = ∃ (d : V), T.DerivationOf d s
Instances For
def
LO.Arith.Language.Theory.Provable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
(p : V)
:
Equations
- T.Provable p = T.Derivable {p}
Instances For
def
LO.FirstOrder.Arith.LDef.TDef.derivationDef
{pL : LO.FirstOrder.Arith.LDef}
(pT : pL.TDef)
:
𝚫₁.Semisentence 1
Equations
- pT.derivationDef = (LO.Arith.Derivation.blueprint pT).fixpointDefΔ₁
Instances For
theorem
LO.Arith.Language.Theory.derivation_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
𝚫₁-Predicate T.Derivation via pT.derivationDef
instance
LO.Arith.Language.Theory.derivation_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
𝚫₁-Predicate T.Derivation
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.Theory.derivation_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
{ Γ := Γ, rank := m + 1 }-Predicate T.Derivation
Equations
- ⋯ = ⋯
def
LO.FirstOrder.Arith.LDef.TDef.derivationOfDef
{pL : LO.FirstOrder.Arith.LDef}
(pT : pL.TDef)
:
𝚫₁.Semisentence 2
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.Theory.derivationOf_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
instance
LO.Arith.Language.Theory.derivationOf_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.Theory.derivationOf_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
{Γ : LO.SigmaPiDelta}
{m : ℕ}
:
Equations
- ⋯ = ⋯
def
LO.FirstOrder.Arith.LDef.TDef.derivableDef
{pL : LO.FirstOrder.Arith.LDef}
(pT : pL.TDef)
:
𝚺₁.Semisentence 1
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.Theory.derivable_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
𝚺₁-Predicate T.Derivable via pT.derivableDef
instance
LO.Arith.Language.Theory.derivable_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
𝚺₁-Predicate T.Derivable
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.Theory.derivable_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
{ Γ := 𝚺, rank := 0 + 1 }-Predicate T.Derivable
instance for definability tactic
Equations
- ⋯ = ⋯
def
LO.FirstOrder.Arith.LDef.TDef.prv
{pL : LO.FirstOrder.Arith.LDef}
(pT : pL.TDef)
:
𝚺₁.Semisentence 1
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.Theory.provable_defined
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
𝚺₁-Predicate T.Provable via pT.prv
instance
LO.Arith.Language.Theory.provable_definable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
𝚺₁-Predicate T.Provable
Equations
- ⋯ = ⋯
instance
LO.Arith.Language.Theory.provable_definable'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.Theory)
{pT : pL.TDef}
[T.Defined pT]
:
{ Γ := 𝚺, rank := 0 + 1 }-Predicate T.Provable
instance for definability tactic
Equations
- ⋯ = ⋯
theorem
LO.Arith.Language.Theory.Derivation.case_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{d : V}
:
T.Derivation d ↔ L.IsFormulaSet (LO.Arith.fstIdx d) ∧ ((∃ (s : V) (p : V), d = LO.Arith.axL s p ∧ p ∈ s ∧ L.neg p ∈ s) ∨ (∃ (s : V), d = LO.Arith.verumIntro s ∧ LO.Arith.qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V),
d = LO.Arith.andIntro s p q dp dq ∧ LO.Arith.qqAnd p q ∈ s ∧ T.DerivationOf dp (insert p s) ∧ T.DerivationOf dq (insert q s)) ∨ (∃ (s : V) (p : V) (q : V) (dpq : V),
d = LO.Arith.orIntro s p q dpq ∧ LO.Arith.qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V),
d = LO.Arith.allIntro s p dp ∧ LO.Arith.qqAll p ∈ s ∧ T.DerivationOf dp (insert (L.free p) (L.setShift s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V),
d = LO.Arith.exIntro s p t dp ∧ LO.Arith.qqEx p ∈ s ∧ L.IsTerm t ∧ T.DerivationOf dp (insert (L.substs₁ t p) s)) ∨ (∃ (s : V) (d' : V), d = LO.Arith.wkRule s d' ∧ LO.Arith.fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V),
d = LO.Arith.shiftRule s d' ∧ s = L.setShift (LO.Arith.fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V),
d = LO.Arith.cutRule s p d₁ d₂ ∧ T.DerivationOf d₁ (insert p s) ∧ T.DerivationOf d₂ (insert (L.neg p) s)) ∨ ∃ (s : V) (p : V), d = LO.Arith.root s p ∧ p ∈ s ∧ p ∈ T)
theorem
LO.Arith.Language.Theory.Derivation.mk
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{d : V}
:
L.IsFormulaSet (LO.Arith.fstIdx d) ∧ ((∃ (s : V) (p : V), d = LO.Arith.axL s p ∧ p ∈ s ∧ L.neg p ∈ s) ∨ (∃ (s : V), d = LO.Arith.verumIntro s ∧ LO.Arith.qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V),
d = LO.Arith.andIntro s p q dp dq ∧ LO.Arith.qqAnd p q ∈ s ∧ T.DerivationOf dp (insert p s) ∧ T.DerivationOf dq (insert q s)) ∨ (∃ (s : V) (p : V) (q : V) (dpq : V),
d = LO.Arith.orIntro s p q dpq ∧ LO.Arith.qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V),
d = LO.Arith.allIntro s p dp ∧ LO.Arith.qqAll p ∈ s ∧ T.DerivationOf dp (insert (L.free p) (L.setShift s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V),
d = LO.Arith.exIntro s p t dp ∧ LO.Arith.qqEx p ∈ s ∧ L.IsTerm t ∧ T.DerivationOf dp (insert (L.substs₁ t p) s)) ∨ (∃ (s : V) (d' : V), d = LO.Arith.wkRule s d' ∧ LO.Arith.fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V),
d = LO.Arith.shiftRule s d' ∧ s = L.setShift (LO.Arith.fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V),
d = LO.Arith.cutRule s p d₁ d₂ ∧ T.DerivationOf d₁ (insert p s) ∧ T.DerivationOf d₂ (insert (L.neg p) s)) ∨ ∃ (s : V) (p : V), d = LO.Arith.root s p ∧ p ∈ s ∧ p ∈ T) →
T.Derivation d
Alias of the reverse direction of LO.Arith.Language.Theory.Derivation.case_iff
.
theorem
LO.Arith.Language.Theory.Derivation.case
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{d : V}
:
T.Derivation d →
L.IsFormulaSet (LO.Arith.fstIdx d) ∧ ((∃ (s : V) (p : V), d = LO.Arith.axL s p ∧ p ∈ s ∧ L.neg p ∈ s) ∨ (∃ (s : V), d = LO.Arith.verumIntro s ∧ LO.Arith.qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V),
d = LO.Arith.andIntro s p q dp dq ∧ LO.Arith.qqAnd p q ∈ s ∧ T.DerivationOf dp (insert p s) ∧ T.DerivationOf dq (insert q s)) ∨ (∃ (s : V) (p : V) (q : V) (dpq : V),
d = LO.Arith.orIntro s p q dpq ∧ LO.Arith.qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V),
d = LO.Arith.allIntro s p dp ∧ LO.Arith.qqAll p ∈ s ∧ T.DerivationOf dp (insert (L.free p) (L.setShift s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V),
d = LO.Arith.exIntro s p t dp ∧ LO.Arith.qqEx p ∈ s ∧ L.IsTerm t ∧ T.DerivationOf dp (insert (L.substs₁ t p) s)) ∨ (∃ (s : V) (d' : V), d = LO.Arith.wkRule s d' ∧ LO.Arith.fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V),
d = LO.Arith.shiftRule s d' ∧ s = L.setShift (LO.Arith.fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V),
d = LO.Arith.cutRule s p d₁ d₂ ∧ T.DerivationOf d₁ (insert p s) ∧ T.DerivationOf d₂ (insert (L.neg p) s)) ∨ ∃ (s : V) (p : V), d = LO.Arith.root s p ∧ p ∈ s ∧ p ∈ T)
Alias of the forward direction of LO.Arith.Language.Theory.Derivation.case_iff
.
theorem
LO.Arith.Language.Theory.Derivation.induction1
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
(Γ : LO.SigmaPiDelta)
{P : V → Prop}
(hP : { Γ := Γ, rank := 1 }-Predicate P)
{d : V}
(hd : T.Derivation d)
(hAxL : ∀ (s : V), L.IsFormulaSet s → ∀ p ∈ s, L.neg p ∈ s → P (LO.Arith.axL s p))
(hVerumIntro : ∀ (s : V), L.IsFormulaSet s → LO.Arith.qqVerum ∈ s → P (LO.Arith.verumIntro s))
(hAnd : ∀ (s : V),
L.IsFormulaSet s →
∀ (p q dp dq : V),
LO.Arith.qqAnd p q ∈ s →
T.DerivationOf dp (insert p s) →
T.DerivationOf dq (insert q s) → P dp → P dq → P (LO.Arith.andIntro s p q dp dq))
(hOr : ∀ (s : V),
L.IsFormulaSet s →
∀ (p q d : V), LO.Arith.qqOr p q ∈ s → T.DerivationOf d (insert p (insert q s)) → P d → P (LO.Arith.orIntro s p q d))
(hAll : ∀ (s : V),
L.IsFormulaSet s →
∀ (p d : V),
LO.Arith.qqAll p ∈ s → T.DerivationOf d (insert (L.free p) (L.setShift s)) → P d → P (LO.Arith.allIntro s p d))
(hEx : ∀ (s : V),
L.IsFormulaSet s →
∀ (p t d : V),
LO.Arith.qqEx p ∈ s →
L.IsTerm t → T.DerivationOf d (insert (L.substs₁ t p) s) → P d → P (LO.Arith.exIntro s p t d))
(hWk : ∀ (s : V), L.IsFormulaSet s → ∀ (d : V), LO.Arith.fstIdx d ⊆ s → T.Derivation d → P d → P (LO.Arith.wkRule s d))
(hShift : ∀ (s : V),
L.IsFormulaSet s → ∀ (d : V), s = L.setShift (LO.Arith.fstIdx d) → T.Derivation d → P d → P (LO.Arith.shiftRule s d))
(hCut : ∀ (s : V),
L.IsFormulaSet s →
∀ (p d₁ d₂ : V),
T.DerivationOf d₁ (insert p s) →
T.DerivationOf d₂ (insert (L.neg p) s) → P d₁ → P d₂ → P (LO.Arith.cutRule s p d₁ d₂))
(hRoot : ∀ (s : V), L.IsFormulaSet s → ∀ p ∈ s, p ∈ T → P (LO.Arith.root s p))
:
P d
theorem
LO.Arith.Language.Theory.Derivation.isFormulaSet
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{d : V}
(h : T.Derivation d)
:
L.IsFormulaSet (LO.Arith.fstIdx d)
theorem
LO.Arith.Language.Theory.DerivationOf.isFormulaSet
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{d : V}
{s : V}
(h : T.DerivationOf d s)
:
L.IsFormulaSet s
theorem
LO.Arith.Language.Theory.Derivation.axL
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
(hs : L.IsFormulaSet s)
(h : p ∈ s)
(hn : L.neg p ∈ s)
:
T.Derivation (LO.Arith.axL s p)
theorem
LO.Arith.Language.Theory.Derivation.verumIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
(hs : L.IsFormulaSet s)
(h : LO.Arith.qqVerum ∈ s)
:
T.Derivation (LO.Arith.verumIntro s)
theorem
LO.Arith.Language.Theory.Derivation.andIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{q : V}
{dp : V}
{dq : V}
(h : LO.Arith.qqAnd p q ∈ s)
(hdp : T.DerivationOf dp (insert p s))
(hdq : T.DerivationOf dq (insert q s))
:
T.Derivation (LO.Arith.andIntro s p q dp dq)
theorem
LO.Arith.Language.Theory.Derivation.orIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{q : V}
{dpq : V}
(h : LO.Arith.qqOr p q ∈ s)
(hdpq : T.DerivationOf dpq (insert p (insert q s)))
:
T.Derivation (LO.Arith.orIntro s p q dpq)
theorem
LO.Arith.Language.Theory.Derivation.allIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{dp : V}
(h : LO.Arith.qqAll p ∈ s)
(hdp : T.DerivationOf dp (insert (L.free p) (L.setShift s)))
:
T.Derivation (LO.Arith.allIntro s p dp)
theorem
LO.Arith.Language.Theory.Derivation.exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{t : V}
{dp : V}
(h : LO.Arith.qqEx p ∈ s)
(ht : L.IsTerm t)
(hdp : T.DerivationOf dp (insert (L.substs₁ t p) s))
:
T.Derivation (LO.Arith.exIntro s p t dp)
theorem
LO.Arith.Language.Theory.Derivation.wkRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{s' : V}
{d : V}
(hs : L.IsFormulaSet s)
(h : s' ⊆ s)
(hd : T.DerivationOf d s')
:
T.Derivation (LO.Arith.wkRule s d)
theorem
LO.Arith.Language.Theory.Derivation.shiftRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{d : V}
(hd : T.DerivationOf d s)
:
T.Derivation (LO.Arith.shiftRule (L.setShift s) d)
theorem
LO.Arith.Language.Theory.Derivation.cutRule
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{d₁ : V}
{d₂ : V}
(hd₁ : T.DerivationOf d₁ (insert p s))
(hd₂ : T.DerivationOf d₂ (insert (L.neg p) s))
:
T.Derivation (LO.Arith.cutRule s p d₁ d₂)
theorem
LO.Arith.Language.Theory.Derivation.root
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
(hs : L.IsFormulaSet s)
(hp : p ∈ s)
(hT : p ∈ T)
:
T.Derivation (LO.Arith.root s p)
theorem
LO.Arith.Language.Theory.Derivation.of_ss
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{U : L.Theory}
{pU : pL.TDef}
[U.Defined pU]
(h : T ⊆ U)
{d : V}
:
T.Derivation d → U.Derivation d
theorem
LO.Arith.Language.Theory.Derivable.isFormulaSet
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
(h : T.Derivable s)
:
L.IsFormulaSet s
theorem
LO.Arith.Language.Theory.Derivable.em
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
(hs : L.IsFormulaSet s)
(p : V)
(h : p ∈ s)
(hn : L.neg p ∈ s)
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.verum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
(hs : L.IsFormulaSet s)
(h : LO.Arith.qqVerum ∈ s)
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.and_m
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{q : V}
(h : LO.Arith.qqAnd p q ∈ s)
(hp : T.Derivable (insert p s))
(hq : T.Derivable (insert q s))
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.or_m
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{q : V}
(h : LO.Arith.qqOr p q ∈ s)
(hpq : T.Derivable (insert p (insert q s)))
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.all_m
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
(h : LO.Arith.qqAll p ∈ s)
(hp : T.Derivable (insert (L.free p) (L.setShift s)))
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.ex_m
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{t : V}
(h : LO.Arith.qqEx p ∈ s)
(ht : L.IsTerm t)
(hp : T.Derivable (insert (L.substs₁ t p) s))
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.wk
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{s' : V}
(hs : L.IsFormulaSet s)
(h : s' ⊆ s)
(hd : T.Derivable s')
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
(hd : T.Derivable s)
:
T.Derivable (L.setShift s)
theorem
LO.Arith.Language.Theory.Derivable.ofSetEq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{s' : V}
(h : ∀ (x : V), x ∈ s' ↔ x ∈ s)
(hd : T.Derivable s')
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.cut
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
(p : V)
(hd₁ : T.Derivable (insert p s))
(hd₂ : T.Derivable (insert (L.neg p) s))
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.by_axm
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
(hs : L.IsFormulaSet s)
(p : V)
(hp : p ∈ s)
(hT : p ∈ T)
:
T.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.of_ss
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{U : L.Theory}
{pU : pL.TDef}
[U.Defined pU]
(h : T ⊆ U)
{s : V}
:
T.Derivable s → U.Derivable s
theorem
LO.Arith.Language.Theory.Derivable.and
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{q : V}
(hp : T.Derivable (insert p s))
(hq : T.Derivable (insert q s))
:
T.Derivable (insert (LO.Arith.qqAnd p q) s)
theorem
LO.Arith.Language.Theory.Derivable.or
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{q : V}
(hpq : T.Derivable (insert p (insert q s)))
:
T.Derivable (insert (LO.Arith.qqOr p q) s)
theorem
LO.Arith.Language.Theory.Derivable.conj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
(ps : V)
{s : V}
(hs : L.IsFormulaSet s)
(ds : ∀ i < LO.Arith.len ps, T.Derivable (insert (LO.Arith.nth ps i) s))
:
T.Derivable (insert (LO.Arith.qqConj ps) s)
Crucial inducion for formalized $\Sigma_1$-completeness.
theorem
LO.Arith.Language.Theory.Derivable.disjDistr
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
(ps : V)
(s : V)
(d : T.Derivable (LO.Arith.vecToSet ps ∪ s))
:
T.Derivable (insert (LO.Arith.qqDisj ps) s)
theorem
LO.Arith.Language.Theory.Derivable.disj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
(ps : V)
(s : V)
{i : V}
(hps : ∀ i < LO.Arith.len ps, L.IsFormula (LO.Arith.nth ps i))
(hi : i < LO.Arith.len ps)
(d : T.Derivable (insert (LO.Arith.nth ps i) s))
:
T.Derivable (insert (LO.Arith.qqDisj ps) s)
theorem
LO.Arith.Language.Theory.Derivable.all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
(hp : L.IsSemiformula 1 p)
(dp : T.Derivable (insert (L.free p) (L.setShift s)))
:
T.Derivable (insert (LO.Arith.qqAll p) s)
theorem
LO.Arith.Language.Theory.Derivable.ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.Theory}
{pT : pL.TDef}
[T.Defined pT]
{s : V}
{p : V}
{t : V}
(hp : L.IsSemiformula 1 p)
(ht : L.IsTerm t)
(dp : T.Derivable (insert (L.substs₁ t p) s))
:
T.Derivable (insert (LO.Arith.qqEx p) s)