In this paper, we prove the wellfoundedness of recursive notation systems for reflecting ordinals up to Π₃-reflection by relevant inductive definitions.

The \-substitution method is a technique for giving consistency proofs for theories of arithmetic. We use this technique to give a proof of the consistency of the impredicative theory \ using a variant of the cut-elimination formalism introduced by Mints.

This paper deals with a proof theory for a theory T3 of Π3-reflecting ordinals using the system O of ordinal diagrams in Arai 1375). This is a sequel to the previous one 1) in which a theory for recursively Mahlo ordinals is analyzed proof-theoretically.

We formulate epsilon substitution method for a theory [Π0 1, Π0 1]-FIX for two steps non-monotonic Π0 1 inductive definitions. Then we give a termination proof of the H-processes based on Ackermann [1].

In this paper we introduce a notation system for the infinitary derivations occurring in the ordinal analysis of KP + Π₃-Reflection due to Michael Rathjen. This allows a finitary ordinal analysis of KP + Π₃-Reflection. The method used is an extension of techniques developed by Wilfried Buchholz, namely operator controlled notation systems for RS∞-derivations. Similarly to Buchholz we obtain a characterisation of the provably recursive functions of KP + Π₃-Reflection as <-recursive functions where < is the ordering on Rathjen's ordinal (...) notation system J(K). Further we show a conservation result for $\Pi _{2}^{0}$-sentences. (shrink)

This paper is intended to give for a general mathematical audience a survey of intriguing connections between analytic combinatorics and logic. We define the ordinals below ε0 in non-logical terms and we survey a selection of recent results about the analytic combinatorics of these ordinals. Using a versatile and flexible compression technique we give applications to phase transitions for independence results, Hilbert’s basis theorem, local number theory, Ramsey theory, Hydra games, and Goodstein sequences. We discuss briefly universality and renormalization issues (...) in this context. Finally, we indicate how regularity properties of ordinal count functions can be used to prove logical limit laws. (shrink)

The technique of using infinitary rules in an ordinal analysis has been one of the most productive developments in ordinal analysis. Unfortunately, one of the most advanced variants, the Buchholz Ωμ rule, does not apply to systems much stronger than -comprehension. In this paper, we propose a new extension of the Ω rule using game-theoretic quantifiers. We apply this to a system of inductive definitions with at least the strength of a recursively inaccessible ordinal.