zbMATH — the first resource for mathematics

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

MSC:
 03B70 Logic in computer science 03F99 Proof theory and constructive mathematics
Full Text:
References:
 [1] Anderson, A.R.; Belnap, N.D., Entailment, Vol 1, (1975), Princeton University Press Princeton, NJ [2] Avron, A.; Honsell, F.; Mason, I., Using typed lambda calculus to implement formal systems on machine, () · 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, () · Zbl 0733.03007 [5] Avron, A., The semantics and proof-theory of relevance logics and non-trivial theories containing contradictions, () [6] Birkhoff, G., Lattice theory, (1948), Amer. Mathematical Soc Providence · Zbl 0126.03801 [7] Dunn, J.M., Relevant logic and entailment, (), 117-224 · Zbl 0875.03051 [8] Gentzen, G., Investigations into logical deduction, (), 68-131 [9] Girard, J.Y., Linear logic, Theoret. comput. sci., 50, 1-102, (1987) · Zbl 0625.03037 [10] Hodges, W., Elementary predicate calculus, (), 1-128 [11] Kleene, S.C., Introduction to mathematics, (1952), Van Nostrand Reinhold New York · Zbl 0047.00703 [12] Prawitz, D., Natural deduction, (1965), 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, (), 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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.