chapter  1
Cut Elimination with Exchange Operators
Pages 15

The translations between K SP -, K^P-and K uP-deri vat ions remain in effect for the corresponding calculi K P C ; also, they preserve the lengths of the derivations. Thus every cut elim ination operator for one of these calculi K PC gives rise to operators for the others: translate a given D into a deri­ vation G for the particular calculus for which an elim ination operator has been found, transform G into a cut free G*, and then translate G* back into a derivation of the given calculus. Similarly, it w ill suffice to eliminate either sim ple or radical cuts, since the adm issibility of the one kind im plies that of the o th er.