Logic seminar

Proof-theoretic analysis of some impredicative theories

In the field of ordinal analysis there is an important boundary between theories of predicative strength and essentially stronger impredicative theories. Calculation of proof-theoretic ordinals of impredicative theories requires considerably more advanced technique. This talk will be about relatively weak impredicative theories: theories of positive inductive definitions, Kripke-Platek set theory, and system of second-order arithmetic Pi^1_1-CA_0.  The key feature exhibiting by ordinal notation systems for this theories (in contrast with ordinal notations for predicative theories) is that they use larger ordinals to denote smaller ordinals. In the present talk I will discuss this ordinal notation systems and outline the method of proof-theoretic analysis of this systems based on operator-controlled derivation.