Sergei Tupailo

		Finitary reductions for local predicativity.


There are two main approaches to ordinal analysis of formal theories:
the finitary Gentzen-Takeuti approach on the one side, and the use of
infinitary derivations initiated by Schuette on the other. Up to now
these approaches were thought of as separated and only vaguely
related. But in the paper of 1997 W. Buchholz made an important step
towards undercovering tight connections, which actually exist between
these two different sides of proof theory. Using a concept of
notations for infinitary derivations, a precise explanation of
Gentzen's and Takeuti's reduction steps in terms of cutelimination for
infinitary derivations was given. Even more, the Gentzen-Takeuti
reduction steps and ordinal assignments were actually derived from
infinitary proof theory.

In his paper W. Buchholz wrote:
"Our general idea is that such investigations may perhaps be helpful
for the understanding and unification of two of the most advanced
achievements in contemporary proof theory, namely the methodically
quite different work of T. Arai and M. Rathjen on the ordinal analysis
of very strong subsystems of 2nd order arithmetic and set theory."

We take up this line. A method for treating infinitary derivations
analyzed by Buchholz in his paper, the method of '$\Omega_{\mu+1}$-rule'
introduced by him in 70-s, has certain limitations as far as its
power is concerned (no generalizations of it for theories stronger
than $ID_\mu$ are known). On the contrary, modern ordinal analysis
employs another very powerful tool, the method of 'local
predicativity', originally introduced by W. Pohlers and further
developed by W. Buchholz, G. Jaeger, M. Rathjen and others.  On the
side of finitary proof theory, Gentzen-Takeuti's line has been pushed
very far by T. Arai.

In a series of two talks we will show how translating infinitary proof
theory into the finitary one can be done for the method of local
predicativity. A general summary is that, while, as shown by Buchholz,
Takeuti's reduction steps for $\Pi^1_1-CA$ can be derived from the
method of $\Omega_{\mu+1}$-rule, Arai's reductions are well
approximated by those which we derive from the method of local
predicativity.

Our first lecture will be devoted solely to the infinitary part. We
consider a theory $T_{\Sigma_1}$ of recursively regular ordinals and
its infinitary version $T_{\Sigma_1}^\infty$ and define cutelimination
and collapsing operators for $T_{\Sigma_1}^\infty$, using a general
outline of the method of local predicativity. It should be noted that
our procedure is closed to W. Pohlers' original presentation of the
method, but not to the method of 'operator-controlled derivations'
introduced later by W. Buchholz.

The second lecture will be devoted completely to the finitary part. We
will show how to make Theorems which we will prove in the Part I into
corresponding rules which we will add to the finitary system (most of
them are repetition rules, so prima facie can just be ignored), and in
this manner absolutely formally derive finitary cutelimination
reductions together with corresponding ordinal assignments. Time
permitting, in the end we will say a few words how our method should
be extended to theories of recursively Mahlo and $\Pi^3$-reflecting
ordinals, and possibly up.