"Page, Bill" <[EMAIL PROTECTED]> writes: | On November 14, 2006 12:01 AM Gaby wrote: | > | | > | > From constructive mathematics point of view, the only things | > | > that are required for a set are: | > | > | > | > (1) say how to build element of a set | > | > (2) equality test. | > | > | > Bill Page wrote: | > | No, there is a lot more to the mathematics of set than that. | > | It would mean that all sets are finite and that is quite far | > | from the case. | | On Tuesday, November 14, 2006 1:20 PM Gaby wrote: | > | > How do you arrive to that conclusion? | > | | I thought I was stating something obvious. Are you asking why I | think all sets would be finite if the only operation you require | to form sets is the ability to "build an element"?
Why all sets would be finite. I hoenestly don't see how it is obvious. | Ok, maybe there | is also induction so that for example we could define the set of | positive integers (natural numbers) as consisting of the element 1 | and the operation +1 that "builds a new element". So depending on | what else you assume about the "environment", I would have to | withdraw my claim of finiteness. But considering complexity issues | in constructing these numbers we would be better off with at least | one more element forming operation - doubling - leading to binary | representation. | | However it is not clear to me that there always exists the | possibility to define a set by it's elements. For example is this | possible if we wish to define the set of exact real numbers such | as suggested by your reference below? | | > | Rather, sets should be strongly related to types. | > | | > | I think the "constructive mathematics" that is most suitable | > | to Axiom is probably is probably Intuitionist type theory | > | (Martin-Löf). See: | > | > In fact, I prefer the definition given by Erret Bishop. See | > chapters 1 and 2 "his" book | > | > "Constructive Analysis", | > | > Erret Bishop | > Douglas Bridges | > | > From my perspective, it shows a much deeper impact. | > | | When it comes to the concept of exact real numbers I think you | are absolutely right but is not clear to me why you would prefer | this text in the context of set theory and Axiom. Can you explain? I don't think Bishop is dealing with exact realy numbers, as opposed to constructive mathametics -- with analysis as an example. I don't believe Axiom has a clear constructive notion of set theory, so I'm not preferring anything. I'm just ignoring what Axiom does :-) Reflecting my view that the requirement of "hash" is non-mathematical. | Exact reals for Axiom is a subject that we have previously | discussed on this list. See: | | http://wiki.axiom-developer.org/RealNumbers | | Here is a recent article on this subject. | | http://www.cs.ru.nl/~herman/PUBS/exactreals.pdf | | by Herman Geuvers et al. http://www.cs.ru.nl/~herman Thanks, I'll have a deeper look. -- Gaby _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
