[Prev][Next][Index][Thread]
report annoucement
We wish to make the following announcement
PROOF NETS FOR INTUITIONISTIC LOGIC I:
ESSSENTIAL NETS
preliminary report
Francois Lamarche
In this paper we develop a theory of proof objects for intuitionistic
logic with the connectors tensor, -o, & and !, that we call *essential
nets*. This allows in particular the interpretation of the simply
typed lamda calculus, with or without product types. We give a
correctness criterion for essential nets: there is an *intrinsic*
property that characterizes the essential nets that come from a proof.
Our methods depend very strongly on the fact that we are dealing with
intuitionistic linear logic (presented in a one-sided sequent fashion
using the Danos-Regnier polarities) and not the full classical
system: notice that all it takes to get full linear logic is the
introduction of linear negation. Some time ago the author realized
that the system described here was very much simpler than the full
one, and this is due to the presence of a *dependence* (or
*causality*) relation between the nodes of a net, that allows
for a simple definition of the empire of the nodes of polarity
Output. We strongly believe that this causality relation is essential
for the extension of this system to ones that contain ``partial
terms'', in other words to systems that allow for the expression of
partial recursive funtions and other related concepts of computer
science.
Let us say briefly what happens to boxes in this
paper. They do not entirely disappear, since some information about
their edges is kept in the net. But this information is incorporated
into the net, in a purely local manner, in the form of special
*links*. For a given &-boxe the information consists in a
string of *additive contraction links*, of arity two. For
!-boxes the information consists in a row of ``boxedge''
links, of arity one.
The paper is available by ftp from theory.doc.ic.ac.uk
in the directory papers/Lamarche