Linear logic displayed.
Nuel Belnap · Notre Dame Journal of Formal Logic · 1989
Linear logic" (LL; see Girard [6]) was proposed to be of use in computer science, but it can be formulated as a "display logic" (DL; see Belnap [2]), which is a kind of Gentzen calculus admitting easy proof of an Elimination Theorem.Thus LL is naturally placed within a wider prooftheoretical framework that is known to include relevance, intuitionist, and modal logics, etc., and that permits coherent variations on LL itselfincluding the definition of "punctual logic".In order to accommodate LL, two independently useful modifications of DL are made.First, DL possessed an unmotivated identification of two of its structural constants.This identification is dropped in order to make room in DL for the several propositional constants in LL.Second, DL possessed an unmotivated bias towards connectives that, when they are introduced as consequents, have restrictions put on their antecedents.This bias is abandoned in order to make room in DL for a dual pair of modal-like "exponential" connectives of LL.The latter modification requires restructuring the proof of the Elimination Theorem for DL, rendering it perfectly symmetrical in antecedent and consequent.