FOM: a world where all definable reals are recursive

[Andrej.Bauer@cs.cmu.edu]

Thanks for your reply. The fact that we're talking about a forcing
construction makes the idea much clearer to me. If I am not mistaken,
a forcing construction can be viewed as a Kripke presheaf model (which
is intuitionistic), followed by a filter quotient which turns the
Kripke model into a classical one.

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. The poset in question are the Medvedev degrees,
right? Hmmm, now I should go back to your paper and try reading it
again.

I think I can clarify this:

Stephen G Simpson <simpson at math.psu.edu> writes:
> Wait a minute.  There is something I don't understand about this.
> Bauer says that *all* reals are present in this particular PER model.
> In particular, the real H which encodes the Halting Problem is
> present.  Right?  But, in the kind of classical situations that I am
> used to, H is *definable* in any omega-model that contains it.  (In
> fact, by the MRDP theorem, H is definable in terms of solvability of a
> Diophantine equation with a parameter.)  So my model definitely
> *cannot* contain H.  I don't understand how this PER model can contain
> H yet satisfy ``all definable reals are computable''.
> 
> Perhaps I am overlooking some basic point about what is meant by
> ``definable in a PER model''.  Is it very different from what we
> normally mean by definability in classical models?

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.

For the purposes of this discussion we can replace reals with infinite
sequences of 0's and 1's. Let H(n) be the predicate on natural numbers
that says "the n-th Turing machine terminates". This can be defined
easily as a suitable existential statement in terms of the Kleene's
predicates U and T.

We cannot define the sequence h : N --> {0,1} by

          /
          |  0    if H(n)
  h(n) = <
          |  1    if not H(n)
          \

because it is NOT provable intuitionistically that

  "forall n. (H(n) or not H(n))"

In other words, the predicate H(n) is not decidable. So we can't
really define the function h in an intuitionistic model because we
can't prove it's total. So, in the PER model I described, h is there
but it's not definable. Does that make sense?


Andrej Bauer

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