FOM: a world where all definable reals are recursive
Stephen G Simpson
simpson at math.psu.edu
Thu Apr 13 17:16:33 EDT 2000
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
> 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.
More information about the FOM