*To*: Andreas Röhler <andreas.roehler at easy-emacs.de>*Subject*: Re: [isabelle] 1/0 = 0?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sun, 4 Mar 2018 13:10:51 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <5c514b09-675a-5dd9-a92b-76c8bd4ec173@easy-emacs.de>*References*: <FE8B48D2-568C-4BCD-913A-13CE201F05D0@data61.csiro.au> <CAHm1DC5LFGbFxCmKf_oR0zu4vAnZDS4ktO8_ZtWONd00kt+f1A@mail.gmail.com> <6182f742-35b4-e2df-c775-42038973e6f3@in.tum.de> <5c514b09-675a-5dd9-a92b-76c8bd4ec173@easy-emacs.de>

Formal systems reveal hidden assumptions. So one might say “1/x is always nonzero", which is certainly true, and we can be more precise and say “1/x is nonzero for all real x", when we may become uneasy that the quantification includes zero. When you formalise that statement in predicate logic, with the usual axioms about the real numbers, it ends up being equivalent to "1/0 is nonzero". And as there are no partial functions in classical predicate logic, any model must give 1/0 some value or other. Then the statement could be true or false. If you formalise this statement in Isabelle/HOL, it turns out to be false because 1/0 = 0. Similar statements will be false in quite a few other formal systems, in many cases because 1/x cannot be shown to be well-defined. There is a formalism known as free logic that deals explicitly in the concept of a defined value, where 1/0 = 0 is false because 1/0 is undefined, and therefore we can prove 1/0 ≠ 0. But that may not look very natural either. Larry Paulson > On 4 Mar 2018, at 09:49, Andreas Röhler <andreas.roehler at easy-emacs.de> wrote: > > that makes me some headache. IMHO the freedom of model making is limited. The task is to represent reality. We know what happens when the quotient goes towards zero. From there don't see any reason why to assume zero as result. This looks like a false positive and might make results unreliable. There should be better ways to deal with.

**Follow-Ups**:**Re: [isabelle] 1/0 = 0?***From:*Andreas Röhler

**References**:**Re: [isabelle] 1/0 = 0?***From:*Manfred Kerber

**Re: [isabelle] 1/0 = 0?***From:*Tobias Nipkow

**Re: [isabelle] 1/0 = 0?***From:*Andreas Röhler

- Previous by Date: Re: [isabelle] 1/0 = 0?
- Next by Date: Re: [isabelle] 1/0 = 0?
- Previous by Thread: Re: [isabelle] 1/0 = 0?
- Next by Thread: Re: [isabelle] 1/0 = 0?
- Cl-isabelle-users March 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list