Abstract:

Reflection principles are axioms expressing that all sentences (of a given logical complexity) provable in a given theoryTare true. The simplest example of such an axiom is Goedel’s formula expressing the consistency ofT. The idea of using reflection principles and their transfinite iterations to classify arithmetical sentences according to strength is due to A. Turing (1939). However, Turing also realized that there are serious difficulties associated with this approach, in particular, due to the lack of understanding how to distinguish ‘canonical’ from ‘pathological’ ordinal notation systems, now a well-known problem in proof theory. The aim of the talk is to outline the main ingredients of the approach to proof theoretic analysis based on reflection algebras. From an abstract algebraic point of view, these structures are semi-lattices enriched by a family of monotone unary operators satisfying some specific sets of identities. The operators can be interpreted in the lattice of arithmetical theories as functions mapping a theoryTto a theory axiomatized by a reflection principle forT. Within this framework it is possible to define appropriate canonical ordinal notation systems and the associated transfinite hierarchies of reflection principles. Hence, it is also possible, to some extent, to push Turing’s ideas on the classification of arithmetical sentences through.