Re:Splitting and cut elimination

At 12:21 +1000 5.10.04, [email protected] wrote:

>  > *** Definition A deductive system is *Kai-esque* if every inference
>>  rule, apart from identity and cut, is such that all its instances in
>>  which an atom is substituted by a generic structure are derivable in
>>  the same system.
>
>At first glance this reminds me of Belnap's condition C6/7:
>  each rule is closed under simultaneous substitution of arbitrary
>  structures for congruent parameters.
>
>But perhaps your requirement that the new rule be derivable is
>stronger?

I tried checking the condition on 
Anderson-Belnap's `Entailment'. I think you're 
correct, that derivability makes for a stronger 
condition, but am not sure because C6/7 are by 
far too complicated for my understanding 
possibilities.

Anyway, take KS and the case for atomic contraction. The rule is

        [a,a]
    ac_ ----- .
          a

When you substitute R it becomes

    [R,R]
    ----- ,
      R

which does not belong to KS. However, this rule 
(which is just contraction) is derivable for 
medial and atomic contraction, which are in the 
system.

The point is that derivability is a `local' 
condition, which only depends on the system and 
not on derivations, so it's easily checkable.


At 11:03 +0200 5.10.04, Kai Brünnler wrote:

>>*** Definition   A deductive system is 
>>*Kai-esque* if every inference rule, apart from 
>>identity and cut, is such that all its 
>>instances in which an atom is substituted by a 
>>generic structure are derivable in the same 
>>system.
>
>Have mercy! Please use "substitution-invariant" or something like that.

OK, I think it's a nice name. Belnap uses 
`closure under substitution'. It would be nice if 
you could choose an official name for your 
technique, something that we can use in a slogan 
like

    cut elimination = substitution invariance + splitting ,

for example. We can then replace `splitting' by 
the names of the properties it entails.

>To straighten the record: contrary to the 
>impression one might get from Alessio's email, 
>splitting (for BV) precedes my cut elimination 
>proof. Splitting (the proof, not necessarily the 
>context) is what I see as the crucial ingredient 
>in my proof.

Nice argument, so we have to thank flour if 
spaghetti are such a great invention.

>  So please stop spattering my name all over the place.

I wasn't spattering, rather I was reverently 
typing it. I would do it in Engravers LH Bold 
Face if I only could.



>The induction rule is not substitution-invariant.

Can you elaborate? How comes?? I mean, once one is careful with variables...

-Alessio