Sequent calculus and variants

This file defines a characterization of Tait style calculus and Gentzen style calculus.

Main Definitions

• LO.Tait
• LO.Gentzen

class LO.OneSided (F : outParam (Type u_1)) (K : Type u_2) : Type (max (max u_1 u_2) (u_3 + 1))

• Derivation : K → List F → Type u_3

Instances

• LO.FirstOrder.instOneSidedSyntacticFormulaTheory
• LO.Propositional.Classical.instOneSidedFormulaTheory

def LO.«term_⟹_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.OneSided.Derivation₁ {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (p : F) : Type u_3

Equations

• (𝓚 ⟹. p) = (𝓚 ⟹ [p])

def LO.«term_⟹._» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.OneSided.Derivable {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (Δ : List F) : Prop

Equations

• (𝓚 ⟹! Δ) = Nonempty (𝓚 ⟹ Δ)

def LO.«term_⟹!_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.OneSided.Derivable₁ {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (p : F) : Prop

Equations

• (𝓚 ⟹!. p) = Nonempty (𝓚 ⟹. p)

def LO.«term_⟹!._» : Lean.TrailingParserDescr

Equations

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

noncomputable def LO.OneSided.Derivable.get {F : Type u_1} {K : Type u_2} [LO.OneSided F K] (𝓚 : K) (Δ : List F) (h : 𝓚 ⟹! Δ) : 𝓚 ⟹ Δ

Equations

• LO.OneSided.Derivable.get 𝓚 Δ h = Classical.choice h

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))

• Derivation : K → List F → Type u_3
• verum : (𝓚 : K) → (Δ : List F) → 𝓚 ⟹ ⊤ :: Δ
• and : {𝓚 : K} → {p q : F} → {Δ : List F} → 𝓚 ⟹ p :: Δ → 𝓚 ⟹ q :: Δ → 𝓚 ⟹ p ⋏ q :: Δ
• or : {𝓚 : K} → {p q : F} → {Δ : List F} → 𝓚 ⟹ p :: q :: Δ → 𝓚 ⟹ p ⋎ q :: Δ
• wk : {𝓚 : K} → {Δ Δ' : List F} → 𝓚 ⟹ Δ → Δ ⊆ Δ' → 𝓚 ⟹ Δ'
• em : {𝓚 : K} → {p : F} → {Δ : List F} → p ∈ Δ → ∼p ∈ Δ → 𝓚 ⟹ Δ

Instances

• LO.FirstOrder.Derivation.instTaitSyntacticFormulaTheory
• LO.Propositional.Classical.Derivation.instTaitFormulaTheory

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)

• cut : {𝓚 : K} → {Δ : List F} → {p : F} → 𝓚 ⟹ p :: Δ → 𝓚 ⟹ ∼p :: Δ → 𝓚 ⟹ Δ

Instances

• LO.FirstOrder.Derivation.instCutSyntacticFormulaTheory
• LO.Propositional.Classical.Derivation.instCutFormulaTheory

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)

• root : {𝓚 : K} → {p : F} → p ∈ 𝓚 → 𝓚 ⟹. p
• trans : {𝓚 𝓛 : K} → {Γ : List F} → ((q : F) → q ∈ 𝓚 → 𝓛 ⟹. q) → 𝓚 ⟹ Γ → 𝓛 ⟹ Γ

Instances

• LO.FirstOrder.Derivation.instAxiomatizedSyntacticFormulaTheory
• LO.Propositional.Classical.Derivation.instAxiomatizedFormulaTheory

@[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

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

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 𝓚 Γ) ⋯

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 :: Γ) : 𝓚 ⟹! p ⋏ 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 :: Γ) : 𝓚 ⟹! 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

theorem 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✝) : 𝓚 ⟹! Γ

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) ⋯

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) ⋯

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 : 𝓚 ⟹ Γ) : 𝓚 ⟹ p :: Γ

Equations

• LO.Tait.wkTail d = LO.Tait.wk d ⋯

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₁ :: Γ) : 𝓚 ⟹ p₁ :: p₂ :: Γ

Equations

• LO.Tait.rotate₁ d = LO.Tait.wk d ⋯

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₂ :: Γ) : 𝓚 ⟹ p₁ :: p₂ :: p₃ :: Γ

Equations

• LO.Tait.rotate₂ d = LO.Tait.wk d ⋯

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₃ :: Γ) : 𝓚 ⟹ p₁ :: p₂ :: p₃ :: p₄ :: Γ

Equations

• LO.Tait.rotate₃ d = LO.Tait.wk d ⋯

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} : 𝓚 ⟹ p :: Δ → 𝓚 ⟹ ∼p :: Δ → 𝓚 ⟹ Δ

Alias of LO.Tait.Cut.cut.

Equations

• @LO.Tait.cut = @LO.Tait.Cut.cut

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} : p ∈ 𝓚 → 𝓚 ⟹. p

Alias of LO.Tait.Axiomatized.root.

Equations

• @LO.Tait.root = @LO.Tait.Axiomatized.root

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) ⋯

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 ⋯

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

Equations

• LO.Tait.system = { Prf := fun (x : K) (x_1 : F) => x ⟹. x_1 }

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] : LO.System.Axiomatized 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] : LO.System.StrongCut K 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] : LO.System.DeductiveExplosion 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} : LO.System.Classical 𝓚

Equations

• LO.Tait.instClassical = LO.System.Classical.mk