Gabriel Dos Reis wrote:
>
> Waldek Hebisch <hebi...@math.uni.wroc.pl> writes:
>
> | 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.
>
> 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.
>
1) I believe that '1/0 = 0' can be used as part of faithful
formalization of Real Analysis. In fact, if you are
interested in elementary part (meaning no sets, no sequences, ...)
and use logic with total functions than there seem to be
no good alternative.
2) As practicioner of Real Analysis I am not interested in conseqences
of '1/0 = 0' -- as I wrote I believe that they do not affect
important matters (in particular system remains consistent).
Of course you may have different opinion.
Coming back to 'exp(-1/x^2)': with '1/0 = 0' this function
formally is discontinuous. Informal reaction is that
you either have wrong definition or ask wrong question
(note that informally uniteresting question is a kind of
wrong question). The point is that sometimes you do not
care what happens at zero and then '1/0 = 0' "works",
sometimes you care, then one has to do definition via
cases.
> | 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.
I do not think you will find a single logical framework that directly
contains all popular conventins. IMHO various conventions are more
like macros in programing languages: they are created to fit
single problem (or domain) and are too specialised to work in
general. Logical framework may (and probably should) contain
a preprocessor to expand statements into canonical form. One
can imagine predefined "macro files" with conventions for
various domains.
Let me add that IMHO when talking about logical framework for
some part of mathematics like Real Analysis one needs mechanical
checking (people are resonably good at inventing and writing
down proofs, but formal checking is too tedious for them).
And doing Real Analysis really means doing all mathematics.
AFAICS current checking systems are limited. One problem
is that to give short proof one needs large volume of
preexisting knowledge (theorems). Connected problem is
that proofs encoded in procedural systems are hard to
read for even for specialists. Some people seem to believe
that if we keep encoding existing theorems in existing
systems then eventually system will have enough "base
knowledge" to allow writing real research results.
I somewhat doubt this: IMHO proof checking systems
should process mathematics in smarter ways. It seems
that when dealing with logic current systems are
more capable than humans. But humans works at many levels:
pragmatics (what is doable and what is intersting),
procedural, logical. Also, people seems to be better
at searching/recalling relevant existing knowledge.
--
Waldek Hebisch
hebi...@math.uni.wroc.pl
------------------------------------------------------------------------------
Benefiting from Server Virtualization: Beyond Initial Workload
Consolidation -- Increasing the use of server virtualization is a top
priority.Virtualization can reduce costs, simplify management, and improve
application availability and disaster protection. Learn more about boosting
the value of server virtualization. http://p.sf.net/sfu/vmware-sfdev2dev
_______________________________________________
open-axiom-devel mailing list
open-axiom-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/open-axiom-devel
