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"? 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? 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 Regards, Bill Page. _______________________________________________ Axiom-developer mailing list [email protected] http://lists.nongnu.org/mailman/listinfo/axiom-developer
