[Prev][Next][Index][Thread]
proof nets for classical logic
Date: Wed, 11 Dec 91 19:22:55 -0800
Return-Path: <@Sunburn.Stanford.EDU:shankar@csl.sri.com>
------- Blind-Carbon-Copy
To: linear@cs.stanford.edu
Subject: proof nets for classical logic
Date: Wed, 11 Dec 91 19:22:55 -0800
Sender: shankar@krypton.csl.sri.com
A few months ago I was working the problem of proof nets for classical
logic LC. I wrote down the notion of privileged empire (see below),
and set to prove that the relation `Q is in the privileged empire of P'
determines a strict ordering on the privileged formula-occurrences.
It seems that this can now be easily proved using the properties
of Danos' notion of kingdom (and in fact that the results announced first
by Danos are the `right way to go' in this problem). Therefore it seems that
a condition characterizing proof nets for classical logic also follows.
I don't know who else (if anyone) is looking at the problem of nets for LC.
I would certainly appreciate comments by Danos or others who have worked out
the notion of kingdom.
- ----------------------------------------------------------------------------
Work in the language of LC, defined in Girard [1991] (A new constructive logic)
with positive and negative polarities, logical symbols V, F, `and', `or',
`forall', `exists', and with the notion of privileged formulas (written ;P;).
Here privilege implies positivity.
(Use P, Q for positive formulas, M, N for negative, A, B for arbitrary.)
This language has a translation into linear logic and one can
use that translation to define proof structures for LC.
More precisely, one has links
axioms:------- --- -- ------ ;P; -P N -N
-P ;P; ;V; -F -F ;P; p-cut: ------- n-cut: -----
A A ;P; - A ;P; N
contr:--- der:--- weak: A forall:-------- exists:----------- -----------
A P forall A ;exists x.P; ;exists x.N;
;P; ;Q; ;P; N N ;P; ;Pi; A B
and:--------- --------- --------- or:--------- ------ where A or B
;P and Q; ;P and N; ;N and P; ;P0 or P1; A or B is negative
In addition, we have additive boxes, with doors of the form M and N, Gamma,
where a t m o s t o n e occurrence in Gamma is privileged; inside the box,
we have disjoint proof structures R1 and R2 with conclusions
M,Gamma and N,Gamma,
respectively. Proof-structures will also satisfy the restriction that
at most one conclusion is privileged.
These are the only boxes we need, since weakening and forall boxes are
eliminated by standard techniques (see Girard [1991a], Quantifiers in LL, II).
In fact, any set of condition characterizing proof nets for multiplicative
linear logic with quantifiers and weakening (e.g., acyclicity, connectedness,
etc. as in Girard [1991a]) will work, if an e x t r a c o n d i t i o n
can be added corresponding to the restriction in Girard [1991] that in LC
a t m o s t o n e occurrence in a sequent is privileged. Such a restriction
(an implicit !-box) forces classical logic into a `functional' style of
reasoning.
Let R be a proof structure satisfying the conditions for multiplicative
proof nets with quantifiers and weakening inside and outside each additive box.
Define the notion of privileged empire of an occurrence A (write pe(A)) in R
inductively as follows:
(1*) A is in pe(A).
(2*) if X, Y are in an axiom or related in a weakening, and X is in pe(A),
then so is Y.
(3*) if ;X and Y; is in pe(A), then so are X and Y. Same for unary links.
(4*) if X or Y (negative) is in pe(A), then so is any occurrence in a
path connecting A and B under any switching. Similarly for the conclusion
of a contraction.
(**) if ;P; is a premise of an `and', `or', `exists' link, ;P; different
>from A, then the conclusion of the link is in pe(A) [notice that here ;P;
must be privileged.]
Cuts are dealt with in a way similar to (**).
Let P < Q be the ordering on privileged occurrences of R defined by
P is in pe(Q). As the additional condition for proof nets in LC take
(***) for every structure inside each box and for the structure R as a whole,
the privileged conclusion (if any) is maximal w.r.t. <.
The condition makes sense since we can prove the following
LEMMA: If P, Q are privileged and Q is in pe(P), then P is not in pe(Q).
Therefore < is strict.
Proof. Notice that the definition of privileged empire coincides with Danos'
definition of kingdom, except for clause (**). We use the following property
of kingdoms, announced by Danos: for X not= Y, X,Y not connected by axiom link,
if X is in k(Y), then Y is not in k(X).
Suppose that above ;P; there are only unary `or', `exists' links and
the privileged conclusion of an axiom link: then clearly pe(P) does not
propagate beyond the axiom link and ;Q; is in pe(P) iff ;Q; is above ;P;.
Conversely, suppose N is the premise of an `exists' link with conclusion
;exists x.N; and no `and' link occurs below it: then ;exists x.N; is in pe(Q)
iff ;Q; is below N. Hence in both cases the result is trivial.
Now the argument depends on the following
Fact: Let ;Q'; be a conjunction and let Z be the conclusion of a negative
disjunctive link L. If ;Q'; occurs in k(Z) by condition (4*),
then Z is not in pe(Q').
Proof: Since the premises and the conclusion Z of L are not privileged,
Z could be in pe(Q') only by an application of conditions (3*) or
(4*) in the definition of privileged empire.
By our assumption, both premises of L are reached from ;Q';, and (3*) would
yield another independent path from ;Q': to Z, contradicting acyclicity.
If on the other hand Z is a part of the connection between the premises of
another negative disjunction link L' with conclusion Z' which is in pe(Q')
(case 4*), again we contradict acyclicity (change switch at L and L').
Therefore let ;Q; be a conjunction not occurring above ;P; , fix a switch S1
and suppose ;Q; is reached from ;P; through PATH1 containing n applications
of clause (**) in the inductive definition of privileged empire.
This is possible, since clearly pe(P) is a subset of e(P), the usual empire.
If n=0, then ;Q; is in k(P) and we may assume that ;Q; is in the connection
between the premises of some negative disjunctive link with conclusion Z,
where Z is in k(P) (clause 4*).
Now ;P; cannot be in pe(Q), since by acyclicity the connection between ;Q;
and ;P; must pass through Z, and Z is not in pe(Q).
Suppose n>0, say that clause (**) is applied at the indicated links
P ... ;X1; Y1 ;Xn; Yn
PATH1: ----------- ... ----------- ...
;X1 and Y1; ;Xn and Yn; ;Q;
where the intermediate steps of the computation are in fact steps in
the computation of kingdoms. In other words, we may assume that each
;Xi and Yi; is not in the kingdom of any occurrence preceding in PATH1.
If n = 1 and ;Q; is precisely ;X1 and Y1;, notice that P is not in pe(Y1).
Indeed ;X1; is already connected to P , and a switch choosing between the
two paths would occur at a negative disjunctive link with conclusion Z,
where Z is in k(P). This would force ;X1 and Y1; in k(P), contrary to our
choice.
The cases when ;Q; is in k(;Xn and Yn;) for n>=1 are treated in a similar way
(using the Fact or contradicting the choice of ;Xn and Yn;) []
To sequentialize proof nets for LC, show that in the crucial case when
every conclusion is a conjunction, the privileged one (if any) will work.
Suppose the privileged ;X and Y; is such that e(X) and e(Y) have doors C and D,
which are premises of an `or' or `contraction' link, and occur above a
non-privileged conclusion U and V . Then ;X and Y; belongs to the path
connecting C and D, which belongs to the k i n g d o m of U and V,
contradicting condition (***) []
- --------------------------------------------------------------------------
------- End of Blind-Carbon-Copy