Waldek Hebisch <[email protected]> writes:
| Gabriel Dos Reis wrote:
| >
| > Bill Page <[email protected]> writes:
| >
| > [...]
| >
| > | >=A0However defining 'x/0' does not
| > | > really change properties of field: normal field axioms only
| > | > say what happens when you divide by nonzero element.
| > |=20
| > | 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=?
|
| A little nitpick: precise traditional definition of such function
| is 'exp(-1/x^2) for x ~= 0, 0 for x = 0'. This definition does
| not depend on what happens with '1/x' at x = 0.
The operational keyword is *discontinue*.
If you make 1/0 = 0 then, by definition, the function
x +-> exp(-1/x^2)
is defined everywhere, including at 0 where it takes the value 1, not 0.
And that definition is just as precise as it can get.
| > How much of Real Analysis do you have to redefine?
|
| If you mean Analysis in informal sense then basicaly nothing. If
I mean the body of knowledge accumulated under the heading of
Real Analysis.
| you mean some set of theorems encoded in mechanically checkable
| formal language, then the problem is essentially of translation
| between closely related formal languages: practice has shown
| that seemingly trival differences may cause trouble. OTOH
I'm not just looking at the practice -- because I don't want to equate
"unfamiliar" with "wrong". As a scholar, I want to look at the
logical consequences.
| apparently at least one such set of theorems (that of Isablelle/HOL)
| already uses this convention, so you will have to "patch"
| existing theorems when you want different convention.
|
| > 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=20
| > *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.
| >
|
| As I wrote in another message: there is no _logical_ problem
| with 1/0 being 0.
I don't think I ever suggested there is a fundamental logical problem
with 1/0 - 0. However, what I do suggest is that I've not yet seen a
single logical framework that contains all the "conventions" (that make
some proofs go through nicely, even if they are not conventional)
in a single place that handles Real Analysis. I've seen bits and pieces.
| Pragmatics of theorem prover make it
| quite reasonable (but prover based on partial functions and
| leaving 1/0 udefined looks quite reasonable too). Pragmatics
| of CAS differs very much form pragmatics of theorem prover
| and for CAS getting error on 1/0 is much better. But if
| somebody wants to swap computations between CAS and
| theorem prover using '1/0 = 0' convention, than having
| this convention also in CAS starts looking reasonable
| (reasonable enough to implement special domain with such
| behaviour).
------------------------------------------------------------------------------
Forrester Wave Report - Recovery time is now measured in hours and minutes
not days. Key insights are discussed in the 2010 Forrester Wave Report as
part of an in-depth evaluation of disaster recovery service providers.
Forrester found the best-in-class provider in terms of services and vision.
Read this report now! http://p.sf.net/sfu/ibm-webcastpromo
_______________________________________________
open-axiom-devel mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
