The semantics and proof theory of linear logic
type: Item
instance of: scholarly article
title: The semantics and proof theory of linear logic
zbMATH Open document ID: 0652.03018
DOI: 10.1016/0304-3975(88)90037-0
author: Arnon Avron
published in: Theoretical Computer Science
publication date: 1988-01-01T00:00:00Z
review text: 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)].
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03F99
zbMATH DE Number: 4063071
zbMATH Keywords: relevant disjunction structure
zbMATH Keywords: Girard structure
zbMATH Keywords: linear logic
zbMATH Keywords: relevant logics
reviewed by: Michel Eytan
MaRDI profile type: Publication
full work available at URL: 0304-3975(88)90037-0
OpenAlex ID: W1974484530
cites work: Q4085699
cites work: Using typed lambda calculus to implement formal systems on a machine
cites work: Relevant entailment—semantics and formal systems
cites work: Simple consequence relations
cites work: Q5331549
cites work: Q4342081
cites work: Q5610986
cites work: Linear logic
cites work: Q5812175
cites work: Q5559220
cites work: The undecidability of entailment and relevant implication
description: scientific article; zbMATH DE number 4063071