FOM: a world where all definable reals are recursive

[Stephen G Simpson]

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 (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 another result of Friedman.)  Indeed, given a
countable model N of Sigma01-PA, I obtain a model of WKL0 having N as
its first order part, in which the above scheme holds.  A corollary is
that WKL0 plus the above scheme is conservative over Sigma01-PA.

Details are in my paper ``Pi01 Sets and Models of WKL0'' at

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

-- Steve