Derivation

def LO.Arith.Language.IsFormulaSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (s : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.isFormulaSet_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : FirstOrder.Arith.Dlt1-Predicate L.IsFormulaSet via pL.isFormulaSetDef

instance LO.Arith.Language.isFormulaSet_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : FirstOrder.Arith.Dlt1-Predicate L.IsFormulaSet

instance LO.Arith.Language.isFormulaSet_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Predicate L.IsFormulaSet

@[simp]

theorem LO.Arith.Language.IsFormulaSet.empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : L.IsFormulaSet ∅

@[simp]

theorem LO.Arith.Language.IsFormulaSet.singleton {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p s : V} : L.IsFormulaSet (Insert.insert p s) ↔ L.IsFormula p ∧ L.IsFormulaSet s

theorem LO.Arith.Language.IsFormulaSet.insert {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p s : V} : L.IsFormulaSet (Insert.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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {s₁ s₂ : V} : L.IsFormulaSet (s₁ ∪ s₂) ↔ L.IsFormulaSet s₁ ∧ L.IsFormulaSet s₂

theorem LO.Arith.setShift_existsUnique {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (s : V) : ∃! t : V, ∀ (y : V), y ∈ t ↔ ∃ x ∈ s, y = L.shift x

noncomputable def LO.Arith.Language.setShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (s : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• L.setShift s = Classical.choose! ⋯

theorem LO.Arith.mem_setShift_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {s y : V} : y ∈ L.setShift s ↔ ∃ x ∈ s, y = L.shift x

theorem LO.Arith.Language.IsFormulaSet.setShift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p s : V} (h : p ∈ s) : L.shift p ∈ L.setShift s

@[simp]

theorem LO.Arith.Language.IsFormulaSet.setShift_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {s t : V} : L.setShift (s ∪ t) = L.setShift s ∪ L.setShift t

@[simp]

theorem LO.Arith.mem_setShift_insert {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {x s : V} : L.setShift (insert x s) = insert (L.shift x) (L.setShift s)

@[simp]

theorem LO.Arith.setShift_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : L.setShift ∅ = ∅

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.setShift_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : FirstOrder.Arith.Sg1-Function₁ L.setShift via pL.setShiftDef

instance LO.Arith.Language.setShift_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : FirstOrder.Arith.Sg1-Function₁ L.setShift

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

noncomputable def LO.Arith.andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dp dq : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.andIntro s p q dp dq = ⟪s, ⟪2, ⟪p, ⟪q, ⟪dp, dq⟫⟫⟫⟫⟫ + 1

noncomputable def LO.Arith.orIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q d : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.orIntro s p q d = ⟪s, ⟪3, ⟪p, ⟪q, d⟫⟫⟫⟫ + 1

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

Imported declaration from the Incompleteness formalization.

Equations

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

noncomputable def LO.Arith.exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p t d : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.exIntro s p t d = ⟪s, ⟪5, ⟪p, ⟪t, d⟫⟫⟫⟫ + 1

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

noncomputable def LO.Arith.cutRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d₁ d₂ : V) : V

Imported declaration from the Incompleteness formalization.

Equations

• LO.Arith.cutRule s p d₁ d₂ = ⟪s, ⟪8, ⟪p, ⟪d₁, d₂⟫⟫⟫⟫ + 1

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.axLDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.axL_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₂ axL via FirstOrder.Arith.axLDef

@[simp]

theorem LO.Arith.eval_axLDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.axLDef) ↔ v 0 = axL (v 1) (v 2)

def LO.FirstOrder.Arith.verumIntroDef : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

def LO.FirstOrder.Arith.andIntroDef : Sg0.Semisentence 6

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.andIntro_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₅ andIntro via FirstOrder.Arith.andIntroDef

@[simp]

theorem LO.Arith.eval_andIntroDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 6 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.andIntroDef) ↔ v 0 = andIntro (v 1) (v 2) (v 3) (v 4) (v 5)

def LO.FirstOrder.Arith.orIntroDef : Sg0.Semisentence 5

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.orIntro_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₄ orIntro via FirstOrder.Arith.orIntroDef

@[simp]

theorem LO.Arith.eval_orIntroDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 5 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.orIntroDef) ↔ v 0 = orIntro (v 1) (v 2) (v 3) (v 4)

def LO.FirstOrder.Arith.allIntroDef : Sg0.Semisentence 4

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.allIntro_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₃ allIntro via FirstOrder.Arith.allIntroDef

@[simp]

theorem LO.Arith.eval_allIntroDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 4 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.allIntroDef) ↔ v 0 = allIntro (v 1) (v 2) (v 3)

def LO.FirstOrder.Arith.exIntroDef : Sg0.Semisentence 5

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.exIntro_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₄ exIntro via FirstOrder.Arith.exIntroDef

@[simp]

theorem LO.Arith.eval_exIntroDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 5 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.exIntroDef) ↔ v 0 = exIntro (v 1) (v 2) (v 3) (v 4)

def LO.FirstOrder.Arith.wkRuleDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.wkRule_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₂ wkRule via FirstOrder.Arith.wkRuleDef

@[simp]

theorem LO.Arith.eval_wkRuleDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.wkRuleDef) ↔ v 0 = wkRule (v 1) (v 2)

def LO.FirstOrder.Arith.shiftRuleDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

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

@[simp]

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

def LO.FirstOrder.Arith.cutRuleDef : Sg0.Semisentence 5

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.cutRule_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₄ cutRule via FirstOrder.Arith.cutRuleDef

@[simp]

theorem LO.Arith.eval_cutRuleDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 5 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.cutRuleDef) ↔ v 0 = cutRule (v 1) (v 2) (v 3) (v 4)

def LO.FirstOrder.Arith.rootDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.root_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] : FirstOrder.Arith.Sg0-Function₂ root via FirstOrder.Arith.rootDef

@[simp]

theorem LO.Arith.eval_rootDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (v : Fin 3 → V) : V ⊧/v (FirstOrder.Arith.HierarchySymbol.Semiformula.val FirstOrder.Arith.rootDef) ↔ v 0 = root (v 1) (v 2)

@[simp]

theorem LO.Arith.seq_lt_axL {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p : V) : s < axL s p

@[simp]

theorem LO.Arith.arity_lt_axL {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p : V) : p < axL s p

@[simp]

theorem LO.Arith.seq_lt_verumIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s : V) : s < verumIntro s

@[simp]

theorem LO.Arith.seq_lt_andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dp dq : V) : s < andIntro s p q dp dq

@[simp]

theorem LO.Arith.p_lt_andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dp dq : V) : p < andIntro s p q dp dq

@[simp]

theorem LO.Arith.q_lt_andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dp dq : V) : q < andIntro s p q dp dq

@[simp]

theorem LO.Arith.dp_lt_andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dp dq : V) : dp < andIntro s p q dp dq

@[simp]

theorem LO.Arith.dq_lt_andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dp dq : V) : dq < andIntro s p q dp dq

@[simp]

theorem LO.Arith.seq_lt_orIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q d : V) : s < orIntro s p q d

@[simp]

theorem LO.Arith.p_lt_orIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q d : V) : p < orIntro s p q d

@[simp]

theorem LO.Arith.q_lt_orIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q d : V) : q < orIntro s p q d

@[simp]

theorem LO.Arith.d_lt_orIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q d : V) : d < orIntro s p q d

@[simp]

theorem LO.Arith.seq_lt_allIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d : V) : s < allIntro s p d

@[simp]

theorem LO.Arith.p_lt_allIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d : V) : p < allIntro s p d

@[simp]

theorem LO.Arith.s_lt_allIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d : V) : d < allIntro s p d

@[simp]

theorem LO.Arith.seq_lt_exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p t d : V) : s < exIntro s p t d

@[simp]

theorem LO.Arith.p_lt_exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p t d : V) : p < exIntro s p t d

@[simp]

theorem LO.Arith.t_lt_exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p t d : V) : t < exIntro s p t d

@[simp]

theorem LO.Arith.d_lt_exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p t d : V) : d < exIntro s p t d

@[simp]

theorem LO.Arith.seq_lt_wkRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s d : V) : s < wkRule s d

@[simp]

theorem LO.Arith.d_lt_wkRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s d : V) : d < wkRule s d

@[simp]

theorem LO.Arith.seq_lt_shiftRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s d : V) : s < shiftRule s d

@[simp]

theorem LO.Arith.d_lt_shiftRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s d : V) : d < shiftRule s d

@[simp]

theorem LO.Arith.seq_lt_cutRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d₁ d₂ : V) : s < cutRule s p d₁ d₂

@[simp]

theorem LO.Arith.p_lt_cutRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d₁ d₂ : V) : p < cutRule s p d₁ d₂

@[simp]

theorem LO.Arith.d₁_lt_cutRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d₁ d₂ : V) : d₁ < cutRule s p d₁ d₂

@[simp]

theorem LO.Arith.d₂_lt_cutRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d₁ d₂ : V) : d₂ < cutRule s p d₁ d₂

@[simp]

theorem LO.Arith.seq_lt_root {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p : V) : s < root s p

@[simp]

theorem LO.Arith.p_lt_root {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p : V) : p < root s p

@[simp]

theorem LO.Arith.fstIdx_axL {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p : V) : fstIdx (axL s p) = s

@[simp]

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

@[simp]

theorem LO.Arith.fstIdx_andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dp dq : V) : fstIdx (andIntro s p q dp dq) = s

@[simp]

theorem LO.Arith.fstIdx_orIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p q dpq : V) : fstIdx (orIntro s p q dpq) = s

@[simp]

theorem LO.Arith.fstIdx_allIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d : V) : fstIdx (allIntro s p d) = s

@[simp]

theorem LO.Arith.fstIdx_exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p t d : V) : fstIdx (exIntro s p t d) = s

@[simp]

theorem LO.Arith.fstIdx_wkRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s d : V) : fstIdx (wkRule s d) = s

@[simp]

theorem LO.Arith.fstIdx_shiftRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s d : V) : fstIdx (shiftRule s d) = s

@[simp]

theorem LO.Arith.fstIdx_cutRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p d₁ d₂ : V) : fstIdx (cutRule s p d₁ d₂) = s

@[simp]

theorem LO.Arith.fstIdx_root {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (s p : V) : fstIdx (root s p) = s

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Arith.Derivation.Phi {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) (C : Set V) (d : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Arith.Derivation.construction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : Fixpoint.Construction V (blueprint pT)

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : Fixpoint.Construction.StrongFinite V (construction T)

def LO.Arith.Language.Theory.Derivation {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : V → Prop

Imported declaration from the Incompleteness formalization.

Equations

• T.Derivation = (LO.Arith.Derivation.construction T).Fixpoint ![]

def LO.Arith.Language.Theory.DerivationOf {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] (d s : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Arith.Language.Theory.Derivable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] (s : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Arith.Language.Theory.Provable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] (p : V) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.LDef.TDef.derivationDef {pL : LDef} (pT : pL.TDef) : Dlt1.Semisentence 1

Imported declaration from the Incompleteness formalization.

Equations

• pT.derivationDef = (LO.Arith.Derivation.blueprint pT).fixpointDefΔ₁

theorem LO.Arith.Language.Theory.derivation_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Dlt1-Predicate T.Derivation via pT.derivationDef

instance LO.Arith.Language.Theory.derivation_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Dlt1-Predicate T.Derivation

instance LO.Arith.Language.Theory.derivation_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Predicate T.Derivation

def LO.FirstOrder.Arith.LDef.TDef.derivationOfDef {pL : LDef} (pT : pL.TDef) : Dlt1.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.Theory.derivationOf_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Dlt1-Relation T.DerivationOf via pT.derivationOfDef

instance LO.Arith.Language.Theory.derivationOf_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Dlt1-Relation T.DerivationOf

instance LO.Arith.Language.Theory.derivationOf_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Relation T.DerivationOf

def LO.FirstOrder.Arith.LDef.TDef.derivableDef {pL : LDef} (pT : pL.TDef) : Sg1.Semisentence 1

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.Theory.derivable_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Sg1-Predicate T.Derivable via pT.derivableDef

instance LO.Arith.Language.Theory.derivable_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Sg1-Predicate T.Derivable

instance LO.Arith.Language.Theory.derivable_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : { Γ := Sg, rank := 0 + 1 }-Predicate T.Derivable

instance for definability tactic

def LO.FirstOrder.Arith.LDef.TDef.prv {pL : LDef} (pT : pL.TDef) : Sg1.Semisentence 1

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.Theory.provable_defined {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Sg1-Predicate T.Provable via pT.prv

instance LO.Arith.Language.Theory.provable_definable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : FirstOrder.Arith.Sg1-Predicate T.Provable

instance LO.Arith.Language.Theory.provable_definable' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : { Γ := Sg, rank := 0 + 1 }-Predicate T.Provable

instance for definability tactic

theorem LO.Arith.Language.Theory.Derivation.case_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} : T.Derivation d ↔ L.IsFormulaSet (fstIdx d) ∧ ((∃ (s : V) (p : V), d = Arith.axL s p ∧ p ∈ s ∧ L.neg p ∈ s) ∨ (∃ (s : V), d = Arith.verumIntro s ∧ qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = Arith.andIntro s p q dp dq ∧ 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 = Arith.orIntro s p q dpq ∧ qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V), d = Arith.allIntro s p dp ∧ qqAll p ∈ s ∧ T.DerivationOf dp (insert (L.free p) (L.setShift s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V), d = Arith.exIntro s p t dp ∧ qqEx p ∈ s ∧ L.IsTerm t ∧ T.DerivationOf dp (insert (L.substs₁ t p) s)) ∨ (∃ (s : V) (d' : V), d = Arith.wkRule s d' ∧ fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V), d = Arith.shiftRule s d' ∧ s = L.setShift (fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = 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 = Arith.root s p ∧ p ∈ s ∧ p ∈ T)

theorem LO.Arith.Language.Theory.Derivation.case {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} : T.Derivation d → L.IsFormulaSet (fstIdx d) ∧ ((∃ (s : V) (p : V), d = Arith.axL s p ∧ p ∈ s ∧ L.neg p ∈ s) ∨ (∃ (s : V), d = Arith.verumIntro s ∧ qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = Arith.andIntro s p q dp dq ∧ 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 = Arith.orIntro s p q dpq ∧ qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V), d = Arith.allIntro s p dp ∧ qqAll p ∈ s ∧ T.DerivationOf dp (insert (L.free p) (L.setShift s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V), d = Arith.exIntro s p t dp ∧ qqEx p ∈ s ∧ L.IsTerm t ∧ T.DerivationOf dp (insert (L.substs₁ t p) s)) ∨ (∃ (s : V) (d' : V), d = Arith.wkRule s d' ∧ fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V), d = Arith.shiftRule s d' ∧ s = L.setShift (fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = 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 = 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.mk {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} : L.IsFormulaSet (fstIdx d) ∧ ((∃ (s : V) (p : V), d = Arith.axL s p ∧ p ∈ s ∧ L.neg p ∈ s) ∨ (∃ (s : V), d = Arith.verumIntro s ∧ qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = Arith.andIntro s p q dp dq ∧ 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 = Arith.orIntro s p q dpq ∧ qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V), d = Arith.allIntro s p dp ∧ qqAll p ∈ s ∧ T.DerivationOf dp (insert (L.free p) (L.setShift s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V), d = Arith.exIntro s p t dp ∧ qqEx p ∈ s ∧ L.IsTerm t ∧ T.DerivationOf dp (insert (L.substs₁ t p) s)) ∨ (∃ (s : V) (d' : V), d = Arith.wkRule s d' ∧ fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V), d = Arith.shiftRule s d' ∧ s = L.setShift (fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = 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 = 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.induction1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] (Γ : 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 (Arith.axL s p)) (hVerumIntro : ∀ (s : V), L.IsFormulaSet s → qqVerum ∈ s → P (Arith.verumIntro s)) (hAnd : ∀ (s : V), L.IsFormulaSet s → ∀ (p q dp dq : V), qqAnd p q ∈ s → T.DerivationOf dp (insert p s) → T.DerivationOf dq (insert q s) → P dp → P dq → P (Arith.andIntro s p q dp dq)) (hOr : ∀ (s : V), L.IsFormulaSet s → ∀ (p q d : V), qqOr p q ∈ s → T.DerivationOf d (insert p (insert q s)) → P d → P (Arith.orIntro s p q d)) (hAll : ∀ (s : V), L.IsFormulaSet s → ∀ (p d : V), qqAll p ∈ s → T.DerivationOf d (insert (L.free p) (L.setShift s)) → P d → P (Arith.allIntro s p d)) (hEx : ∀ (s : V), L.IsFormulaSet s → ∀ (p t d : V), qqEx p ∈ s → L.IsTerm t → T.DerivationOf d (insert (L.substs₁ t p) s) → P d → P (Arith.exIntro s p t d)) (hWk : ∀ (s : V), L.IsFormulaSet s → ∀ (d : V), fstIdx d ⊆ s → T.Derivation d → P d → P (Arith.wkRule s d)) (hShift : ∀ (s : V), L.IsFormulaSet s → ∀ (d : V), s = L.setShift (fstIdx d) → T.Derivation d → P d → P (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 (Arith.cutRule s p d₁ d₂)) (hRoot : ∀ (s : V), L.IsFormulaSet s → ∀ p ∈ s, p ∈ T → P (Arith.root s p)) : P d

theorem LO.Arith.Language.Theory.Derivation.isFormulaSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d : V} (h : T.Derivation d) : L.IsFormulaSet (fstIdx d)

theorem LO.Arith.Language.Theory.DerivationOf.isFormulaSet {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {d s : V} (h : T.DerivationOf d s) : L.IsFormulaSet s

theorem LO.Arith.Language.Theory.Derivation.axL {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p : V} (hs : L.IsFormulaSet s) (h : p ∈ s) (hn : L.neg p ∈ s) : T.Derivation (Arith.axL s p)

theorem LO.Arith.Language.Theory.Derivation.verumIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (hs : L.IsFormulaSet s) (h : qqVerum ∈ s) : T.Derivation (Arith.verumIntro s)

theorem LO.Arith.Language.Theory.Derivation.andIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p q dp dq : V} (h : qqAnd p q ∈ s) (hdp : T.DerivationOf dp (insert p s)) (hdq : T.DerivationOf dq (insert q s)) : T.Derivation (Arith.andIntro s p q dp dq)

theorem LO.Arith.Language.Theory.Derivation.orIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p q dpq : V} (h : qqOr p q ∈ s) (hdpq : T.DerivationOf dpq (insert p (insert q s))) : T.Derivation (Arith.orIntro s p q dpq)

theorem LO.Arith.Language.Theory.Derivation.allIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p dp : V} (h : qqAll p ∈ s) (hdp : T.DerivationOf dp (insert (L.free p) (L.setShift s))) : T.Derivation (Arith.allIntro s p dp)

theorem LO.Arith.Language.Theory.Derivation.exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p t dp : V} (h : qqEx p ∈ s) (ht : L.IsTerm t) (hdp : T.DerivationOf dp (insert (L.substs₁ t p) s)) : T.Derivation (Arith.exIntro s p t dp)

theorem LO.Arith.Language.Theory.Derivation.wkRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s s' d : V} (hs : L.IsFormulaSet s) (h : s' ⊆ s) (hd : T.DerivationOf d s') : T.Derivation (Arith.wkRule s d)

theorem LO.Arith.Language.Theory.Derivation.shiftRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s d : V} (hd : T.DerivationOf d s) : T.Derivation (Arith.shiftRule (L.setShift s) d)

theorem LO.Arith.Language.Theory.Derivation.cutRule {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p d₁ d₂ : V} (hd₁ : T.DerivationOf d₁ (insert p s)) (hd₂ : T.DerivationOf d₂ (insert (L.neg p) s)) : T.Derivation (Arith.cutRule s p d₁ d₂)

theorem LO.Arith.Language.Theory.Derivation.root {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p : V} (hs : L.IsFormulaSet s) (hp : p ∈ s) (hT : p ∈ T) : T.Derivation (Arith.root s p)

theorem LO.Arith.Language.Theory.Derivation.of_ss {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s : V} (hs : L.IsFormulaSet s) (h : qqVerum ∈ s) : T.Derivable s

theorem LO.Arith.Language.Theory.Derivable.and_m {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p q : V} (h : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p q : V} (h : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p : V} (h : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p t : V} (h : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p q : V} (hp : T.Derivable (insert p s)) (hq : T.Derivable (insert q s)) : T.Derivable (insert (qqAnd p q) s)

theorem LO.Arith.Language.Theory.Derivable.or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p q : V} (hpq : T.Derivable (insert p (insert q s))) : T.Derivable (insert (qqOr p q) s)

theorem LO.Arith.Language.Theory.Derivable.conj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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 < len ps, T.Derivable (insert (nth ps i) s)) : T.Derivable (insert (qqConj ps) s)

Crucial inducion for formalized $\Sigma_1$-completeness.

theorem LO.Arith.Language.Theory.Derivable.disjDistr {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] (ps s : V) (d : T.Derivable (vecToSet ps ∪ s)) : T.Derivable (insert (qqDisj ps) s)

theorem LO.Arith.Language.Theory.Derivable.disj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] (ps s : V) {i : V} (hps : ∀ i < len ps, L.IsFormula (nth ps i)) (hi : i < len ps) (d : T.Derivable (insert (nth ps i) s)) : T.Derivable (insert (qqDisj ps) s)

theorem LO.Arith.Language.Theory.Derivable.all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p : V} (hp : L.IsSemiformula 1 p) (dp : T.Derivable (insert (L.free p) (L.setShift s))) : T.Derivable (insert (qqAll p) s)

theorem LO.Arith.Language.Theory.Derivable.ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : pL.TDef} [T.Defined pT] {s p t : V} (hp : L.IsSemiformula 1 p) (ht : L.IsTerm t) (dp : T.Derivable (insert (L.substs₁ t p) s)) : T.Derivable (insert (qqEx p) s)