Re: [isabelle] 1/0 = 0?



Hi Lawrence,

thanks for your kind response.

That matter seems worth digging in further and probably more fundamental.

Why do we care for math and logic? Because we want to solve real problem in the world outside, right? From there (the outer world) I guess some guidance might be derived how the build the model:

Question: Who needs to divide by zero and what does it mean, should that need arrive? May someone point me to such a real case?

Guess a kind of non-normal state is reached when that necessity arrives. I.e. that would mean, we can't go on with true/false or some number. Throwing an exception then must not mean an error --at least being not sure about that--, but trigger special treatment.

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