Linear logic displayed (Q918548)

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.