Axiom of Extension

The most important undefined notion in set theory is being a member of a set. If $a$ is a member of $A$ then we shall write, according to Halmos: $$ a \in A $$ Fortunately, this notion can be mapped upon our TObject arrays in a well defined manner. Calling sequence is defined by:

function is_in(e : TObject; X : Objects) : boolean;

It can also be mapped upon our bitmapped and integer mapped arrays in a well defined manner. Calling sequences are defined by:

function is_in(e : integer; X : bitmap) : boolean;
function is_in(e : integer; X : integers) : boolean;

Programming such calling sequences for a strings implementation is a bit less trivial, because it would require a parsing mechanism. Therefore any strings implementation will be postponed until we bounce against limitations of the others.
If A and B are sets and each member of A is also a member of B then we say that A is a subset of B. And, according to Halmos, this shall be written as: $$ A \subseteq B \quad \mbox{or} \quad B \supseteq A $$ This can be implemented in software quite easily. Calling sequences are defined by:

function SubSet(A,B : Objects) : boolean;
function SubSet(A,B : bitmap) : boolean;
function SubSet(A,B : integers) : boolean;

The Axiom of Extension states that two sets are equal if and only if they have the same elements. If $A$ is equal to $B$ then we write: $$ A = B $$ And the fact that $A$ and $B$ are not equal is expressed by writing: $$ A \neq B $$ Equality of sets $A = B$ can be conveniently defined as: A is a subset of B and B is a subset of A. Formally: $$ (A = B) \qquad \equiv \qquad ((A \subseteq B) \quad \mbox{and} \quad (A \supseteq B)) $$ This too can be easily implemented in software. Calling sequences defined by:

function Equal(A,B : Objects) : boolean;
function Equal(A,B : bitmap) : boolean;
function Equal(A,B : integers) : boolean;

We conclude that the Axiom of Extension is piece of an implementable set theory. And three implementations have been provided already.
A warning is in place, though. Extension might be not as simple as it looks like, at first sight. Especially with complicated sets, where the elements themselves in turn are sets of sets (towers of sets), the look and feel of a set can become quite messy. One way to get rid of that messiness, at least in part, is to adopt the following more detailed rules:

if $x$ and $y$ are members of a set, so are $y$ and $x$ ($x$ and $y$ can be swapped)
if $x$ and $x$ are members of a set $S$, then only $x$ is a member of $S$ (squeeze $x$)

Example: swap $c$ and $d$, squeeze $d$ and $d$, swap $b$ and $a$, swap $b$ and $d$. In: $$ \{b,d,c,d,a\} = \{b,d,d,c,a\} = \{b,d,c,a\} = \{a,d,c,b\} = \{a,b,c,d\} $$ In practice, this means that duplicate elements in a set should be removed (terse sets). And that a set should be sorted "in (reverse) alphabetic order".

In case our sets have become equivalent with bitmaps and natural numbers - which is the case to be preferred - then it's important to establish some other equivalencies.
The one for equality ($A = B$) is more than trivial. However ..
Theorem. \begin{eqnarray*} A \subseteq B \quad \Longrightarrow \quad A \le B\\ A \supseteq B \quad \Longrightarrow \quad A \ge B \end{eqnarray*} It may be not a coincidence that $\le$ and $\ge$ are used with Object Pascal set implementations as a substitute for $\subseteq$ and $\supseteq$. The reverse is not true, though: $7 < 8$ but $7 \not\subset 8$: $$ \require{cancel} \cancel{A \le B \quad \Longrightarrow \quad A \subseteq B} \\ \cancel{A \ge B \quad \Longrightarrow \quad A \supseteq B} $$

Herewith, chapter 1 of Halmos' book is covered a great deal. The reader is encouraged to look up there any details of common naive set theory which might be missing in our treatment. We are not going to repeat all of the well known stuff that is common to traditional and implementable set theory.

The chapter 'Aviom of Specification' will be skipped altogether for the moment being. The reason is that logic and predicates have not been done yet as an implementable theory, at least not by this author.