Annals of Pure and Applied Logic 64 (3):273-291 (1993)

Valeria Correa Vaz De Paiva
University of Birmingham
In this paper we give a brief treatment of a theory of proofs for a system of Full Intuitionistic Linear Logic. This system is distinct from Classical Linear Logic, but unlike the standard Intuitionistic Linear Logic of Girard and Lafont includes the multiplicative disjunction par. This connective does have an entirely natural interpretation in a variety of categorical models of Intuitionistic Linear Logic. The main proof-theoretic problem arises from the observation of Schellinx that cut elimination fails outright for an intuitive formulation of Full Intuitionistic Linear Logic; the nub of the problem is the interaction between par and linear implication. We present here a term assignment system which gives an interpretation of proofs as some kind of non-deterministic function. In this way we find a system which does enjoy cut elimination. The system is a direct result of an analysis of the categorical semantics, though we make an effort to present the system as if it were purely a proof-theoretic construction.
Keywords full intuitionistic linear logic  multiconclusion sequents  constructive par
Categories (categorize this paper)
DOI 10.1016/0168-0072(93)90146-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 65,657
Through your library

References found in this work BETA

Natural Deduction: A Proof-Theoretical Study.Dag Prawitz - 1965 - Stockholm, Sweden: Dover Publications.
Natural Deduction: A Proof-Theoretical Study.Richmond Thomason - 1965 - Journal of Symbolic Logic 32 (2):255-256.
A Game Semantics for Linear Logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
The Correspondence Between Cut-Elimination and Normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.
Normalization as a Homomorphic Image of Cut-Elimination.Garrel Pottinger - 1977 - Annals of Mathematical Logic 12 (3):323.

View all 9 references / Add more references

Citations of this work BETA

A Comparison Between Monoidal and Substructural Logics.Clayton Peterson - 2016 - Journal of Applied Non-Classical Logics 26 (2):126-159.
Investigations Into a Left-Structural Right-Substructural Sequent Calculus.Lloyd Humberstone - 2007 - Journal of Logic, Language and Information 16 (2):141-171.
Proof Theory in the Abstract.J. M. E. Hyland - 2002 - Annals of Pure and Applied Logic 114 (1-3):43-78.
Studies in the Logic of K -Onfirmation.Clayton Peterson - 2019 - Philosophical Studies 176 (2):437-471.

View all 9 citations / Add more citations

Similar books and articles

On the Unity of Logic.Jean-Yves Girard - 1993 - Annals of Pure and Applied Logic 59 (3):201-217.
The Logic of Bunched Implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
A Note on Full Intuitionistic Linear Logic.G. M. Bierman - 1996 - Annals of Pure and Applied Logic 79 (3):281-287.
Linearizing Intuitionistic Implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
Imperative Programs as Proofs Via Game Semantics.Martin Churchill, Jim Laird & Guy McCusker - 2013 - Annals of Pure and Applied Logic 164 (11):1038-1078.
Reflections on “Difficult” Embeddings.Andreja Prijatelj - 1995 - Journal of Philosophical Logic 24 (1):71 - 84.
A Normalizing System of Natural Deduction for Intuitionistic Linear Logic.Sara Negri - 2002 - Archive for Mathematical Logic 41 (8):789-810.
Normal Deduction in the Intuitionistic Linear Logic.G. Mints - 1998 - Archive for Mathematical Logic 37 (5-6):415-425.
Lineales.Martin Hyland & Valeria de Paiva - 1991 - O Que Nos Faz Pensar:107-123.


Added to PP index

Total views
32 ( #345,944 of 2,462,368 )

Recent downloads (6 months)
2 ( #299,176 of 2,462,368 )

How can I increase my downloads?


My notes