Abstract

For any extension $T$ of $I\Sigma_{1}$ having a cut-elimination property extending that of $I\Sigma_{1}$ , the number of different proofs that can be obtained by cut elimination from a single $T$ -proof cannot be bound by a function which is provably total in $T$.