Linear logic displayed
The author's Display Logic is a kind of Gentzen consecution calculus designed to effect an easy proof of an Elimination Theorem. Here the original version of Display Logic is modified to make it more elegant, and to extend it to all for the display of the Linear Logic of Girard, a system originally introduced for use in computer science. Linear Logic is displayed in the sense that a Display Logic is constructed that is provably equivalent to Linear Logic's original Hilbert-style formulation. This locates Linear Logic within a proof-theoretic framework which includes intuitionist, relevance and modal logics. It also allows variations of Linear Logic which are not accessible in the Hilbert formulation. This paper presupposes familiarity with Girard's prior work on Linear Logic and the author's prior work on Display Logic.
- Displaying and deciding substructural logics. I: Logics with contraposition
- Displaying modal logic
- Bilattice logic properly displayed
- Disentangling structural connectives or life without display property
- The decidability of the intensional fragment of classical linear logic
- Current trends in substructural logics
- Sequent Calculi for Normal Modal Propositional Logics
- The display problem revisited
- Linear Logic Properly Displayed
- Display calculi and other modal calculi: a comparison
This page was built for publication: Linear logic displayed
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q918548)
