FOM: a world where all definable reals are recursive

[Stephen G Simpson]

Andrej Bauer (FOM, 13 April 2000) writes:

 > So if we're going to look for a connection with intuitionistic
 > models, we should look at the Kripke model, *before* we collapse it
 > into a classical model.

Yes, that seems exactly right.

 > The poset in question are the Medvedev degrees, right? 

The poset that I use is set of nonempty Pi^0_1 subsets of 2^omega,
ordered by inclusion.  To carry out my forcing argument, I use the
fact that the Medvedev complete part of this poset has a strong
homogeneity property: any two Pi^0_1 sets in it are recursively
homeomorphic.

 > To say that some point p in a PER model is definable is to say that
 > there exists a formula P(x), whose only free variable is x, such that
 > it is provable (intuitionistically) that
 > 
 >         "there exists exactly one x such that P(x)"
 > 
 > and, when we interpret P(x) in the PER model, P(p) is valid.

OK, that clears up the discrepency.  You are talking about what I
would call ``definability in a theory'' (the intuitionistic theory in
which ``there exists exactly one x such that P(x)'' is provable), but
I have been talking about ``definability in a model''.  To say that a
point p of a model M is definable in M is to say that there exists a
formula P(x) whose only free variable is x, such that M satisfies
``there exists exactly one x such that P(x)'', and M satisfies P(p).
This kind of definability is purely model-theoretic and has nothing to
do with provability.  In this sense of definability, the Halting
Problem is definable in any omega-model which contains it.  (An
omega-model is a model where the integers are standard.)

My result is that there is an omega-model M of WKL_0 such that for all
reals x and y in M, if x is definable in M using y as a parameter,
then x is Turing reducible to y, i.e., computable from y.  

The fact that M is an omega-model of WKL_0 implies that M contains
lots of non-computable reals.  The definability property of M implies
that M does not contain the real which encodes the Halting Problem.
I hope this makes sense to you.

-- Steve