FOM: a world where all definable reals are recursive

[Andrej.Bauer@cs.cmu.edu]

Stephen G Simpson <simpson at math.psu.edu> writes:

> Namely, I obtain an omega-model of WKL0 satistying this scheme:
> 
>       For all reals X and Y, if X is definable from Y, 
>       then X is Turing reducible to Y.
>

This sounds very interesting. Unfortunately I had a hard time
understanding the paper--it's a bit too remote from what I do. I would
love to hear any comments on how your results relate to approaches
taken in theoretical computer science and intuitionistic logic, where
the models also have the property that whenever x is definable from y,
then x is computable from y.

To be a little bit more specific, in the PER models (PER = partial
equivalence relation) we start with a partial combinatory algebra, say
the graph model P(omega), find a computable subalgebra, say the r.e.
graph model RE of r.e. sets, and then build the category of PERs on
P(omega), where we require that the morphisms be realized by elements
of RE. In other words, we allow arbitrary pers on P(omega) to be
objects, but only computable morphisms between them. This way we get
lots of classical spaces (for example, the Euclidean real numbers are
a subspace of P(omega) equipped with the Scott topology). The logic is
intuitionistic, and many theorems from (intuitionistic) analysis are
valid (all the reals are still there). Nevertheless, the models can
still be understood as "constructive" since all the functions are
computable.

Do these ideas have anything to do with Stephen Simpson's work? Can
his model be viewed as an intuitionistic model somehow, or is it
"genuinely" classical?


Andrej Bauer
Graduate student in Pure and Applied Logic
School of Computer Science
Carnegie Mellon University
http://andrej.com