*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] 1/0 = 0?*From*: Andreas Röhler <andreas.roehler at easy-emacs.de>*Date*: Sun, 4 Mar 2018 16:56:41 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <15C336B3-B507-46B0-BFB9-33BA0A69A8A9@cam.ac.uk>*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> <15C336B3-B507-46B0-BFB9-33BA0A69A8A9@cam.ac.uk>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:52.0) Gecko/20100101 Thunderbird/52.6.0

Hi Lawrence, thanks for your kind response. That matter seems worth digging in further and probably more fundamental.

Best, Andreas Röhler On 04.03.2018 14:10, Lawrence Paulson wrote:

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 PaulsonOn 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:*Lawrence Paulson

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

**Re: [isabelle] 1/0 = 0?***From:*Lawrence Paulson

- 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