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

Avron, Arnon

Theor. Comput. Sci. 57, No. 2-3, 161-184 (1988).

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

MSC:

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

Keywords:

relevant disjunction structure; Girard structure; linear logic; relevant logics

Citations:

Zbl 0625.03037

References:

[1]	Anderson, A. R.; Belnap, N. D., Entailment, Vol 1 (1975), Princeton University Press: Princeton University Press Princeton, NJ
[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
[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