Waldek Hebisch <hebi...@math.uni.wroc.pl> writes:
| 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.
And you are entitled to your belief :-)
And clearly there are at least as many interests as mathematicians.
As a trained differential geometer using formal systems to "algebraize"
topological and differential concepts, I am interested in the consequences
of the various formal axioms. For example, if I take a system that
tries to formalize (as an algebraic construction) the notion of limit [1]
and come to some formal rules where I can do lim(f/g) = lim(f)/lim(g),
it is not obvious a priori that the axiom 1/0 = 0 is entirely
inconsequential. One might wish it is inconsequential, but that is only
a wish or a belief and we hope our computation algebra systems do not
engage in wishful thinking.
[1] Michael Beeson and Freek Wiedij
"The meaning of infinity in calculus and computer algebra systems"
http://dx.doi.org/10.1016/j.jsc.2004.12.002
|
| Coming back to 'exp(-1/x^2)': with '1/0 = 0' this function
| formally is discontinuous. Informal reaction is that
Formal computer systems do not have "informal reactions".
If that expression is buried deep in some intermediary computation that
a human does not readily have access to, it is unlikely that one would
"informal" react in a timely manner to assess whether that formal or
informal continuity would affect the rest of the computation or not.
| 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.
and I think I asked
# what parts of the usual classical theorems remain true and to what
# extent?
| > | 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.
Notice that I am not talking about notation conventions, but definitional
conventions. I do not know how you measure "popular conventions", but I
would go with the conventions in Bourbaki adaquately amended by
Geddes et al, as a start.
| 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.
I have the odacity to believe that the definitional conventions by
Bourbaki is more that just "macros in programming languages" 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).
absolutely.
| And doing Real Analysis really means doing all mathematics.
I would not go as far as saying "all mathematics".
Bourbaki left a good part of geometry from its treatment of Real Analysis.
| 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.
we all agree; getting there, however, is distinctly non-trivial.
Our conventional practice of mathematics is highly ambiguous -- it
always amazes me that we manage to get through.
I learnt quite a few things from an experiment conducted with
colleagues: mechanization of the operational semantics of some advanced
object oriented programming language features. I learnt quite a few
things from that experiment
http://parasol.tamu.edu/~gdr/C++/layout/popl11.pdf
http://gallium.inria.fr/~tramanan/cpp/object-layout/
* Technologies available in modern PA/ATP systems are quite
advanced -- compared to the bad press they occasionaly get.
But we have a long way to go.
* Proof intended for machines is no proof intended for humans. :-)
| 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.
Sure.
------------------------------------------------------------------------------
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
