Discontinuities of Provably Correct Operators on the Provably Recursive Real Numbers
Collins, William J. ; Young, Paul
J. Symbolic Logic, Tome 48 (1983) no. 1, p. 913-920 / Harvested from Project Euclid
In this paper we continue, from [2], the development of provably recursive analysis, that is, the study of real numbers defined by programs which can be proven to be correct in some fixed axiom system $\mathbf{S}$. In particular we develop the provable analogue of an effective operator on the set $\mathscr{C}$ of recursive real numbers, namely, a provably correct operator on the set $\mathscr{P}$ of provably recursive real numbers. In Theorems 1 and 2 we exhibit a provably correct operator on $\mathscr{P}$ which is discontinuous at 0; we thus disprove the analogue of the Ceitin-Moschovakis theorem of recursive analysis, which states that every effective operator on $\mathscr{C}$ is (effectively) continuous. Our final theorems show, however, that no provably correct operator on $\mathscr{P}$ can be proven (in $\mathbf{S}$) to be discontinuous.
Publié le : 1983-12-14
Classification: 
@article{1183741402,
     author = {Collins, William J. and Young, Paul},
     title = {Discontinuities of Provably Correct Operators on the Provably Recursive Real Numbers},
     journal = {J. Symbolic Logic},
     volume = {48},
     number = {1},
     year = {1983},
     pages = { 913-920},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183741402}
}
Collins, William J.; Young, Paul. Discontinuities of Provably Correct Operators on the Provably Recursive Real Numbers. J. Symbolic Logic, Tome 48 (1983) no. 1, pp.  913-920. http://gdmltest.u-ga.fr/item/1183741402/