Sequent calculus and variants

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

Main Definitions

• FFL.OneSidedLK

Structural rules

class FFL.Structural {F : Type u_1} (𝔇 : Multiset F → Type u_2) : Type (max u_1 u_2)

• weakening {Γ : Multiset F} {φ : F} : 𝔇 Γ → 𝔇 (Γ + ⦃φ⦄)
• contraction {Γ : Multiset F} {φ : F} : 𝔇 (Γ + (⦃φ⦄ + ⦃φ⦄)) → 𝔇 (Γ + ⦃φ⦄)

One-sided $\mathbf{LK}$

class FFL.OneSidedLK {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] (𝔇 : Multiset F → Type u_2) extends FFL.Structural 𝔇 : Type (max u_1 u_2)

• weakening {Γ : Multiset F} {φ : F} : 𝔇 Γ → 𝔇 (Γ + ⦃φ⦄)
• contraction {Γ : Multiset F} {φ : F} : 𝔇 (Γ + (⦃φ⦄ + ⦃φ⦄)) → 𝔇 (Γ + ⦃φ⦄)
• identity (φ : F) : 𝔇 (⦃φ⦄ + ⦃∼φ⦄)
• verum : 𝔇 ⦃⊤⦄
• and {Γ : Multiset F} {φ ψ : F} : 𝔇 (Γ + ⦃φ⦄) → 𝔇 (Γ + ⦃ψ⦄) → 𝔇 (Γ + ⦃φ ⋏ ψ⦄)
• or {Γ : Multiset F} {φ ψ : F} : 𝔇 (Γ + (⦃φ⦄ + ⦃ψ⦄)) → 𝔇 (Γ + ⦃φ ⋎ ψ⦄)

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

• weakening {Γ : Multiset F} {φ : F} : 𝔇 Γ → 𝔇 (Γ + ⦃φ⦄)
• contraction {Γ : Multiset F} {φ : F} : 𝔇 (Γ + (⦃φ⦄ + ⦃φ⦄)) → 𝔇 (Γ + ⦃φ⦄)
• identity (φ : F) : 𝔇 (⦃φ⦄ + ⦃∼φ⦄)
• verum : 𝔇 ⦃⊤⦄
• and {Γ : Multiset F} {φ ψ : F} : 𝔇 (Γ + ⦃φ⦄) → 𝔇 (Γ + ⦃ψ⦄) → 𝔇 (Γ + ⦃φ ⋏ ψ⦄)
• or {Γ : Multiset F} {φ ψ : F} : 𝔇 (Γ + (⦃φ⦄ + ⦃ψ⦄)) → 𝔇 (Γ + ⦃φ ⋎ ψ⦄)
• cut {Γ : Multiset F} {φ : F} {Δ : Multiset F} : 𝔇 (Γ + ⦃φ⦄) → 𝔇 (Δ + ⦃∼φ⦄) → 𝔇 (Γ + Δ)

def FFL.Structural.cast {F : Type u_1} {𝔇 : Multiset F → Type u_2} {Γ Δ : Multiset F} (d : 𝔇 Γ) (h : Γ = Δ := by abel) : 𝔇 Δ

Equations

• FFL.Structural.cast d h = h ▸ d

def FFL.Structural.weakenMany {F : Type u_1} {𝔇 : Multiset F → Type u_2} [Structural 𝔇] {Γ Δ : Multiset F} (t : Δ.Traversal) (d : 𝔇 Γ) : 𝔇 (Γ + Δ)

Repeated weakening along a traversal (a routine structural derivation).

Equations

• FFL.Structural.weakenMany Multiset.Traversal.zero d = FFL.Structural.cast d ⋯
• FFL.Structural.weakenMany (Multiset.Traversal.succ φ t_2) d = FFL.Structural.cast (FFL.Structural.weakening (FFL.Structural.weakenMany t_2 d)) ⋯

def FFL.Structural.contractMany {F : Type u_1} {𝔇 : Multiset F → Type u_2} [Structural 𝔇] {Γ Δ : Multiset F} (t : Γ.Traversal) (d : 𝔇 (Δ + Γ + Γ)) : 𝔇 (Δ + Γ)

Repeated contraction along a traversal (a routine structural derivation).

Equations

• One or more equations did not get rendered due to their size.
• FFL.Structural.contractMany Multiset.Traversal.zero d_2 = FFL.Structural.cast d_2 ⋯

def FFL.Structural.absorb {F : Type u_1} {𝔇 : Multiset F → Type u_2} {Γ : Multiset F} {φ : F} [Structural 𝔇] [DecidableEq F] (d : 𝔇 (Γ + ⦃φ⦄)) (h : φ ∈ Γ) : 𝔇 Γ

Absorbs a formula already in the context (a routine structural derivation).

Equations

• FFL.Structural.absorb d h = FFL.Structural.cast (FFL.Structural.contraction (FFL.Structural.cast d ⋯)) ⋯

def FFL.Structural.ofSubset {F : Type u_1} {𝔇 : Multiset F → Type u_2} {Γ Δ : Multiset F} [Structural 𝔇] [DecidableEq F] (tΓ : Γ.Traversal) (tΔ : Δ.Traversal) (d : 𝔇 Γ) (h : Γ ⊆ Δ) : 𝔇 Δ

Expands multiset inclusion into local structural rules using traversals.

Equations

• FFL.Structural.ofSubset tΓ tΔ d h = FFL.Structural.ofSubset.go tΓ h (FFL.Structural.cast (FFL.Structural.weakenMany tΔ d) ⋯)

def FFL.Structural.ofSubset.go {F : Type u_1} {𝔇 : Multiset F → Type u_2} {Δ : Multiset F} [Structural 𝔇] [DecidableEq F] {Γ : Multiset F} (t : Γ.Traversal) (h : Γ ⊆ Δ) (d : 𝔇 (Δ + Γ)) : 𝔇 Δ

Equations

• FFL.Structural.ofSubset.go Multiset.Traversal.zero h_2 d_2 = FFL.Structural.cast d_2 ⋯
• FFL.Structural.ofSubset.go (Multiset.Traversal.succ φ t_2) h_2 d_2 = FFL.Structural.ofSubset.go t_2 ⋯ (FFL.Structural.absorb (FFL.Structural.cast d_2 ⋯) ⋯)

def FFL.OneSidedLK.cast {F : Type u_1} {𝔇 : Multiset F → Type u_2} {Γ Δ : Multiset F} (d : 𝔇 Γ) (h : Γ = Δ := by abel) : 𝔇 Δ

Alias of FFL.Structural.cast.

Equations

• @FFL.OneSidedLK.cast = @FFL.Structural.cast

def FFL.OneSidedLK.weakenMany {F : Type u_1} {𝔇 : Multiset F → Type u_2} [Structural 𝔇] {Γ Δ : Multiset F} (t : Δ.Traversal) (d : 𝔇 Γ) : 𝔇 (Γ + Δ)

Alias of FFL.Structural.weakenMany.

---

Repeated weakening along a traversal (a routine structural derivation).

Equations

• @FFL.OneSidedLK.weakenMany = @FFL.Structural.weakenMany

def FFL.OneSidedLK.ofSubset {F : Type u_1} {𝔇 : Multiset F → Type u_2} {Γ Δ : Multiset F} [Structural 𝔇] [DecidableEq F] (tΓ : Γ.Traversal) (tΔ : Δ.Traversal) (d : 𝔇 Γ) (h : Γ ⊆ Δ) : 𝔇 Δ

Alias of FFL.Structural.ofSubset.

---

Expands multiset inclusion into local structural rules using traversals.

Equations

• @FFL.OneSidedLK.ofSubset = @FFL.Structural.ofSubset

def FFL.OneSidedLK.contra {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {Γ Δ : Multiset F} [OneSidedLK 𝔇] [DecidableEq F] (tΓ : Γ.Traversal) (tΔ : Δ.Traversal) (d : 𝔇 Γ) (h : Γ ⊆ Δ := by simp) : 𝔇 Δ

Equations

• FFL.OneSidedLK.contra tΓ tΔ d h = FFL.OneSidedLK.ofSubset tΓ tΔ d h

def FFL.OneSidedLK.close {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {Γ : Multiset F} [OneSidedLK 𝔇] [DecidableEq F] (φ : F) (t : Γ.Traversal) (hp : φ ∈ Γ := by simp) (hn : ∼φ ∈ Γ := by simp) : 𝔇 Γ

Equations

• FFL.OneSidedLK.close φ t hp hn = FFL.OneSidedLK.contra (Multiset.Traversal.succ (∼φ) (Multiset.Traversal.atom φ)) t (FFL.OneSidedLK.identity φ) ⋯

def FFL.OneSidedLK.top {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {Γ : Multiset F} [OneSidedLK 𝔇] [DecidableEq F] (t : Γ.Traversal) (h : ⊤ ∈ Γ := by simp) : 𝔇 Γ

Equations

• FFL.OneSidedLK.top t h = FFL.OneSidedLK.contra (Multiset.Traversal.atom ⊤) t FFL.OneSidedLK.verum ⋯

def FFL.OneSidedLK.tensor {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {Γ Δ : Multiset F} [OneSidedLK 𝔇] {φ ψ : F} (tΓ : Γ.Traversal) (tΔ : Δ.Traversal) (dφ : 𝔇 (Γ + ⦃φ⦄)) (dψ : 𝔇 (Δ + ⦃ψ⦄)) : 𝔇 (Γ + Δ + ⦃φ ⋏ ψ⦄)

Equations

• FFL.OneSidedLK.tensor tΓ tΔ dφ dψ = FFL.OneSidedLK.and (FFL.OneSidedLK.cast (FFL.OneSidedLK.weakenMany tΔ dφ) ⋯) (FFL.OneSidedLK.cast (FFL.OneSidedLK.weakenMany tΓ dψ) ⋯)

def FFL.OneSidedLK.cut {F : Type u_1} {inst✝ : LogicalConnective F} {inst✝¹ : LogicalNeutral F} {inst✝² : TildeInvolutive F} {inst✝³ : LogicalConnective.DeMorgan F} {inst✝⁴ : LogicalNeutral.DeMorgan F} {𝔇 : Multiset F → Type u_2} [self : Cut 𝔇] {Γ : Multiset F} {φ : F} {Δ : Multiset F} : 𝔇 (Γ + ⦃φ⦄) → 𝔇 (Δ + ⦃∼φ⦄) → 𝔇 (Γ + Δ)

Alias of FFL.OneSidedLK.Cut.cut.

Equations

• @FFL.OneSidedLK.cut = @FFL.OneSidedLK.Cut.cut

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

Equations

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

def FFL.OneSidedLK.removeBot {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {Γ : Multiset F} [Cut 𝔇] (d : 𝔇 (Γ + ⦃⊥⦄)) : 𝔇 Γ

Eliminating falsum is the routine cut against the verum rule.

Equations

• FFL.OneSidedLK.removeBot d = FFL.OneSidedLK.cast (FFL.OneSidedLK.cut d (FFL.OneSidedLK.cast FFL.OneSidedLK.verum ⋯)) ⋯

def FFL.OneSidedLK.modusPonens {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {Γ : Multiset F} {φ ψ : F} {Δ : Multiset F} [Cut 𝔇] (di : 𝔇 (Γ + ⦃φ 🡒 ψ⦄)) (dp : 𝔇 (Δ + ⦃φ⦄)) : 𝔇 (Γ + Δ + ⦃ψ⦄)

Modus ponens with independent side contexts. This is the routine cut derivation.

Equations

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

@[irreducible]

def FFL.OneSidedLK.disj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {Γ : List F} {Δ : Multiset F} [OneSidedLK 𝔇] : 𝔇 (↑Γ + Δ) → 𝔇 (Δ + ⦃⋁Γ⦄)

Equations

• FFL.OneSidedLK.disj₂ d_2 = FFL.OneSidedLK.cast (FFL.Structural.weakening (FFL.OneSidedLK.cast d_2 ⋯)) ⋯
• FFL.OneSidedLK.disj₂ d_2 = FFL.OneSidedLK.cast d_2 ⋯
• FFL.OneSidedLK.disj₂ d_2 = FFL.OneSidedLK.or (FFL.OneSidedLK.cast (FFL.OneSidedLK.disj₂ (FFL.OneSidedLK.cast d_2 ⋯)) ⋯)

def FFL.OneSidedLK.conj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] {Γ : List F} {Δ : Multiset F} (tΔ : Δ.Traversal) (d : (φ : F) → φ ∈ Γ → 𝔇 (Δ + ⦃φ⦄)) : 𝔇 (Δ + ⦃⋀Γ⦄)

Equations

• FFL.OneSidedLK.conj₂ tΔ d_2 = FFL.OneSidedLK.cast (FFL.OneSidedLK.weakenMany tΔ FFL.OneSidedLK.verum) ⋯
• FFL.OneSidedLK.conj₂ tΔ d_2 = d_2 φ ⋯
• FFL.OneSidedLK.conj₂ tΔ d_2 = FFL.OneSidedLK.and (d_2 φ ⋯) (FFL.OneSidedLK.conj₂ tΔ fun (χ : F) (h : χ ∈ ψ :: Γ_2) => d_2 χ ⋯)

def FFL.OneSidedLK.AxiomDerivation.identityWith {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] {Γ : Multiset F} (φ : F) (t : Γ.Traversal) : 𝔇 (Γ + (⦃φ⦄ + ⦃∼φ⦄))

Equations

• FFL.OneSidedLK.AxiomDerivation.identityWith φ t = FFL.OneSidedLK.cast (FFL.Structural.weakenMany t (FFL.OneSidedLK.identity φ)) ⋯

def FFL.OneSidedLK.AxiomDerivation.introOr {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] {φ ψ : F} (d : 𝔇 (⦃φ⦄ + ⦃ψ⦄)) : 𝔇 ⦃φ ⋎ ψ⦄

Equations

• FFL.OneSidedLK.AxiomDerivation.introOr d = FFL.OneSidedLK.cast (FFL.OneSidedLK.or (FFL.OneSidedLK.cast d ⋯)) ⋯

def FFL.OneSidedLK.AxiomDerivation.introDisj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] {Γ : List F} (d : 𝔇 ↑Γ) : 𝔇 ⦃⋁Γ⦄

Equations

• FFL.OneSidedLK.AxiomDerivation.introDisj d = FFL.OneSidedLK.cast (FFL.OneSidedLK.disj₂ (FFL.OneSidedLK.cast d ⋯)) ⋯

def FFL.OneSidedLK.AxiomDerivation.negEquiv {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ : F) : 𝔇 ⦃(φ ⋎ ∼φ ⋎ ⊥) ⋏ (φ ⋏ ⊤ ⋎ ∼φ)⦄

The rule expansion of the classical negation equivalence axiom. This is a routine syntactic derivation.

Equations

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

def FFL.OneSidedLK.AxiomDerivation.implyK {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ : F) : 𝔇 ⦃∼φ ⋎ ∼ψ ⋎ φ⦄

The rule expansion of the K axiom. This is a routine syntactic derivation.

Equations

• FFL.OneSidedLK.AxiomDerivation.implyK φ ψ = FFL.OneSidedLK.AxiomDerivation.introDisj (FFL.OneSidedLK.cast (FFL.OneSidedLK.AxiomDerivation.identityWith φ (Multiset.Traversal.atom (∼ψ))) ⋯)

def FFL.OneSidedLK.AxiomDerivation.implyS {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ χ : F) : 𝔇 ⦃φ ⋏ ψ ⋏ ∼χ ⋎ φ ⋏ ∼ψ ⋎ ∼φ ⋎ χ⦄

The rule expansion of the S axiom. This is a routine syntactic derivation.

Equations

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

def FFL.OneSidedLK.AxiomDerivation.and₁ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ : F) : 𝔇 ⦃(∼φ ⋎ ∼ψ) ⋎ φ⦄

The rule expansion of the first conjunction axiom. This is a routine syntactic derivation.

Equations

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

def FFL.OneSidedLK.AxiomDerivation.and₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ : F) : 𝔇 ⦃(∼φ ⋎ ∼ψ) ⋎ ψ⦄

The rule expansion of the second conjunction axiom. This is a routine syntactic derivation.

Equations

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

def FFL.OneSidedLK.AxiomDerivation.and₃ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ : F) : 𝔇 ⦃∼φ ⋎ ∼ψ ⋎ φ ⋏ ψ⦄

The rule expansion of conjunction introduction. This is a routine syntactic derivation.

Equations

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

def FFL.OneSidedLK.AxiomDerivation.or₁ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ : F) : 𝔇 ⦃∼φ ⋎ φ ⋎ ψ⦄

The rule expansion of the first disjunction axiom. This is a routine syntactic derivation.

Equations

• FFL.OneSidedLK.AxiomDerivation.or₁ φ ψ = FFL.OneSidedLK.AxiomDerivation.introDisj (FFL.OneSidedLK.cast (FFL.OneSidedLK.AxiomDerivation.identityWith φ (Multiset.Traversal.atom ψ)) ⋯)

def FFL.OneSidedLK.AxiomDerivation.or₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ : F) : 𝔇 ⦃∼ψ ⋎ φ ⋎ ψ⦄

The rule expansion of the second disjunction axiom. This is a routine syntactic derivation.

Equations

• FFL.OneSidedLK.AxiomDerivation.or₂ φ ψ = FFL.OneSidedLK.AxiomDerivation.introDisj (FFL.OneSidedLK.cast (FFL.OneSidedLK.AxiomDerivation.identityWith ψ (Multiset.Traversal.atom φ)) ⋯)

def FFL.OneSidedLK.AxiomDerivation.or₃ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ ψ χ : F) : 𝔇 ⦃φ ⋏ ∼χ ⋎ ψ ⋏ ∼χ ⋎ ∼φ ⋏ ∼ψ ⋎ χ⦄

The rule expansion of disjunction elimination. This is a routine syntactic derivation.

Equations

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

def FFL.OneSidedLK.AxiomDerivation.dne {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} [OneSidedLK 𝔇] (φ : F) : 𝔇 ⦃∼φ ⋎ φ⦄

The rule expansion of double-negation elimination. This is a routine syntactic derivation.

Equations

• FFL.OneSidedLK.AxiomDerivation.dne φ = FFL.OneSidedLK.AxiomDerivation.introOr (FFL.OneSidedLK.cast (FFL.OneSidedLK.identity φ) ⋯)

@[reducible, inline]

abbrev FFL.OneSidedLK.AxiomDerivation.cl {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset F → Type u_2} {P : Type u_3} [Entailment P F] (𝓟 : P) [Entailment.ModusPonens 𝓟] [OneSidedLK 𝔇] (lift : {φ : F} → 𝔇 ⦃φ⦄ → 𝓟 ⊢! φ) : Entailment.Cl 𝓟

A one-sided classical calculus induces classical entailment whenever singleton derivations can be embedded as proofs. This is the routine translation of the Hilbert axioms into one-sided sequent rules.

Equations

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

class FFL.OneSidedLK.PrincipalEntailment {F : Type u_1} (𝔇 : outParam (Multiset 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 FFL.OneSidedLK.PrincipalEntailment.provable_iff {F : Type u_1} {𝔇 : Multiset F → Type u_2} {P : Type u_3} [Entailment P F] {𝓟 : P} [PrincipalEntailment 𝔇 𝓟] {φ : F} : 𝓟 ⊢ φ ↔ Nonempty (𝔇 ⦃φ⦄)

@[instance_reducible]

instance FFL.OneSidedLK.PrincipalEntailment.instModusPonens {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [TildeInvolutive F] [LogicalConnective.DeMorgan F] [LogicalNeutral.DeMorgan F] {𝔇 : Multiset 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.

@[instance_reducible]

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

Equations

• FFL.OneSidedLK.PrincipalEntailment.instCl 𝓟 = FFL.OneSidedLK.AxiomDerivation.cl 𝓟 fun {φ : F} => ⇑FFL.OneSidedLK.PrincipalEntailment.equiv.symm

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

@[reducible, inline]

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

Equations

• FFL.OneSidedLK.Pullback 𝔇 f Γ = 𝔇 (Multiset.map (⇑f) Γ)

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

Equations

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

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

Equations

• d.uncast h = ⋯ ▸ d

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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