[FOM] 618: Adventures in Formalization 4

[Anthony Coulter]

Joe Shipman 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).

Harvey Friedman replied:
 > 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.

And I reply:
     I would be very surprised if this turns out to be correct. To 
reinterpret our working definition of a polynomial-time-computable real 
number, we're essentially saying that we can approximate it to an 
accuracy of epsilon in f(epsilon) steps, where
f(epsilon) is of order O(-log(epsilon)).
     What we keep forgetting is that the first-order theory of the reals 
includes more than just addition and multiplication; it also includes 
equality and inequalities. Being able to approximate a number to any 
precision in a small number of steps does *not* translate into the 
ability to tell whether that number equals zero exactly (or is positive, 
or negative) just as efficiently. Likewise, given two such numbers 
(again represented by computer programs which approximate them to an 
epsilon of your choice) you cannot efficiently determine whether they 
converge to the same limit and are thus exactly equal. A decidable 
theory of computable numbers can thus have neither equalities nor 
inequalities in it (though you need inequalities to define your 
approximations, or equivalently your "shrinking sequence of intervals"); 
such a theory would end up having no predicates at all.

Regards,
Anthony