Supporting results for pointwise provable equality.

Sequent calculus and variants

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

Main Definitions

• FFL.OneSidedLK

Structural rules

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

Weakening and contraction rules for a multiset-indexed derivation family.

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

  The weakening construction in FFL.Structural.

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

  The contraction construction in FFL.Structural.

One-sided $\mathbf{LK}$

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

The structural and logical rules of the one-sided classical sequent calculus.

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

  The identity construction in FFL.OneSidedLK.

• verum : 𝔇 ⦃⊤⦄

  The verum construction in FFL.OneSidedLK.

• and {Γ : Multiset F} {φ ψ : F} : 𝔇 (Γ + ⦃φ⦄) → 𝔇 (Γ + ⦃ψ⦄) → 𝔇 (Γ + ⦃φ ⋏ ψ⦄)

  The and construction in FFL.OneSidedLK.

• or {Γ : Multiset F} {φ ψ : F} : 𝔇 (Γ + (⦃φ⦄ + ⦃ψ⦄)) → 𝔇 (Γ + ⦃φ ⋎ ψ⦄)

  The or construction in FFL.OneSidedLK.

class PointwiseComposition.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 PointwiseComposition.FFL.OneSidedLK 𝔇 : Type (max u_1 u_2)

Data and laws for Cut in FFL.OneSidedLK.

• 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} : 𝔇 (Γ + ⦃φ⦄) → 𝔇 (Δ + ⦃∼φ⦄) → 𝔇 (Γ + Δ)

  The cut construction in FFL.OneSidedLK.Cut.

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

The cast construction in FFL.Structural.

Equations

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

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

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

Equations

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

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

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

Equations

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

def PointwiseComposition.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

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

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

Contract a traversed subcontext already contained in the target context.

Equations

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

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

Expands multiset inclusion into local structural rules using traversals.

Equations

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

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

Alias of PointwiseComposition.FFL.Structural.cast.

---

The cast construction in FFL.Structural.

Equations

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

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

Alias of PointwiseComposition.FFL.Structural.weakenMany.

---

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

Equations

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

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

Alias of PointwiseComposition.FFL.Structural.ofSubset.

---

Expands multiset inclusion into local structural rules using traversals.

Equations

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

def PointwiseComposition.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Γ : Multiset.Traversal Γ) (tΔ : Multiset.Traversal Δ) (d : 𝔇 Γ) (h : Γ ⊆ Δ := by simp) : 𝔇 Δ

The contra construction in FFL.OneSidedLK.

Equations

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

def PointwiseComposition.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 : Multiset.Traversal Γ) (hp : φ ∈ Γ := by simp) (hn : ∼φ ∈ Γ := by simp) : 𝔇 Γ

The close construction in FFL.OneSidedLK.

Equations

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

def PointwiseComposition.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 : Multiset.Traversal Γ) (h : ⊤ ∈ Γ := by simp) : 𝔇 Γ

The top construction in FFL.OneSidedLK.

Equations

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

def PointwiseComposition.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Γ : Multiset.Traversal Γ) (tΔ : Multiset.Traversal Δ) (dφ : 𝔇 (Γ + ⦃φ⦄)) (dψ : 𝔇 (Δ + ⦃ψ⦄)) : 𝔇 (Γ + Δ + ⦃φ ⋏ ψ⦄)

The tensor construction in FFL.OneSidedLK.

Equations

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

def PointwiseComposition.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 PointwiseComposition.FFL.OneSidedLK.Cut.cut.

---

The cut construction in FFL.OneSidedLK.Cut.

Equations

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

def PointwiseComposition.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) : 𝔇 (Γ + Δ)

The e Cut construction in FFL.OneSidedLK.

Equations

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

def PointwiseComposition.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

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

def PointwiseComposition.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 PointwiseComposition.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 𝔇] : 𝔇 (↑Γ + Δ) → 𝔇 (Δ + ⦃⋁Γ⦄)

The disj₂ construction in FFL.OneSidedLK.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.OneSidedLK.disj₂ d_2 = PointwiseComposition.FFL.OneSidedLK.cast (PointwiseComposition.FFL.Structural.weakening (PointwiseComposition.FFL.OneSidedLK.cast d_2 ⋯)) ⋯
• PointwiseComposition.FFL.OneSidedLK.disj₂ d_2 = PointwiseComposition.FFL.OneSidedLK.cast d_2 ⋯

def PointwiseComposition.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Δ : Multiset.Traversal Δ) (d : (φ : F) → φ ∈ Γ → 𝔇 (Δ + ⦃φ⦄)) : 𝔇 (Δ + ⦃⋀Γ⦄)

The conj₂ construction in FFL.OneSidedLK.

Equations

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

def PointwiseComposition.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 : Multiset.Traversal Γ) : 𝔇 (Γ + (⦃φ⦄ + ⦃∼φ⦄))

The identity With construction in FFL.OneSidedLK.AxiomDerivation.

Equations

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

def PointwiseComposition.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 : 𝔇 (⦃φ⦄ + ⦃ψ⦄)) : 𝔇 ⦃φ ⋎ ψ⦄

The intro Or construction in FFL.OneSidedLK.AxiomDerivation.

Equations

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

def PointwiseComposition.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 : 𝔇 ↑Γ) : 𝔇 ⦃⋁Γ⦄

The intro Disj construction in FFL.OneSidedLK.AxiomDerivation.

Equations

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

def PointwiseComposition.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 PointwiseComposition.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

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

def PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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

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

def PointwiseComposition.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

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

def PointwiseComposition.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 PointwiseComposition.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

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

@[reducible, inline]

abbrev PointwiseComposition.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 PointwiseComposition.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} : 𝓟 ⊢! φ ≃ 𝔇 ⦃φ⦄

  The equiv construction in FFL.OneSidedLK.PrincipalEntailment.

theorem PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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

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

theorem PointwiseComposition.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 PointwiseComposition.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

The Pullback construction in FFL.OneSidedLK.

Equations

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

def PointwiseComposition.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 Γ

The cast construction in FFL.OneSidedLK.Pullback.

Equations

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

def PointwiseComposition.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) : 𝔇 Δ

The uncast construction in FFL.OneSidedLK.Pullback.

Equations

• d.uncast h = ⋯ ▸ d

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.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

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

@[simp]

theorem PointwiseComposition.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 PointwiseComposition.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) Γ))