Full intuitionistic linear logic

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

Authors
Valeria Correa Vaz De Paiva
University of Birmingham
Abstract
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
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


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

References found in this work BETA

Natural Deduction: A Proof-Theoretical Study.Dag Prawitz - 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 II.J. Zucker - 1974 - Annals of Pure and Applied Logic 7 (2):113.
The Correspondence Between Cut-Elimination and Normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.

View all 8 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.
Monoidal Logics: Completeness and Classical Systems.Clayton Peterson - 2019 - Journal of Applied Non-Classical Logics 29 (2):121-151.

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.

Analytics

Added to PP index
2014-01-16

Total views
26 ( #331,929 of 2,265,147 )

Recent downloads (6 months)
3 ( #447,493 of 2,265,147 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature