ABSTRACT
Calculi for classical logic were introduced as LK and as IvK0, K K 2 . L -se quents are special cases of M -sequents, and the structural and logical rules of LK are special cases of the corresponding rules of M K ; in particular, (AIN) is a special case of (AI). There remains the rule (K 0) which, even in the generalized form
. w = * v,N = > v,N ^ 0 } M =4 v 9N
is adm issible in MK since
M = > w ,v,N w,M = $ v,N
and since JE-i , applied to a derivation D M of (K 0' ) ?s right prem iss, produ ces a derivation of M = $ w ,v ,N not longer than D M . Defining the degree of classicality ccdg(D) of an LK -derivation D to be 2 plus the maximum of all | w | for formulas w in instances of (K 0), I so obtain the
LEMMA 3 Every LK -derivation D can be transformed into an M K C -derivation C of the same endsequent w ith length{C) < length (D ) and cdg(C) = ccdg(D ) , hence also into a M K -deriva tion M (D) whose length is bounded exponentially in length {D ) and ccdg{D) by Theorem 1 .
