[Prev][Next][Index][Thread]
PAPER ABSTRACT
NEW LINEAR LOGIC PROOF THEORY AND SEMANTIC -part I-
Giorgia Ricci and Aldo Ursini
Dipartimento di Matematica
Universita' di Siena
via del Capitano 15
53100 SIENA-Italy-
phone (577)288240
fax (577)270582
e-mail URSINI@SIVAX.CINECA.IT
extended abstract
Submitted for the Ninth Annual IEEE Symposium on
LOGIC IN COMPUTER SCIENCE
July 4-7 ,1994,Paris,France
We propose a different presentation of linear logic, which
is half-way between sequent calculus and natural deduction.
Our "sequents" have at most one formula at the right side.
This allows a quick and prompt proof of cut-elimination.
Moreover,an interesting geometry -or semantic- of linear
proofs is then at hand, and for full linear logic.
Of course there are connections with proof nets, but
we need no boxes...A proof of completeness, namely an
abstract characterization of the graphs involved will
be delayed for another occasion.
Introduction.
The title is ambiguous, and we wanted it to be so: here
there is no "new linear logic", rather it is old dear linear
logic (see GIRARD [1]) in disguise. However in future
papers with the same title, somethimg new may arise there too.
Also, we mean to deal here with proof theory of linear logic
and with geometry of proofs therein. Namely, with a
"proofnets-like" semantic of linear proofs. Hence, semantic
referes here to this. But, in subsequent papers, something new
on "truth" semantic, namely phase semantic, is likely to
appear...
Because the requirements of this Symposium on originality,
copyrights, et cetera are so stringent, we decided to be vague,
if such a behaviuor is allowed. Here we base ourselves on the
historical fact that: in Germany it is prohibited whatever
is not explicitely allowed, in China it is prohibited whatever is
explicitely allowed, in Italy it is allowed whatever is
explicitely prohibited, BUT in England it is allowed whatever
is not explicitely prohibited.
1.LINEAR LOGIC IN DISGUISE.
Let us take seriously the recurrent suggections by GIRARD about
linear logic -shortly:LL- being apt for dealing with symmetric
input-output relations . Hence formulas are really (physical)
forms of plugs, a sequent is provable iff plugs in it fit well
together, et cetera.
In trying to make explicit this approach from the beginning of the
deductive system, we are driven towards the following syntax.
Let A,B,... denote formulas of (propositional) LL as in [1][;
let S,S',T,... denote multisets, or finite sequences up to order,
of formulas.
A SEQUENT in LL* is a pair (S,S') such that S' has lenght
at most 1. Notation:
S ====> S'
Notation for sequents of LL will be :
|- S
In case A,B,C,...F are formulas, we also write:
A,B,C,...====> F
or else
A,B,C,... ====>
which will create the main question, namely: What the hell
is the comma here ? We will address this question subsequently.
RULES OF LL*
axiom NOT A ====> A
S====>A S'====> NOT A
cut _________________________
S,S' ====>
S====>A
plus ____________________
S====> A PLUS B
S====>A S====>B
with ________________________
S====> A WITH B
S , B ====> A
par ________________________
S ====> A PAR B
S====>A S'====>B
tensor ________________________
S,S'====> A TENSOR B
S , T ====> T'
cross Provided T,T' are short : _____________________
S , T' ====> T
one _____________
====> ONE
all _____________
S ====> ALL
S ====>
bottom _____________
S ====> BOTTOM
S ====> S====>A
interrogation _________ ___________
S====>?A S====>?A
S,?A ====> ?A
_____________
S,?A====>
?S ====> A
exclamation ______________
?S ====> !A
(of course, why not S means empty if S empty, and means
of course A,of course B,... if S is A,B,... )
Proposition 1.
There are translations from proofs in LL into proofs in LL*
and viceversa, such that:
i.given a proof of S====>S' in LL*, the translation is
a proof of |- S,S' in LL;
ii.given a proof of |-A,B,C,... in LL, the translation is
a proof of A,B,C,...====> in LL*.
Moreover, the translation does not introduce new cuts:
a cut is present in the translated proof in LL* iff
a cut were present in the source proof in LL.
LL* admits an Hauptsatz, based on the following
Lemma.Given a proof of S====>S' (in LL*) whose last rule
be a cut of degree d ( greater than 0 ) , and the
degree of the proofs of both premisses is lower than d,
one can construct a proof of the same SEQUENT of degree
lower then d.
The proof of this is remarkably neat and straight.
Remark also that - of course via proposition 1 - you get
cut elimination for LL....in a neat and straight way.
2 . GEOMETRY OF PROOFS.
We have to consider certain unoriented labeled finite
graphs ,also called ULKs ,in each of which a certain
finite multiset of (labeled) vertices, called the
FRONTIER, is singled out.
Labels will be formulas of LL, and hence the frontier
of an ulk is a finite multiset of formulas,modulo
some trivial bureaucracy.
Ulks , and their frontiers, are defined inductively
by following the inductive notion of proof in LL*.
The following is the definition, and a double line
means in it: a new link.
ULK FRONTIER
A ====== NOT A { A, NOT A}
If
G is an ulk with frontier S U {A,B}
then the following is an ulk:
with frontier S U {A PAR B }.(Here U is multi-union of
multisets).
If
G and F are ulks with frontiers S U {A} and
S' U {B},
then the following is an ulk :
with frontier S U S' U { A TENSOR B } ,
Etc,Etc. Let us get into details for the villain of
the situation, namely WITH.
The GLUEING of two ulks, relative to a multiset S,is a
purely graph theoretic matter, and is defined separately
below.(The idea is that you have that S is "common"to
both, that they are written on two transparencies,so
that S's formula occurrencies appear at the same spots,
and that formula occurrences different from S's and
the relevant links are in red for one ulk,and in blue
for the other one: then you superimpose one on the other
and you get their glueing -rel. to S-)
Then we define:
If
G,F are ulks with frontiers S U {A},S U {B}
then : first get the glueing of G and F relative to S,
thus getting a graph G.F,whose frontier be S'; secondly
is, by definition, an ulk, with frontier S' U {A WITH B}.
Another tough guy is weakening ( on ? ). But observe that
-by an easy induction- the frontier of an ulk is never empty
(even the cut is not goig to annihilate a frontier....).
Hence we define :
If
G is an ulk with frontier S
then ,choose an entry X in S, and the following
is an ulk, with frontier S U {?X}.
The other induction steps corresponding to dereliction,
contraction and the rule (!) are obvious.
Then we get
Proposition 2.If G is an ulk with frontier S , then
there is a proof in LL* of S ====> .Moreover, the
translation of this proof is -modulo some redtape-
exactly G .
Obviously, one has to pay attention to the separation
of glued ulks, if one wants to recover the components of the
glueing. That is why we postpone the investigation of
a characterization (Correctness Criteria) of which graphs
are possibly ulks.
REFERENCE
[1] J-Y.Girard, Linear Logic, Theoretical Conmputer Science,
50,1987.
A P P E N D I X.
This appendix is dedicated to the definition of glueing
of two ulks,relative to S; but this is left to the reader.
END OF THE EXTENDED ABSTRACT
Dear LINEAR customer,
in the condensed form of the extended abstract of the paper:
"New Linear Logic Semantic and Proof Theory,I"
which was in the e-mail box a couple of days ago, the pictures- in the
definition of ULK's- where not present.The careful reader may easily
rebuild them, or otherwise please ask me for a hard copy of the
abstract.
Happy New Year,
Aldo Ursini
Aldo Ursini
Universita' di Siena
Dipartimento di Matematica
Via del Capitano 15
53100 Siena - Italy
ph: 577-286244
fax: 577-270581
email: ursini@sivax.cineca.it