Realization of Analysis into Explicit Mathematics
Abstract
We define a novel interpretation $\mathscr{R}$ of second order arithmetic into Explicit Mathematics. As a difference from standard $\mathscr{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 $\mathscr{R}$-interpretation is an adaptation of Kleene's recursive realizability, and is applicable only to intuitionistic theories.