Re: Splitting, cut elimination and classical logic

Hi,

answers to Kai and Lutz:


At 23:32 +0200 5.10.04, Kai Brünnler wrote:

> > > The induction rule is not substitution-invariant.
> >
> > Can you elaborate? How comes?? I mean, once one is careful with variables...
>
> Your definition talks about atoms and thus 
> treats the two occurrences of the propositional 
> variable a in [a,a] as being the same but in 
> [a,-a] as different. This makes perfect sense, 
> for otherwise either contraction would not be 
> substitution invariant (which it should be) or 
> identity would be substitution invariant (which 
> it shouldn't be).
>
> Now, induction, here on an atomic formula, is something like this:
>
> (a0, forall x [-ax,asx])
> --------------------------  .
>     forall x ax
>
> It's clearly not substitution invariant 
> according to your definition, just as cut and 
> identity aren't. This has nothing to do with 
> variables, terms or the like but just with the 
> fact that a occurs positively and negatively: 
> the exact same problem also occurs in 
> propositional temporal logics.
>
> It seems easy to avoid breaking the induction 
> rule: when substituting for a, then simply also 
> substitute for -a. However, that's no solution: 
> once you break an identity above by substituting 
> for -a then how do you fix it?

Well, I would say that induction *is* 
substitution invariant, exactly as identity and 
cut are: of course you substitute a and -a at the 
same time, and, as you say, this doesn't break 
the rule.

That said, I see your point: doing this breaks 
the cut-elimination procedure. We have then to 
revise the criterion for ensuring that this 
doesn't happen. What about:

*** Definition   A deductive system is *Kai-cool* 
if all rules, at the exception of identity and 
cut, are substitution invariant and such that the 
same atom meta-variables don't appear positively 
and negatively at the same time.

Is this enough to validate the slogan

   cut elimination = Kai-coolness + splitting ?

(In case this notion is OK we can look for a more 
professional and less cool name, otherwise better 
waiting until we have the right one.)


At 20:17 +0200 7.10.04, Lutz Strassburger wrote:

> On Tue, 5 Oct 2004, Alessio Guglielmi wrote:
>
> >  Speaking of which: there wasn't much time to discuss because Lutz had
> >  to leave, so perhaps we can do so on the list. Lutz has a splitting
> >  proof for classical logic, but for a different system than KS (no
> >  medial, in particular). I don't think this solves the problem as I
> >  stated it, because if we have to look for general criteria, we
> >  probably want to deal with medial, since this rule pops up so often,
> >  also in completely unrelated systems and in different shapes, like
> >  unary versions for classical logic. But let's discuss the pros and
>  > cons.
>
> Sorry, your mail was too long. I did not get what you mean by
>
>   "the problem as I stated it"

For me two things are most important: 1) a good 
bound on the complexity of proofs and 2) a 
technique that is as independent as possible of 
classical logic.

The reason for 2 is that, since medial appears 
everywhere, including logics with different units 
than classical logic, an independent technique is 
most likely to give us hints for general criteria 
which ensure cut elimination.

In addition, I'd like to see one more, admittedly 
vague thing in the normalisation procedure, 
namely a possible understanding as transformation 
of deductive proof nets, whatever they will be. 
The reason for this is actually using splitting 
as one of the properties to require during the 
design of deductive proof nets.

I also always check whether formalism A would 
deal graciously with a given transformation, 
since I consider A the first step towards 
deductive proof nets.

I certainly didn't grasp your technique well 
enough, but, as a first impression, the use of a 
super rule looked to me particularly difficult to 
digest in a proof net setting (and probably also 
in formalism A). I might be wrong on this, of 
course, and I certainly wasn't happy with the way 
my `proof' was dealing with this problem, too. 
What I ask for might also be an impossible 
requirement, by the way, and in this case I'd 
like to understand why.

> I know that for proving my splitting I deliberately avoid medial, but as a
> corollary you get splitting for KS in a very strong way. You also get it
> for the system {ai_, s, m}, which means that there is no additional
> weakening or contraction. My method of putting medial into some super-rule
> realizes exactly the idea that Elaine tried to explain after Roy found the
> bug in your proof.
> Of course, since splitting holds for {ai_, s, m}, there might also be a
> direct proof, without using the super-rule, but it is most like going
> to be quite messy.

Are you sure that what you're doing is correct? 
The fact that you get splitting for {ai_, s, m} 
looks very suspicious to me. Consider P = [a,c], 
Q = [b,-a], R = [-c,-b] (see a splitting 
statement below) and the proof

                t
          ai_ ------
              [b,-b]
      ai_ ---------------
          [([a,-a],b),-b]
        s ---------------
           [(a,b),-a,-b]
   ai_ ----------------------
       [(a,b),([c,-c],-a),-b]
     s ----------------------
        [(a,b),(c,-a),-c,-b]
     m ---------------------- .
       [([a,c],[b,-a]),-c,-b]

I don't see how you can get rid of a and -a in 
the `split' proofs, without weakening.

Ciao,

-Alessio



*** Theorem (Shallow Splitting)    In KS, for every P, Q, R and for every proof

       _
       |
   [(P,Q),R]

there exist U, V and derivations such that

               _             _
   [U,V]       |             |
     |   ,     |     and     |   .
     R       [P,U]         [Q,V]