Consistency Proofs and Representable Functions. Part I

摘要

The paper lays a basis for studies of incompleteness phenomena manifest in analogues, within axiomatic theories, of known mathematical structures like the group of number theoretic permutations and the Boolean Algebra of subsets of the natural numbers. It establishes the basic facts about functions strongly represented by recursively enumerable formulas of number theory which are consequences of the usual constructive consistency proofs for arithmetic. To do this a pair of new normal form theorems for proofs in arithmetic are established by transfinite induction over the ordinals less than epsilon sub o. As consequences of these theorems, the usual statements of consistency are obtained, including Kreisel's no-counterexample interpretation by recursive functionals of finite type. (Author)