The semantics and proof theory of linear logic (Q1106836)

Linear logic [see \textit{J.-Y. Girard}, Theor. Comput. Sci. 50, 1-102 (1987; Zbl 0625.03037)] ``provides a continuation of the constructivization began with intuitionistic logic'' (Girard). It seems to have important fallout in Computer Science, viz programming theory, parallel computation, data bases and logic programming. The paper under review aims to provide more standard proof systems and semantics then Girard did. It gives strong completeness theorems (whereas Girard only gave weak ones) and relates linear logic to relevant logics, the most simply stated relation being: Linear \(\log ic+contraction=R\) without distribution. Reviewer's remark: The reader be better warned that the situation is not at all simple, since ``... the existence of a (self-dual) contraction in relevance logic (with, as in classical logic, the impossibility of a normalization theorem, i.e. some kind of Church-Rosser property), makes it hopeless to push the connection beyond the level of mere probability...'' [\textit{J.-Y. Girard}, ``Geometry of interaction'', typescript (1988)].