Typed internal Tait-calculus

@[reducible, inline]

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.tmem φ T = (φ.val ∈ T.Δ₁Class)

def LO.FirstOrder.Arithmetic.Bootstrapping.«term_∈'_» : Lean.TrailingParserDescr

Equations

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

structure LO.FirstOrder.Arithmetic.Bootstrapping.Sequent (V : Type u_1) [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : Type u_1

• val : V
• val_formulaSet : IsFormulaSet L self.val

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instEmptyCollectionSequent {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : EmptyCollection (Sequent V L)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instEmptyCollectionSequent = { emptyCollection := { val := ∅, val_formulaSet := ⋯ } }

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.instSingletonFormulaSequent {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : Singleton (Formula V L) (Sequent V L)

Equations

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

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.instInsertFormulaSequent {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : Insert (Formula V L) (Sequent V L)

Equations

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

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.instUnionSequent {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : Union (Sequent V L)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instUnionSequent = { union := fun (Γ Δ : LO.FirstOrder.Arithmetic.Bootstrapping.Sequent V L) => { val := Γ.val ∪ Δ.val, val_formulaSet := ⋯ } }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instMembershipFormulaSequent {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : Membership (Formula V L) (Sequent V L)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instHasSubsetSequent {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : HasSubset (Sequent V L)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instHasSubsetSequent = { Subset := fun (x1 x2 : LO.FirstOrder.Arithmetic.Bootstrapping.Sequent V L) => x1.val ⊆ x2.val }

def LO.FirstOrder.Arithmetic.Bootstrapping.«term_⫽_» : Lean.TrailingParserDescr

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.mem_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : Sequent V L} {φ : Formula V L} : φ ∈ Γ ↔ φ.val ∈ Γ.val

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.subset_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ Δ : Sequent V L} : Γ ⊆ Δ ↔ Γ.val ⊆ Δ.val

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.val_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : ∅.val = ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.val_singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Formula V L) : {φ}.val = {φ.val}

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.val_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Formula V L) (Γ : Sequent V L) : (insert φ Γ).val = insert φ.val Γ.val

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.val_union {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ Δ : Sequent V L) : (Γ ∪ Δ).val = Γ.val ∪ Δ.val

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.not_mem_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (φ : Formula V L) : φ ∉ ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.mem_singleton_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {φ ψ : Formula V L} : φ ∈ {ψ} ↔ φ = ψ

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.mem_insert_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : Sequent V L} {φ ψ : Formula V L} : φ ∈ insert ψ Γ ↔ φ = ψ ∨ φ ∈ Γ

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.mem_union_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ Δ : Sequent V L} {φ : Formula V L} : φ ∈ Γ ∪ Δ ↔ φ ∈ Γ ∨ φ ∈ Δ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.ext {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ Δ : Sequent V L} (h : ∀ (x : Formula V L), x ∈ Γ ↔ x ∈ Δ) : Γ = Δ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.ext_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ Δ : Sequent V L} : Γ = Δ ↔ ∀ (x : Formula V L), x ∈ Γ ↔ x ∈ Δ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.ext' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ Δ : Sequent V L} (h : Γ.val = Δ.val) : Γ = Δ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.insert_empty_eq_singleton {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {φ : Formula V L} : insert φ ∅ = {φ}

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

Equations

• s.shift = { val := LO.FirstOrder.Arithmetic.Bootstrapping.setShift L s.val, val_formulaSet := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.shift_empty {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : ∅.shift = ∅

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.shift_insert {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : Sequent V L} {φ : Formula V L} : (insert φ Γ).shift = insert (Semiformula.shift φ) Γ.shift

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Sequent.insert_eq_of_mem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {Γ : Sequent V L} {φ : Formula V L} (h : φ ∈ Γ) : insert φ Γ = Γ

structure LO.FirstOrder.Arithmetic.Bootstrapping.InternalTheory (V : Type u_2) (L : Language) [L.Encodable] [L.LORDefinable] : Type u_3

Auxiliary theories for the typed internal proof.

• theory : Theory L
• Δ₁ : self.theory.Δ₁

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instCoeOutInternalTheoryTheory {V : Type u_1} {L : Language} [L.Encodable] [L.LORDefinable] : CoeOut (InternalTheory V L) (Theory L)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instCoeOutInternalTheoryTheory = { coe := LO.FirstOrder.Arithmetic.Bootstrapping.InternalTheory.theory }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Theory {V : Type u_1} {L : Language} [L.Encodable] [L.LORDefinable] (T : InternalTheory V L) : T.theory.Δ₁

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instΔ₁Theory T = T.Δ₁

def LO.FirstOrder.Theory.internalize (V : Type u_1) {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : Arithmetic.Bootstrapping.InternalTheory V L

Equations

• LO.FirstOrder.Theory.internalize V T = { theory := T, Δ₁ := inferInstance }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.internalize_theory {V : Type u_1} {L : Language} [L.Encodable] [L.LORDefinable] (T : Theory L) [T.Δ₁] : (Theory.internalize V T).theory = T

structure LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : InternalTheory V L) (Γ : Sequent V L) : Type u_1

• val : V
• derivationOf : DerivationOf T.theory self.val Γ.val

def LO.FirstOrder.Arithmetic.Bootstrapping.«term_⊢!ᵈᵉʳ_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.TProof {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (T : InternalTheory V L) (φ : Formula V L) : Type u_1

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof T φ = LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation T (insert φ ∅)

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instEntailmentInternalTheoryFormula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : Entailment (InternalTheory V L) (Formula V L)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.instEntailmentInternalTheoryFormula = { Prf := LO.FirstOrder.Arithmetic.Bootstrapping.TProof }

@[implicit_reducible]

instance LO.FirstOrder.Arithmetic.Bootstrapping.instHasSubsetInternalTheory {V : Type u_1} [ORingStructure V] {L : Language} [L.Encodable] [L.LORDefinable] : HasSubset (InternalTheory V L)

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.toTDerivation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} (Γ : Sequent V L) (h : Derivable T.theory Γ.val) : TDerivation T Γ

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.toDerivable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (d : TDerivation T Γ) : Derivable T.theory Γ.val

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProvable.iff_provable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {σ : Formula V L} : T ⊢ σ ↔ Provable T.theory σ.val

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Provable.toTProvable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {σ : Formula V L} : Provable T.theory σ.val → T ⊢ σ

Alias of the reverse direction of LO.FirstOrder.Arithmetic.Bootstrapping.TProvable.iff_provable.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.toProvable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {σ : Formula V L} : T ⊢ σ → Provable T.theory σ.val

Alias of the forward direction of LO.FirstOrder.Arithmetic.Bootstrapping.TProvable.iff_provable.

def LO.FirstOrder.Arithmetic.Bootstrapping.proof_to_tDerivation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {σ : Formula V L} : T ⊢! σ → TDerivation T (insert σ ∅)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.proof_to_tDerivation x = x

theorem LO.FirstOrder.Arithmetic.Bootstrapping.tprovable_iff_provable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {σ : Formula V L} : Theory.internalize V T ⊢ σ ↔ Provable T σ.val

theorem LO.FirstOrder.Arithmetic.Bootstrapping.tprovable_tquote_iff_provable_quote {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {φ : Proposition L} : Theory.internalize V T ⊢ ⌜φ⌝ ↔ Provable T ⌜φ⌝

theorem LO.FirstOrder.Arithmetic.Bootstrapping.tprovable_tquote_iff_provable_quote_sentence {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : Theory L} [T.Δ₁] {σ : Sentence L} : Theory.internalize V T ⊢ ⌜σ⌝ ↔ Provable T ⌜σ⌝

def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.toTProof {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Formula V L} (d : TDerivation T (insert φ ∅)) : T ⊢! φ

Equations

• d.toTProof = d

def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.of_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ Δ : Sequent V L} (d : TDerivation T Γ) (e : Γ = Δ) : TDerivation T Δ

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.toTDerivation {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Formula V L} (d : T ⊢! φ) : TDerivation T (insert φ ∅)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.toTDerivation d = d

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.cast {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ Δ : Sequent V L} (e : Γ = Δ) : TDerivation T Γ → TDerivation T Δ

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.cast_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ Δ : Sequent V L} (e : Γ = Δ) (d : TDerivation T Γ) : (TDerivation.cast e d).val = d.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.byAxm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (φ : Formula V L) (h : tmem φ T.theory) (hΓ : φ ∈ Γ) : TDerivation T Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.byAxm φ h hΓ = { val := LO.FirstOrder.Arithmetic.Bootstrapping.axm Γ.val φ.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.byAxm_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (φ : Formula V L) (h : tmem φ T.theory) (hΓ : φ ∈ Γ) : (byAxm φ h hΓ).val = axm Γ.val φ.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.em {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (φ : Formula V L) (h : φ ∈ Γ := by simp) (hn : ∼φ ∈ Γ := by simp) : TDerivation T Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.em φ h hn = { val := LO.FirstOrder.Arithmetic.Bootstrapping.axL Γ.val φ.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.em_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (φ : Formula V L) (h : φ ∈ Γ) (hn : ∼φ ∈ Γ) : (em φ h hn).val = axL Γ.val φ.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (h : ⊤ ∈ Γ := by simp) : TDerivation T Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.verum h = { val := LO.FirstOrder.Arithmetic.Bootstrapping.verumIntro Γ.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.verum_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (h : ⊤ ∈ Γ) : (verum h).val = verumIntro Γ.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.and' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (H : φ ⋏ ψ ∈ Γ) (dp : TDerivation T (insert φ Γ)) (dq : TDerivation T (insert ψ Γ)) : TDerivation T Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.and' H dp dq = { val := LO.FirstOrder.Arithmetic.Bootstrapping.andIntro Γ.val φ.val ψ.val dp.val dq.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.and'_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (H : φ ⋏ ψ ∈ Γ) (dp : TDerivation T (insert φ Γ)) (dq : TDerivation T (insert ψ Γ)) : (and' H dp dq).val = andIntro Γ.val φ.val ψ.val dp.val dq.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.or' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (H : φ ⋎ ψ ∈ Γ) (dpq : TDerivation T (insert φ (insert ψ Γ))) : TDerivation T Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.or' H dpq = { val := LO.FirstOrder.Arithmetic.Bootstrapping.orIntro Γ.val φ.val ψ.val dpq.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.or'_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (H : φ ⋎ ψ ∈ Γ) (dpq : TDerivation T (insert φ (insert ψ Γ))) : (or' H dpq).val = orIntro Γ.val φ.val ψ.val dpq.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.all' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Semiformula V L 1} (H : ∀¹ φ ∈ Γ) (dp : TDerivation T (insert φ.free Γ.shift)) : TDerivation T Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.all' H dp = { val := LO.FirstOrder.Arithmetic.Bootstrapping.allIntro Γ.val φ.val dp.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.all'_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Semiformula V L 1} (H : ∀¹ φ ∈ Γ) (dp : TDerivation T (insert φ.free Γ.shift)) : (all' H dp).val = allIntro Γ.val φ.val dp.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.exs' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Semiformula V L 1} (H : ∃¹ φ ∈ Γ) (t : Term V L) (dp : TDerivation T (insert (Semiformula.subst ![t] φ) Γ)) : TDerivation T Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.exs' H t dp = { val := LO.FirstOrder.Arithmetic.Bootstrapping.exsIntro Γ.val φ.val t.val dp.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.exs'_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Semiformula V L 1} (H : ∃¹ φ ∈ Γ) (t : Term V L) (dp : TDerivation T (insert (Semiformula.subst ![t] φ) Γ)) : (exs' H t dp).val = exsIntro Γ.val φ.val t.val dp.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.wk {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ Δ : Sequent V L} (d : TDerivation T Δ) (h : Δ ⊆ Γ) : TDerivation T Γ

Equations

• d.wk h = { val := LO.FirstOrder.Arithmetic.Bootstrapping.wkRule Γ.val d.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.wk_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ Δ : Sequent V L} (d : TDerivation T Δ) (h : Δ ⊆ Γ) : (d.wk h).val = wkRule Γ.val d.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (d : TDerivation T Γ) : TDerivation T Γ.shift

Equations

• d.shift = { val := LO.FirstOrder.Arithmetic.Bootstrapping.shiftRule Γ.shift.val d.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.shift_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} (d : TDerivation T Γ) : d.shift.val = shiftRule Γ.shift.val d.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.cut {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Formula V L} (d₁ : TDerivation T (insert φ Γ)) (d₂ : TDerivation T (insert (∼φ) Γ)) : TDerivation T Γ

Equations

• d₁.cut d₂ = { val := LO.FirstOrder.Arithmetic.Bootstrapping.cutRule Γ.val φ.val d₁.val d₂.val, derivationOf := ⋯ }

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.cut_val {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Formula V L} (d₁ : TDerivation T (insert φ Γ)) (d₂ : TDerivation T (insert (∼φ) Γ)) : (d₁.cut d₂).val = cutRule Γ.val φ.val d₁.val d₂.val

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (dp : TDerivation T (insert φ Γ)) (dq : TDerivation T (insert ψ Γ)) : TDerivation T (insert (φ ⋏ ψ) Γ)

Equations

• dp.and dq = LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.toTDerivation (insert (φ ⋏ ψ) Γ) ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (dpq : TDerivation T (insert φ (insert ψ Γ))) : TDerivation T (insert (φ ⋎ ψ) Γ)

Equations

• dpq.or = LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.toTDerivation (insert (φ ⋎ ψ) Γ) ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Semiformula V L 1} (dp : TDerivation T (insert φ.free Γ.shift)) : TDerivation T (insert (∀¹ φ) Γ)

Equations

• dp.all = LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.toTDerivation (insert (∀¹ φ) Γ) ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.exs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Semiformula V L 1} (t : Term V L) (dp : TDerivation T (insert (Semiformula.subst ![t] φ) Γ)) : TDerivation T (insert (∃¹ φ) Γ)

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.exs t dp = LO.FirstOrder.Arithmetic.Bootstrapping.Derivable.toTDerivation (insert (∃¹ φ) Γ) ⋯

def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.ofSubset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T U : InternalTheory V L} {Γ : Sequent V L} (h : T ⊆ U) (d : TDerivation T Γ) : TDerivation U Γ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.ofSubset h d = { val := d.val, derivationOf := ⋯ }

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.cut' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ Δ : Sequent V L} {φ : Formula V L} (d₁ : TDerivation T (insert φ Γ)) (d₂ : TDerivation T (insert (∼φ) Δ)) : TDerivation T (Γ ∪ Δ)

Equations

• d₁.cut' d₂ = (d₁.wk ⋯).cut (d₂.wk ⋯)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.modusPonens {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (dpq : TDerivation T (insert (φ 🡒 ψ) Γ)) (dp : TDerivation T (insert φ Γ)) : TDerivation T (insert ψ Γ)

Equations

• dpq.modusPonens dp = (dpq.wk ⋯).cut (⋯.mpr ((dp.wk ⋯).and (LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.em ψ ⋯ ⋯)))

def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.ofEq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ Δ : Sequent V L} (d : TDerivation T Γ) (h : Γ = Δ) : TDerivation T Δ

Equations

• d.ofEq h = h ▸ d

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.rotate₁ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {p₀ p₁ : Formula V L} (d : TDerivation T (insert p₀ (insert p₁ Γ))) : TDerivation T (insert p₁ (insert p₀ Γ))

Equations

• d.rotate₁ = d.ofEq ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.rotate₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {p₀ p₁ p₂ : Formula V L} (d : TDerivation T (insert p₀ (insert p₁ (insert p₂ Γ)))) : TDerivation T (insert p₂ (insert p₁ (insert p₀ Γ)))

Equations

• d.rotate₂ = d.ofEq ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.rotate₃ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {p₀ p₁ p₂ p₃ : Formula V L} (d : TDerivation T (insert p₀ (insert p₁ (insert p₂ (insert p₃ Γ))))) : TDerivation T (insert p₃ (insert p₁ (insert p₂ (insert p₀ Γ))))

Equations

• d.rotate₃ = d.ofEq ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.orInv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ ψ : Formula V L} (d : TDerivation T (insert (φ ⋎ ψ) Γ)) : TDerivation T (insert φ (insert ψ Γ))

Equations

• d.orInv = (d.wk ⋯).cut (⋯.mpr ((LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.em φ ⋯ ⋯).and (LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.em ψ ⋯ ⋯)))

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.specialize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : Sequent V L} {φ : Semiformula V L 1} (b : TDerivation T (insert (∀¹ φ) Γ)) (t : Term V L) : TDerivation T (insert (Semiformula.subst ![t] φ) Γ)

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.modusPonens {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ ψ : Formula V L} (d : T ⊢! φ 🡒 ψ) (b : T ⊢! φ) : T ⊢! ψ

Condition D2

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.modusPonens d b = LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.modusPonens d b

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.byAxm {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Formula V L} (h : tmem φ T.theory) : T ⊢! φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.byAxm h = LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.byAxm φ h ⋯

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.ofSubset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T U : InternalTheory V L} (h : T ⊆ U) {φ : Formula V L} : T ⊢! φ → U ⊢! φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.ofSubset h = LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.ofSubset h

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.of_subset {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T U : InternalTheory V L} (h : T ⊆ U) {φ : Formula V L} : T ⊢ φ → U ⊢ φ

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.TProof.instModusPonensInternalTheoryFormula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} : Entailment.ModusPonens T

Equations

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

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.TProof.instNegationEquivInternalTheoryFormula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} : Entailment.NegationEquiv T

Equations

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

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.TProof.instMinimalInternalTheoryFormula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} : Entailment.Minimal T

Equations

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

@[implicit_reducible]

noncomputable instance LO.FirstOrder.Arithmetic.Bootstrapping.TProof.instClFormulaInternalTheory {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} : Entailment.Cl T

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.exsIntro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} (φ : Semiformula V L 1) (t : Term V L) (b : T ⊢! Semiformula.subst ![t] φ) : T ⊢! ∃¹ φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.exsIntro φ t b = LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.exs t b

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.ex_intro! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} (φ : Semiformula V L 1) (t : Term V L) (b : T ⊢ Semiformula.subst ![t] φ) : T ⊢ ∃¹ φ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 1} (b : T ⊢! ∀¹ φ) (t : Term V L) : T ⊢! Semiformula.subst ![t] φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize b t = LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.specialize b t

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 2} (b : T ⊢! ∀¹ ∀¹ φ) (t u : Term V L) : T ⊢! Semiformula.subst ![t, u] φ

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₃ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 3} (b : T ⊢! ∀¹ ∀¹ ∀¹ φ) (t₁ t₂ t₃ : Term V L) : T ⊢! Semiformula.subst ![t₁, t₂, t₃] φ

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₄ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 4} (b : T ⊢! ∀¹ ∀¹ ∀¹ ∀¹ φ) (t₁ t₂ t₃ t₄ : Term V L) : T ⊢! Semiformula.subst ![t₁, t₂, t₃, t₄] φ

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 1} (b : T ⊢ ∀¹ φ) (t : Term V L) : T ⊢ Semiformula.subst ![t] φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₂! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 2} (b : T ⊢ ∀¹ ∀¹ φ) (t u : Term V L) : T ⊢ Semiformula.subst ![t, u] φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₃! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 3} (b : T ⊢ ∀¹ ∀¹ ∀¹ φ) (t₁ t₂ t₃ : Term V L) : T ⊢ Semiformula.subst ![t₁, t₂, t₃] φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₄! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 4} (b : T ⊢ ∀¹ ∀¹ ∀¹ ∀¹ φ) (t₁ t₂ t₃ t₄ : Term V L) : T ⊢ Semiformula.subst ![t₁, t₂, t₃, t₄] φ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Formula V L} (d : T ⊢! φ) : T ⊢! Semiformula.shift φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.shift d = ⋯.mp (LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.shift d)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.shift! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Formula V L} (d : T ⊢ φ) : T ⊢ Semiformula.shift φ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 1} (dp : T ⊢! φ.free) : T ⊢! ∀¹ φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.all dp = (⋯.mpr dp).all

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.all₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 2} (d : T ⊢! Semiformula.subst ![Semiterm.fvar 0, Semiterm.fvar 1] φ.shift.shift) : T ⊢! ∀¹ ∀¹ φ

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.all₂! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 2} (d : T ⊢ Semiformula.subst ![Semiterm.fvar 0, Semiterm.fvar 1] φ.shift.shift) : T ⊢ ∀¹ ∀¹ φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.all! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 1} (dp : T ⊢ φ.free) : T ⊢ ∀¹ φ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 1} (b : T ⊢! ∀¹ φ) (t : Term V L) : T ⊢! Semiformula.subst ![t] φ.shift

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize_shift b t = LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize (⋯.mp (LO.FirstOrder.Arithmetic.Bootstrapping.TProof.shift b)) t

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₂_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 2} (b : T ⊢! ∀¹ ∀¹ φ) (t u : Term V L) : T ⊢! Semiformula.subst ![t, u] φ.shift.shift

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize₂_shift! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 2} (b : T ⊢ ∀¹ ∀¹ φ) (t u : Term V L) : T ⊢ Semiformula.subst ![t, u] φ.shift.shift

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.generalizeAux {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {C : Formula V L} {φ : Semiformula V L 1} (dp : T ⊢! Semiformula.shift C 🡒 φ.free) : T ⊢! C 🡒 ∀¹ φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.generalizeAux dp = ⋯.mpr ((LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.orInv (⋯.mp dp)).wk ⋯).all.rotate₁.or

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.conj_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (Γ : List (Formula V L)) : Semiformula.shift (⋀Γ) = ⋀List.map Semiformula.shift Γ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.generalize {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ : Semiformula V L 1} (d : List.map Semiformula.shift Γ ⊢[T]! φ.free) : Γ ⊢[T]! ∀¹ φ

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.generalize! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ : Semiformula V L 1} (d : List.map Semiformula.shift Γ ⊢[T] φ.free) : Γ ⊢[T] ∀¹ φ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specializeWithCtxAux {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {C : Formula V L} {φ : Semiformula V L 1} (d : T ⊢! C 🡒 ∀¹ φ) (t : Term V L) : T ⊢! C 🡒 Semiformula.subst ![t] φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specializeWithCtxAux d t = ⋯.mpr (((LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.orInv (⋯.mp d)).wk ⋯).specialize t).rotate₁.or

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specializeWithCtx {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ : Semiformula V L 1} (d : Γ ⊢[T]! ∀¹ φ) (t : Semiterm V L 0) : Γ ⊢[T]! Semiformula.subst ![t] φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specializeWithCtx d t = LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specializeWithCtxAux d t

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.specialize_with_ctx! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ : Semiformula V L 1} (d : Γ ⊢[T] ∀¹ φ) (t : Semiterm V L 0) : Γ ⊢[T] Semiformula.subst ![t] φ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.allImpAll {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ ψ : Semiformula V L 1} (d : List.map Semiformula.shift Γ ⊢[T]! φ.free 🡒 ψ.free) : Γ ⊢[T]! ∀¹ φ 🡒 ∀¹ ψ

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.all_imp_all! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ ψ : Semiformula V L 1} (d : List.map Semiformula.shift Γ ⊢[T] φ.free 🡒 ψ.free) : Γ ⊢[T] ∀¹ φ 🡒 ∀¹ ψ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.exsImpExs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ ψ : Semiformula V L 1} (d : List.map Semiformula.shift Γ ⊢[T]! φ.free 🡒 ψ.free) : Γ ⊢[T]! ∃¹ φ 🡒 ∃¹ ψ

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.exs_imp_exs! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {Γ : List (Semiformula V L 0)} {φ ψ : Semiformula V L 1} (d : List.map Semiformula.shift Γ ⊢[T] φ.free 🡒 ψ.free) : Γ ⊢[T] ∃¹ φ 🡒 ∃¹ ψ

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.TProof.exs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 1} (t : Semiterm V L 0) (dp : T ⊢! Semiformula.subst ![t] φ) : T ⊢! ∃¹ φ

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.TProof.exs t dp = LO.FirstOrder.Arithmetic.Bootstrapping.TDerivation.exs t (id dp)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.exs! {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {T : InternalTheory V L} {φ : Semiformula V L 1} (t : Semiterm V L 0) (dp : T ⊢ Semiformula.subst ![t] φ) : T ⊢ ∃¹ φ

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.substItrDisj_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (A : InternalTheory V ℒₒᵣ) {m : ℕ} {i z : V} (w : TermVec V ℒₒᵣ m) (φ : Semiformula V ℒₒᵣ (m + 1)) (hi : i < z) : A ⊢ Semiformula.subst (Arithmetic.typedNumeral i :> w) φ 🡒 Semiformula.substItrDisj w φ z

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.substItrDisj_right_intro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (A : InternalTheory V ℒₒᵣ) {m : ℕ} {ψ : Semiformula V ℒₒᵣ 0} {i z : V} {w : TermVec V ℒₒᵣ m} {φ : Semiformula V ℒₒᵣ (m + 1)} (hi : i < z) (h : A ⊢ ψ 🡒 Semiformula.subst (Arithmetic.typedNumeral i :> w) φ) : A ⊢ ψ 🡒 Semiformula.substItrDisj w φ z

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.substItrConj_right_intro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (A : InternalTheory V ℒₒᵣ) {m : ℕ} {ψ : Semiformula V ℒₒᵣ 0} {w : TermVec V ℒₒᵣ m} {φ : Semiformula V ℒₒᵣ (m + 1)} {z : V} (h : ∀ i < z, A ⊢ ψ 🡒 Semiformula.subst (Arithmetic.typedNumeral i :> w) φ) : A ⊢ ψ 🡒 Semiformula.substItrConj w φ z

theorem LO.FirstOrder.Arithmetic.Bootstrapping.TProof.substItrDisj_left_intro {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (A : InternalTheory V ℒₒᵣ) {m : ℕ} {ψ : Semiformula V ℒₒᵣ 0} {w : TermVec V ℒₒᵣ m} {φ : Semiformula V ℒₒᵣ (m + 1)} {z : V} (h : ∀ i < z, A ⊢ Semiformula.subst (Arithmetic.typedNumeral i :> w) φ 🡒 ψ) : A ⊢ Semiformula.substItrDisj w φ z 🡒 ψ