[Prev][Next][Index][Thread]
paper announcement
The following paper is available as LC-pnets.ps or LC-pnets.dvi
by anonymous ftp from
theory.doc.ic.ac.uk in the directory /theory/papers/Bellin
================================================================
Proof-nets for LC, with an appendix on GL.
Gianluigi Bellin
Equipe de Logique, Universite' de Paris VII
Abstract
In the paper [1991] J-Y.Girard proposed the new system LC
for classical logic. Well-known features of LC are:
a new sequent calculus, with a mixed (classical and linear)
consequence relation, a translation into linear logic,
a denotational semantics and a refinement of Goedel's double negation
interpretation into intuitionistic logic. The flow of information
in the process of cut-elimination is controlled by a system of
*polarities* assigned to formulas; strong normalization and confluence
are transferred from LJ to LC in a natural way.
In section 1.5. of Girard [1991] the following open problem was indicated:
to find a system which is to LC ``what typed Lambda-calculus is to LJ;
... a kind of proof-net'' was indicated as a possible solution.
Given the sequent calculus LC and its interpretation in the sequent calculus
LL for linear logic, it is not too difficult to transfer the formalism of
proof-nets *with additive and exponential boxes* from LL to LC.
It is less obvious to determine whether we can express the restrictions
on the linear part of LC-sequents by conditions on the proof-structure
without using *promotion boxes*: i.e., can we ``remove the exponential boxes''
in this particular class of proof-nets?
We give here our contribution. We show that a formalism without exponential
boxes (*quasi-nets*) identifies ``too many'' sequent derivation.
It turns out that for a proper definition of proof-nets it is enough to use
*promotion boxes* in the case of links with a *negative* premise and
*positive* conclusion (including the negative premise of a n-cut).
These are the situations where the flow of information changes;
in the corresponding inferences of the sequent calculus sequents
without privileged occurrence are required.
(Remember also that positive formulas can be defined as
P =: 1 | 0 | p | P\otimes P | P\oplus P | \exists P | !N
where p stands for atoms.)
With such a device the proofs of correctness of the representation become
remarkably simple (almost trivial -- as it should be).
It should be added that several other `constructivizations' of classical logic
are available, e.g., M.Parigot's system of Free Deduction (FD) [Parigot 1991]
where strong normalization and confluence for classical logic
are guaranteed simply by introducing additional parameters on formulas
to determine the flow of information in the process of cut-elimination.
A study of all possible embeddings of Gentzen's sequent calculus LK
directly into LL-proof-nets is done in a separate work by V.Danos, J-B.Joinet
and H.Schellinx. It would seem that after all, the choice of a formalism
for classical logic should depend essentially on its use in applications.
In the appendix we sketch the formalization of a fragment of Peano arithmetic
in LC, namely the modal logic GL for Goedel's Provability predicate.
Gentzen systems for GL presented non-trivial problems a decade ago,
particularly in the context of natural deduction. Some of these problems
vanish when GL is formulated in LC-proof-nets or in Free Deduction.
References:
J-Y.Girard [1991] A new constructive logic: classical logic, MSCS, 1.3., 1991
M.Parigot [1991] Free Deduction: an analysis of `computations' in classical
logic, Russian Conference on Logic Programming, St.Petersburgh 1991
On Gentzen-style systems for GL, see works by Avron, Bellin, Leivant,
Sambin and Valentini referred to in the paper.