[FOM] 618: Adventures in Formalization 4

[Rob Arthan]

> 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.