Grigori Mints

	    Reductions of finite and infinite proofs


Standard expansion of a finite proof d in arithmetic into an infinite
proof h(d) provides normalization theorems for finite proofs of simple
formulas, usually of complexity at most \Sigma_1. A slight
modification of this expansion allows to normalize finite proofs of
arbitrary formulas, even if the normal form contains eigenvariables.

This approach extends to subsystems of analysis. 

It can be used to extract a set of reductions for finite proofs from
cut-elimination for infinite proofs.