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

Imported declaration from the Incompleteness formalization.

• Derivation : K → List F → Type u_3

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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} [OneSided F K] (𝓚 : K) (φ : F) : Type u_3

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [OneSided F K] (𝓚 : K) (Δ : List F) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [OneSided F K] (𝓚 : K) (φ : F) : Prop

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [OneSided F K] (𝓚 : K) (Δ : List F) (h : 𝓚 ⟹! Δ) : 𝓚 ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• Derivation : K → List F → Type u_3
• verum (𝓚 : K) (Δ : List F) : 𝓚 ⟹ ⊤ :: Δ

  Imported declaration from the Incompleteness formalization.

• and {𝓚 : K} {φ ψ : F} {Δ : List F} : 𝓚 ⟹ φ :: Δ → 𝓚 ⟹ ψ :: Δ → 𝓚 ⟹ φ ⋏ ψ :: Δ

  Imported declaration from the Incompleteness formalization.

• or {𝓚 : K} {φ ψ : F} {Δ : List F} : 𝓚 ⟹ φ :: ψ :: Δ → 𝓚 ⟹ φ ⋎ ψ :: Δ

  Imported declaration from the Incompleteness formalization.

• wk {𝓚 : K} {Δ Δ' : List F} : 𝓚 ⟹ Δ → Δ ⊆ Δ' → 𝓚 ⟹ Δ'

  Imported declaration from the Incompleteness formalization.

• em {𝓚 : K} {φ : F} {Δ : List F} : φ ∈ Δ → ∼φ ∈ Δ → 𝓚 ⟹ Δ

  Imported declaration from the Incompleteness formalization.

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)

Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

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)

Imported declaration from the Incompleteness formalization.

• root {𝓚 : K} {φ : F} : φ ∈ 𝓚 → 𝓚 ⟹. φ

  Imported declaration from the Incompleteness formalization.

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

  Imported declaration from the Incompleteness formalization.

@[reducible, inline]

abbrev LO.OneSided.cast {F : Type u_1} {K : Type u_3} [OneSided F K] {𝓚 : K} {Γ Δ : List F} (d : 𝓚 ⟹ Δ) (e : Δ = Γ) : 𝓚 ⟹ Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.OneSided.cast d e = cast ⋯ d

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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.and! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {𝓚 : K} {Γ : List F} {φ ψ : F} (hp : 𝓚 ⟹! φ :: Γ) (hq : 𝓚 ⟹! ψ :: Γ) : 𝓚 ⟹! φ ⋏ ψ :: Γ

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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.

---

Imported declaration from the Incompleteness formalization.

Equations

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

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.

---

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Tait.cut! {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] {Δ : List F} {φ : F} {𝓚 : K} [Cut F K] (hp : 𝓚 ⟹! φ :: Δ) (hn : 𝓚 ⟹! ∼φ :: Δ) : 𝓚 ⟹! Δ

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

Imported declaration from the Incompleteness formalization.

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 : 𝓚 ⊆ 𝓛) : 𝓚 ⟹ Γ → 𝓛 ⟹ Γ

Imported declaration from the Incompleteness formalization.

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 : 𝓚 ⊆ 𝓛) : 𝓚 ⟹! Γ → 𝓛 ⟹! Γ

@[implicit_reducible]

instance LO.Tait.system {F : Type u_1} {K : Type u_3} [LogicalConnective F] [Collection F K] [DeMorgan F] [Tait F K] : Entailment F K

Equations

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

@[implicit_reducible]

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] : Entailment.Axiomatized 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 : 𝓚 ⊆ 𝓛) : 𝓚 wkn 𝓛

@[implicit_reducible]

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] : Entailment.StrongCut K K

Equations

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

@[implicit_reducible]

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] : Entailment.DeductiveExplosion 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] : Entailment.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] : Entailment.Consistent 𝓚 ↔ IsEmpty (𝓚 ⟹ [])

@[implicit_reducible]

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] : Entailment.Classical 𝓚

Equations

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