FOM: a world where all definable reals are recursive (revised)

[Stephen G Simpson]

This is a revised and expanded version of my posting of April 2, 2000,
on the same subject.

----------

A well known and attractive foundational program is ``computable
analysis'', i.e., the development of mathematics in the computable
world.  However, it is also known that the assumption that all real
numbers are computable conflicts with many basic, well known theorems
of real analysis.  For example, the assumption ``all real numbers are
computable'' is in conflict with the maximum principle for continuous
real-valued functions on a closed bounded interval.

In a new paper that I have written, I attempt to strike a balance
between these conflicting requirements.  I do this by exhibiting a
world where the main theorems of real analysis hold, yet all
*definable* real numbers are computable.

In technical terms, I obtain an omega-model of WKL0 in which all
definable reals are recursive.  It turns out that this result is
orginally due to Friedman (Theorem 1.10 of Friedman 1974,
unpublished).  However, my proof is different from Friedman's, and I
obtain a better result.  

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 contradicts Theorem 1.12 of Friedman 1974, unpublished.
Friedman's proof of this theorem is erroneous.)  Indeed, given a
countable model N of Sigma01-PA, I obtain a model of WKL0 having N as
its first order part, in which (*) holds.  A corollary is that WKL0
plus (*) is conservative over Sigma01-PA.

The scheme (*) is interesting, for the following reason.  Often in
mathematics one has the situation that, under some assumptions on a
real parameter X, there exists a unique real Y having some property
stated in terms of X.  In this kind of situation, (*) allows one to
conclude that Y is Turing reducible to X.

Details of the proof and references are in my paper ``Pi01 Sets and
Models of WKL0'', which is available on-line at

        http://www.math.psu.edu/simpson/papers/

-- Steve