Transfinite recursive progressions of axiomatic theories

Abstract

The theories considered here are based on the classical functional calculus (possibly of higher order) together with a set A of non-logical axioms; they are also assumed to contain classical first-order number theory. In foundational investigations it is customary to further restrict attention to the case that A is recursive, or at least recursively enumerable (an equivalent restriction, by [1]). For such axiomatic theories we have the well-known incompleteness phenomena discovered by Godei [6]. Quite far removed from such theories are those based on non-constructive sets of axioms, for example the set of all true sentences of first-order number theory. According to Tarski's theorem, there is not even an arithmetically definable set of axioms A which will give the same result (cf. [18] for exposition).