chapter  7
Cut Elimination Resumed
Pages 2

O bserve, however, that this construction still requires that sufficiently many unused new variables be available, in order to choose the new eigenvariable <re(z). They are available since my derivations are finite and so w ill use only finitely many variables. A generalization of the theorem to the case of infinite derivations H w ill, therefore, be possible only under additional hypotheses, ensuring the availability of unused variables.