Re: [isabelle] 1/0 = 0?



The advantage of defining x/0 = 0 is that it allows a number of common identities to be used without side conditions. One example (of many) is x/z + y/z = (x+y)/z.

It seems to me you are too focused on programming. You do not throw exceptions in mathematics, and division does not exist in the world outside. If you do want to reason about programming (including exceptions), then you need to formalise the semantics of your language, but that is separate from the formalisation of mathematics itself.

As I mentioned in my previous message, there are a number of formalisms that allow you to reason about things being defined. But they never catch on because they are tiresome to use. Generally they force you to show things to be defined (and if you have a large expression, that means every single subexpression). Proving theorems is difficult, which is why we try to avoid introducing additional complications.

Larry Paulson



> On 4 Mar 2018, at 15:56, Andreas Röhler <andreas.roehler at easy-emacs.de> wrote:
> 
> 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.