We define a novel interpretation R of second order arithmetic into Explicit Mathematics. As a difference from standard D-interpretation, which was used before and was shown to interpret only subsystems proof-theoretically weaker than T 0 , our interpretation can reach the full strength of T 0 . The R-interpretation is an adaptation of Kleene's recursive realizability, and is applicable only to intuitionistic theories.

This paper deals with universes in explicit mathematics. After introducing some basic definitions, the limit axiom and possible ordering principles for universes are discussed. Later, we turn to least universes, strictness and name induction. Special emphasis is put on theories for explicit mathematics with universes which are proof-theoretically equivalent to Feferman's.

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.

In this paper we discuss extensions of Feferman's theory T 0 for explicit mathematics by the so-called limit and Mahlo axioms and present a novel approach to constructing natural recursion-theoretic models for systems of explicit mathematics which is based on nonmonotone inductive definitions.

We define a realizability interpretation of Aczel's Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of T 0 , thus providing relative lower bounds for the proof-theoretic strength of the latter.

We give an overview of recent results in ordinal analysis. Therefore, we discuss the different frameworks used in mathematical proof-theory, namely "subsystem of analysis" including "reverse mathematics", "Kripke-Platek set theory", "explicit mathematics", "theories of inductive definitions", "constructive set theory", and "Martin-Löf's type theory".