[ notation ]

Set Theory

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 if x 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.

Zermelo-Fränkel Set Theory

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 ;^)

Written by Eddy.