[FOM] What are sets?

[Zuhair Abdul Ghafoor Al-Johar]

Dear FOMers.

The following reflect the same idea of my previous post, but using units
instead of atoms. The number of primitives is reduced to two binary
relations only.

Language: FOL + Primitive binary relations: "is a part of" denoted by p
and "is collected by" denoted by @.

Axiom: (for all x. x p y -> x p z) -> y p z

Axiom: x p y & y p z -> x p z

Define (=): x=y <-> x p y & y p x

Define (pp): x pp y <-> x p y & ~ y p x

Axiom: x @ y & z p x -> z @ y

Define (unit): unit(x) <-> (exist c. for all y. y @ c <-> y p x) &
(~ exist c,z. z pp x & for all y. y @ c <-> y p z)

Axiom: unit(x) & unit(y) & ~ x=y -> ~ exist z. z p x & z p y

A particle is a proper part of a unit.

Define (collection): collection(x) <->
(for all y. y p x -> exist c,z. z p y & z p c & unit(c) & c p x)

Define (e): x e y <-> unit(x) & x p y & collection(y)

e is read as: is a trivial member of.

Axiom schema: if phi is a formula in which x is not free, then
(exist z. unit(z)phi -> (exist x. for all y. y e x <-> unit(y)phi)) is an axiom.

Define [|]: y=[x|phi] <-> collection(y)&(for all x. x e y <-> unit(x)phi)

Define (precollector): precollector(x) <-> exist y. y @ x

Define (collector): collector(x) <-> unit(x) & exist y. y @ x

A proper precollector is a precollector that is not a unit.

A class is a collection of collectors where distinct collectors do collect
distinct collections.

Define (class): class(x) <-> collection(x) &(for all y. y e x -> collector(y)) & 
(for all y,z. y e x & z e x & ~ y=z -> exist u,w. u=[k| k @ y] & w=[k| k @ z] & ~ u=w)

For every collector x the collection [y| y @ x] is called
the *extension* of x, and x is its *exclusive* collector.
When this extension is a class, it's called
a *class extension* of x.

A set is a class extension of a collector.

An Ur-element is a unit that is not a collector, which is an extension of
a collector.

Epsilon membership is defined as:

x epsilon y <->  class(y) & exist z. collector(z) & x=[u| u @ z] & z e y.

This explains those terms in standard set\class theories.

However in set theories it is sufficient to interpret sets as collectors
and epsilon membership as "is a unit collected by the collector".

Zuhair Al-Johar