[FOM] 618: Adventures in Formalization 4

[Harvey Friedman]

I am under the distinct impression that it is not too hard to see that
the polynomial time computable real numbers in the sense you mean form
a real closed field, and hence have the same decidable theory as all
real numbers, or all real algebraic numbers.

Harvey Friedman

On Wed, Sep 23, 2015 at 1:22 PM, Joe Shipman <joeshipman at aol.com> wrote:
> Do the real numbers which are computable in polynomial time (that includes the real algebraic numbers)  also form a field with a decidable first order theory?
>
> ("Polynomial time" means with appropriate provision for decimal expansions ending in 999999.... so that you are considered to have computed the number adequately if you can confine it to the intersection of a shrinking sequence of intervals in a time polynomial in the log of the reciprocal of the width of the smallest interval).
>
> Note that such a field might have strange properties when you try to do calculus on it--definite integrals of polynomial-time-computable functions wouldn't necessarily have values in the field, even though the roots of such functions would be in the field.