[Prev][Next][Index][Thread]

natural deduction for linear logic; corrections;bibliography



The following is the abstract of a paper delivered on occassion of
Dirk van Dalen's 60th birthday, in april.

ABSTRACT

Natural deduction for intuitionistic linear logic 
by A.S. Troelstra

The paper deals with two versions of the fragment with unit, tensor,
linear implication and storage operator (the exponential !) of
intuitionistic linear logic. The first version, ILL, appears in a
paper by Benton, Bierman, Hyland and de Paiva; the second one, ILLP,
is described in this paper. ILL has a contraction rule and an
introduction rule !I for the exponential; in ILLP, instead of a
contraction rule, multiple occurrences of labels for assumptions are
permitted under certain conditions; moreover, there is a different
introduction rule for the exponential, !I+, which is closer in spirit
to the necessitation rule for the normalizable version of S4 discussed
by Prawitz in his monograph ``Natural Deduction''.

It is relatively easy to adapt Prawitz's treatment of natural
deduction for intuitionistic logic to ILLP; in particular one can
formulate a notion of strong validity (as in Prawitz's ``Ideas and
Results in Proof Theory'') permitting a proof of strong normalization.

The conversion rules for ILL explicitly mentioned in the paper by
Benton et. al. do not suffice for normal forms with subformula
property, but we can show that this can be remedied by addition of a
single conversion rule.

ILLP also suggests the study of a class of categorical models, more
special than the class introduced by Benton et. al.


The paper just mentioned can be obtained by anonymous ftp to
vera.fwi.uva.nl, login name: anonymous, password ident.  The paper,
and two others (sse below) are contianed in the file pub/illc/astro


The directory "astro" contains files of papers by A.S.Troelstra.

Description of the contents:

1. The file nat.ps is the postscript file of the paper "Natural
deduction for intuitionistic linear logic", report ML-93-09 of The
Institute for Logic.  Language and Computation of the University of
Amsterdam (ILLC). The paper is 28 pages.

2. The file lincorr.ps contains corrections to the book "Lectures on
linear logic" by A.S. Troelstra and will be updated if necessary. The
list of errata is three pages long.

3. The file linbib.bib is a bibtex file and contains a bibliography of
linear logic compiled by H.A.J.M. Schellinx and A.S. Troelstra; the
file is regularly updated.  Corrections and additions for the
bibliography to anne@fwi.uva.nl or harold@fwi.uva.nl are always
welcome.


				A. S. Troelstra