I don't intend to treat set theory anything like fully. The
notion set

is a refinement on the naïve notion collection

:
the aim is to put enough constraints on what may be a set

that certain
definitions can make sense and not lead to paradoxes. My main requirements of
the notion set

are that: the collection of natural numbers is a set; the
ordinals one obtains from this notion of set

have certain structural
properties that resemble those of the natural numbers; the collection of these
ordinals is *not* a set. The notion finite

, which yields the
natural numbers as its ordinals

, satisfies the last two but not the first
of these.

So identify some properties of the notion finite

which imply that
its ordinals

, the natural numbers, are they way they are: these are the
properties we'll be calling on when we prove that the ordinals have the
structural properties they do have.

- all sets are collections
or, at least, all the ones that interest us are – namely the ordinals. The important aspect of this is that a set can be

characterized by its elements

– equality of two sets S, R means simply that, for every value x,x in S

exactly ifx in R

. This is simply the notion of equality induced from that for relations by the definition of collections as sub-relations of equality.I'll try to see what appropriate notions can generalize this – e.g. a relation, r, is finite if (r:x←x:) is finite and (| r :{x}) is finite for each x in (:r|). With mappings, the second of these constraints becomes trivial – since (|r:{x}) = {r(x)}. Indeed, I think the definition of a function is a mapping, f, for which (f:x←x:) is a set – the axiom of replacement effectively asserts that (:x←x:f) is also a set, which seems to mean that, for any mapping f and any set S, (:f:S) is a function and {f(x): x in S} is a set.

- any sub-collection of a set is a set
Hence, in particular, empty is a set: and the intersection of a collection of collections will be a set whenever at least one of the collections intersected is a set.

- the union of a set of sets is a set
But note that unions of certain collections of sets need not yield sets – e.g. the union of the collection of all sets won't be a set, and one of my requirements, above, is that the collection of ordinals (which is its own union) isn't a set. Proving that the collection of finite sets obeys its analogue of this looks like it's going to be an interesting exercise, probably depending on the relationship between the finite collections and the natural numbers.

- the successor of any set is a set
This one deduces from an axiom which asserts that, for any sets A and B one may construct the pair-set {A, B} (which will have only one element if A=B); combined with the above truth about unions, we can now obtain the successor of a set S as unite({S, {S}}), in which {S} = {S, S} is a set, using the pair operation once (with the same element as both parts of the pair), and {S, {S}} is a set of sets using it a second time.

Here's what Z-F becomes in the notation I'm using. This turns (for
instance) the F in F(x,y) is a formula such that for any x, there is a unique
y making F true

into a relation, f, which relates y to x iff F(x,y) is true,
with the uniqueness property given being the assertion f is a mapping

,
and the for any x

clause would appear to suggest that (f:x←x:) is
the universal identity (of the context being discussed, so it's the collection
of all pure sets), but I don't think that's the meaning Z-F intended, so I've
left that out. It should be noted that this transcription may thus be
unfaithful in places: for the
original, see
Wombat for my source, which is probably more faithful to the
original.

- Replacement or Projection
- For any mapping f and any set S, {f(x): x in S} is a set
- Extensionality
- Two sets are equal iff they have the same members
– that is, S=T iff
x in S iff x in T

. - Union
- for any set, S, of sets, unite(S) is also a set.
- Pair-Set
- if S and T are sets, so is {S, T}
- Foundation
- Every set subsumes a set disjoint from itself – i.e. having no members in common with it: this is the empty set.
- Comprehension or Restriction
- any sub-collection of a set is a set. In particular, the intersection of a set with a collection is a set.
- Infinity
- There exists an infinite set – that is, a set N for which {monic (N:|N)} and {mapping (N|:N)} are distinct.
- Power-Set
- If X is a set, then so is the collection of subsets of X.

This is usually to be found in conjunction with Peano's axiom, which I must look up. It says, roughly, that you can build up the naturals by applying successor to empty and to each value successor yields, given what you're feeding it.

An aside, for those who wonder is it useful ?

:
I earn my living making computers more useful and one of
the jobs I've done along the way was to design and implement a query language
for the Gothic Object-Oriented GIS (for more info on which, visit
the Laser-Scan website). The simple fact
that I was dealing with a close relative of a *very* well explored
problem made the Z-F solution to that problem (with Peano's axiom thrown in
where it was needed) an excellent guide to how to design and implement the query
language. That's parcelled up a diverse body of query functionality in a simple
API – which in turn makes it easier for application code, built on the
API, to deploy rich querying functionality in serving users better. So: Z-F has
been commercially useful ;^)