Finitary Reductions for Local Predicativity, I: Recursively Regular Ordinals
Sergei Tupailo · Cambridge University Press eBooks · 2017
We define notation system for infinitary derivations arising from cutelimination for a theory T 1 \\Sigma of recursively regular ordinals by the method of local predicativity. Using these notations, we derive finitary cutelimination steps together with corresponding ordinal assignments. Introduction There is an extensive literature connecting infinitary "Schutte-style" and finitary "Gentzen-Takeuti-style" sides of proof theory. For example, in papers [Mi75, Mi75a, Mi79, Bu91, Bu97a] this was done for systems not exceeding in strength Peano Arithmetic. But most recently, there has been an interest to what one can get on the side of finitary proof theory from the methods which are used for proof-theoretical analysis of impredicative theories (see [Wei96, Bu97]). Especially we want to mention paper [Bu97], where it was shown that Takeuti's reduction steps for \\Pi 1 1 \\Gamma CA+ BI [Tak87, x27] can be derived from Buchholz' method of\\Omega +1 -rule ([BFPS, Ch. IV--V], [BS88]). Here we ...