Re: Anyone coded Zermelo-Fraenkel axioms in scheme?

On Aug 15, 8:02 am, "narutocan...@xxxxxxxxx" <narutocan...@xxxxxxxxx>
wrote:
On Aug 15, 5:40 am, Pascal Bourguignon <p...@xxxxxxxxxxxxxxxxx> wrote:



"narutocan...@xxxxxxxxx" <narutocan...@xxxxxxxxx> writes:
Anyone coded Zermelo-Fraenkel axioms in scheme?
I can only go as far as axiom 3, I am stumped by axiom 4.
;; 1. Empty Set: There exists an empty set. (ok, I have
it) (list)
;; 2. Extensionality: If two sets have the same members then they're
equal. (set-cmp? = x y) (I just need "=" from someone)
;; 3. Pairing: For all sets x,y there exists a set
{x,y}. (list x y) (this one is easy)
;; 4. Union: For all sets x, there exists a set equal to the union of
all sets in x.

Anyone know what does it mean "all sets in x", does it mean (powerset
x) ?

What are we speaking about?

1. Empty Set.

Ok, we have a SET that is named "empty".

2. If two sets have the same members then they're equal.

SETs have MEMBERs. (the members must be comparable, "same" or not).
SETs can be compared, "equal" or not.

3. x is a SET and y is a SET ==> {x,y} is a SET.

Yay! We can build new SETs beside the empty set!.

{empty,empty}
{empty,{empty,empty}}
{empty,{empty,{empty,empty}}}
{empty,{empty,{empty,{empty,empty}}}}
{{empty,{empty,empty}},{empty,{empty,{empty,empty}}}}
...

Notice how the only way to build new sets beside the empty set is to
make sets that contains other sets. So the members mentionned in
point 3 so far can be only other sets.

4. Union: For all sets x, there exists a set equal to the union of all sets in x.

Here we get a new procedure to build new sets. "sets in x" must refer to
the members of x mentionned in axiom 2.

For example, if x = {empty,{empty,empty}} then all the sets in x are
- empty, and
- {empty,empty}.
That's all.

So now, we can build a new set: (union empty {empty,empty})
and of course:

(union empty {empty,{empty,empty}})
(union empty {empty,{empty,{empty,empty}}})
(union {empty,{empty,empty}} {empty,{empty,{empty,empty}}})
...
and also:
(union {empty,{empty,{empty,empty}}}
(union {empty,{empty,empty}}
{empty,{empty,{empty,empty}}}))
...

Now we would like to know what elements
are in (union empty {empty,{empty,empty}}).

Formally, these four axioms are not really precise. For example, we
don't know what it means for to sets to have the same members.

Do {empty} and {empty,empty} have the same members?

Depending on the definition of "having the same members", we could
have normal sets or multi-sets or perhaps even stranger things...

But if we define it as we usually do, that is:

The sets A and B "have the same members"
<=> (for all x in A, x is in B) and (for all x in B, x is in A)

then we can see that {empty} "have the same members" {empty,empty}
since
empty is in {empty,empty}
and
empty is in {empty} and
empty is in {empty}.

Therefore {empty} "equal" {empty,empty}.

And going from here, we can demonstrate that

(union empty {empty,{empty,empty}}) "equal" {empty,{empty}}.

ok, I better list the entire axioms first:
* Empty Set: There exists an empty set.
* Extensionality: If two sets have the same members then they're
equal.
* Pairing: For all sets x,y there exists a set {x,y}.
* Union: For all sets x, there exists a set equal to the union of
all sets in x.
* Existence of Infinite Sets: There exists a set x that contains
the empty set and that contains y union {y} for every y in x.
* Power Set: For all sets x there exists a set consisting of the
subsets of x.
* Replacement (for every function A): For all sets x, there exists
a set {A(y) | y in x}.
* Foundation: All nonempty sets x have a member y such that for
all z, either z not in x or z not in y. (This is a technical axiom,
whose point is to rule out sets like {{{{...}}}}.)

(define (make-set contains? for-each map) ...)
;; axiom 2
(define (same-set? x y)
(call/ec (lambda (return)
(for-each (lambda (e)
(if (not (contains? e y)) (return #f))
x)
#t))
)
;; axiom 3
(define (pair x y) (list x y))
;; axiom 4
(define (union x y) (append x y))
;; axiom 5
(define (infinite-set x) (map (lambda (e) (union empty-set e (list
e))) x))
;; axiom 6
(define this-is-just-map map)

actually, this is "axiom 7". "axiom 6" powerset is boring.


Now when I really think hard about this system, nearly all the
required functions has to come from "the user" of this system.
Why do they call it an axiom system, it's more like "throwing the
questions back at you system" or "perfectly reflective system".
Interestingly, the more I code in scheme, the more my functions look
like rhetorical system.



--
__Pascal Bourguignon__ http://www.informatimago.com/

NOTE: The most fundamental particles in this product are held
together by a "gluing" force about which little is currently known
and whose adhesive power can therefore not be permanently
guaranteed.


.

Relevant Pages