Sequent calculus and variants

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

Main Definitions

• LO.OneSidedLK

One-sided $\mathbf{LK}$

class LO.OneSidedLK {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] (𝔇 : List F → Type u_2) : Type (max u_1 u_2)

• identity (φ : F) : 𝔇 [φ, ∼φ]
• contraction {Δ Γ : List F} : 𝔇 Δ → Δ ⊆ Γ → 𝔇 Γ
• verum : 𝔇 [⊤]
• and {φ : F} {Γ : List F} {ψ : F} : 𝔇 (φ :: Γ) → 𝔇 (ψ :: Γ) → 𝔇 (φ ⋏ ψ :: Γ)
• or {φ ψ : F} {Γ : List F} : 𝔇 (φ :: ψ :: Γ) → 𝔇 (φ ⋎ ψ :: Γ)

class LO.OneSidedLK.Cut {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] (𝔇 : List F → Type u_2) extends LO.OneSidedLK 𝔇 : Type (max u_1 u_2)

• identity (φ : F) : 𝔇 [φ, ∼φ]
• contraction {Δ Γ : List F} : 𝔇 Δ → Δ ⊆ Γ → 𝔇 Γ
• verum : 𝔇 [⊤]
• and {φ : F} {Γ : List F} {ψ : F} : 𝔇 (φ :: Γ) → 𝔇 (ψ :: Γ) → 𝔇 (φ ⋏ ψ :: Γ)
• or {φ ψ : F} {Γ : List F} : 𝔇 (φ :: ψ :: Γ) → 𝔇 (φ ⋎ ψ :: Γ)
• cut {φ : F} {Γ Δ : List F} : 𝔇 (φ :: Γ) → 𝔇 (∼φ :: Δ) → 𝔇 (Γ ++ Δ)

def LO.OneSidedLK.cast {F : Type u_1} {𝔇 : List F → Type u_2} {Γ Δ : List F} (b : 𝔇 Γ) (h : Γ = Δ := by simp) : 𝔇 Δ

Equations

• LO.OneSidedLK.cast b h = h ▸ b

def LO.OneSidedLK.contra {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {Γ Δ : List F} [OneSidedLK 𝔇] (d : 𝔇 Γ) (h : Γ ⊆ Δ := by simp) : 𝔇 Δ

Equations

• LO.OneSidedLK.contra d h = LO.OneSidedLK.contraction d h

def LO.OneSidedLK.rotate {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {φ : F} {Γ : List F} [OneSidedLK 𝔇] (d : 𝔇 (φ :: Γ)) : 𝔇 (Γ ++ [φ])

Equations

• LO.OneSidedLK.rotate d = LO.OneSidedLK.contra d ⋯

def LO.OneSidedLK.close {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {Γ : List F} [OneSidedLK 𝔇] (φ : F) (hp : φ ∈ Γ := by simp) (hn : ∼φ ∈ Γ := by simp) : 𝔇 Γ

Equations

• LO.OneSidedLK.close φ hp hn = LO.OneSidedLK.contraction (LO.OneSidedLK.identity φ) ⋯

def LO.OneSidedLK.top {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {Γ : List F} [OneSidedLK 𝔇] (h : ⊤ ∈ Γ := by simp) : 𝔇 Γ

Equations

• LO.OneSidedLK.top h = LO.OneSidedLK.contraction LO.OneSidedLK.verum ⋯

def LO.OneSidedLK.tensor {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {Γ Δ : List F} [OneSidedLK 𝔇] {φ ψ : F} (dφ : 𝔇 (φ :: Γ)) (dψ : 𝔇 (ψ :: Δ)) : 𝔇 (φ ⋏ ψ :: Γ ++ Δ)

Equations

• LO.OneSidedLK.tensor dφ dψ = LO.OneSidedLK.and (LO.OneSidedLK.contraction dφ ⋯) (LO.OneSidedLK.contraction dψ ⋯)

def LO.OneSidedLK.swap₁ {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {φ₂ φ₁ : F} {Γ : List F} [OneSidedLK 𝔇] (d : 𝔇 (φ₂ :: φ₁ :: Γ)) : 𝔇 (φ₁ :: φ₂ :: Γ)

Equations

• LO.OneSidedLK.swap₁ d = LO.OneSidedLK.contraction d ⋯

def LO.OneSidedLK.swap₂ {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {φ₃ φ₁ φ₂ : F} {Γ : List F} [OneSidedLK 𝔇] (d : 𝔇 (φ₃ :: φ₁ :: φ₂ :: Γ)) : 𝔇 (φ₁ :: φ₂ :: φ₃ :: Γ)

Equations

• LO.OneSidedLK.swap₂ d = LO.OneSidedLK.contraction d ⋯

def LO.OneSidedLK.swap₃ {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {φ₄ φ₁ φ₂ φ₃ : F} {Γ : List F} [OneSidedLK 𝔇] (d : 𝔇 (φ₄ :: φ₁ :: φ₂ :: φ₃ :: Γ)) : 𝔇 (φ₁ :: φ₂ :: φ₃ :: φ₄ :: Γ)

Equations

• LO.OneSidedLK.swap₃ d = LO.OneSidedLK.contraction d ⋯

def LO.OneSidedLK.cut {F : Type u_1} {inst✝ : LogicalConnective F} {inst✝¹ : DeMorgan F} {inst✝² : TildeInvolutive F} {𝔇 : List F → Type u_2} [self : Cut 𝔇] {φ : F} {Γ Δ : List F} : 𝔇 (φ :: Γ) → 𝔇 (∼φ :: Δ) → 𝔇 (Γ ++ Δ)

Alias of LO.OneSidedLK.Cut.cut.

Equations

• @LO.OneSidedLK.cut = @LO.OneSidedLK.Cut.cut

def LO.OneSidedLK.eCut {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {φ : F} {Γ : List F} {ψ : F} {Δ : List F} [Cut 𝔇] (d₁ : 𝔇 (φ :: Γ)) (d₂ : 𝔇 (ψ :: Δ)) (e : ∼φ = ψ := by simp) : 𝔇 (Γ ++ Δ)

Equations

• LO.OneSidedLK.eCut d₁ d₂ e = LO.OneSidedLK.cut d₁ (LO.OneSidedLK.cast d₂ ⋯)

@[irreducible]

def LO.OneSidedLK.disj₂ {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {Γ Δ : List F} [Cut 𝔇] : 𝔇 (Γ ++ Δ) → 𝔇 (⋁Γ :: Δ)

Equations

• One or more equations did not get rendered due to their size.
• LO.OneSidedLK.disj₂ d_2 = LO.OneSidedLK.contra d_2 ⋯
• LO.OneSidedLK.disj₂ d_2 = d_2
• LO.OneSidedLK.disj₂ d_2 = LO.OneSidedLK.or d_2

def LO.OneSidedLK.conj₂ {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} [OneSidedLK 𝔇] {Γ Δ : List F} (d : (φ : F) → φ ∈ Γ → 𝔇 (φ :: Δ)) : 𝔇 (⋀Γ :: Δ)

Equations

• LO.OneSidedLK.conj₂ d_2 = LO.OneSidedLK.contra LO.OneSidedLK.verum ⋯
• LO.OneSidedLK.conj₂ d_2 = d_2 φ ⋯
• LO.OneSidedLK.conj₂ d_2 = LO.OneSidedLK.and (d_2 φ ⋯) (LO.OneSidedLK.conj₂ fun (χ : F) (h : χ ∈ ψ :: Γ_2) => d_2 χ ⋯)

class LO.OneSidedLK.PrincipalEntailment {F : Type u_1} (𝔇 : outParam (List F → Type u_3)) {P : Type u_4} [Entailment P F] (𝓟 : P) : Type (max (max u_1 u_3) u_5)

An entailment relation which is determined solely by derivability.

• equiv {φ : F} : 𝓟 ⊢! φ ≃ 𝔇 [φ]

theorem LO.OneSidedLK.PrincipalEntailment.provable_iff {F : Type u_1} {𝔇 : List F → Type u_2} {P : Type u_3} [Entailment P F] {𝓟 : P} [PrincipalEntailment 𝔇 𝓟] {φ : F} : 𝓟 ⊢ φ ↔ Nonempty (𝔇 [φ])

@[implicit_reducible]

instance LO.OneSidedLK.PrincipalEntailment.instModusPonens {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {P : Type u_3} [Entailment P F] (𝓟 : P) [PrincipalEntailment 𝔇 𝓟] [Cut 𝔇] : Entailment.ModusPonens 𝓟

Equations

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

@[implicit_reducible]

instance LO.OneSidedLK.PrincipalEntailment.instCl {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {P : Type u_3} [Entailment P F] (𝓟 : P) [PrincipalEntailment 𝔇 𝓟] [Cut 𝔇] : Entailment.Cl 𝓟

Equations

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

theorem LO.OneSidedLK.PrincipalEntailment.derivable_iff_provable_disj {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {P : Type u_3} [Entailment P F] {𝓟 : P} [PrincipalEntailment 𝔇 𝓟] [Cut 𝔇] {Γ : List F} : Nonempty (𝔇 Γ) ↔ 𝓟 ⊢ ⋁Γ

@[reducible, inline]

abbrev LO.OneSidedLK.Pullback {F : Type u_1} [LogicalConnective F] (𝔇 : List F → Type u_3) {G : Type u_4} [LogicalConnective G] (f : G →ˡᶜ F) : List G → Type u_3

Equations

• LO.OneSidedLK.Pullback 𝔇 f Γ = 𝔇 (List.map (⇑f) Γ)

def LO.OneSidedLK.Pullback.cast {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {G : Type u_3} [LogicalConnective G] {f : G →ˡᶜ F} {Δ : List F} {Γ : List G} (d : 𝔇 Δ) (h : Δ = List.map (⇑f) Γ := by simp) : Pullback 𝔇 f Γ

Equations

• LO.OneSidedLK.Pullback.cast d h = id (h ▸ d)

def LO.OneSidedLK.Pullback.uncast {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {G : Type u_3} [LogicalConnective G] {f : G →ˡᶜ F} {Γ : List G} {Δ : List F} (d : Pullback 𝔇 f Γ) (h : Δ = List.map (⇑f) Γ := by simp) : 𝔇 Δ

Equations

• d.uncast h = ⋯ ▸ d

@[implicit_reducible]

instance LO.OneSidedLK.Pullback.oneSidedLK {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {G : Type u_3} [LogicalConnective G] [DeMorgan G] [TildeInvolutive G] {f : G →ˡᶜ F} [OneSidedLK 𝔇] : OneSidedLK (Pullback 𝔇 f)

Equations

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

@[implicit_reducible]

instance LO.OneSidedLK.Pullback.cut {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {G : Type u_3} [LogicalConnective G] [DeMorgan G] [TildeInvolutive G] {f : G →ˡᶜ F} [Cut 𝔇] : Cut (Pullback 𝔇 f)

Equations

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

@[implicit_reducible]

instance LO.OneSidedLK.Pullback.instPrincipalEntailmentPullbackCoeHomPullback {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {G : Type u_3} [LogicalConnective G] {f : G →ˡᶜ F} {P : Type u_4} [Entailment P F] (𝓟 : P) [PrincipalEntailment 𝔇 𝓟] : PrincipalEntailment (Pullback 𝔇 f) (Entailment.pullback 𝓟 ⇑f)

Equations

• LO.OneSidedLK.Pullback.instPrincipalEntailmentPullbackCoeHomPullback 𝓟 = { equiv := fun {φ : G} => LO.OneSidedLK.PrincipalEntailment.equiv }

@[simp]

theorem LO.OneSidedLK.Pullback.nonempty_iff {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {G : Type u_3} [LogicalConnective G] {f : G →ˡᶜ F} {Γ : List G} : Nonempty (Pullback 𝔇 f Γ) ↔ Nonempty (𝔇 (List.map (⇑f) Γ))

@[simp]

theorem LO.OneSidedLK.Pullback.isEmpty_iff {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {G : Type u_3} [LogicalConnective G] {f : G →ˡᶜ F} {Γ : List G} : IsEmpty (Pullback 𝔇 f Γ) ↔ IsEmpty (𝔇 (List.map (⇑f) Γ))

class LO.OneSidedLK.ContextualEntailment {F : Type u_1} [LogicalConnective F] (𝔇 : outParam (List F → Type u_3)) (S : Type u_4) [Entailment S F] [AdjunctiveSet F S] : Type (max (max (max u_1 u_3) u_4) u_5)

An entailment relation which is determined by a context and derivability.

• equiv {𝓢 : S} {φ : F} : 𝓢 ⊢! φ ≃ (l : { l : List F // ∀ φ ∈ l, φ ∈ 𝓢 }) × 𝔇 (φ :: ∼↑l)

theorem LO.OneSidedLK.ContextualEntailment.provable_iff {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] {φ : F} {𝓢 : S} : 𝓢 ⊢ φ ↔ ∃ (Γ : List F), (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (φ :: ∼Γ))

def LO.OneSidedLK.ContextualEntailment.toProof {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] {φ : F} (𝓢 : S) (d : 𝔇 [φ]) : 𝓢 ⊢! φ

Equations

• LO.OneSidedLK.ContextualEntailment.toProof 𝓢 d = LO.OneSidedLK.ContextualEntailment.equiv.symm ⟨⟨[], ⋯⟩, d⟩

def LO.OneSidedLK.ContextualEntailment.ofAxiom {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] {φ : F} [OneSidedLK 𝔇] {𝓢 : S} (h : φ ∈ 𝓢) : 𝓢 ⊢! φ

Equations

• LO.OneSidedLK.ContextualEntailment.ofAxiom h = LO.OneSidedLK.ContextualEntailment.equiv.symm ⟨⟨[φ], ⋯⟩, LO.OneSidedLK.identity φ⟩

def LO.OneSidedLK.ContextualEntailment.ofAxiomSubset {F : Type u_1} [LogicalConnective F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] {φ : F} {𝓢 𝓤 : S} : 𝓢 ⊢! φ → 𝓢 ⊆ 𝓤 → 𝓤 ⊢! φ

Equations

• LO.OneSidedLK.ContextualEntailment.ofAxiomSubset b h = match LO.OneSidedLK.ContextualEntailment.equiv b with | ⟨l, d⟩ => LO.OneSidedLK.ContextualEntailment.equiv.symm ⟨⟨↑l, ⋯⟩, d⟩

@[implicit_reducible]

instance LO.OneSidedLK.ContextualEntailment.instAxiomatized {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [OneSidedLK 𝔇] : Entailment.Axiomatized S

Equations

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

@[implicit_reducible]

instance LO.OneSidedLK.ContextualEntailment.instModusPonens {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] (𝓢 : S) : Entailment.ModusPonens 𝓢

Equations

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

@[implicit_reducible]

instance LO.OneSidedLK.ContextualEntailment.instStrongCut {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] : Entailment.StrongCut S S

Equations

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

def LO.OneSidedLK.ContextualEntailment.instStrongCut.bl {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] {T U : S} {bs : T ⊢!* AdjunctiveSet.set U} (l : List F) (hl : ∀ ψ ∈ l, ψ ∈ U) (χ : F) (d : 𝔇 (χ :: ∼l)) : T ⊢! χ

Equations

• One or more equations did not get rendered due to their size.
• LO.OneSidedLK.ContextualEntailment.instStrongCut.bl [] hl_2 χ d_2 = LO.OneSidedLK.ContextualEntailment.equiv.symm ⟨⟨[], ⋯⟩, d_2⟩

@[implicit_reducible]

instance LO.OneSidedLK.ContextualEntailment.instDeductiveExplosion {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] : Entailment.DeductiveExplosion S

Equations

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

theorem LO.OneSidedLK.ContextualEntailment.inconsistent_iff {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] {𝓢 : S} : Entailment.Inconsistent 𝓢 ↔ ∃ (Γ : List F), (∀ ψ ∈ Γ, ψ ∈ 𝓢) ∧ Nonempty (𝔇 (∼Γ))

@[implicit_reducible]

instance LO.OneSidedLK.ContextualEntailment.cl {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] (𝓢 : S) : Entailment.Cl 𝓢

Equations

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

theorem LO.OneSidedLK.ContextualEntailment.empty_provable_iff_eprovable {F : Type u_1} [LogicalConnective F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] {P : Type u_4} [Entailment P F] {φ : F} {𝓟 : P} [PrincipalEntailment 𝔇 𝓟] : ∅ ⊢ φ ↔ 𝓟 ⊢ φ

theorem LO.OneSidedLK.ContextualEntailment.iff_context {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] {P : Type u_4} [Entailment P F] {φ : F} {𝓢 : S} {𝓟 : P} [PrincipalEntailment 𝔇 𝓟] : 𝓢 ⊢ φ ↔ AdjunctiveSet.set 𝓢 *⊢[𝓟] φ

theorem LO.OneSidedLK.ContextualEntailment.of_principal_provable {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] {P : Type u_4} [Entailment P F] {φ : F} {𝓟 : P} [PrincipalEntailment 𝔇 𝓟] {𝓢 : S} : 𝓟 ⊢ φ → 𝓢 ⊢ φ

@[reducible, inline]

noncomputable abbrev LO.OneSidedLK.ContextualEntailment.deduction {F : Type u_1} [LogicalConnective F] [DeMorgan F] [TildeInvolutive F] {𝔇 : List F → Type u_2} {S : Type u_3} [Entailment S F] [AdjunctiveSet F S] [ContextualEntailment 𝔇 S] [Cut 𝔇] {P : Type u_4} [Entailment P F] (𝓟 : P) [PrincipalEntailment 𝔇 𝓟] : Entailment.Deduction S

Equations

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