[FOM] 618: Adventures in Formalization 4

[Freek Wiedijk]

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?

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

Freek