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

Equations

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

noncomputable def FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚫₁-Predicate IsFormulaSet L

instance FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : IsFormulaSet L ∅

@[simp]

theorem FFL.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 FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.IsFormulaSet.insert_iff.

@[simp]

theorem FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.setShift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (s : V) : V

Equations

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

noncomputable def FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.setShift_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : setShift L ∅ = ∅

instance FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.setShift.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ setShift L

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.axL {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : V

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.verumIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : V

Equations

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

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

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.orIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p q d : V) : V

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.allIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p d : V) : V

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.exsIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p t d : V) : V

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.wkRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : V

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.shiftRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : V

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.cutRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p d₁ d₂ : V) : V

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.axm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : V

Equations

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

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.axL.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ axL via axLGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.verumIntro.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ verumIntro via verumIntroGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.andIntro.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₅ andIntro via andIntroGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.orIntro.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₄ orIntro via orIntroGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.allIntro.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₃ allIntro via allIntroGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.exsIntro.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₄ exsIntro via exsIntroGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.wkRule.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ wkRule via wkRuleGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.shiftRule.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ shiftRule via shiftRuleGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.cutRule_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₄ cutRule via cutRuleGraph

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

Equations

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.axm_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₂ axm via axmGraph

instance FFL.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₄OrIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₄ orIntro

instance FFL.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₂Axm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₂ axm

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.seq_lt_axL {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : s < axL s p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.arity_lt_axL {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : p < axL s p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.seq_lt_verumIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : s < verumIntro s

@[simp]

theorem FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.seq_lt_allIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p d : V) : s < allIntro s p d

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.p_lt_allIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p d : V) : p < allIntro s p d

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.s_lt_allIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p d : V) : d < allIntro s p d

@[simp]

theorem FFL.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 FFL.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 FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.seq_lt_wkRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : s < wkRule s d

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.d_lt_wkRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : d < wkRule s d

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.seq_lt_shiftRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : s < shiftRule s d

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.d_lt_shiftRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : d < shiftRule s d

@[simp]

theorem FFL.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 FFL.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 FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.seq_lt_axm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : s < axm s p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.p_lt_axm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : p < axm s p

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.fstIdx_axL {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : fstIdx (axL s p) = s

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.fstIdx_verumIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s : V) : fstIdx (verumIntro s) = s

@[simp]

theorem FFL.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 FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.fstIdx_allIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p d : V) : fstIdx (allIntro s p d) = s

@[simp]

theorem FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.fstIdx_wkRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : fstIdx (wkRule s d) = s

@[simp]

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.fstIdx_shiftRule {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s d : V) : fstIdx (shiftRule s d) = s

@[simp]

theorem FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.fstIdx_axm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (s p : V) : fstIdx (axm s p) = s

@[reducible, inline]

noncomputable abbrev FFL.FirstOrder.Arithmetic.Bootstrapping.Derivation.conseq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x : V) : V

Equations

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

def FFL.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 FFL.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 FFL.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 FFL.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

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

instance FFL.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 FFL.FirstOrder.Arithmetic.Bootstrapping.Derivation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : V → Prop

Equations

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

def FFL.FirstOrder.Arithmetic.Bootstrapping.DerivationOf {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (d s : V) : Prop

Equations

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

def FFL.FirstOrder.Arithmetic.Bootstrapping.Derivable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (s : V) : Prop

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Derivable T s = ∃ (d : V), FFL.FirstOrder.Arithmetic.Bootstrapping.DerivationOf T d s

def FFL.FirstOrder.Arithmetic.Bootstrapping.Proof {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (d φ : V) : Prop

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Proof T d φ = FFL.FirstOrder.Arithmetic.Bootstrapping.DerivationOf T d {φ}

def FFL.FirstOrder.Arithmetic.Bootstrapping.Provable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (φ : V) : Prop

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.Provable T φ = ∃ (d : V), FFL.FirstOrder.Arithmetic.Bootstrapping.Proof T d φ

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

Equations

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

noncomputable def FFL.FirstOrder.Arithmetic.Bootstrapping.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 FFL.FirstOrder.Arithmetic.Bootstrapping.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 FFL.FirstOrder.Arithmetic.Bootstrapping.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 FFL.FirstOrder.Arithmetic.Bootstrapping.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 FFL.FirstOrder.Arithmetic.Bootstrapping.provabilityPred {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] (σ : Sentence L) : ArithmeticSentence

Equations

• FFL.FirstOrder.Arithmetic.Bootstrapping.provabilityPred T σ = ↑(FFL.FirstOrder.Arithmetic.Bootstrapping.provable T)/[⌜σ⌝]

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

Equations

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

@[simp]

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

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Derivation.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Predicate Derivation T via derivation T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Derivation.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Predicate Derivation T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.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 Derivation T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.DerivationOf.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation DerivationOf T via derivationOf T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.DerivationOf.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation DerivationOf T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.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 DerivationOf T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Derivable.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate Derivable T via derivable T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Derivable.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate Derivable T

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

instance for definability tactic

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Proof.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation Proof T via proof T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Proof.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚫₁-Relation Proof T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.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 Proof T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Provable.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate Provable T via provable T

instance FFL.FirstOrder.Arithmetic.Bootstrapping.Provable.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] : 𝚺₁-Predicate Provable T

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

instance for definability tactic

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

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

Alias of the forward direction of FFL.FirstOrder.Arithmetic.Bootstrapping.Derivation.case_iff.

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

Alias of the reverse direction of FFL.FirstOrder.Arithmetic.Bootstrapping.Derivation.case_iff.

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : Derivation T d) (hAxL : ∀ (s : V), IsFormulaSet L s → ∀ p ∈ s, neg L p ∈ s → P (Bootstrapping.axL s p)) (hVerumIntro : ∀ (s : V), IsFormulaSet L s → qqVerum ∈ s → P (Bootstrapping.verumIntro s)) (hAnd : ∀ (s : V), IsFormulaSet L s → ∀ (p q dp dq : V), qqAnd p q ∈ s → DerivationOf T dp (insert p s) → DerivationOf T dq (insert q s) → P dp → P dq → P (Bootstrapping.andIntro s p q dp dq)) (hOr : ∀ (s : V), IsFormulaSet L s → ∀ (p q d : V), qqOr p q ∈ s → DerivationOf T d (insert p (insert q s)) → P d → P (Bootstrapping.orIntro s p q d)) (hAll : ∀ (s : V), IsFormulaSet L s → ∀ (p d : V), qqAll p ∈ s → DerivationOf T d (insert (free L p) (setShift L s)) → P d → P (Bootstrapping.allIntro s p d)) (hExs : ∀ (s : V), IsFormulaSet L s → ∀ (p t d : V), qqExs p ∈ s → IsTerm L t → DerivationOf T d (insert (substs1 L t p) s) → P d → P (Bootstrapping.exsIntro s p t d)) (hWk : ∀ (s : V), IsFormulaSet L s → ∀ (d : V), fstIdx d ⊆ s → Derivation T d → P d → P (Bootstrapping.wkRule s d)) (hShift : ∀ (s : V), IsFormulaSet L s → ∀ (d : V), s = setShift L (fstIdx d) → Derivation T d → P d → P (Bootstrapping.shiftRule s d)) (hCut : ∀ (s : V), IsFormulaSet L s → ∀ (p d₁ d₂ : V), DerivationOf T d₁ (insert p s) → DerivationOf T d₂ (insert (neg L p) s) → P d₁ → P d₂ → P (Bootstrapping.cutRule s p d₁ d₂)) (hRoot : ∀ (s : V), IsFormulaSet L s → ∀ p ∈ s, p ∈ T.Δ₁Class → P (Bootstrapping.axm s p)) : P d

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

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

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

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : qqAnd p q ∈ s) (hdp : DerivationOf T dp (insert p s)) (hdq : DerivationOf T dq (insert q s)) : Derivation T (Bootstrapping.andIntro s p q dp dq)

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : qqOr p q ∈ s) (hdpq : DerivationOf T dpq (insert p (insert q s))) : Derivation T (Bootstrapping.orIntro s p q dpq)

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : qqExs p ∈ s) (ht : IsTerm L t) (hdp : DerivationOf T dp (insert (substs1 L t p) s)) : Derivation T (Bootstrapping.exsIntro s p t dp)

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

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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₁ : DerivationOf T d₁ (insert p s)) (hd₂ : DerivationOf T d₂ (insert (neg L p) s)) : Derivation T (Bootstrapping.cutRule s p d₁ d₂)

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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} : Derivation T d → Derivation U d

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

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

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : qqAnd p q ∈ s) (hp : Derivable T (insert p s)) (hq : Derivable T (insert q s)) : Derivable T s

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : qqOr p q ∈ s) (hpq : Derivable T (insert p (insert q s))) : Derivable T s

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : qqExs p ∈ s) (ht : IsTerm L t) (hp : Derivable T (insert (substs1 L t p) s)) : Derivable T s

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

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 : Derivable T s') : Derivable T s

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Derivable.exchange {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {s p q : V} (h : Derivable T (insert p (insert q s))) : Derivable T (insert q (insert p s))

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

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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} : Derivable T s → Derivable U s

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

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

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

Crucial inducion for formalized $\Sigma_1$-completeness.

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 < len ps, IsFormula L (nth ps i)) (hi : i < len ps) (d : Derivable T (insert (nth ps i) s)) : Derivable T (insert (qqDisj ps) s)

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

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.internal_provable_iff_internal_derivable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : Provable T φ ↔ Derivable T (insert φ ∅)

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Derivable.toProvable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : Derivable T (insert φ ∅) → Provable T φ

Alias of the reverse direction of FFL.FirstOrder.Arithmetic.Bootstrapping.internal_provable_iff_internal_derivable.

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.Provable.toDerivable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : V} : Provable T φ → Derivable T (insert φ ∅)

Alias of the forward direction of FFL.FirstOrder.Arithmetic.Bootstrapping.internal_provable_iff_internal_derivable.

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

theorem FFL.FirstOrder.Arithmetic.Bootstrapping.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 < len ps, IsFormula L (nth ps i)) (hi : i < len ps) (d : Provable T (nth ps i)) : Provable T (qqDisj ps)