[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.