Re: Splitting, cut elimination and classical logic

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

This reminds me of Belnap's conditions C4:

C4: Congruent parameters are either all antecedent ("negative") or all
    succedent ("positive") parts of their respective sequents. 

This forbids a positive and negative occurrence of a formula if they
fall into the same congruence class (are ancestors of the original cut
formula in the instance of cut we are trying to eliminate).

Raj