Iterated Godelian extensions of theories. The idea of iterating ad infinitum the operation of extending a theory T by adding as a new axiom a Godel sentence for T or equivalently a formalization of "T is consistent", thus obtaining an infinite sequence of theories, arose naturally when Godel's incompleteness theorem first appeared, and occurs today to many non-specialists when they ponder the theorem. In the logical literature this idea has been thoroughly explored through two main approaches. One is that initiated by Turing in his "ordinal logics" (see Gandy and Yates [2001]) and taken very much further in Feferman's work on transfinite progressions, which also introduced the more general study of extensions by reflection principles, of which consistency statements are a special case. This approach starts from an assignment of theories to ordinal notations, and extracts sequences of theories through a suitable choice of a path in the set of ordinal notations. The second approach, illustrated in particular by the work of Schmerl and Beklemishev, starts instead from a suitably well-behaved primitive recursive well-ordering, which is used to define a sequence of theories. This second approach has led to precise results about the relative proof-theoretical strength of sequences of theories obtained by iterating different reflection principles. The Turing-Feferman approach, on the other hand, lends itself well to an investigation in qualitative and philosophical terms of the relevance of such iterated reflection extensions to mathematical knowledge, in particular because of two developments associated with this approach. First, there is Feferman's famous completeness theorem for transfinite progressions based on full (uniform) reflection, which exercises a powerful appeal on the imagination, but which (perhaps because of the somewhat inaccessible character of Feferman [1962b]) is not widely known in any detail. Second, there is the concept of the autonomous part of a progression, introduced by Kreisel and Feferman, which allows us to reason in qualitative terms about what it is we do know, potentially at least, on the basis of iterated reflection principles.
展开▼
