def LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (s : V) : Prop

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet L s = ∀ p ∈ s, LO.FirstOrder.Arithmetic.Bootstrapping.IsFormula L p

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.isFormulaSet (L : Language) [L.Encodable] [L.LORDefinable] : 𝚫₁.Semisentence 1

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Predicate IsFormulaSet L via isFormulaSet L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Predicate IsFormulaSet L

instance LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Predicate IsFormulaSet L

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.empty {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : IsFormulaSet L ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.singleton {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsFormulaSet L {p} ↔ IsFormula L p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.insert_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p s : V} : IsFormulaSet L (Insert.insert p s) ↔ IsFormula L p ∧ IsFormulaSet L s

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.insert {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p s : V} : IsFormulaSet L (Insert.insert p s) → IsFormula L p ∧ IsFormulaSet L s

Alias of the forward direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.insert_iff.

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.union {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {s₁ s₂ : V} : IsFormulaSet L (s₁ ∪ s₂) ↔ IsFormulaSet L s₁ ∧ IsFormulaSet L s₂

theorem LO.FirstOrder.Arithmetic.Bootstrapping.setShift_existsUnique {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (s : V) : ∃! t : V, ∀ (y : V), y ∈ t ↔ ∃ x ∈ s, y = shift L x

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.setShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (s : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.setShift L s = Classical.choose! ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.setShiftGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.mem_setShift_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {s y : V} : y ∈ setShift L s ↔ ∃ x ∈ s, y = shift L x

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.setShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {s : V} (h : IsFormulaSet L s) : IsFormulaSet L (Bootstrapping.setShift L s)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_mem_setShift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p s : V} (h : p ∈ s) : shift L p ∈ setShift L s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.setShift_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {s : V} : IsFormulaSet L (Bootstrapping.setShift L s) ↔ IsFormulaSet L s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.mem_setShift_union {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {s t : V} : setShift L (s ∪ t) = setShift L s ∪ setShift L t

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.mem_setShift_insert {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {x s : V} : setShift L (insert x s) = insert (shift L x) (setShift L s)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.setShift_empty {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : setShift L ∅ = ∅

instance LO.FirstOrder.Arithmetic.Bootstrapping.setShift.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ setShift L via setShiftGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.setShift.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ setShift L

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.axL {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.axL s p = ⟪s, ⟪0, p⟫⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.verumIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.verumIntro s = ⟪s, ⟪1, 0⟫⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dp dq : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.orIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q d : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.orIntro s p q d = ⟪s, ⟪3, ⟪p, ⟪q, d⟫⟫⟫⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.allIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.allIntro s p d = ⟪s, ⟪4, ⟪p, d⟫⟫⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.exsIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p t d : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.exsIntro s p t d = ⟪s, ⟪5, ⟪p, ⟪t, d⟫⟫⟫⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.wkRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.wkRule s d = ⟪s, ⟪6, d⟫⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.shiftRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.shiftRule s d = ⟪s, ⟪7, d⟫⟫ + 1

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.cutRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d₁ d₂ : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.axm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.axm s p = ⟪s, ⟪9, p⟫⟫ + 1

def LO.FirstOrder.Arithmetic.Bootstrapping.axLGraph : 𝚺₀.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.axL.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₂ axL via axLGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.verumIntroGraph : 𝚺₀.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.verumIntro.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₁ verumIntro via verumIntroGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.andIntroGraph : 𝚺₀.Semisentence 6

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.andIntro.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₅ andIntro via andIntroGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.orIntroGraph : 𝚺₀.Semisentence 5

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.orIntro.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₄ orIntro via orIntroGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.allIntroGraph : 𝚺₀.Semisentence 4

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.allIntro.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₃ allIntro via allIntroGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.exsIntroGraph : 𝚺₀.Semisentence 5

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.exsIntro.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₄ exsIntro via exsIntroGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.wkRuleGraph : 𝚺₀.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.wkRule.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₂ wkRule via wkRuleGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.shiftRuleGraph : 𝚺₀.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.shiftRule.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₂ shiftRule via shiftRuleGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.cutRuleGraph : 𝚺₀.Semisentence 5

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.cutRule_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₄ cutRule via cutRuleGraph

def LO.FirstOrder.Arithmetic.Bootstrapping.axmGraph : 𝚺₀.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.axm_defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] : 𝚺₀-Function₂ axm via axmGraph

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_axL {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : s < axL s p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.arity_lt_axL {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : p < axL s p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_verumIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s : V) : s < verumIntro s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dp dq : V) : s < andIntro s p q dp dq

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.p_lt_andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dp dq : V) : p < andIntro s p q dp dq

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.q_lt_andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dp dq : V) : q < andIntro s p q dp dq

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.dp_lt_andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dp dq : V) : dp < andIntro s p q dp dq

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.dq_lt_andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dp dq : V) : dq < andIntro s p q dp dq

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_orIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q d : V) : s < orIntro s p q d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.p_lt_orIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q d : V) : p < orIntro s p q d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.q_lt_orIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q d : V) : q < orIntro s p q d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.d_lt_orIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q d : V) : d < orIntro s p q d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_allIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d : V) : s < allIntro s p d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.p_lt_allIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d : V) : p < allIntro s p d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.s_lt_allIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d : V) : d < allIntro s p d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_exsIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p t d : V) : s < exsIntro s p t d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.p_lt_exsIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p t d : V) : p < exsIntro s p t d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.t_lt_exsIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p t d : V) : t < exsIntro s p t d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.d_lt_exsIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p t d : V) : d < exsIntro s p t d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_wkRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : s < wkRule s d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.d_lt_wkRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : d < wkRule s d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_shiftRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : s < shiftRule s d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.d_lt_shiftRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : d < shiftRule s d

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_cutRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d₁ d₂ : V) : s < cutRule s p d₁ d₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.p_lt_cutRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d₁ d₂ : V) : p < cutRule s p d₁ d₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.d₁_lt_cutRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d₁ d₂ : V) : d₁ < cutRule s p d₁ d₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.d₂_lt_cutRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d₁ d₂ : V) : d₂ < cutRule s p d₁ d₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.seq_lt_axm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : s < axm s p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.p_lt_axm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : p < axm s p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_axL {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : fstIdx (axL s p) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_verumIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s : V) : fstIdx (verumIntro s) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dp dq : V) : fstIdx (andIntro s p q dp dq) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_orIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p q dpq : V) : fstIdx (orIntro s p q dpq) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_allIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d : V) : fstIdx (allIntro s p d) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_exsIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p t d : V) : fstIdx (exsIntro s p t d) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_wkRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : fstIdx (wkRule s d) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_shiftRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s d : V) : fstIdx (shiftRule s d) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_cutRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p d₁ d₂ : V) : fstIdx (cutRule s p d₁ d₂) = s

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fstIdx_axm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (s p : V) : fstIdx (axm s p) = s

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.conseq {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] (x : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.conseq x = π₁ x

def LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.Phi {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (C : Set V) (d : V) : Prop

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.blueprint {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Fixpoint.Blueprint 0

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.Phi_definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : HierarchySymbol.Defined (fun (v : Fin 2 → V) => Phi T {x : V | x ∈ v 1} (v 0)) (blueprint T).core

def LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.construction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Fixpoint.Construction V (blueprint T)

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.instStrongFiniteConstruction {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Fixpoint.Construction.StrongFinite V (construction T)

def LO.FirstOrder.Theory.Derivation {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : V → Prop

Equations

• T.Derivation = (LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.construction T).Fixpoint ![]

def LO.FirstOrder.Theory.DerivationOf {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (d s : V) : Prop

Equations

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

def LO.FirstOrder.Theory.Derivable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (s : V) : Prop

Equations

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

def LO.FirstOrder.Theory.Proof {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (d φ : V) : Prop

Equations

• T.Proof d φ = T.DerivationOf d {φ}

def LO.FirstOrder.Theory.Provable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (φ : V) : Prop

Equations

• T.Provable φ = ∃ (d : V), T.Proof d φ

noncomputable def LO.FirstOrder.Theory.derivation {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚫₁.Semisentence 1

Equations

• T.derivation = (LO.FirstOrder.Arithmetic.Bootstrapping.Derivation.blueprint T).fixpointDefΔ₁

noncomputable def LO.FirstOrder.Theory.derivationOf {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚫₁.Semisentence 2

Equations

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

noncomputable def LO.FirstOrder.Theory.derivable {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚺₁.Semisentence 1

Equations

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

noncomputable def LO.FirstOrder.Theory.proof {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚫₁.Semisentence 2

Equations

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

noncomputable def LO.FirstOrder.Theory.provable {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : 𝚺₁.Semisentence 1

Equations

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

@[reducible, inline]

noncomputable abbrev LO.FirstOrder.Theory.provabilityPred {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : Sentence ℒₒᵣ

Equations

• T.provabilityPred σ = ↑T.provable/[⌜σ⌝]

noncomputable def LO.FirstOrder.Theory.provabilityPred' {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : 𝚺₁.Sentence

Equations

• T.provabilityPred' σ = LO.FirstOrder.Arithmetic.HierarchySymbol.Semiformula.mkSigma (↑T.provable/[⌜σ⌝]) ⋯

@[simp]

theorem LO.FirstOrder.Theory.provabilityPred'_val {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : ↑(T.provabilityPred' σ) = T.provabilityPred σ

instance LO.FirstOrder.Theory.Derivation.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Predicate T.Derivation via T.derivation

instance LO.FirstOrder.Theory.Derivation.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Predicate T.Derivation

instance LO.FirstOrder.Theory.Derivation.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Predicate T.Derivation

instance LO.FirstOrder.Theory.DerivationOf.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation T.DerivationOf via T.derivationOf

instance LO.FirstOrder.Theory.DerivationOf.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation T.DerivationOf

instance LO.FirstOrder.Theory.DerivationOf.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Relation T.DerivationOf

instance LO.FirstOrder.Theory.Derivable.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate T.Derivable via T.derivable

instance LO.FirstOrder.Theory.Derivable.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate T.Derivable

instance LO.FirstOrder.Theory.Derivable.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : { Γ := 𝚺, rank := 0 + 1 }-Predicate T.Derivable

instance for definability tactic

instance LO.FirstOrder.Theory.Proof.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation T.Proof via T.proof

instance LO.FirstOrder.Theory.Proof.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation T.Proof

instance LO.FirstOrder.Theory.Proof.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Relation T.Proof

instance LO.FirstOrder.Theory.Provable.defined {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate T.Provable via T.provable

instance LO.FirstOrder.Theory.Provable.definable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate T.Provable

instance LO.FirstOrder.Theory.Provable.definable' {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : { Γ := 𝚺, rank := 0 + 1 }-Predicate T.Provable

instance for definability tactic

theorem LO.FirstOrder.Theory.Derivation.case_iff {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {d : V} : T.Derivation d ↔ Arithmetic.Bootstrapping.IsFormulaSet L (Arithmetic.fstIdx d) ∧ ((∃ (s : V) (p : V), d = Arithmetic.Bootstrapping.axL s p ∧ p ∈ s ∧ Arithmetic.Bootstrapping.neg L p ∈ s) ∨ (∃ (s : V), d = Arithmetic.Bootstrapping.verumIntro s ∧ Arithmetic.Bootstrapping.qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = Arithmetic.Bootstrapping.andIntro s p q dp dq ∧ Arithmetic.Bootstrapping.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 = Arithmetic.Bootstrapping.orIntro s p q dpq ∧ Arithmetic.Bootstrapping.qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V), d = Arithmetic.Bootstrapping.allIntro s p dp ∧ Arithmetic.Bootstrapping.qqAll p ∈ s ∧ T.DerivationOf dp (insert (Arithmetic.Bootstrapping.free L p) (Arithmetic.Bootstrapping.setShift L s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V), d = Arithmetic.Bootstrapping.exsIntro s p t dp ∧ Arithmetic.Bootstrapping.qqExs p ∈ s ∧ Arithmetic.Bootstrapping.IsTerm L t ∧ T.DerivationOf dp (insert (Arithmetic.Bootstrapping.substs1 L t p) s)) ∨ (∃ (s : V) (d' : V), d = Arithmetic.Bootstrapping.wkRule s d' ∧ Arithmetic.fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V), d = Arithmetic.Bootstrapping.shiftRule s d' ∧ s = Arithmetic.Bootstrapping.setShift L (Arithmetic.fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = Arithmetic.Bootstrapping.cutRule s p d₁ d₂ ∧ T.DerivationOf d₁ (insert p s) ∧ T.DerivationOf d₂ (insert (Arithmetic.Bootstrapping.neg L p) s)) ∨ ∃ (s : V) (p : V), d = Arithmetic.Bootstrapping.axm s p ∧ p ∈ s ∧ p ∈ T.Δ₁Class)

theorem LO.FirstOrder.Theory.Derivation.case {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {d : V} : T.Derivation d → Arithmetic.Bootstrapping.IsFormulaSet L (Arithmetic.fstIdx d) ∧ ((∃ (s : V) (p : V), d = Arithmetic.Bootstrapping.axL s p ∧ p ∈ s ∧ Arithmetic.Bootstrapping.neg L p ∈ s) ∨ (∃ (s : V), d = Arithmetic.Bootstrapping.verumIntro s ∧ Arithmetic.Bootstrapping.qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = Arithmetic.Bootstrapping.andIntro s p q dp dq ∧ Arithmetic.Bootstrapping.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 = Arithmetic.Bootstrapping.orIntro s p q dpq ∧ Arithmetic.Bootstrapping.qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V), d = Arithmetic.Bootstrapping.allIntro s p dp ∧ Arithmetic.Bootstrapping.qqAll p ∈ s ∧ T.DerivationOf dp (insert (Arithmetic.Bootstrapping.free L p) (Arithmetic.Bootstrapping.setShift L s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V), d = Arithmetic.Bootstrapping.exsIntro s p t dp ∧ Arithmetic.Bootstrapping.qqExs p ∈ s ∧ Arithmetic.Bootstrapping.IsTerm L t ∧ T.DerivationOf dp (insert (Arithmetic.Bootstrapping.substs1 L t p) s)) ∨ (∃ (s : V) (d' : V), d = Arithmetic.Bootstrapping.wkRule s d' ∧ Arithmetic.fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V), d = Arithmetic.Bootstrapping.shiftRule s d' ∧ s = Arithmetic.Bootstrapping.setShift L (Arithmetic.fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = Arithmetic.Bootstrapping.cutRule s p d₁ d₂ ∧ T.DerivationOf d₁ (insert p s) ∧ T.DerivationOf d₂ (insert (Arithmetic.Bootstrapping.neg L p) s)) ∨ ∃ (s : V) (p : V), d = Arithmetic.Bootstrapping.axm s p ∧ p ∈ s ∧ p ∈ T.Δ₁Class)

Alias of the forward direction of LO.FirstOrder.Theory.Derivation.case_iff.

theorem LO.FirstOrder.Theory.Derivation.mk {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {d : V} : Arithmetic.Bootstrapping.IsFormulaSet L (Arithmetic.fstIdx d) ∧ ((∃ (s : V) (p : V), d = Arithmetic.Bootstrapping.axL s p ∧ p ∈ s ∧ Arithmetic.Bootstrapping.neg L p ∈ s) ∨ (∃ (s : V), d = Arithmetic.Bootstrapping.verumIntro s ∧ Arithmetic.Bootstrapping.qqVerum ∈ s) ∨ (∃ (s : V) (p : V) (q : V) (dp : V) (dq : V), d = Arithmetic.Bootstrapping.andIntro s p q dp dq ∧ Arithmetic.Bootstrapping.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 = Arithmetic.Bootstrapping.orIntro s p q dpq ∧ Arithmetic.Bootstrapping.qqOr p q ∈ s ∧ T.DerivationOf dpq (insert p (insert q s))) ∨ (∃ (s : V) (p : V) (dp : V), d = Arithmetic.Bootstrapping.allIntro s p dp ∧ Arithmetic.Bootstrapping.qqAll p ∈ s ∧ T.DerivationOf dp (insert (Arithmetic.Bootstrapping.free L p) (Arithmetic.Bootstrapping.setShift L s))) ∨ (∃ (s : V) (p : V) (t : V) (dp : V), d = Arithmetic.Bootstrapping.exsIntro s p t dp ∧ Arithmetic.Bootstrapping.qqExs p ∈ s ∧ Arithmetic.Bootstrapping.IsTerm L t ∧ T.DerivationOf dp (insert (Arithmetic.Bootstrapping.substs1 L t p) s)) ∨ (∃ (s : V) (d' : V), d = Arithmetic.Bootstrapping.wkRule s d' ∧ Arithmetic.fstIdx d' ⊆ s ∧ T.Derivation d') ∨ (∃ (s : V) (d' : V), d = Arithmetic.Bootstrapping.shiftRule s d' ∧ s = Arithmetic.Bootstrapping.setShift L (Arithmetic.fstIdx d') ∧ T.Derivation d') ∨ (∃ (s : V) (p : V) (d₁ : V) (d₂ : V), d = Arithmetic.Bootstrapping.cutRule s p d₁ d₂ ∧ T.DerivationOf d₁ (insert p s) ∧ T.DerivationOf d₂ (insert (Arithmetic.Bootstrapping.neg L p) s)) ∨ ∃ (s : V) (p : V), d = Arithmetic.Bootstrapping.axm s p ∧ p ∈ s ∧ p ∈ T.Δ₁Class) → T.Derivation d

Alias of the reverse direction of LO.FirstOrder.Theory.Derivation.case_iff.

theorem LO.FirstOrder.Theory.Derivation.induction1 {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (Γ : SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) {d : V} (hd : T.Derivation d) (hAxL : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ p ∈ s, Arithmetic.Bootstrapping.neg L p ∈ s → P (Arithmetic.Bootstrapping.axL s p)) (hVerumIntro : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → Arithmetic.Bootstrapping.qqVerum ∈ s → P (Arithmetic.Bootstrapping.verumIntro s)) (hAnd : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ (p q dp dq : V), Arithmetic.Bootstrapping.qqAnd p q ∈ s → T.DerivationOf dp (insert p s) → T.DerivationOf dq (insert q s) → P dp → P dq → P (Arithmetic.Bootstrapping.andIntro s p q dp dq)) (hOr : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ (p q d : V), Arithmetic.Bootstrapping.qqOr p q ∈ s → T.DerivationOf d (insert p (insert q s)) → P d → P (Arithmetic.Bootstrapping.orIntro s p q d)) (hAll : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ (p d : V), Arithmetic.Bootstrapping.qqAll p ∈ s → T.DerivationOf d (insert (Arithmetic.Bootstrapping.free L p) (Arithmetic.Bootstrapping.setShift L s)) → P d → P (Arithmetic.Bootstrapping.allIntro s p d)) (hExs : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ (p t d : V), Arithmetic.Bootstrapping.qqExs p ∈ s → Arithmetic.Bootstrapping.IsTerm L t → T.DerivationOf d (insert (Arithmetic.Bootstrapping.substs1 L t p) s) → P d → P (Arithmetic.Bootstrapping.exsIntro s p t d)) (hWk : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ (d : V), Arithmetic.fstIdx d ⊆ s → T.Derivation d → P d → P (Arithmetic.Bootstrapping.wkRule s d)) (hShift : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ (d : V), s = Arithmetic.Bootstrapping.setShift L (Arithmetic.fstIdx d) → T.Derivation d → P d → P (Arithmetic.Bootstrapping.shiftRule s d)) (hCut : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ (p d₁ d₂ : V), T.DerivationOf d₁ (insert p s) → T.DerivationOf d₂ (insert (Arithmetic.Bootstrapping.neg L p) s) → P d₁ → P d₂ → P (Arithmetic.Bootstrapping.cutRule s p d₁ d₂)) (hRoot : ∀ (s : V), Arithmetic.Bootstrapping.IsFormulaSet L s → ∀ p ∈ s, p ∈ T.Δ₁Class → P (Arithmetic.Bootstrapping.axm s p)) : P d

theorem LO.FirstOrder.Theory.Derivation.isFormulaSet {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {d : V} (h : T.Derivation d) : Arithmetic.Bootstrapping.IsFormulaSet L (Arithmetic.fstIdx d)

theorem LO.FirstOrder.Theory.DerivationOf.isFormulaSet {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {d s : V} (h : T.DerivationOf d s) : Arithmetic.Bootstrapping.IsFormulaSet L s

theorem LO.FirstOrder.Theory.Derivation.axL {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (h : p ∈ s) (hn : Arithmetic.Bootstrapping.neg L p ∈ s) : T.Derivation (Arithmetic.Bootstrapping.axL s p)

theorem LO.FirstOrder.Theory.Derivation.verumIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (h : Arithmetic.Bootstrapping.qqVerum ∈ s) : T.Derivation (Arithmetic.Bootstrapping.verumIntro s)

theorem LO.FirstOrder.Theory.Derivation.andIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q dp dq : V} (h : Arithmetic.Bootstrapping.qqAnd p q ∈ s) (hdp : T.DerivationOf dp (insert p s)) (hdq : T.DerivationOf dq (insert q s)) : T.Derivation (Arithmetic.Bootstrapping.andIntro s p q dp dq)

theorem LO.FirstOrder.Theory.Derivation.orIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q dpq : V} (h : Arithmetic.Bootstrapping.qqOr p q ∈ s) (hdpq : T.DerivationOf dpq (insert p (insert q s))) : T.Derivation (Arithmetic.Bootstrapping.orIntro s p q dpq)

theorem LO.FirstOrder.Theory.Derivation.allIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p dp : V} (h : Arithmetic.Bootstrapping.qqAll p ∈ s) (hdp : T.DerivationOf dp (insert (Arithmetic.Bootstrapping.free L p) (Arithmetic.Bootstrapping.setShift L s))) : T.Derivation (Arithmetic.Bootstrapping.allIntro s p dp)

theorem LO.FirstOrder.Theory.Derivation.exsIntro {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p t dp : V} (h : Arithmetic.Bootstrapping.qqExs p ∈ s) (ht : Arithmetic.Bootstrapping.IsTerm L t) (hdp : T.DerivationOf dp (insert (Arithmetic.Bootstrapping.substs1 L t p) s)) : T.Derivation (Arithmetic.Bootstrapping.exsIntro s p t dp)

theorem LO.FirstOrder.Theory.Derivation.wkRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s s' d : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (h : s' ⊆ s) (hd : T.DerivationOf d s') : T.Derivation (Arithmetic.Bootstrapping.wkRule s d)

theorem LO.FirstOrder.Theory.Derivation.shiftRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s d : V} (hd : T.DerivationOf d s) : T.Derivation (Arithmetic.Bootstrapping.shiftRule (Arithmetic.Bootstrapping.setShift L s) d)

theorem LO.FirstOrder.Theory.Derivation.cutRule {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p d₁ d₂ : V} (hd₁ : T.DerivationOf d₁ (insert p s)) (hd₂ : T.DerivationOf d₂ (insert (Arithmetic.Bootstrapping.neg L p) s)) : T.Derivation (Arithmetic.Bootstrapping.cutRule s p d₁ d₂)

theorem LO.FirstOrder.Theory.Derivation.axm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (hp : p ∈ s) (hT : p ∈ T.Δ₁Class) : T.Derivation (Arithmetic.Bootstrapping.axm s p)

theorem LO.FirstOrder.Theory.Derivation.of_ss {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {U : Theory L} [U.Δ₁] (h : T.Δ₁Class ⊆ U.Δ₁Class) {d : V} : T.Derivation d → U.Derivation d

theorem LO.FirstOrder.Theory.Derivable.isFormulaSet {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s : V} (h : T.Derivable s) : Arithmetic.Bootstrapping.IsFormulaSet L s

theorem LO.FirstOrder.Theory.Derivable.em {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (p : V) (h : p ∈ s) (hn : Arithmetic.Bootstrapping.neg L p ∈ s) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.verum {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (h : Arithmetic.Bootstrapping.qqVerum ∈ s) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.and_m {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q : V} (h : Arithmetic.Bootstrapping.qqAnd p q ∈ s) (hp : T.Derivable (insert p s)) (hq : T.Derivable (insert q s)) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.or_m {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q : V} (h : Arithmetic.Bootstrapping.qqOr p q ∈ s) (hpq : T.Derivable (insert p (insert q s))) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.all_m {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p : V} (h : Arithmetic.Bootstrapping.qqAll p ∈ s) (hp : T.Derivable (insert (Arithmetic.Bootstrapping.free L p) (Arithmetic.Bootstrapping.setShift L s))) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.ex_m {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p t : V} (h : Arithmetic.Bootstrapping.qqExs p ∈ s) (ht : Arithmetic.Bootstrapping.IsTerm L t) (hp : T.Derivable (insert (Arithmetic.Bootstrapping.substs1 L t p) s)) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.wk {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s s' : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (h : s' ⊆ s) (hd : T.Derivable s') : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.shift {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s : V} (hd : T.Derivable s) : T.Derivable (Arithmetic.Bootstrapping.setShift L s)

theorem LO.FirstOrder.Theory.Derivable.ofSetEq {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s s' : V} (h : ∀ (x : V), x ∈ s' ↔ x ∈ s) (hd : T.Derivable s') : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.exchange {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q : V} (h : T.Derivable (insert p (insert q s))) : T.Derivable (insert q (insert p s))

theorem LO.FirstOrder.Theory.Derivable.cut {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s : V} (p : V) (hd₁ : T.Derivable (insert p s)) (hd₂ : T.Derivable (insert (Arithmetic.Bootstrapping.neg L p) s)) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.by_axm {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (p : V) (hp : p ∈ s) (hT : p ∈ T.Δ₁Class) : T.Derivable s

theorem LO.FirstOrder.Theory.Derivable.of_ss {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T U : Theory L} [T.Δ₁] [U.Δ₁] (h : T.Δ₁Class ⊆ U.Δ₁Class) {s : V} : T.Derivable s → U.Derivable s

theorem LO.FirstOrder.Theory.Derivable.and {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q : V} (hp : T.Derivable (insert p s)) (hq : T.Derivable (insert q s)) : T.Derivable (insert (Arithmetic.Bootstrapping.qqAnd p q) s)

theorem LO.FirstOrder.Theory.Derivable.or {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q : V} (hpq : T.Derivable (insert p (insert q s))) : T.Derivable (insert (Arithmetic.Bootstrapping.qqOr p q) s)

theorem LO.FirstOrder.Theory.Derivable.conj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (ps : V) {s : V} (hs : Arithmetic.Bootstrapping.IsFormulaSet L s) (ds : ∀ i < Arithmetic.len ps, T.Derivable (insert (Arithmetic.nth ps i) s)) : T.Derivable (insert (Arithmetic.Bootstrapping.qqConj ps) s)

Crucial inducion for formalized $\Sigma_1$-completeness.

theorem LO.FirstOrder.Theory.Derivable.disjDistr {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (ps s : V) (d : T.Derivable (Arithmetic.vecToSet ps ∪ s)) : T.Derivable (insert (Arithmetic.Bootstrapping.qqDisj ps) s)

theorem LO.FirstOrder.Theory.Derivable.disj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (ps s : V) {i : V} (hps : ∀ i < Arithmetic.len ps, Arithmetic.Bootstrapping.IsFormula L (Arithmetic.nth ps i)) (hi : i < Arithmetic.len ps) (d : T.Derivable (insert (Arithmetic.nth ps i) s)) : T.Derivable (insert (Arithmetic.Bootstrapping.qqDisj ps) s)

theorem LO.FirstOrder.Theory.Derivable.all {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {p s : V} (hp : Arithmetic.Bootstrapping.IsSemiformula L 1 p) (dp : T.Derivable (insert (Arithmetic.Bootstrapping.free L p) (Arithmetic.Bootstrapping.setShift L s))) : T.Derivable (insert (Arithmetic.Bootstrapping.qqAll p) s)

theorem LO.FirstOrder.Theory.Derivable.exs {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {p t s : V} (hp : Arithmetic.Bootstrapping.IsSemiformula L 1 p) (ht : Arithmetic.Bootstrapping.IsTerm L t) (dp : T.Derivable (insert (Arithmetic.Bootstrapping.substs1 L t p) s)) : T.Derivable (insert (Arithmetic.Bootstrapping.qqExs p) s)

theorem LO.FirstOrder.Theory.internal_provable_iff_internal_derivable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : T.Provable φ ↔ T.Derivable (insert φ ∅)

theorem LO.FirstOrder.Theory.Provable.toDerivable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : T.Provable φ → T.Derivable (insert φ ∅)

Alias of the forward direction of LO.FirstOrder.Theory.internal_provable_iff_internal_derivable.

theorem LO.FirstOrder.Theory.Derivable.toProvable {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : T.Derivable (insert φ ∅) → T.Provable φ

Alias of the reverse direction of LO.FirstOrder.Theory.internal_provable_iff_internal_derivable.

theorem LO.FirstOrder.Theory.Provable.conj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (ps : V) (ds : ∀ i < Arithmetic.len ps, T.Provable (Arithmetic.nth ps i)) : T.Provable (Arithmetic.Bootstrapping.qqConj ps)

theorem LO.FirstOrder.Theory.Provable.disj {V : Type u_1} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] (ps : V) {i : V} (hps : ∀ i < Arithmetic.len ps, Arithmetic.Bootstrapping.IsFormula L (Arithmetic.nth ps i)) (hi : i < Arithmetic.len ps) (d : T.Provable (Arithmetic.nth ps i)) : T.Provable (Arithmetic.Bootstrapping.qqDisj ps)