Thomas Strahm

     Recent results in metapredicative proof theory


Metapredicativity is a new general term in proof theory
which describes the analysis and study of formal systems whose
proof-theoretic strength is beyond the Feferman-Schuette
ordinal Gamma-0 but which are nevertheless amenable 
to predicative methods. 

In this talk we give a general survey and introduction to 
metapredicativity. In particular, we discuss various examples
of metapredicative systems, including (i) subsystems of
second order arithmetic, (ii) first and second order fixed 
point theories, (iii) extensions of Kripke-Platek set 
theory without foundation, and (iv) systems of explicit 
mathematics with universes.

Relevant keywords for our talk are: arithmetical transfinite 
recursion and dependent choice; restricted bar induction;
transfinite hierarchies of fixed points; transfinite fixed
point recursion; hyper inaccessibility, Mahloness and
Pi-3 reflection without foundation; universe operators.