The symbols used to build formulas stating concepts of set theory.   Below is one such notation, which I have adapted from Paul Bernays' Axiomatic Set Theory to work with the limited character set available to E2.

Important Note: HTML entities

When I first composed this writeup, browsers were not very good at representing mathematical symbols via HTML entities. Now, many browsers support traditional set theory symbols. However, keep the old symbols in mind for reading older writeups.

() - is (not) an element of (Use &isin; and &notin; instead of e and !e)
() - is as subset (proper subset) of (Use &sube; and &sub; instead of <= and <)
() - is a superset (proper superset) of (Use &supe; and &sup; instead of >= and >)
- union (Use &cup; instead of U)
- intersection (Use &cap; instead of INT)
- not equal (Use &ne; instead of !=)
- aleph (Use &alefsym; instead of "Aleph")
- existential quantifier (Use &exist; instead of E)
- universal quantifier, not necessary (The entity is &forall; but this symbol is not necessary in our notation).

Basic terms

A formula is a string of symbols built according to the rules presented below.  Each formula results in a particular type of object.
A set is a collection of items (always other sets) that has been proven to be "complete" by the axioms of set theory.
A predicate is a formula which results in a true or false value after values have been substituted for the variables in it.
A class is the extension of a predicate; that is, all sets for which the predicate is true.
A term is a formula which results in a set or class, after all of the variables have been filled in.
A schema is a formula containing terms with variables.  Each substitution of a schema's term variables with appropriate   formulae results in a unique predicate.

Wherever formulae and commentary have to mix, fixed width will be used for the formulae and variable width for the commentary.

Variables

A variable is a symbol used to stand in for a set, class or term.
Each variable is a formula unto itself.

• A free variable represents a set which has not previously been identified in the formula.  If a predicate containing a free variable is proven true (or false), it is true (false) for all values (of the correct type) of the variable (i.e. all sets for a set term, or all classes for a class term).  Lower case letters (a, b, c, d) usually represent free variables, but other lower case letters may occasionally be used, in which case the reader will have to infer the variable's status.

•
• A bound variable represents a set has been previously identified in the formula. If a predicate containing a bound variable is proven true (or false), it is true (false) only for the value identified.  Lower case letters (f, g, ... z) represent bound variables, with the caveat stated above.

Upper case letters (A, B, C, ...) stand for classes.

Bernays used German Gothic letters to stand in for predicates and terms.  We will have to be content with using bold, italic forms of upper case letters (A, B, C, ..., J) for predicates, upper case letters (K, L, M, ..., Z) for class terms, and and lower case letters (a, b, c, d, f, ...) for set terms.

Formula building schemas

Given a set a, we may construct a predicate asserting that another set b is an element of a, using the operator b e a.
It is possible to define elementhood for a particular predicate A(x) by stating a e A(x) <-> A (a).
Lower-case e will always be used for elementhood, not for any variable.

Given a set a, we can define another set containing only a: {a}. Square brackets are normally used, but you know where that leads....

Given two predicates or schemas, we may construct a new predicate or schema whose truth or falsehood results from the binary logic tables:

A & B means A is true, and B is also true.
A or B means A is true, or B is true, or both.
A -> B means that whenever A is true, B is also true.
A <-> B  and A iff B mean that whenever A is true, B is also true, and whenever A is false, B is also false.
A xor B&nbpsp; means that whenever A is true, B is false, and whenever A is false, B is also true.  Rarely used.

Given a predicate or schema, we may construct another predicate (schema) asserting the original formula's falsehood:

~A(x)

Given a schema involving a set term, we may construct a formula referring to the class which is the value of the predicate we get after substituting a formula to represent the set term.

{ x | A(x) }

The Church schema defines elementhood for a class schema:

a e {x | A(x) } <-> A(a)

And congruence (equality) of classes can be defined:

A = B <-> (a e A <-> a e B)

There is the universal quantifier  (x)A(x) "For all values of x, the predicate A(x) is true."

And the existential quantifier  (Ex)A(x) "For some value of x, the predicate A(x) is true."

You have to prove it first....

Many constructions are meaningful only after something has been proven.

Bernays' axiom of equality defines equality for sets:

a = b <-> (s e a <-> s E b)

And we will occasionally use a != b to assert ~(a=b). Similarly, A != B.

Sets and classes may be compared, given the Equality and extensionality axioms.

Often, a predicate is true for exactly one value of a set variable.  We often wish to identify that value.  However, any schema needs to work for all predicates.  We must provide an alternative value for the other predicates.

So, when we say

y = ixA(x, m)

we really mean

(A(y) & (z)(A(z) <-> y = z)) or (y = m).

The concept of the empty set 0 is introduced early in set theory. y = ixA(x) means y = ixA(x, 0).

With the axioms of general set theory, we can refer to

The empty set 0
The set containing everything in a, and also b. {a;b} = { x | x E a OR x = b } aka a U {b}.

Ordinal theory shows that natural numbers are sets.  We will often refer to a range of numbers as  i..j

Functors

A function is a class of ordered pairs, the first element of which comes from some set, and the second element of which comes from some other set or class.

Although functions on sets and classes must be proven by set theory, once their existence has been proven, it is frequently useful to assign them a name and refer only to their variables.

Although Bernays used Fix to mean  iy(x, y) e F, where (x, y) is an ordered pair, we will use F(x) as it is more readily understood. Some function classes can be proven to be represented by sets, and we will often refer to f(x) as well.

Functions on two variables frequently use infix notation, similar to what we have seen for some of the schema operators defined above.  Some frequently encountered ones are:

a F b refers to F(a,b) for some class variable that represents a function.

a U b and A U B (a ∪ b and A ∪ B) refer to the set (class) resulting from the union of the two sets (classes).
a INT b and A INT B (a ∩ b and A ∩ B) refer to the set  (class) resulting from the intersection of the two sets (classes).
a X b and A X B refers  to the cartesian product of the two sets (classes).

Since we don't have the symbols for the subset relation, we must use the traditional ordering symbols:

a <= b -> (x e b -> x e a) "a is a subset of b" (a ⊆ b)
b < a -> ( b <= a & (Ex) ( x e a & ~(xeb))) "a is a proper subset of b" (a ⊂ b)

We must infer the particular ordering relation we are using from context, or with a subscript.

We will also frequently use a subscript to refer to the value for a function. Thus,  Fa = F(a). This is used when such a function is used only to index another set, that is, to identify individual members of sets.  For example, when we when we are indexing an array of terms with numbers,  we refer to a1, a2, a3, and so on.

Aggregate functions

We can refer to the sum of several set terms. sum (m, t(r)) = { x | r e m & x e t(r) }.

When we have a binary function on sets, we can aggregate this to three or more operands. Given a range of numbers, we will  refer to

F (i=1..n, ti)

which is equivalent to

t1 F t2 F ... F tn.

Of course, if the function is commutative, we can use any indexing set:

F (m, ti) = ix ( ({i} = m -> x = F (ti))
OR ({i} < m -> x = F (F ({i}, ti), F (m-{i}, ti))

but it hardly seems worth it.