We show that true first-order arithmetic is interpretable over the real-algebraic structure of models of intuitionistic analysis built upon a certain class of complete Heyting algebras. From this the undecidability of the structures follows. We also show that Scott's model is equivalent to true second-order arithmetic. In the appendix we argue that undecidability on the language of ordered rings follows from intuitionistically plausible properties of the real numbers.
@article{1183746167,
author = {Erdelyi-Szabo, Miklos},
title = {Undecidability of the Real-Algebraic Structure of Models of Intuitionistic Elementary Analysis},
journal = {J. Symbolic Logic},
volume = {65},
number = {1},
year = {2000},
pages = { 1014-1030},
language = {en},
url = {http://dml.mathdoc.fr/item/1183746167}
}
Erdelyi-Szabo, Miklos. Undecidability of the Real-Algebraic Structure of Models of Intuitionistic Elementary Analysis. J. Symbolic Logic, Tome 65 (2000) no. 1, pp. 1014-1030. http://gdmltest.u-ga.fr/item/1183746167/