The well-known incompleteness results of Gödel assert that there is no recursively enumerable set of sentences of formalized first order arithmetic which entails all true statements of that theory. It is equally well known that by introducing sufficiently nonconstructive rules, such as the ω-rule of induction, completeness can be re-established.

Starting from the work of Turing [4] Feferman in [1] developed another method, viz. the study of transfinite recursive progressions of theories, for closing the gap between Gödel (recursively enumerable sets of axioms yield incompleteness) and Tarski (number-theoretic truth is not arithmetically definable).