Bill Page <bill.p...@newsynthesis.org> 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 ------------------------------------------------------------------------------ Xperia(TM) PLAY It's a major breakthrough. An authentic gaming smartphone on the nation's most reliable network. And it wants your games. http://p.sf.net/sfu/verizon-sfdev _______________________________________________ open-axiom-devel mailing list open-axiom-devel@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
