FOM: a world where all definable reals are recursive

[Stephen G Simpson]

Andrej Bauer (FOM, 11 Apr 2000) commented on my result that there is
an omega-model satisfying WKL0 plus ``for all reals X and Y, if X is
definable from Y, then X is computable from Y''.

Bauer:

 > 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.

and

 > Can his model be viewed as an intuitionistic model somehow, or is
 > it "genuinely" classical?

Well, my model is of course genuinely classical, in the sense that it
satisfies classical logic.  But it is a *generic* model, obtained from
a certain forcing construction.  And there is a sense (I'm sure Bauer
understands this better than I do) in which any forcing construction
can be viewed as a kind of Kripke model for intuitionistic logic, with
classical models being obtained by specialization to particular
generic filters.  So there is certainly some relationship between my
model and an intuitionistic model.

By the way, another possible connection is that my paper mentions
Medvedev degrees.  The original theorem of Medvedev (see Rogers,
section 13.7) is that the Medvedev degrees form a Heyting algebra, and
the identities which hold there are just the theorems of
intuitionistic propositional calculus.

Beyond that, I don't have a more specific answer to Bauer's question.
Let's try to persuade Harvey Friedman to comment on this.  Harvey
knows a huge amount about models of intuitionism, while I know very
little about them.

To my mind, the interesting thing about my model is that it *contains*
lots of non-computable reals (even though none of them are *definable*
there).  Indeed, by the Reverse Mathematics of WKL0, my model contains
just enough non-computable reals to secure the truth of many theorems
of classical analysis that are false intuitionistically and
constructivistically (because they are contradicted by the assumption
that all reals are computable).

One could compare my model to the set-theoretic model L[G], where L is
G"odel's model of set theory, the constructible universe, and G is a
Cohen-generic real.  In this model of ZFC, there are plenty of
non-constructible reals (G is one of them), but all *definable* reals
are constructible.

Bauer goes on to discuss a particular class of intuitionistic models:

 > To be a little bit more specific, in the PER models [....]  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.

Wait a minute.  There is something I don't understand about this.
Bauer says this particular PER model contains *all* reals.  In
particular, it contains the real H which encodes the Halting Problem.
Right?  But, in the kind of classical situations that I am familiar
with, 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.)  In particular, my model of
``all definable reals are computable'' definitely *cannot* contain H.
So I don't understand how Bauer's 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?

-- Steve