Reflective closures of formal systems

Thomas Strahm
University of Bern


The foundational program to study the principles of proof and ordinals which are implicit in given concepts was first spelled out by Kreisel. A paradigmatic example in this respect is the analysis of predicativity by Feferman and Schütte in the early sixties, which led to the progression of systems of ramified analysis up the the famous Feferman-Schütte ordinal Gamma_0. Since then various means of extending a formal system by principles which are implicit in its axioms have been proposed and pushed forward by Feferman.

In this talk we survey different notions of reflective closure. This includes the discussion of numerous characterizations of predicativity, the reflective closure of axiom systems by means of a self-applicative truth predicate as well as Feferman's most recent concept of unfolding a schematic formal system. Special emphasis is put on characterizing the reflective closure of specific systems in more familiar proof-theoretic terms.