[FOM] 618: Adventures in Formalization 4

[Rob Arthan]

> On 17 Sep 2015, at 07:36, Dominic Mulligan <dominic.p.mulligan at googlemail.com> wrote:
> 
> Dear Harvey,
> 
> Many in the theorem proving community would be likewise disgusted with a definition of division that admitted equations like 1/0=0, or ..., and in HOL based systems like Isabelle, HOL4 and HOL Light division is left undefined in that case.
> 
> 

Sorry to disappoint, but in all of those systems (at least for real operands) x/y is defined to be xy^{-1} and 0^{-1} is defined to be 0. The main justification is that decision procedures are really important in these systems and taking 0^{-1} = 0 is the easiest way to make the first order theory of the reals with division included in the signature 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).

Regards,

Rob
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150918/b92bc0d0/attachment.html>