Typed Formalized Tait-Calculus #
@[reducible, inline]
abbrev
LO.Arith.Language.Semiformula.substs₁
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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]
Instances For
@[reducible, inline]
abbrev
LO.Arith.Language.Semiformula.free
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Semiformula (0 + 1))
:
L.Formula
Equations
- p.free = p.shift.substs₁ (L.fvar 0)
Instances For
@[simp]
theorem
LO.Arith.Language.Semiformula.val_substs₁
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Semiformula (0 + 1))
:
p.free.val = L.substs ?[LO.Arith.qqFvar 0] (L.shift p.val)
@[simp]
theorem
LO.Arith.substs₁_neg
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Semiformula (0 + 1))
(t : L.Term)
:
@[simp]
theorem
LO.Arith.substs₁_all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Semiformula (0 + 1 + 1))
(t : L.Term)
:
p.all.substs₁ t = p^/[(LO.Arith.Language.Semiterm.sing t).q].all
@[simp]
theorem
LO.Arith.substs₁_ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Semiformula (0 + 1 + 1))
(t : L.Term)
:
p.ex.substs₁ t = p^/[(LO.Arith.Language.Semiterm.sing t).q].ex
@[reducible, inline]
abbrev
LO.Arith.Language.Theory.tmem
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Formula)
(T : L.Theory)
:
Equations
- LO.Arith.Language.Theory.tmem p T = (p.val ∈ T)
Instances For
Equations
- LO.Arith.«term_∈'_» = Lean.ParserDescr.trailingNode `LO.Arith.term_∈'_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈' ") (Lean.ParserDescr.cat `term 51))
Instances For
structure
LO.Arith.Language.Sequent
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Type u_1
- val : V
- val_formulaSet : L.IsFormulaSet self.val
Instances For
@[simp]
theorem
LO.Arith.Language.Sequent.val_formulaSet
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(self : L.Sequent)
:
L.IsFormulaSet self.val
instance
LO.Arith.instEmptyCollectionSequent
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
EmptyCollection L.Sequent
instance
LO.Arith.instSingletonFormulaSequent
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Insert L.Formula L.Sequent
instance
LO.Arith.instUnionSequent
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Union L.Sequent
instance
LO.Arith.instMembershipFormulaSequent
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Membership L.Formula L.Sequent
instance
LO.Arith.instHasSubsetSequent
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
HasSubset L.Sequent
Equations
- LO.Arith.«term_⫽_» = Lean.ParserDescr.trailingNode `LO.Arith.term_⫽_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⫽ ") (Lean.ParserDescr.cat `term 50))
Instances For
theorem
LO.Arith.Language.Sequent.mem_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : L.Sequent}
{p : L.Formula}
:
theorem
LO.Arith.Language.Sequent.subset_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : L.Sequent}
{Δ : L.Sequent}
:
@[simp]
theorem
LO.Arith.Language.Sequent.val_empty
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
@[simp]
theorem
LO.Arith.Language.Sequent.val_singleton
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Formula)
(Γ : L.Sequent)
:
@[simp]
theorem
LO.Arith.Language.Sequent.val_union
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(Γ : L.Sequent)
(Δ : L.Sequent)
:
@[simp]
theorem
LO.Arith.Language.Sequent.not_mem_empty
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(p : L.Formula)
:
p ∉ ∅
@[simp]
theorem
LO.Arith.Language.Sequent.mem_singleton_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{p : L.Formula}
{q : L.Formula}
:
@[simp]
theorem
LO.Arith.Language.Sequent.mem_insert_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : L.Sequent}
{p : L.Formula}
{q : L.Formula}
:
@[simp]
theorem
LO.Arith.Language.Sequent.mem_union_iff
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : L.Sequent}
{Δ : L.Sequent}
{p : L.Formula}
:
theorem
LO.Arith.Language.Sequent.ext
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : L.Sequent}
{Δ : L.Sequent}
(h : ∀ (x : L.Formula), x ∈ Γ ↔ x ∈ Δ)
:
Γ = Δ
theorem
LO.Arith.Language.Sequent.ext'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : L.Sequent}
{Δ : L.Sequent}
(h : Γ.val = Δ.val)
:
Γ = Δ
def
LO.Arith.Language.Sequent.shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(s : L.Sequent)
:
L.Sequent
Equations
- s.shift = { val := L.setShift s.val, val_formulaSet := ⋯ }
Instances For
@[simp]
theorem
LO.Arith.Language.Sequent.shift_empty
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
@[simp]
theorem
LO.Arith.Language.Sequent.shift_insert
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{Γ : L.Sequent}
{p : L.Formula}
:
(insert p Γ).shift = insert (LO.Arith.Language.Semiformula.shift p) Γ.shift
structure
LO.Arith.Language.TTheory
{V : Type u_1}
[LO.ORingStruc V]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
Type u_1
- thy : L.Theory
- pthy : pL.TDef
- defined : self.thy.Defined self.pthy
Instances For
instance
LO.Arith.instDefinedThyPthy
{V : Type u_1}
[LO.ORingStruc V]
(L : LO.Arith.Language V)
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.TTheory)
:
T.thy.Defined T.pthy
Equations
- LO.Arith.instDefinedThyPthy L T = T.defined
structure
LO.Arith.Language.Theory.TDerivation
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.TTheory)
(Γ : L.Sequent)
:
Type u_1
- derivation : V
- derivationOf : T.thy.DerivationOf self.derivation Γ.val
Instances For
theorem
LO.Arith.Language.Theory.TDerivation.derivationOf
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(self : LO.Arith.Language.Theory.TDerivation T Γ)
:
T.thy.DerivationOf self.derivation Γ.val
Equations
- LO.Arith.«term_⊢¹_» = Lean.ParserDescr.trailingNode `LO.Arith.term_⊢¹_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊢¹ ") (Lean.ParserDescr.cat `term 46))
Instances For
def
LO.Arith.Language.Theory.TProof
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(T : L.TTheory)
(p : L.Formula)
:
Type u_1
Equations
Instances For
instance
LO.Arith.instSystemFormulaTTheory
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
LO.System L.Formula L.TTheory
Equations
- LO.Arith.instSystemFormulaTTheory = { Prf := LO.Arith.Language.Theory.TProof }
instance
LO.Arith.instHasSubsetTTheory
{V : Type u_1}
[LO.ORingStruc V]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
:
HasSubset L.TTheory
def
LO.Arith.Language.Theory.Derivable.toTDerivation
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
(Γ : L.Sequent)
(h : T.thy.Derivable Γ.val)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.Arith.Language.Theory.TDerivation.toDerivable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(d : LO.Arith.Language.Theory.TDerivation T Γ)
:
T.thy.Derivable Γ.val
theorem
LO.Arith.Language.Theory.TProvable.iff_provable
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{σ : L.Formula}
:
def
LO.Arith.Language.Theory.TDerivation.toTProof
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{p : L.Formula}
(d : LO.Arith.Language.Theory.TDerivation T (insert p ∅))
:
T ⊢ p
Equations
- d.toTProof = d
Instances For
def
LO.Arith.Language.Theory.TProof.toTDerivation
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{p : L.Formula}
(d : T ⊢ p)
:
Equations
Instances For
def
LO.Arith.Language.Theory.TDerivation.byAxm
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(p : L.Formula)
(h : LO.Arith.Language.Theory.tmem p T.thy)
(hΓ : p ∈ Γ)
:
Equations
Instances For
def
LO.Arith.Language.Theory.TDerivation.em
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(p : L.Formula)
(h : autoParam (p ∈ Γ) _auto✝)
(hn : autoParam (∼p ∈ Γ) _auto✝)
:
Equations
Instances For
def
LO.Arith.Language.Theory.TDerivation.verum
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(h : autoParam (⊤ ∈ Γ) _auto✝)
:
Equations
Instances For
def
LO.Arith.Language.Theory.TDerivation.and
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Formula}
{q : L.Formula}
(dp : LO.Arith.Language.Theory.TDerivation T (insert p Γ))
(dq : LO.Arith.Language.Theory.TDerivation T (insert q Γ))
:
LO.Arith.Language.Theory.TDerivation T (insert (p ⋏ q) Γ)
Equations
- dp.and dq = LO.Arith.Language.Theory.Derivable.toTDerivation (insert (p ⋏ q) Γ) ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.or
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Formula}
{q : L.Formula}
(dpq : LO.Arith.Language.Theory.TDerivation T (insert p (insert q Γ)))
:
LO.Arith.Language.Theory.TDerivation T (insert (p ⋎ q) Γ)
Equations
- dpq.or = LO.Arith.Language.Theory.Derivable.toTDerivation (insert (p ⋎ q) Γ) ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Semiformula (0 + 1)}
(dp : LO.Arith.Language.Theory.TDerivation T (insert p.free Γ.shift))
:
LO.Arith.Language.Theory.TDerivation T (insert p.all Γ)
Equations
- dp.all = LO.Arith.Language.Theory.Derivable.toTDerivation (insert p.all Γ) ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Semiformula (0 + 1)}
(t : L.Term)
(dp : LO.Arith.Language.Theory.TDerivation T (insert (p.substs₁ t) Γ))
:
LO.Arith.Language.Theory.TDerivation T (insert p.ex Γ)
Equations
Instances For
def
LO.Arith.Language.Theory.TDerivation.wk
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{Δ : L.Sequent}
(d : LO.Arith.Language.Theory.TDerivation T Δ)
(h : Δ ⊆ Γ)
:
Equations
Instances For
def
LO.Arith.Language.Theory.TDerivation.shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(d : LO.Arith.Language.Theory.TDerivation T Γ)
:
LO.Arith.Language.Theory.TDerivation T Γ.shift
Equations
- d.shift = LO.Arith.Language.Theory.Derivable.toTDerivation Γ.shift ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.cut
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Formula}
(d₁ : LO.Arith.Language.Theory.TDerivation T (insert p Γ))
(d₂ : LO.Arith.Language.Theory.TDerivation T (insert (∼p) Γ))
:
Equations
- d₁.cut d₂ = LO.Arith.Language.Theory.Derivable.toTDerivation Γ ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.ofSubset
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{U : L.TTheory}
{Γ : L.Sequent}
(h : T ⊆ U)
(d : LO.Arith.Language.Theory.TDerivation T Γ)
:
Equations
- LO.Arith.Language.Theory.TDerivation.ofSubset h d = { derivation := d.derivation, derivationOf := ⋯ }
Instances For
def
LO.Arith.Language.Theory.TDerivation.cut'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{Δ : L.Sequent}
{p : L.Formula}
(d₁ : LO.Arith.Language.Theory.TDerivation T (insert p Γ))
(d₂ : LO.Arith.Language.Theory.TDerivation T (insert (∼p) Δ))
:
Equations
- d₁.cut' d₂ = (d₁.wk ⋯).cut (d₂.wk ⋯)
Instances For
def
LO.Arith.Language.Theory.TDerivation.conj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(ps : LO.Arith.Language.SemiformulaVec 0)
(ds : (i : V) → (hi : i < LO.Arith.len ps.val) → LO.Arith.Language.Theory.TDerivation T (insert (ps.nth i hi) Γ))
:
LO.Arith.Language.Theory.TDerivation T (insert ps.conj Γ)
Equations
- LO.Arith.Language.Theory.TDerivation.conj ps ds = let_fun this := ⋯; let_fun this := ⋯; LO.Arith.Language.Theory.Derivable.toTDerivation (insert ps.conj Γ) ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.disj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
(ps : LO.Arith.Language.SemiformulaVec 0)
{i : V}
(hi : i < LO.Arith.len ps.val)
(d : LO.Arith.Language.Theory.TDerivation T (insert (ps.nth i hi) Γ))
:
LO.Arith.Language.Theory.TDerivation T (insert ps.disj Γ)
Equations
- LO.Arith.Language.Theory.TDerivation.disj ps hi d = let_fun this := ⋯; LO.Arith.Language.Theory.Derivable.toTDerivation (insert ps.disj Γ) ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.modusPonens
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Formula}
{q : L.Formula}
(dpq : LO.Arith.Language.Theory.TDerivation T (insert (p ➝ q) Γ))
(dp : LO.Arith.Language.Theory.TDerivation T (insert p Γ))
:
Equations
- dpq.modusPonens dp = let d := dpq.wk ⋯; let b := ⋯.mpr ((dp.wk ⋯).and (LO.Arith.Language.Theory.TDerivation.em q ⋯ ⋯)); d.cut b
Instances For
def
LO.Arith.Language.Theory.TDerivation.ofEq
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{Δ : L.Sequent}
(d : LO.Arith.Language.Theory.TDerivation T Γ)
(h : Γ = Δ)
:
Equations
- d.ofEq h = h ▸ d
Instances For
def
LO.Arith.Language.Theory.TDerivation.rotate₁
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p₀ : L.Formula}
{p₁ : L.Formula}
(d : LO.Arith.Language.Theory.TDerivation T (insert p₀ (insert p₁ Γ)))
:
LO.Arith.Language.Theory.TDerivation T (insert p₁ (insert p₀ Γ))
Equations
- d.rotate₁ = d.ofEq ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.rotate₂
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p₀ : L.Formula}
{p₁ : L.Formula}
{p₂ : L.Formula}
(d : LO.Arith.Language.Theory.TDerivation T (insert p₀ (insert p₁ (insert p₂ Γ))))
:
LO.Arith.Language.Theory.TDerivation T (insert p₂ (insert p₁ (insert p₀ Γ)))
Equations
- d.rotate₂ = d.ofEq ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.rotate₃
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p₀ : L.Formula}
{p₁ : L.Formula}
{p₂ : L.Formula}
{p₃ : L.Formula}
(d : LO.Arith.Language.Theory.TDerivation T (insert p₀ (insert p₁ (insert p₂ (insert p₃ Γ)))))
:
LO.Arith.Language.Theory.TDerivation T (insert p₃ (insert p₁ (insert p₂ (insert p₀ Γ))))
Equations
- d.rotate₃ = d.ofEq ⋯
Instances For
def
LO.Arith.Language.Theory.TDerivation.orInv
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Formula}
{q : L.Formula}
(d : LO.Arith.Language.Theory.TDerivation T (insert (p ⋎ q) Γ))
:
LO.Arith.Language.Theory.TDerivation T (insert p (insert q Γ))
Equations
- d.orInv = let_fun b := d.wk ⋯; let_fun this := ⋯.mpr ((LO.Arith.Language.Theory.TDerivation.em p ⋯ ⋯).and (LO.Arith.Language.Theory.TDerivation.em q ⋯ ⋯)); b.cut this
Instances For
def
LO.Arith.Language.Theory.TDerivation.specialize
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : L.Sequent}
{p : L.Semiformula (0 + 1)}
(b : LO.Arith.Language.Theory.TDerivation T (insert p.all Γ))
(t : L.Term)
:
LO.Arith.Language.Theory.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) ⋯ ⋯)))
Instances For
def
LO.Arith.Language.Theory.TProof.modusPonens
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{p : L.Formula}
{q : L.Formula}
(d : T ⊢ p ➝ q)
(b : T ⊢ p)
:
T ⊢ q
Condition D2
Equations
Instances For
def
LO.Arith.Language.Theory.TProof.byAxm
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{p : L.Formula}
(h : LO.Arith.Language.Theory.tmem p T.thy)
:
T ⊢ p
Instances For
def
LO.Arith.Language.Theory.TProof.ofSubset
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{U : L.TTheory}
(h : T ⊆ U)
{p : L.Formula}
:
Equations
Instances For
theorem
LO.Arith.Language.Theory.TProof.of_subset
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{U : L.TTheory}
(h : T ⊆ U)
{p : L.Formula}
:
instance
LO.Arith.Language.Theory.TProof.instModusPonensTTheoryFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
:
Equations
- LO.Arith.Language.Theory.TProof.instModusPonensTTheoryFormula = { mdp := fun {p q : L.Formula} => LO.Arith.Language.Theory.TProof.modusPonens }
instance
LO.Arith.Language.Theory.TProof.instNegationEquivTTheoryFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
:
Equations
- One or more equations did not get rendered due to their size.
instance
LO.Arith.Language.Theory.TProof.instMinimalTTheoryFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
:
Equations
- LO.Arith.Language.Theory.TProof.instMinimalTTheoryFormula = LO.System.Minimal.mk
instance
LO.Arith.Language.Theory.TProof.instClassicalTTheoryFormula
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
:
Equations
- LO.Arith.Language.Theory.TProof.instClassicalTTheoryFormula = LO.System.Classical.mk
def
LO.Arith.Language.Theory.TProof.exIntro
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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
Instances For
theorem
LO.Arith.Language.Theory.TProof.ex_intro!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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
Instances For
theorem
LO.Arith.Language.Theory.TProof.specialize!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
(ps : LO.Arith.Language.SemiformulaVec 0)
(ds : (i : V) → (hi : i < LO.Arith.len ps.val) → T ⊢ ps.nth i hi)
:
T ⊢ ps.conj
Equations
Instances For
theorem
LO.Arith.Language.Theory.TProof.conj!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
(ps : LO.Arith.Language.SemiformulaVec 0)
(ds : ∀ (i : V) (hi : i < LO.Arith.len ps.val), T ⊢! ps.nth i hi)
:
T ⊢! ps.conj
def
LO.Arith.Language.Theory.TProof.conj'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
(ps : LO.Arith.Language.SemiformulaVec 0)
(ds : (i : V) → (hi : i < LO.Arith.len ps.val) → T ⊢ ps.nth (LO.Arith.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)) ⋯)
Instances For
def
LO.Arith.Language.Theory.TProof.conjOr'
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
(ps : LO.Arith.Language.SemiformulaVec 0)
(q : L.Semiformula 0)
(ds : (i : V) → (hi : i < LO.Arith.len ps.val) → T ⊢ ps.nth (LO.Arith.len ps.val - (i + 1)) ⋯ ⋎ q)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
LO.Arith.Language.Theory.TProof.disj
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
(ps : LO.Arith.Language.SemiformulaVec 0)
{i : V}
(hi : i < LO.Arith.len ps.val)
(d : T ⊢ ps.nth i hi)
:
T ⊢ ps.disj
Equations
Instances For
def
LO.Arith.Language.Theory.TProof.shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{p : L.Formula}
(d : T ⊢ p)
:
Equations
Instances For
theorem
LO.Arith.Language.Theory.TProof.shift!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{p : L.Formula}
(d : T ⊢! p)
:
def
LO.Arith.Language.Theory.TProof.all
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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
Instances For
theorem
LO.Arith.Language.Theory.TProof.all!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{C : L.Formula}
{p : L.Semiformula (0 + 1)}
(dp : T ⊢ LO.Arith.Language.Semiformula.shift C ➝ p.free)
:
Equations
- LO.Arith.Language.Theory.TProof.generalizeAux dp = ⋯.mpr ((LO.Arith.Language.Theory.TDerivation.orInv (⋯.mp dp)).wk ⋯).all.rotate₁.or
Instances For
theorem
LO.Arith.Language.Theory.TProof.conj_shift
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
(Γ : List L.Formula)
:
LO.Arith.Language.Semiformula.shift (⋀Γ) = ⋀List.map LO.Arith.Language.Semiformula.shift Γ
def
LO.Arith.Language.Theory.TProof.generalize
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : List (L.Semiformula 0)}
{p : L.Semiformula (0 + 1)}
(d : List.map LO.Arith.Language.Semiformula.shift Γ ⊢[T] p.free)
:
Equations
Instances For
theorem
LO.Arith.Language.Theory.TProof.generalize!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.FirstOrder.Arith.LDef}
[L.Defined pL]
{T : L.TTheory}
{Γ : List (L.Semiformula 0)}
{p : L.Semiformula (0 + 1)}
(d : List.map LO.Arith.Language.Semiformula.shift Γ ⊢[T]! p.free)
:
def
LO.Arith.Language.Theory.TProof.specializeWithCtxAux
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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)
:
Equations
- LO.Arith.Language.Theory.TProof.specializeWithCtxAux d t = ⋯.mpr (((LO.Arith.Language.Theory.TDerivation.orInv (⋯.mp d)).wk ⋯).specialize t).rotate₁.or
Instances For
def
LO.Arith.Language.Theory.TProof.specializeWithCtx
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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)
:
Equations
Instances For
theorem
LO.Arith.Language.Theory.TProof.specialize_with_ctx!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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)
:
def
LO.Arith.Language.Theory.TProof.ex
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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
Instances For
theorem
LO.Arith.Language.Theory.TProof.ex!
{V : Type u_1}
[LO.ORingStruc V]
[V ⊧ₘ* 𝐈𝚺₁]
{L : LO.Arith.Language V}
{pL : LO.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