Typed Formalized Tait-Calculus

@[reducible, inline]

abbrev LO.Arith.Language.Semiformula.substs₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) (t : L.Term) : L.Formula

Equations

• p.substs₁ t = p^/[LO.Arith.Language.Semiterm.sing t]

@[reducible, inline]

abbrev LO.Arith.Language.Semiformula.free {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) : L.Formula

Equations

• p.free = p.shift.substs₁ (L.fvar 0)

@[simp]

theorem LO.Arith.Language.Semiformula.val_substs₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) (t : L.Term) : (p.substs₁ t).val = L.substs ?[t.val] p.val

@[simp]

theorem LO.Arith.Language.Semiformula.val_free {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) : p.free.val = L.substs ?[qqFvar 0] (L.shift p.val)

@[simp]

theorem LO.Arith.substs₁_neg {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1)) (t : L.Term) : (∼p).substs₁ t = ∼p.substs₁ t

@[simp]

theorem LO.Arith.substs₁_all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1 + 1)) (t : L.Term) : p.all.substs₁ t = p^/[(Language.Semiterm.sing t).q].all

@[simp]

theorem LO.Arith.substs₁_ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Semiformula (0 + 1 + 1)) (t : L.Term) : p.ex.substs₁ t = p^/[(Language.Semiterm.sing t).q].ex

@[reducible, inline]

abbrev LO.Arith.Language.Theory.tmem {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) (T : L.Theory) : Prop

Equations

• LO.Arith.Language.Theory.tmem p T = (p.val ∈ T)

def LO.Arith.«term_∈'_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_∈'_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_∈'_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈' ") (Lean.ParserDescr.cat `term 51))

structure LO.Arith.Language.Sequent {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Type u_1

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

Instances For

• LO.Arith.instEmptyCollectionSequent
• LO.Arith.instHasSubsetSequent
• LO.Arith.instInsertFormulaSequent
• LO.Arith.instMembershipFormulaSequent
• LO.Arith.instSingletonFormulaSequent
• LO.Arith.instUnionSequent

instance LO.Arith.instEmptyCollectionSequent {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : EmptyCollection L.Sequent

Equations

• LO.Arith.instEmptyCollectionSequent = { emptyCollection := { val := ∅, val_formulaSet := ⋯ } }

instance LO.Arith.instSingletonFormulaSequent {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Singleton L.Formula L.Sequent

Equations

• LO.Arith.instSingletonFormulaSequent = { singleton := fun (p : L.Formula) => { val := {p.val}, val_formulaSet := ⋯ } }

instance LO.Arith.instInsertFormulaSequent {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Insert L.Formula L.Sequent

Equations

• LO.Arith.instInsertFormulaSequent = { insert := fun (p : L.Formula) (Γ : L.Sequent) => { val := insert p.val Γ.val, val_formulaSet := ⋯ } }

instance LO.Arith.instUnionSequent {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Union L.Sequent

Equations

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

instance LO.Arith.instMembershipFormulaSequent {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Membership L.Formula L.Sequent

Equations

• LO.Arith.instMembershipFormulaSequent = { mem := fun (Γ : L.Sequent) (p : L.Formula) => p.val ∈ Γ.val }

instance LO.Arith.instHasSubsetSequent {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : HasSubset L.Sequent

Equations

• LO.Arith.instHasSubsetSequent = { Subset := fun (x1 x2 : L.Sequent) => x1.val ⊆ x2.val }

def LO.Arith.«term_⫽_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_⫽_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_⫽_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⫽ ") (Lean.ParserDescr.cat `term 50))

theorem LO.Arith.Language.Sequent.mem_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {p : L.Formula} : p ∈ Γ ↔ p.val ∈ Γ.val

theorem LO.Arith.Language.Sequent.subset_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ Δ : L.Sequent} : Γ ⊆ Δ ↔ Γ.val ⊆ Δ.val

@[simp]

theorem LO.Arith.Language.Sequent.val_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : ∅.val = ∅

@[simp]

theorem LO.Arith.Language.Sequent.val_singleton {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) : {p}.val = {p.val}

@[simp]

theorem LO.Arith.Language.Sequent.val_insert {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) (Γ : L.Sequent) : (insert p Γ).val = insert p.val Γ.val

@[simp]

theorem LO.Arith.Language.Sequent.val_union {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (Γ Δ : L.Sequent) : (Γ ∪ Δ).val = Γ.val ∪ Δ.val

@[simp]

theorem LO.Arith.Language.Sequent.not_mem_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (p : L.Formula) : p ∉ ∅

@[simp]

theorem LO.Arith.Language.Sequent.mem_singleton_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p q : L.Formula} : p ∈ {q} ↔ p = q

@[simp]

theorem LO.Arith.Language.Sequent.mem_insert_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {p q : L.Formula} : p ∈ insert q Γ ↔ p = q ∨ p ∈ Γ

@[simp]

theorem LO.Arith.Language.Sequent.mem_union_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ Δ : L.Sequent} {p : L.Formula} : p ∈ Γ ∪ Δ ↔ p ∈ Γ ∨ p ∈ Δ

theorem LO.Arith.Language.Sequent.ext {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ Δ : L.Sequent} (h : ∀ (x : L.Formula), x ∈ Γ ↔ x ∈ Δ) : Γ = Δ

theorem LO.Arith.Language.Sequent.ext' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ Δ : L.Sequent} (h : Γ.val = Δ.val) : Γ = Δ

def LO.Arith.Language.Sequent.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (s : L.Sequent) : L.Sequent

Equations

• s.shift = { val := L.setShift s.val, val_formulaSet := ⋯ }

@[simp]

theorem LO.Arith.Language.Sequent.shift_empty {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : ∅.shift = ∅

@[simp]

theorem LO.Arith.Language.Sequent.shift_insert {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {Γ : L.Sequent} {p : L.Formula} : (insert p Γ).shift = insert (Semiformula.shift p) Γ.shift

structure LO.Arith.Language.TTheory {V : Type u_1} [ORingStruc V] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Type u_1

• thy : L.Theory
• pthy : pL.TDef
• defined : self.thy.Defined self.pthy

Instances For

• LO.Arith.instHasSubsetTTheory
• LO.Arith.instSystemFormulaTTheory

instance LO.Arith.instDefinedThyPthy {V : Type u_1} [ORingStruc V] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.TTheory) : T.thy.Defined T.pthy

structure LO.Arith.Language.Theory.TDerivation {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.TTheory) (Γ : L.Sequent) : Type u_1

• derivation : V
• derivationOf : T.thy.DerivationOf self.derivation Γ.val

def LO.Arith.«term_⊢¹_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_⊢¹_» = Lean.ParserDescr.trailingNode `LO.Arith.«term_⊢¹_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢¹ ") (Lean.ParserDescr.cat `term 46))

def LO.Arith.Language.Theory.TProof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.TTheory) (p : L.Formula) : Type u_1

Equations

• LO.Arith.Language.Theory.TProof T p = LO.Arith.Language.Theory.TDerivation T (insert p ∅)

instance LO.Arith.instSystemFormulaTTheory {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : System L.Formula L.TTheory

Equations

• LO.Arith.instSystemFormulaTTheory = { Prf := LO.Arith.Language.Theory.TProof }

instance LO.Arith.instHasSubsetTTheory {V : Type u_1} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : HasSubset L.TTheory

Equations

• LO.Arith.instHasSubsetTTheory = { Subset := fun (T U : L.TTheory) => T.thy ⊆ U.thy }

def LO.Arith.Language.Theory.Derivable.toTDerivation {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (Γ : L.Sequent) (h : T.thy.Derivable Γ.val) : TDerivation T Γ

Equations

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

theorem LO.Arith.Language.Theory.TDerivation.toDerivable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (d : TDerivation T Γ) : T.thy.Derivable Γ.val

theorem LO.Arith.Language.Theory.TProvable.iff_provable {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {σ : L.Formula} : T ⊢! σ ↔ T.thy.Provable σ.val

def LO.Arith.Language.Theory.TDerivation.toTProof {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Formula} (d : TDerivation T (insert p ∅)) : T ⊢ p

Equations

• d.toTProof = d

def LO.Arith.Language.Theory.TProof.toTDerivation {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Formula} (d : T ⊢ p) : TDerivation T (insert p ∅)

Equations

• LO.Arith.Language.Theory.TProof.toTDerivation d = d

def LO.Arith.Language.Theory.TDerivation.byAxm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (p : L.Formula) (h : tmem p T.thy) (hΓ : p ∈ Γ) : TDerivation T Γ

Equations

• LO.Arith.Language.Theory.TDerivation.byAxm p h hΓ = LO.Arith.Language.Theory.Derivable.toTDerivation Γ ⋯

def LO.Arith.Language.Theory.TDerivation.em {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (p : L.Formula) (h : p ∈ Γ := by simp) (hn : ∼p ∈ Γ := by simp) : TDerivation T Γ

Equations

• LO.Arith.Language.Theory.TDerivation.em p h hn = LO.Arith.Language.Theory.Derivable.toTDerivation Γ ⋯

def LO.Arith.Language.Theory.TDerivation.verum {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (h : ⊤ ∈ Γ := by simp) : TDerivation T Γ

Equations

• LO.Arith.Language.Theory.TDerivation.verum h = LO.Arith.Language.Theory.Derivable.toTDerivation Γ ⋯

def LO.Arith.Language.Theory.TDerivation.and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p q : L.Formula} (dp : TDerivation T (insert p Γ)) (dq : TDerivation T (insert q Γ)) : TDerivation T (insert (p ⋏ q) Γ)

Equations

• dp.and dq = LO.Arith.Language.Theory.Derivable.toTDerivation (insert (p ⋏ q) Γ) ⋯

def LO.Arith.Language.Theory.TDerivation.or {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p q : L.Formula} (dpq : TDerivation T (insert p (insert q Γ))) : TDerivation T (insert (p ⋎ q) Γ)

Equations

• dpq.or = LO.Arith.Language.Theory.Derivable.toTDerivation (insert (p ⋎ q) Γ) ⋯

def LO.Arith.Language.Theory.TDerivation.all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Semiformula (0 + 1)} (dp : TDerivation T (insert p.free Γ.shift)) : TDerivation T (insert p.all Γ)

Equations

• dp.all = LO.Arith.Language.Theory.Derivable.toTDerivation (insert p.all Γ) ⋯

def LO.Arith.Language.Theory.TDerivation.ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Semiformula (0 + 1)} (t : L.Term) (dp : TDerivation T (insert (p.substs₁ t) Γ)) : TDerivation T (insert p.ex Γ)

Equations

• LO.Arith.Language.Theory.TDerivation.ex t dp = LO.Arith.Language.Theory.Derivable.toTDerivation (insert p.ex Γ) ⋯

def LO.Arith.Language.Theory.TDerivation.wk {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ Δ : L.Sequent} (d : TDerivation T Δ) (h : Δ ⊆ Γ) : TDerivation T Γ

Equations

• d.wk h = LO.Arith.Language.Theory.Derivable.toTDerivation Γ ⋯

def LO.Arith.Language.Theory.TDerivation.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (d : TDerivation T Γ) : TDerivation T Γ.shift

Equations

• d.shift = LO.Arith.Language.Theory.Derivable.toTDerivation Γ.shift ⋯

def LO.Arith.Language.Theory.TDerivation.cut {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Formula} (d₁ : TDerivation T (insert p Γ)) (d₂ : TDerivation T (insert (∼p) Γ)) : TDerivation T Γ

Equations

• d₁.cut d₂ = LO.Arith.Language.Theory.Derivable.toTDerivation Γ ⋯

def LO.Arith.Language.Theory.TDerivation.ofSubset {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T U : L.TTheory} {Γ : L.Sequent} (h : T ⊆ U) (d : TDerivation T Γ) : TDerivation U Γ

Equations

• LO.Arith.Language.Theory.TDerivation.ofSubset h d = { derivation := d.derivation, derivationOf := ⋯ }

def LO.Arith.Language.Theory.TDerivation.cut' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ Δ : L.Sequent} {p : L.Formula} (d₁ : TDerivation T (insert p Γ)) (d₂ : TDerivation T (insert (∼p) Δ)) : TDerivation T (Γ ∪ Δ)

Equations

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

def LO.Arith.Language.Theory.TDerivation.conj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (ps : SemiformulaVec 0) (ds : (i : V) → (hi : i < len ps.val) → TDerivation T (insert (ps.nth i hi) Γ)) : TDerivation T (insert ps.conj Γ)

Equations

• LO.Arith.Language.Theory.TDerivation.conj ps ds = LO.Arith.Language.Theory.Derivable.toTDerivation (insert ps.conj Γ) ⋯

def LO.Arith.Language.Theory.TDerivation.disj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} (ps : SemiformulaVec 0) {i : V} (hi : i < len ps.val) (d : TDerivation T (insert (ps.nth i hi) Γ)) : TDerivation T (insert ps.disj Γ)

Equations

• LO.Arith.Language.Theory.TDerivation.disj ps hi d = LO.Arith.Language.Theory.Derivable.toTDerivation (insert ps.disj Γ) ⋯

def LO.Arith.Language.Theory.TDerivation.modusPonens {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p q : L.Formula} (dpq : TDerivation T (insert (p ➝ q) Γ)) (dp : TDerivation T (insert p Γ)) : TDerivation T (insert q Γ)

Equations

• dpq.modusPonens dp = (dpq.wk ⋯).cut (⋯.mpr ((dp.wk ⋯).and (LO.Arith.Language.Theory.TDerivation.em q ⋯ ⋯)))

def LO.Arith.Language.Theory.TDerivation.ofEq {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ Δ : L.Sequent} (d : TDerivation T Γ) (h : Γ = Δ) : TDerivation T Δ

Equations

• d.ofEq h = h ▸ d

def LO.Arith.Language.Theory.TDerivation.rotate₁ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p₀ p₁ : L.Formula} (d : TDerivation T (insert p₀ (insert p₁ Γ))) : TDerivation T (insert p₁ (insert p₀ Γ))

Equations

• d.rotate₁ = d.ofEq ⋯

def LO.Arith.Language.Theory.TDerivation.rotate₂ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p₀ p₁ p₂ : L.Formula} (d : TDerivation T (insert p₀ (insert p₁ (insert p₂ Γ)))) : TDerivation T (insert p₂ (insert p₁ (insert p₀ Γ)))

Equations

• d.rotate₂ = d.ofEq ⋯

def LO.Arith.Language.Theory.TDerivation.rotate₃ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p₀ p₁ p₂ p₃ : L.Formula} (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 ⋯

def LO.Arith.Language.Theory.TDerivation.orInv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p q : L.Formula} (d : TDerivation T (insert (p ⋎ q) Γ)) : TDerivation T (insert p (insert q Γ))

Equations

• d.orInv = (d.wk ⋯).cut (⋯.mpr ((LO.Arith.Language.Theory.TDerivation.em p ⋯ ⋯).and (LO.Arith.Language.Theory.TDerivation.em q ⋯ ⋯)))

def LO.Arith.Language.Theory.TDerivation.specialize {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : L.Sequent} {p : L.Semiformula (0 + 1)} (b : TDerivation T (insert p.all Γ)) (t : L.Term) : TDerivation T (insert (p.substs₁ t) Γ)

Equations

• b.specialize t = (b.wk ⋯).cut (⋯.mpr (LO.Arith.Language.Theory.TDerivation.ex t (LO.Arith.Language.Theory.TDerivation.em (p.substs₁ t) ⋯ ⋯)))

def LO.Arith.Language.Theory.TProof.modusPonens {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p q : L.Formula} (d : T ⊢ p ➝ q) (b : T ⊢ p) : T ⊢ q

Condition D2

Equations

• LO.Arith.Language.Theory.TProof.modusPonens d b = LO.Arith.Language.Theory.TDerivation.modusPonens d b

def LO.Arith.Language.Theory.TProof.byAxm {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Formula} (h : tmem p T.thy) : T ⊢ p

Equations

• LO.Arith.Language.Theory.TProof.byAxm h = LO.Arith.Language.Theory.TDerivation.byAxm p h ⋯

def LO.Arith.Language.Theory.TProof.ofSubset {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T U : L.TTheory} (h : T ⊆ U) {p : L.Formula} : T ⊢ p → U ⊢ p

Equations

• LO.Arith.Language.Theory.TProof.ofSubset h = LO.Arith.Language.Theory.TDerivation.ofSubset h

theorem LO.Arith.Language.Theory.TProof.of_subset {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T U : L.TTheory} (h : T ⊆ U) {p : L.Formula} : T ⊢! p → U ⊢! p

instance LO.Arith.Language.Theory.TProof.instModusPonensTTheoryFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} : System.ModusPonens T

Equations

• LO.Arith.Language.Theory.TProof.instModusPonensTTheoryFormula = { mdp := fun {φ ψ : L.Formula} => LO.Arith.Language.Theory.TProof.modusPonens }

instance LO.Arith.Language.Theory.TProof.instNegationEquivTTheoryFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} : System.NegationEquiv T

Equations

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

instance LO.Arith.Language.Theory.TProof.instMinimalTTheoryFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} : System.Minimal T

Equations

• LO.Arith.Language.Theory.TProof.instMinimalTTheoryFormula = LO.System.Minimal.mk

instance LO.Arith.Language.Theory.TProof.instClassicalTTheoryFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} : System.Classical T

Equations

• LO.Arith.Language.Theory.TProof.instClassicalTTheoryFormula = LO.System.Classical.mk

def LO.Arith.Language.Theory.TProof.exIntro {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (p : L.Semiformula (0 + 1)) (t : L.Term) (b : T ⊢ p.substs₁ t) : T ⊢ p.ex

Equations

• LO.Arith.Language.Theory.TProof.exIntro p t b = LO.Arith.Language.Theory.TDerivation.ex t b

theorem LO.Arith.Language.Theory.TProof.ex_intro! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (p : L.Semiformula (0 + 1)) (t : L.Term) (b : T ⊢! p.substs₁ t) : T ⊢! p.ex

def LO.Arith.Language.Theory.TProof.specialize {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (b : T ⊢ p.all) (t : L.Term) : T ⊢ p.substs₁ t

Equations

• LO.Arith.Language.Theory.TProof.specialize b t = LO.Arith.Language.Theory.TDerivation.specialize b t

theorem LO.Arith.Language.Theory.TProof.specialize! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (b : T ⊢! p.all) (t : L.Term) : T ⊢! p.substs₁ t

def LO.Arith.Language.Theory.TProof.conj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : SemiformulaVec 0) (ds : (i : V) → (hi : i < len ps.val) → T ⊢ ps.nth i hi) : T ⊢ ps.conj

Equations

• LO.Arith.Language.Theory.TProof.conj ps ds = LO.Arith.Language.Theory.TDerivation.conj ps ds

theorem LO.Arith.Language.Theory.TProof.conj! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : SemiformulaVec 0) (ds : ∀ (i : V) (hi : i < len ps.val), T ⊢! ps.nth i hi) : T ⊢! ps.conj

def LO.Arith.Language.Theory.TProof.conj' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : SemiformulaVec 0) (ds : (i : V) → (hi : i < len ps.val) → T ⊢ ps.nth (len ps.val - (i + 1)) ⋯) : T ⊢ ps.conj

Equations

• LO.Arith.Language.Theory.TProof.conj' ps ds = LO.Arith.Language.Theory.TDerivation.conj ps fun (i : V) (hi : i < LO.Arith.len ps.val) => ⋯.mp (ds (LO.Arith.len ps.val - (i + 1)) ⋯)

def LO.Arith.Language.Theory.TProof.conjOr' {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : SemiformulaVec 0) (q : L.Semiformula 0) (ds : (i : V) → (hi : i < len ps.val) → T ⊢ ps.nth (len ps.val - (i + 1)) ⋯ ⋎ q) : T ⊢ ps.conj ⋎ q

Equations

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

def LO.Arith.Language.Theory.TProof.disj {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} (ps : SemiformulaVec 0) {i : V} (hi : i < len ps.val) (d : T ⊢ ps.nth i hi) : T ⊢ ps.disj

Equations

• LO.Arith.Language.Theory.TProof.disj ps hi d = LO.Arith.Language.Theory.TDerivation.disj ps hi d

def LO.Arith.Language.Theory.TProof.shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Formula} (d : T ⊢ p) : T ⊢ Semiformula.shift p

Equations

• LO.Arith.Language.Theory.TProof.shift d = ⋯.mp (LO.Arith.Language.Theory.TDerivation.shift d)

theorem LO.Arith.Language.Theory.TProof.shift! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Formula} (d : T ⊢! p) : T ⊢! Semiformula.shift p

def LO.Arith.Language.Theory.TProof.all {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (dp : T ⊢ p.free) : T ⊢ p.all

Equations

• LO.Arith.Language.Theory.TProof.all dp = (⋯.mpr dp).all

theorem LO.Arith.Language.Theory.TProof.all! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (dp : T ⊢! p.free) : T ⊢! p.all

def LO.Arith.Language.Theory.TProof.generalizeAux {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {C : L.Formula} {p : L.Semiformula (0 + 1)} (dp : T ⊢ Semiformula.shift C ➝ p.free) : T ⊢ C ➝ p.all

Equations

• LO.Arith.Language.Theory.TProof.generalizeAux dp = ⋯.mpr ((LO.Arith.Language.Theory.TDerivation.orInv (⋯.mp dp)).wk ⋯).all.rotate₁.or

theorem LO.Arith.Language.Theory.TProof.conj_shift {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (Γ : List L.Formula) : Semiformula.shift (⋀Γ) = ⋀List.map Semiformula.shift Γ

def LO.Arith.Language.Theory.TProof.generalize {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : List.map Semiformula.shift Γ ⊢[T] p.free) : Γ ⊢[T] p.all

Equations

• LO.Arith.Language.Theory.TProof.generalize d = LO.System.FiniteContext.ofDef (LO.Arith.Language.Theory.TProof.generalizeAux (⋯.mpr (LO.System.FiniteContext.toDef d)))

theorem LO.Arith.Language.Theory.TProof.generalize! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : List.map Semiformula.shift Γ ⊢[T]! p.free) : Γ ⊢[T]! p.all

def LO.Arith.Language.Theory.TProof.specializeWithCtxAux {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {C : L.Formula} {p : L.Semiformula (0 + 1)} (d : T ⊢ C ➝ p.all) (t : L.Term) : T ⊢ C ➝ p.substs₁ t

Equations

• LO.Arith.Language.Theory.TProof.specializeWithCtxAux d t = ⋯.mpr (((LO.Arith.Language.Theory.TDerivation.orInv (⋯.mp d)).wk ⋯).specialize t).rotate₁.or

def LO.Arith.Language.Theory.TProof.specializeWithCtx {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : Γ ⊢[T] p.all) (t : L.Term) : Γ ⊢[T] p.substs₁ t

Equations

• LO.Arith.Language.Theory.TProof.specializeWithCtx d t = LO.Arith.Language.Theory.TProof.specializeWithCtxAux d t

theorem LO.Arith.Language.Theory.TProof.specialize_with_ctx! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {Γ : List (L.Semiformula 0)} {p : L.Semiformula (0 + 1)} (d : Γ ⊢[T]! p.all) (t : L.Term) : Γ ⊢[T]! p.substs₁ t

def LO.Arith.Language.Theory.TProof.ex {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (t : L.Term) (dp : T ⊢ p.substs₁ t) : T ⊢ p.ex

Equations

• LO.Arith.Language.Theory.TProof.ex t dp = LO.Arith.Language.Theory.TDerivation.ex t dp

theorem LO.Arith.Language.Theory.TProof.ex! {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {T : L.TTheory} {p : L.Semiformula (0 + 1)} (t : L.Term) (dp : T ⊢! p.substs₁ t) : T ⊢! p.ex