Introduction to Part I

Abstract

One of the most important outcomes of the study of linear logic, much more than the formal system itself, is its revealing of the computational significance of the structural rules of Weakening and Contraction [Girard, 1987]. Logically, their absence leads to the decomposition of conjunction into additive (&) and multiplicative (⊗) forms, which may be given a sequential natural deduction presentation as follows:

$$\begin{gathered} \frac{{\Gamma | - \phi | - \psi }}{{\Gamma | - \phi \& \psi }}\& I\frac{{\Gamma | - {\phi _1}\& {\phi _2}}}{{\Gamma | - {\phi _i}}}(i = 1,2)\& E \hfill \\ \frac{{\Gamma | - \phi \Delta | - \psi }}{{\Gamma ,\Delta | - \phi \otimes \psi }} \otimes I\frac{{\Gamma ,\phi ,\psi | - x\Delta | - \phi \otimes \psi }}{{\Gamma ,\Delta | - x}} \otimes E. \hfill \\ \end{gathered} $$

Some of the content of Part I has appeared in [O ‘Hearn and Pym, 1999, Pym, 1999, Pym et al., 2000, Armel{n and Pym, 2001]. References are given in the text as appropriate.

—DJP