The Computational Content of Arithmetical Proofs
Stefan Hetzl · Notre Dame Journal of Formal Logic · 2012
For any extension T of IΣ1 having a cut-elimination property extending that of IΣ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.