Linear Logic Displayed


Συγγραφέας: Nuel Belnap


Nuel Belnap: Linear Logic Displayed (pdf, 1379K)
"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 itself including 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 iden-