Realization of analysis into Explicit Mathematics
From MaRDI portal
Recommendations
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
- Encoding true second‐order arithmetic in the real‐algebraic structure of models of intuitionistic elementary analysis
- Functional interpretations. From the Dialectica interpretation to interpretations of classical and constructive set theory
- Realisability in weak systems of explicit mathematics
- Systems of explicit mathematics with non-constructive -operator. II
Cites work
Cited in
(7)- Characterizing the interpretation of set theory in Martin-Löf type theory
- Theories of Frege structure equivalent to Feferman's system \(\mathsf{T}_0\)
- On the strength of the interpretation method
- A new model construction by making a detour via intuitionistic theories. I: Operational set theory without choice is \(\Pi_1\)-equivalent to KP
- A direct computational interpretation of second-order arithmetic via update recursion
- Realization of constructive set theory into explicit mathematics: A lower bound for impredicative Mahlo universe
- Encoding true second‐order arithmetic in the real‐algebraic structure of models of intuitionistic elementary analysis
This page was built for publication: Realization of analysis into Explicit Mathematics
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4328839)
