🚀 go-pugleaf

Date: Tue, 15 Sep 1992 11:39:05 -0500
To: linear@cs.stanford.edu

I think that the lack of sequent calculi for quantum logics is no 
accident.  I looked at this pretty seriously about ten years ago,
and also had discussions with Gary Hardegree and Nuel Belnap, but
we all included that it is either impossible or at least needs 
some brand new ideas.  I should mention that I know that there has 
been a recent paper titled "Sequential method in Quantum Logic"
by Hirokazu Nishimura, JSL, 1990, 45, 339-352.  But as he himself
acknowledges this formulation fails to have the cut-elimination
theorem, which was the name of the game for Hardegree, Belnap,
and myself.  He also starts with an axiomatization of orthologic by
Goldblatt, which has a sequent-type look, but it is not really
an orthodox (no pun intended) Gentzen style sequent calculus,
with separate rules for introducing each connective on the left and
the right of the turnstyle.  Goldblatt's system has this for conjunction
(disjunction is defined), but not for negation (it has
on each side which gets in the way o the usual "switching sides"
rules that give both forms of double negation), and furthermore this
system has a primitive postulate for transitivity (in effect cut).

By "orthologic" I mean as usual a lattice with an orthocomplement
of period two satisfying the De Morgan laws and also so that
a & -a is the least element (and so a v -a is the greatest).  While
some people might regard this as a "quantum logic," the usual
quantum logic is an ortho*modular* lattice, by which is meant an
ortholattice that satisfies the orthomodular law.  Defining the
"Sasaki hook" so  a -> b = -a v (a v (a & b)), a good way of
remembering a statement of the orthomodular law (equivalent to
other statements more closely related to the modular law) is
that "modus ponens" holds for the Sasaki hook:

	a & (a -> b) < b

(for reasons of avoiding visual clutter, I use here < for the lattice
"less than or equal)".

It turns out that there seems to be even a problem about a sequent
calculus for orthologic.  The problem is that in order to get double
negation in both forms, one needs (as in Gentzen's system LK for classical
logic) multiple right as well as left hand sides.  But if the commas on the
left are interpreted as conjunction (meet) and those on the left as 
disjunction (join), by some standard fiddling one can get distribution
of & over v out of the cut-elimination theorem.

If one has orthomodular logic, one can interpret say  a, b |- c, d 
as  a ->(b -> (-c ->d)), as I recall (using the Sasaki hook) and avoid
this problem.  One would have rules for & and v as in linear 
logic, or actually more like system of relevance logic (often called 
"lattice R") devised by Robert K. Meyer in his dissertation (Pittsburgh) 
1966, since one needs contraction as well (but not thinning of course)
for the Sasaki hook.  To simplify things I am going to assume here that
the Sasaki hook is defined.  So we need then only to add rules for 
the orthocomplement, which I would think would be the usual "flip" and
"flop":

	G, a |- H	G |- a, H
	__________	__________ .

	G |- -a, H	G, -a |- H

	One needs to worry about being able to prove things like

	a & -a |- b	a |- b v -b.

The idea would seem to be to allow left and right sides to empty out 
using flip or flop, and to allow a restricted form of thinning that
allows one to thin in only when a side is empty.  (Algebraically this
is the same as treating the empty left side as the greatest element 
1 and the empty left side as least element 0,  and requiring them to 
be identities, respectively, under the operations  a o b = -(a -> -b)
and a + b = -a -> b (in linear logic the multiplicative conjunction
and disjunction, in relevance logic the intensional conjunction and
disjunction, sometimes called fusion and fission).

But we still have not taken care of the orthomodular law.  Frankly
I hardly know how to begin on the problems regarding this, and  so
will simply say that "things seem to go the wrong direction."  The
fact that  a & b < b somehow needs to be used to get  a  to distribute
over  -a v (a & b).  My best shot (I am vague on this) was to introduce
besides the usual sequents, also statements that said that pairs (or 
sets?) of propositions were pair-wise commutative (in the technical sense 
that aCb iff a = (a & b) v (a & -b)).  These had there own rules, based
on things like aCa; aCb and aCc imply aC-b, aCb&c, aCbvc; aCb implies bCa;
and there were rules that let them interact, e.g. a |- b implies aCb.  
Note that these all have the usual subformula property.  But I never could
prove a cut elimination theorem (as I recall not even state it).

As a last historical footnote, Ian Hacking, sometime in the middle
to late 1970's, wrote a series of papers developing a "philosophical
criterion" for a logic to be a real logic as opposed to a mere
formalism, or something like that.  He thought that he had a sequenzen
system for quantum logic, which proved it to be a real logic.  Although
he had some neat ideas, there were, as I recall, serious problems and I
do not know how much, if any of this, was actually published.