Re: [isabelle] 1/0 = 0?



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.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.