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) : Prop

Equations

• L.IsFormulaSet s = ∀ p ∈ s, L.IsFormula p

def LO.FirstOrder.Arith.LDef.isFormulaSetDef (pL : LO.FirstOrder.Arith.LDef) : 𝚫₁.Semisentence 1

Equations

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

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} : L.IsFormulaSet (insert p s) ↔ L.IsFormula p ∧ L.IsFormulaSet s

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} : L.IsFormulaSet (insert p s) → L.IsFormula p ∧ L.IsFormulaSet s

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} : L.IsFormulaSet (s₁ ∪ s₂) ↔ L.IsFormulaSet s₁ ∧ L.IsFormulaSet s₂

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) : ∃! t : V, ∀ (y : V), y ∈ t ↔ ∃ x ∈ s, y = L.shift x

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

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} : y ∈ L.setShift s ↔ ∃ x ∈ s, y = L.shift x

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} : L.setShift (s ∪ t) = L.setShift s ∪ L.setShift t

@[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} : L.setShift (insert x s) = insert (L.shift x) (L.setShift s)

@[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] : L.setShift ∅ = ∅

def LO.FirstOrder.Arith.LDef.setShiftDef (pL : LO.FirstOrder.Arith.LDef) : 𝚺₁.Semisentence 2

Equations

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

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

• ⋯ = ⋯

def LO.Arith.axL {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) : V

Equations

• LO.Arith.axL s p = ⟪s, ⟪0, p⟫⟫ + 1

def LO.Arith.verumIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : V

Equations

• LO.Arith.verumIntro s = ⟪s, ⟪1, 0⟫⟫ + 1

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

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

def LO.Arith.allIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) (d : V) : V

Equations

• LO.Arith.allIntro s p d = ⟪s, ⟪4, ⟪p, d⟫⟫⟫ + 1

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

def LO.Arith.wkRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) : V

Equations

• LO.Arith.wkRule s d = ⟪s, ⟪6, d⟫⟫ + 1

def LO.Arith.shiftRule {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (d : V) : V

Equations

• LO.Arith.shiftRule s d = ⟪s, ⟪7, d⟫⟫ + 1

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

def LO.Arith.root {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) (p : V) : V

Equations

• LO.Arith.root s p = ⟪s, ⟪9, p⟫⟫ + 1

def LO.FirstOrder.Arith.axLDef : 𝚺₀.Semisentence 3

Equations

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

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)

def LO.FirstOrder.Arith.verumIntroDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.verumIntro_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.verumIntro via LO.FirstOrder.Arith.verumIntroDef

@[simp]

theorem LO.Arith.eval_verumIntroDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.verumIntroDef) ↔ v 0 = LO.Arith.verumIntro (v 1)

def LO.FirstOrder.Arith.andIntroDef : 𝚺₀.Semisentence 6

Equations

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

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)

def LO.FirstOrder.Arith.orIntroDef : 𝚺₀.Semisentence 5

Equations

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

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)

def LO.FirstOrder.Arith.allIntroDef : 𝚺₀.Semisentence 4

Equations

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

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)

def LO.FirstOrder.Arith.exIntroDef : 𝚺₀.Semisentence 5

Equations

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

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)

def LO.FirstOrder.Arith.wkRuleDef : 𝚺₀.Semisentence 3

Equations

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

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)

def LO.FirstOrder.Arith.shiftRuleDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.shiftRule_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ LO.Arith.shiftRule via LO.FirstOrder.Arith.shiftRuleDef

@[simp]

theorem LO.Arith.eval_shiftRuleDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.shiftRuleDef) ↔ v 0 = LO.Arith.shiftRule (v 1) (v 2)

def LO.FirstOrder.Arith.cutRuleDef : 𝚺₀.Semisentence 5

Equations

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

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)

def LO.FirstOrder.Arith.rootDef : 𝚺₀.Semisentence 3

Equations

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

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]

theorem LO.Arith.fstIdx_verumIntro {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (s : V) : LO.Arith.fstIdx (LO.Arith.verumIntro s) = s

@[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]

abbrev LO.Arith.Derivation.conseq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (x : V) : V

Equations

• LO.Arith.Derivation.conseq x = π₁ x

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) : Prop

Equations

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

def LO.Arith.Derivation.blueprint {pL : LO.FirstOrder.Arith.LDef} (pT : pL.TDef) : LO.Arith.Fixpoint.Blueprint 0

Equations

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

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] : LO.Arith.Fixpoint.Construction V (LO.Arith.Derivation.blueprint pT)

Equations

• LO.Arith.Derivation.construction T = { Φ := fun (x : Fin 0 → V) => LO.Arith.Derivation.Phi T, defined := ⋯, monotone := ⋯ }

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] : LO.Arith.Fixpoint.Construction.StrongFinite V (LO.Arith.Derivation.construction T)

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 ![]

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) : Prop

Equations

• T.DerivationOf d s = (LO.Arith.fstIdx d = s ∧ T.Derivation d)

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) : Prop

Equations

• T.Derivable s = ∃ (d : V), T.DerivationOf d s

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) : Prop

Equations

• T.Provable p = T.Derivable {p}

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Δ₁

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.

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] : 𝚫₁-Relation T.DerivationOf via pT.derivationOfDef

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] : 𝚫₁-Relation T.DerivationOf

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 : ℕ} : { Γ := Γ, rank := m + 1 }-Relation T.DerivationOf

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.

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.

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)