Sequent calculus and variants #
This file defines a characterization of Tait style calculus and Gentzen style calculus.
Main Definitions #
LO.Tait
LO.Gentzen
Equations
- LO.«term_⟹_» = Lean.ParserDescr.trailingNode `LO.term_⟹_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 46))
Instances For
@[reducible, inline]
abbrev
LO.OneSided.Derivation₁
{F : Type u_1}
{K : Type u_2}
[LO.OneSided F K]
(𝓚 : K)
(p : F)
:
Type u_3
Instances For
Equations
- LO.«term_⟹._» = Lean.ParserDescr.trailingNode `LO.term_⟹._ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹. ") (Lean.ParserDescr.cat `term 46))
Instances For
Equations
- LO.«term_⟹!_» = Lean.ParserDescr.trailingNode `LO.term_⟹!_ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹! ") (Lean.ParserDescr.cat `term 46))
Instances For
@[reducible, inline]
Instances For
Equations
- LO.«term_⟹!._» = Lean.ParserDescr.trailingNode `LO.term_⟹!._ 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹!. ") (Lean.ParserDescr.cat `term 46))
Instances For
noncomputable def
LO.OneSided.Derivable.get
{F : Type u_1}
{K : Type u_2}
[LO.OneSided F K]
(𝓚 : K)
(Δ : List F)
(h : 𝓚 ⟹! Δ)
:
𝓚 ⟹ Δ
Equations
Instances For
class
LO.Tait
(F : Type u_1)
(K : Type u_2)
[LO.LogicalConnective F]
[Collection F K]
extends
LO.OneSided
:
Type (max (max u_1 u_2) (u_3 + 1))
Instances
class
LO.Tait.Cut
(F : Type u_1)
(K : Type u_2)
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
:
Type (max (max u_1 u_2) u_3)
Instances
class
LO.Tait.Axiomatized
(F : Type u_1)
(K : Type u_2)
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
:
Type (max (max u_1 u_2) u_3)
Instances
@[reducible, inline]
abbrev
LO.OneSided.cast
{F : Type u_1}
{K : Type u_3}
[LO.OneSided F K]
{𝓚 : K}
{Γ : List F}
{Δ : List F}
(d : 𝓚 ⟹ Δ)
(e : Δ = Γ)
:
𝓚 ⟹ Γ
Equations
- LO.OneSided.cast d e = cast ⋯ d
Instances For
def
LO.Tait.ofEq
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{Δ : List F}
(b : 𝓚 ⟹ Γ)
(h : Γ = Δ)
:
𝓚 ⟹ Δ
Equations
- LO.Tait.ofEq b h = h ▸ b
Instances For
theorem
LO.Tait.of_eq
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{Δ : List F}
(b : 𝓚 ⟹! Γ)
(h : Γ = Δ)
:
𝓚 ⟹! Δ
def
LO.Tait.verum'
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
(h : autoParam (⊤ ∈ Γ) _auto✝)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.verum' h = LO.Tait.wk (LO.Tait.verum 𝓚 Γ) ⋯
Instances For
theorem
LO.Tait.verum!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
(𝓚 : K)
(Γ : List F)
:
theorem
LO.Tait.verum'!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
(h : ⊤ ∈ Γ)
:
𝓚 ⟹! Γ
theorem
LO.Tait.and!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p : F}
{q : F}
(hp : 𝓚 ⟹! p :: Γ)
(hq : 𝓚 ⟹! q :: Γ)
:
theorem
LO.Tait.or!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p : F}
{q : F}
(h : 𝓚 ⟹! p :: q :: Γ)
:
theorem
LO.Tait.wk!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{Δ : List F}
(h : 𝓚 ⟹! Γ)
(ss : Γ ⊆ Δ)
:
𝓚 ⟹! Δ
theorem
LO.Tait.em!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p : F}
(hp : p ∈ Γ)
(hn : ∼p ∈ Γ)
:
𝓚 ⟹! Γ
def
LO.Tait.close
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
(p : F)
(hp : autoParam (p ∈ Γ) _auto✝)
(hn : autoParam (∼p ∈ Γ) _auto✝)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.close p hp hn = LO.Tait.em hp hn
Instances For
def
LO.Tait.and'
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p : F}
{q : F}
(h : p ⋏ q ∈ Γ)
(dp : 𝓚 ⟹ p :: Γ)
(dq : 𝓚 ⟹ q :: Γ)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.and' h dp dq = LO.Tait.wk (LO.Tait.and dp dq) ⋯
Instances For
def
LO.Tait.or'
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p : F}
{q : F}
(h : p ⋎ q ∈ Γ)
(dpq : 𝓚 ⟹ p :: q :: Γ)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.or' h dpq = LO.Tait.wk (LO.Tait.or dpq) ⋯
Instances For
def
LO.Tait.wkTail
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p : F}
(d : 𝓚 ⟹ Γ)
:
Equations
- LO.Tait.wkTail d = LO.Tait.wk d ⋯
Instances For
def
LO.Tait.rotate₁
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p₁ : F}
{p₂ : F}
(d : 𝓚 ⟹ p₂ :: p₁ :: Γ)
:
Equations
- LO.Tait.rotate₁ d = LO.Tait.wk d ⋯
Instances For
def
LO.Tait.rotate₂
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p₁ : F}
{p₂ : F}
{p₃ : F}
(d : 𝓚 ⟹ p₃ :: p₁ :: p₂ :: Γ)
:
Equations
- LO.Tait.rotate₂ d = LO.Tait.wk d ⋯
Instances For
def
LO.Tait.rotate₃
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{𝓚 : K}
{Γ : List F}
{p₁ : F}
{p₂ : F}
{p₃ : F}
{p₄ : F}
(d : 𝓚 ⟹ p₄ :: p₁ :: p₂ :: p₃ :: Γ)
:
Equations
- LO.Tait.rotate₃ d = LO.Tait.wk d ⋯
Instances For
def
LO.Tait.cut
{F : Type u_1}
{K : Type u_2}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[self : LO.Tait.Cut F K]
{𝓚 : K}
{Δ : List F}
{p : F}
:
Alias of LO.Tait.Cut.cut
.
Equations
Instances For
def
LO.Tait.root
{F : Type u_1}
{K : Type u_2}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[self : LO.Tait.Axiomatized F K]
{𝓚 : K}
{p : F}
:
Alias of LO.Tait.Axiomatized.root
.
Equations
Instances For
theorem
LO.Tait.cut!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
{Δ : List F}
{p : F}
[LO.Tait.Cut F K]
{𝓚 : K}
(hp : 𝓚 ⟹! p :: Δ)
(hn : 𝓚 ⟹! ∼p :: Δ)
:
𝓚 ⟹! Δ
theorem
LO.Tait.root!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
{𝓚 : K}
{p : F}
(h : p ∈ 𝓚)
:
𝓚 ⟹!. p
def
LO.Tait.byAxm
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
{𝓚 : K}
{Γ : List F}
(p : F)
(h : p ∈ 𝓚)
(hΓ : autoParam (p ∈ Γ) _auto✝)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.byAxm p h hΓ = LO.Tait.wk (LO.Tait.root h) ⋯
Instances For
theorem
LO.Tait.byAxm!
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
{𝓚 : K}
{Γ : List F}
(p : F)
(h : p ∈ 𝓚)
(hΓ : autoParam (p ∈ Γ) _auto✝)
:
𝓚 ⟹! Γ
def
LO.Tait.ofAxiomSubset
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
{𝓚 : K}
{𝓛 : K}
{Γ : List F}
(h : 𝓚 ⊆ 𝓛)
:
Equations
- LO.Tait.ofAxiomSubset h = LO.Tait.Axiomatized.trans fun (x : F) (hq : x ∈ 𝓚) => LO.Tait.Axiomatized.root ⋯
Instances For
theorem
LO.Tait.of_axiom_subset
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
{𝓚 : K}
{𝓛 : K}
{Γ : List F}
(h : 𝓚 ⊆ 𝓛)
:
instance
LO.Tait.system
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
:
LO.System F K
instance
LO.Tait.instAxiomatized
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
:
Equations
- LO.Tait.instAxiomatized = { prfAxm := fun {𝓢 : K} {f : F} (hf : f ∈ Collection.set 𝓢) => LO.Tait.Axiomatized.root hf, weakening := fun {f : F} {𝓢 𝓣 : K} => LO.Tait.ofAxiomSubset }
theorem
LO.Tait.waekerThan_of_subset
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
{𝓚 : K}
{𝓛 : K}
(h : 𝓚 ⊆ 𝓛)
:
𝓚 ≤ₛ 𝓛
instance
LO.Tait.instStrongCut
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.Tait F K]
[LO.Tait.Axiomatized F K]
:
Equations
- LO.Tait.instStrongCut = { cut := fun {x x_1 : K} {x_2 : F} {bs : x ⊢* Collection.set x_1} {b : x_1 ⊢ x_2} => LO.Tait.Axiomatized.trans (fun (x : F) (hq : x ∈ x_1) => bs hq) b }
theorem
LO.Tait.provable_bot_iff_derivable_nil
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.DeMorgan F]
[LO.Tait F K]
[LO.Tait.Cut F K]
{𝓚 : K}
:
instance
LO.Tait.instDeductiveExplosion
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.DeMorgan F]
[LO.Tait F K]
[LO.Tait.Cut F K]
:
Equations
- LO.Tait.instDeductiveExplosion = { dexp := fun {𝓚 : K} {b : 𝓚 ⊢ ⊥} {p : F} => LO.Tait.wk (LO.Tait.Cut.cut b (⋯.mpr (LO.Tait.verum 𝓚 []))) ⋯ }
theorem
LO.Tait.inconsistent_iff_provable
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.DeMorgan F]
[LO.Tait F K]
[LO.Tait.Cut F K]
{𝓚 : K}
:
LO.System.Inconsistent 𝓚 ↔ 𝓚 ⟹! []
theorem
LO.Tait.consistent_iff_unprovable
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.DeMorgan F]
[LO.Tait F K]
[LO.Tait.Cut F K]
{𝓚 : K}
:
LO.System.Consistent 𝓚 ↔ IsEmpty (𝓚 ⟹ [])
instance
LO.Tait.instClassical
{F : Type u_1}
{K : Type u_3}
[LO.LogicalConnective F]
[Collection F K]
[LO.DeMorgan F]
[LO.Tait F K]
[LO.Tait.Cut F K]
{𝓚 : K}
:
Equations
- LO.Tait.instClassical = LO.System.Classical.mk