Linearizing intuitionistic implication

, &
Annals of Pure and Applied Logic 60 (2):151-177 (1993)
  Copy   BIBTEX

Abstract

An embedding of the implicational propositional intuitionistic logic into the nonmodal fragment of intuitionistic linear logic is given. The embedding preserves cut-free proofs in a proof system that is a variant of IIL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of resources in IIL proofs

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(93)90041-b

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,386

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

A weak intuitionistic propositional logic with purely constructive implication.Mitsuhiro Okada - 1987 - Studia Logica 46 (4):371 - 382.
The logic of bunched implications.Peter W. O'Hearn & David J. Pym - 1999 - Bulletin of Symbolic Logic 5 (2):215-244.
Expressing Second-order Sentences in Intuitionistic Dependence Logic.Fan Yang - 2013 - Studia Logica 101 (2):323-342.
Decision problems for propositional linear logic.Patrick Lincoln, John Mitchell, Andre Scedrov & Natarajan Shankar - 1992 - Annals of Pure and Applied Logic 56 (1-3):239-311.
The pleasures of anticipation: Enriching intuitionistic logic. [REVIEW]Lloyd Humberstone - 2001 - Journal of Philosophical Logic 30 (5):395-438.
Natural Semantics: Why Natural Deduction is Intuitionistic.James W. Garson - 2001 - Theoria 67 (2):114-139.
From if to bi.Samson Abramsky & Jouko Väänänen - 2009 - Synthese 167 (2):207 - 230.
Grafting modalities onto substructural implication systems.Marcello D'agostino, Dov M. Gabbay & Alessandra Russo - 1997 - Studia Logica 59 (1):65-102.
Combining Derivations and Refutations for Cut-free Completeness in Bi-intuitionistic Logic.Linda Postniece - unknown
Structuralist logic: Implications, inferences, and consequences. [REVIEW]Arnold Koslow - 2007 - Logica Universalis 1 (1):167-181.
Contrariety and Subcontrariety: The Anatomy of Negation (with Special Reference to an Example of J.-Y. Béziau).Lloyd Humberstone - 2005 - Theoria 71 (3):241-262.
A Finite Hilbert‐Style Axiomatization of the Implication‐Less Fragment of the Intuitionistic Propositional Calculus.Jordi Rebagliato & Ventura Verdú - 1994 - Mathematical Logic Quarterly 40 (1):61-68.
Intuitionistic mathematics does not needex falso quodlibet.Neil Tennant - 1994 - Topoi 13 (2):127-133.
Disjunction and existence under implication in elementary intuitionistic formalisms.S. C. Kleene - 1962 - Journal of Symbolic Logic 27 (1):11-18.
An addendum: Disjunction and existence under implication in elementary intuitionistic formalisms.S. C. Kleene - 1963 - Journal of Symbolic Logic 28 (2):154-156.

Analytics

Added to PP
2014-01-16

Downloads
29 (#536,973)

6 months
17 (#141,290)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Natarajan Shankar
International University College

Citations of this work

Linearizing intuitionistic implication.Patrick Lincoln, Andre Scedrov & Natarajan Shankar - 1993 - Annals of Pure and Applied Logic 60 (2):151-177.
The complexity of Horn fragments of Linear Logic.Max I. Kanovich - 1994 - Annals of Pure and Applied Logic 69 (2-3):195-241.
Linear logic.Roberto Di Cosmo & Dale Miller - unknown - Stanford Encyclopedia of Philosophy.
Petri nets, Horn programs, Linear Logic and vector games.Max I. Kanovich - 1995 - Annals of Pure and Applied Logic 75 (1-2):107-135.
Linear logic as a logic of computations.Max I. Kanovich - 1994 - Annals of Pure and Applied Logic 67 (1-3):183-212.

View all 7 citations / Add more citations

References found in this work

Proofs and types.Jean-Yves Girard - 1989 - New York: Cambridge University Press.
A game semantics for linear logic.Andreas Blass - 1992 - Annals of Pure and Applied Logic 56 (1-3):183-220.
Contraction-free sequent calculi for intuitionistic logic.Roy Dyckhoff - 1992 - Journal of Symbolic Logic 57 (3):795-807.

View all 7 references / Add more references