axiom-developer
[Top][All Lists]

## Re: FW: data structure vs. mathematical structure (was: [Axiom-developer

 From: Gabriel Dos Reis Subject: Re: FW: data structure vs. mathematical structure (was: [Axiom-developer] Graph theory) Date: 15 Nov 2006 02:26:28 +0100

```"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

```