Re: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory)

[Gabriel Dos Reis]

"Page, Bill" <address@hidden> 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