Bill Page <[email protected]> writes: [...]
| > However defining 'x/0' does not | > really change properties of field: normal field axioms only | > say what happens when you divide by nonzero element. | | If the inverse of 0 is 0 then the domain should not even be a Group | let alone a Field. I am not sure that is the real issue. The real problem is if you take that axiom, what parts of the usual classical theorems remain true and to what extent? Anybody wants to make the function x +-> exp(-1/x^2) discontinue at x=0? How much of Real Analysis do you have to redefine? The notion that "it is done in Isabelle/HOL therefore it must be right" has to be tempered with the fact that Isabelle/HOL is a *logical framework* in which one develops logics. What is often left under-appreciated is that there are -many- logics used to prove this and that theorem, but we don't have yet a coherent set of logics to handle all that has been accomplished in computational mathematics. Of course, if you are into Calculemus, you already know this. -- Gaby -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To post to this group, send email to [email protected]. To unsubscribe from this group, send email to [email protected]. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en.
