[FOM] 618: Adventures in Formalization 4

[Joe Shipman]

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.

-- JS

Sent from my iPhone

> On Sep 23, 2015, at 6:47 AM, Rob Arthan <rda at lemma-one.com> wrote:
> 
> 
>> On 18 Sep 2015, at 17:21, Freek Wiedijk <freek at cs.ru.nl> wrote:
>> 
>> Rob:
>> 
>>> taking 0^{-1} = 0 is the easiest way to make the first
>>> order theory of the reals with division included in the
>>> signature decidable.
>> 
>> Note that this won't work if you're a constructivist in the
>> style of Bishop, as that way division won't be continuous
>> (and aren't all computable functions continuous)?  However,
>> I guess that even in Bishop's mathematics the theory you
>> mention still is decidable?
> 
> A constructivist ought to be be quite happy with
> the first order of the reals except for the name:
> it’s the first order theory of the real algebraic numbers
> and the real algebraic numbers form a computable field
> with a decidable first order theory.
> 
>> 
>>> Model theorists adopt the same convention when they want
>>> substructures of fields to be subfields (e.g., see Hodges:
>>> Model Theory Appendix A.5).
>> 
>> My PhD advisor (very long ago :-)) Jan Bergstra has
>> a theory of "meadows", which in my understanding are
>> fields with the equation 1/0 = 0 added.  See for example
>> <arxiv.org/pdf/0901.0823>.
> 
> It looks like Bergstra, Hirshfeld and Tucker also want their
> meadows to be closed under products, so they add an inverse
> operator satisfying x(xx^{-1}) = (x^{-1})^{-1} =x, but not
> xx^{-1} = 1.
> 
> Regards,
> 
> Rob.
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom