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