Reflective closures of formal systems
Thomas Strahm
University of Bern
Switzerland
Abstract
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.