Realization of Analysis into Explicit Mathematics
Tupailo, Sergei
J. Symbolic Logic, Tome 66 (2001) no. 1, p. 1848-1864 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
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.
Publié le : 2001-12-14
Classification:  
@article{1183746630,
     author = {Tupailo, Sergei},
     title = {Realization of Analysis into Explicit Mathematics},
     journal = {J. Symbolic Logic},
     volume = {66},
     number = {1},
     year = {2001},
     pages = { 1848-1864},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183746630}
}

Tupailo, Sergei. Realization of Analysis into Explicit Mathematics. J. Symbolic Logic, Tome 66 (2001) no. 1, pp.  1848-1864. http://gdmltest.u-ga.fr/item/1183746630/