Sequent calculus and variants #
This file defines a characterization of Tait style calculus and Gentzen style calculus.
Main Definitions #
LO.TaitLO.Gentzen
Equations
- LO.«term_⟹_» = Lean.ParserDescr.trailingNode `LO.«term_⟹_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹ ") (Lean.ParserDescr.cat `term 46))
Equations
- LO.«term_⟹._» = Lean.ParserDescr.trailingNode `LO.«term_⟹._» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹. ") (Lean.ParserDescr.cat `term 46))
Equations
- LO.«term_⟹!_» = Lean.ParserDescr.trailingNode `LO.«term_⟹!_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹! ") (Lean.ParserDescr.cat `term 46))
Equations
- LO.«term_⟹!._» = Lean.ParserDescr.trailingNode `LO.«term_⟹!._» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟹!. ") (Lean.ParserDescr.cat `term 46))
class
LO.Tait
(F : Type u_1)
(K : Type u_2)
[LogicalConnective F]
[DeMorgan F]
[Collection F K]
extends LO.OneSided F K :
Type (max (max u_1 u_2) (u_3 + 1))
- Derivation : K → List F → Type u_3
class
LO.Tait.Cut
(F : Type u_1)
(K : Type u_2)
[LogicalConnective F]
[DeMorgan F]
[Collection F K]
[Tait F K]
:
Type (max (max u_1 u_2) u_3)
class
LO.Tait.Axiomatized
(F : Type u_1)
(K : Type u_2)
[LogicalConnective F]
[DeMorgan F]
[Collection F K]
[Tait F K]
:
Type (max (max u_1 u_2) u_3)
def
LO.Tait.ofEq
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ Δ : List F}
(b : 𝓚 ⟹ Γ)
(h : Γ = Δ)
:
𝓚 ⟹ Δ
Equations
- LO.Tait.ofEq b h = h ▸ b
theorem
LO.Tait.of_eq
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ Δ : List F}
(b : 𝓚 ⟹! Γ)
(h : Γ = Δ)
:
𝓚 ⟹! Δ
def
LO.Tait.verum'
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
(h : ⊤ ∈ Γ := by simp)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.verum' h = LO.Tait.wk (LO.Tait.verum 𝓚 Γ) ⋯
theorem
LO.Tait.verum!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
(𝓚 : K)
(Γ : List F)
:
theorem
LO.Tait.verum'!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
(h : ⊤ ∈ Γ)
:
𝓚 ⟹! Γ
theorem
LO.Tait.or!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ ψ : F}
(h : 𝓚 ⟹! φ :: ψ :: Γ)
:
theorem
LO.Tait.wk!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ Δ : List F}
(h : 𝓚 ⟹! Γ)
(ss : Γ ⊆ Δ)
:
𝓚 ⟹! Δ
theorem
LO.Tait.em!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ : F}
(hp : φ ∈ Γ)
(hn : ∼φ ∈ Γ)
:
𝓚 ⟹! Γ
def
LO.Tait.close
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
(φ : F)
(hp : φ ∈ Γ := by simp)
(hn : ∼φ ∈ Γ := by simp)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.close φ hp hn = LO.Tait.em hp hn
theorem
LO.Tait.close!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
(φ : F)
(hp : φ ∈ Γ := by simp)
(hn : ∼φ ∈ Γ := by simp)
:
𝓚 ⟹! Γ
def
LO.Tait.and'
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ ψ : F}
(h : φ ⋏ ψ ∈ Γ)
(dp : 𝓚 ⟹ φ :: Γ)
(dq : 𝓚 ⟹ ψ :: Γ)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.and' h dp dq = LO.Tait.wk (LO.Tait.and dp dq) ⋯
def
LO.Tait.or'
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ ψ : F}
(h : φ ⋎ ψ ∈ Γ)
(dpq : 𝓚 ⟹ φ :: ψ :: Γ)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.or' h dpq = LO.Tait.wk (LO.Tait.or dpq) ⋯
def
LO.Tait.wkTail
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ : F}
(d : 𝓚 ⟹ Γ)
:
Equations
- LO.Tait.wkTail d = LO.Tait.wk d ⋯
def
LO.Tait.rotate₁
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ₁ φ₂ : F}
(d : 𝓚 ⟹ φ₂ :: φ₁ :: Γ)
:
Equations
- LO.Tait.rotate₁ d = LO.Tait.wk d ⋯
def
LO.Tait.rotate₂
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ₁ φ₂ φ₃ : F}
(d : 𝓚 ⟹ φ₃ :: φ₁ :: φ₂ :: Γ)
:
Equations
- LO.Tait.rotate₂ d = LO.Tait.wk d ⋯
def
LO.Tait.rotate₃
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
{φ₁ φ₂ φ₃ φ₄ : F}
(d : 𝓚 ⟹ φ₄ :: φ₁ :: φ₂ :: φ₃ :: Γ)
:
Equations
- LO.Tait.rotate₃ d = LO.Tait.wk d ⋯
def
LO.Tait.cut
{F : Type u_1}
{K : Type u_2}
{inst✝ : LogicalConnective F}
{inst✝¹ : DeMorgan F}
{inst✝² : Collection F K}
{inst✝³ : Tait F K}
[self : Cut F K]
{𝓚 : K}
{Δ : List F}
{φ : F}
:
Alias of LO.Tait.Cut.cut.
Equations
def
LO.Tait.root
{F : Type u_1}
{K : Type u_2}
{inst✝ : LogicalConnective F}
{inst✝¹ : DeMorgan F}
{inst✝² : Collection F K}
{inst✝³ : Tait F K}
[self : Axiomatized F K]
{𝓚 : K}
{φ : F}
:
Alias of LO.Tait.Axiomatized.root.
Equations
theorem
LO.Tait.root!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
[Axiomatized F K]
{φ : F}
(h : φ ∈ 𝓚)
:
𝓚 ⟹!. φ
def
LO.Tait.byAxm
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
[Axiomatized F K]
(φ : F)
(h : φ ∈ 𝓚)
(hΓ : φ ∈ Γ := by simp)
:
𝓚 ⟹ Γ
Equations
- LO.Tait.byAxm φ h hΓ = LO.Tait.wk (LO.Tait.root h) ⋯
theorem
LO.Tait.byAxm!
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
{Γ : List F}
[Axiomatized F K]
(φ : F)
(h : φ ∈ 𝓚)
(hΓ : φ ∈ Γ := by simp)
:
𝓚 ⟹! Γ
def
LO.Tait.ofAxiomSubset
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 𝓛 : K}
{Γ : List F}
[Axiomatized F K]
(h : 𝓚 ⊆ 𝓛)
:
Equations
- LO.Tait.ofAxiomSubset h = LO.Tait.Axiomatized.trans fun (x : F) (hq : x ∈ 𝓚) => LO.Tait.Axiomatized.root ⋯
theorem
LO.Tait.of_axiom_subset
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 𝓛 : K}
{Γ : List F}
[Axiomatized F K]
(h : 𝓚 ⊆ 𝓛)
:
instance
LO.Tait.system
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
:
System F K
Equations
- LO.Tait.system = { Prf := fun (x1 : K) (x2 : F) => x1 ⟹. x2 }
instance
LO.Tait.instAxiomatizedOfAxiomatized
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
[Axiomatized F K]
:
Equations
- LO.Tait.instAxiomatizedOfAxiomatized = { 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.provable_bot_iff_derivable_nil
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
[Cut F K]
:
theorem
LO.Tait.waekerThan_of_subset
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 𝓛 : K}
[Axiomatized F K]
(h : 𝓚 ⊆ 𝓛)
:
𝓚 ≤ₛ 𝓛
instance
LO.Tait.instStrongCutOfAxiomatized
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
[Axiomatized F K]
:
System.StrongCut K K
Equations
- One or more equations did not get rendered due to their size.
instance
LO.Tait.instDeductiveExplosionOfCut
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
[Cut F K]
:
Equations
- LO.Tait.instDeductiveExplosionOfCut = { dexp := fun {𝓚 : K} {b : 𝓚 ⊢ ⊥} {φ : 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}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
[Cut F K]
:
System.Inconsistent 𝓚 ↔ 𝓚 ⟹! []
theorem
LO.Tait.consistent_iff_unprovable
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
[Axiomatized F K]
[Cut F K]
:
System.Consistent 𝓚 ↔ IsEmpty (𝓚 ⟹ [])
instance
LO.Tait.instClassicalOfCut
{F : Type u_1}
{K : Type u_3}
[LogicalConnective F]
[Collection F K]
[DeMorgan F]
[Tait F K]
{𝓚 : K}
[Cut F K]
: