Re:Splitting and cut elimination

At 12:21 +1000 5.10.04, Rajeev.Gore-FCV4sgi5zeUQrrorzV6ljw@xxxxxxxxxxxxxxxx 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