Re: Splitting and cut elimination

> *** 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.

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. So please stop spattering my name all 
over the place.


> Checking this condition is trivial and, as far as I know, this holds 
> for all the systems we've designed so far in the calculus of 
> structures (which means tens). In general, there is no reason why a 
> system should not be Kai-esque, because the only reasonable cause for 
> breaking the property is dealing with negation, which is precisely the 
> business of identity and cut, taken care of by the definition.
>
All the systems for which we have cut elimination are 
substitution-invariant, yes. As soon as induction rules enter the 
picture (temporal logics, mu-calculus, and the logic of common knowledge 
which I'm studying) cut elimination generally fails. More precisely, we 
have yet to find out whether there is a way of designing the rules in 
order to make cut admissible. The induction rule is not 
substitution-invariant.


-Kai