Documentation

Cslib.Logics.LinearLogic.CLL.EtaExpansion

η-expansion for Classical Linear Logic (CLL) #

source
@[irreducible]
def Cslib.CLL.Proposition.expand {Atom : Type u} (a : Proposition Atom) :
Logic.InferenceSystem.derivation {a, a.dual}

The η-expansion of a proposition a is a Proof of {a, a⫠} that applies the axiom only to atomic propositions.

Equations
Instances For
    source
    def Cslib.CLL.Proof.onlyAtomicAxioms {Atom : Type u} {Γ : Sequent Atom} (p : Logic.InferenceSystem.derivation Γ) :
    Bool

    A Proof has only atomic axioms if all its instances of the axiom treat atomic propositions.

    Equations
    Instances For
      source
      theorem Cslib.CLL.Proof.onlyAtomicAxioms_rwConclusion {Atom : Type u} {Γ Δ : Sequent Atom} {heq : Γ = Δ} {p : Logic.InferenceSystem.derivation Γ} (h : onlyAtomicAxioms p = true) :
      onlyAtomicAxioms (rwConclusion heq p) = true

      Proof.onlyAtomicAxioms is preserved by Proof.rwConclusion.

      source
      theorem Cslib.CLL.Proof.expand_onlyAtomicAxioms {Atom : Type u} (a : Proposition Atom) :
      onlyAtomicAxioms a.expand = true

      η-expansion is correct: the proof returned by η-expansion contains only atomic axioms.