The semantics and proof theory of linear logic. (English) Zbl 0652.03018

Linear logic [see 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...” [J.-Y. Girard, “Geometry of interaction”, typescript (1988)].
Reviewer: M.Eytan


03B70 Logic in computer science
03F99 Proof theory and constructive mathematics


Zbl 0625.03037
Full Text: DOI


[1] Anderson, A. R.; Belnap, N. D., Entailment, Vol 1 (1975), Princeton University Press: Princeton University Press Princeton, NJ · Zbl 0323.02030
[2] Avron, A.; Honsell, F.; Mason, I., Using typed lambda calculus to implement formal systems on machine, (Technical Report ECS-LFCS-87-31 (1987), Laboratory for the Foundations of Computer Science, Edinburgh University) · Zbl 0784.68072
[3] Avron, A., Relevant entailment: semantics and formal systems, J. Symbolic Logic, 49, 334-342 (1984) · Zbl 0586.03017
[4] Avron, A., Simple consequence relations, (Technical Report ECS-LFCS-87-30 (1987), Laboratory for the Foundations of Computer Science, Edinburgh University) · Zbl 0733.03007
[5] Avron, A., The semantics and proof-theory of relevance logics and non-trivial theories containing contradictions, (Thesis (1984), Tel-Aviv University)
[6] Birkhoff, G., Lattice Theory (1948), Amer. Mathematical Soc: Amer. Mathematical Soc Providence · Zbl 0126.03801
[7] Dunn, J. M., Relevant logic and entailment, (Gabbay, D.; Guenther, F., Handbook of Philosophical Logic, Vol III (1984), Reidel: Reidel Dordrecht), 117-224 · Zbl 0875.03051
[8] Gentzen, G., Investigations into logical deduction, (Szabo, M. E., The Collected Work of Gerhard Gentzen (1969), North-Holland: North-Holland Amsterdam), 68-131 · Zbl 0209.30001
[9] Girard, J. Y., Linear Logic, Theoret. Comput. Sci., 50, 1-102 (1987) · Zbl 0625.03037
[10] Hodges, W., Elementary predicate calculus, (Gabbay, D.; Guenther, F., Handbook of Philosophical Logic, Vol I (1983), Reidel: Reidel Dordrecht), 1-128
[11] Kleene, S. C., Introduction to Mathematics (1952), Van Nostrand Reinhold: Van Nostrand Reinhold New York · Zbl 0047.00703
[12] Prawitz, D., Natural Deduction (1965), Almquist & Wiksell: Almquist & Wiksell Stockholm · Zbl 0173.00205
[13] Urquhart, A., The undecidability of entailment and relevant implication, J. Symbolic Logic, 49, 1059-1073 (1984) · Zbl 0581.03011
[14] Schwichtenberg, H., Proof-theory: some applications of cut-elimination, (Barwise, J., Handbook of Mathematical Logic (1977), North-Holland: North-Holland Amsterdam), 867-895
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.