Annals of Pure and Applied Logic 64 (3):273-291 (1993)
Authors |
|
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 |
![]() ![]() ![]() ![]() |
Download options
References found in this work BETA
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 Formalization of Kant’s Transcendental Logic.Theodora Achourioti & Michiel van Lambalgen - 2011 - Review of Symbolic Logic 4 (2):254-289.
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.
A Note on Full Intuitionistic Linear Logic.G. M. Bierman - 1996 - Annals of Pure and Applied Logic 79 (3):281-287.
View all 9 citations / Add more citations
Similar books and articles
An Analysis of Gödel's Dialectica Interpretation Via Linear Logic.Paulo Oliva - 2008 - Dialectica 62 (2):269–290.
An Analysis of Gödel's Dialectica Interpretation Via Linear Logic.Paulo Oliva - 2008 - Dialectica 62 (2):269-290.
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.
The Finite Model Property for Various Fragments of Intuitionistic Linear Logic.Mitsuhiro Okada & Kazushige Terui - 1999 - Journal of Symbolic Logic 64 (2):790-802.
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.
Pretopology Semantics for Bimodal Intuitionistic Linear Logic.C. Hartonas - 1997 - Logic Journal of the IGPL 5 (1):65-78.
The Finite Model Property for Various Fragments of Intuitionistic Linear Logic.Mitsuhiro Okada & Kazushige Terui - 1999 - Journal of Symbolic Logic 64 (2):790-802.
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.
On the Linear Decoration of Intuitionistic Derivations.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - Archive for Mathematical Logic 33 (6):387-412.
Analytics
Added to PP index
2014-01-16
Total views
29 ( #357,454 of 2,409,841 )
Recent downloads (6 months)
1 ( #541,271 of 2,409,841 )
2014-01-16
Total views
29 ( #357,454 of 2,409,841 )
Recent downloads (6 months)
1 ( #541,271 of 2,409,841 )
How can I increase my downloads?
Downloads