Gabriel Dos Reis wrote:
>
> Bill Page <bill.p...@newsynthesis.org> 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.
> How much of Real Analysis do you have to redefine?
If you mean Analysis in informal sense then basicaly nothing. If
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
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. 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).
--
Waldek Hebisch
hebi...@math.uni.wroc.pl
------------------------------------------------------------------------------
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
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
