Go up to 3 Sets, Relations, and FunctionsGo forward to 3.2 Tuples

## 3.1 The Datatype Set

The domain of sets has a single binary predicate  is element of (ist Element von) denoted by the infix constant ` in '. All other predicates and functions are defined by this predicate.

The formula x in y is read as

• x is element of y;
• x is part of y;
• y contains x.

Please note that in set theory all objects are sets (e.g. also the number 1 is just a particular set). Thus in a statement x in y, both x and y denote sets the first of which is element of the second one.

The following axiom states that sets have no other property than being element containers:

Axiom 1 (Equality of Sets) Two sets are equal if and only if they have the same elements, i.e., for all x and y, we have
x = y <=> (forall z: z in x <=> z in y).

Furthermore, we have a "minimal" set:

Axiom 2 (Empty Set) There exists a set that is empty, i.e., that does not contain any elements:
exists x: forall y: y not  in x.
Because of Axiom Equality of Sets, there is only one empty set such that we can define
0:= such x: forall y: y not  in x.

Finite sets (i.e., sets with a finite number of elements) can be constructed by explicit enumeration.

Proposition 20 (Set Enumeration) Let T0, T1, ..., Tn-1 be terms (for any n). Then
{T0, T1, ..., Tn-1}
is a term that denotes the set of all the Ti values, i.e., for every x, we have
x in {T0, T1, ..., Tn-1} <=> (x = T0 \/ x = T1 \/ ... \/ x = Tn-1).
As a special case, we have {} = 0.

Example  The set S := {1, 0, {1, 2}, a} contains the values
1, 0, {1, 2}, a,
i.e., 1 in S, 0 in S, {1, 2} in S, a in S.

We have the following set equalities:

 {1, 2} = {2, 1}; {1, 2} = {1, 1, 2, 1}.

Logic Evaluator  The predicate "is element of" is denoted by (prefix) `in` and the empty set is denoted by `{}`. The binary function `join` adds an element to a set, i.e.,

`join`(T0, `join`(T1, ..., `join`(Tn-1, `{}`))) = {T0, T1, ..., Tn-1}.
The binary predicate `=` also denotes set equality (we will see later how we can define a corresponding predicate ourselves).

Sets have an important "ordering" relationship:

Definition 21 (Subset)  x is a  subset (Teilmenge) of y, if every element of x is also an element of y, i.e.,
x subset y : <=> (forall z in x: z in y).

The subset relationship is an ordering in the following sense.

Proposition 21 (Subset Properties) For every x, y, and z we have:
Minimum (Kleinstes Element)

0 subset x;

Reflexivity (Reflexivität)

x subset x;

Antisymmetry (Antisymmetrie)

(x subset y /\  y subset x) => y = x;

Transitivity (Transitivität)

(x subset y /\  y subset z) => x subset z.

Furthermore, we have the following relationship between equality and the subset predicate:

Proposition 22 (Equality and Subset) For every x and y, we have
x = y <=> (x subset y /\  y subset x).

Proof  Take arbitrary x and y. We have to prove x = y <=> (x subset y /\  y subset x).
• We prove x = y => (x subset y /\  y subset x). Assume x = y, i.e., by definition of `=',
(1) forall z: z in x <=> z in y.
We have to prove x subset y /\  y subset x.
• We prove x subset y, i.e., by definition of ` subset ', forall z in x: z in y. Take arbitrary z. We have to prove z in x => z in y. Assume (2) z in x. We have to prove z in y which is a consequence of (1) and (2).
• The proof of y subset x proceeds analogously.
• We prove (x subset y /\  y subset x) => x = y. Assume x subset y /\  y subset x, i.e., by definition of ` subset '
 (1) forall z in x: z in y; (2) forall z in y: z in x.
We prove x = y, i.e., by definition of `=', forall z: z in x <=> z in y. Take arbitrary z. We have to prove z in x <=> z in y.
• We prove z in x => z in y. Assume (3) z in x. We have to prove z in y which is a consequence of (1) and (3).
• We prove z in y => z in x. Assume (4) z in y. We have to prove z in x which is a consequence of (2) and (4).

Logic Evaluator  Using the knowledge proved above, we may define equality of sets as follows:

Most frequently, sets are constructed with the help of the following special quantifier that builds a term from a term and a formula:

Proposition 24 (Set Quantifier) Let x be a variable, S a term, and A a formula; then the following is a term:
{x in S: A}.
The value of this term is the set of all elements x in S such that A holds, i.e., for all x, we have
x in {x in S: A} <=> (x in S /\  A).
We call S the  variable domain (Variablenbereich) of x. If S is clear from the context, we may just write {x: A}.

Example  Let S be {1, 2, 3, ..., 10}. Then the set
{x in S: x <= 3 \/ x is even}
is {1, 2, 3, 4, 6, 8, 10}.

Remark  The set quantifier allows us to construct sets only from elements of a (possibly implicitly) given set. We might want to lift this restriction, i.e., work with a general quantifier

{x: A},
such that, for every x, x in {x: A} <=> A. However, with such a general quantifier we could also define a set S := {x: x not  in x}, i.e., the set of all sets that do not contain themselves as elements. Then we might ask ourself whether S in S. If yes, then this would contradict the construction principle. If no, then S in S would be true by the construction principle, which would contradict our assumption. In any case, we would have a contradiction, therefore neither S in S nor S not  in S could hold. This so called  Russel Paradox is avoided by restricting the quantifier as shown above.

Generalization  The set quantifier is often used in a more general form. Let Tx be a term with free variable x, S be a term, and A be a proposition. Then the term

{Tx: x in S /\  A}
denotes the set of all values of Tx such that A holds where x is an element of S, i.e., it is the same as
{y: (exists x in S: y = Tx /\  A)}.
If S is clear, the formula x in S is often skipped; the bound variable x then has to be deduced from the context.

Example  The term
{2*x: 1 <= x <= 5}
is usually interpreted as
{2*x: x in N /\  1 <= x <= 5}
(where N is the set of natural numbers) which denotes the set {2, 4, 6, 8, 10}. Likewise, the term
{x+y: 1 <= x <= 5}
denotes in assignment [y |-> 1] the set {2, 3, 4, 5, 6} (assuming that y is not bound by the set quantifier).

Logic Evaluator  The general form of the set quantifier is available as

`set`(x in S: A, T) = {T_x: x in S /\  A}.

Generalization  Set quantifiers may also range over multiple variables, e.g.

{Zx, y: x in S /\  y in T /\  A}
with the meaning
{z: (exists x in S, y in T: z = Zx, y /\  A)}.
Again, the formula x in S /\  y in T is frequently skipped and the quantified variables have to be deduced from the context.

Example  The term
{x+y: 1 <= x <= 3 /\  0 <= y <= 2}
is usually interpreted as
{x+y: x in N /\  y in N /\  1 <= x <= 3 /\  0 <= y <= 2}.
Its value is the same as that of the term
{s: (exists x in N, y in N: s = x+y /\  1 <= x <= 3 /\  0 <= y <= 2)}.
which is the set
{1+0, 1+1, 1+2, 2+0, 2+1, 2+2, 3+0, 3+1, 3+2}
which again equals
{1, 2, 3, 4, 5}.

Logic Evaluator  The set quantifier also binds multiple variables:

Operational Interpretation  In the Logic Evaluator, set quantifiers with single variables are instances of the following Java class:

```public final class SetTerm implements Term
{
private String variable;
private Term domain;
private Formula formula;
private Term element;

public SetTerm(String _variable, Term _domain,
Formula _formula, Term _element)
{
variable = _variable;
domain = _domain;
formula = _formula;
element = _element;
}

public Value eval() throws EvalException
{
Set set = new Set();
Iterator iterator = Model.iterator(domain);
while (iterator.hasNext())
{
Context.begin(variable, iterator.next());
if (formula.eval())
Context.end();
}
return set;
}
}
```

The evaluation of the Java term ```(new SetTerm(x, S, A, T)).eval()``` results in the set {Tx: x in S /\  A}. We iterate over the set denoted by S and establish new contexts in which x is mapped to each element of S in turn. In each context, we evaluate the formula A and, if the result is true, evaluate the term T whose value is added to the set.

With the help of the set quantifier, we can define a number of important functions on sets3:

Definition 22 (Set Functions) We define the following functions on sets:
Union (Vereinigung)

"the union of x and y"

x union y := {z: z in x \/ z in y}
also denoted by x + y;

"the union of all elements of x"

union x := {z: (exists y in x: z in y)}
also used as a quantor union x in S /\  A T := union {T: x in S /\  A}.
Intersection (Durchschnitt)

"the intersection of x and y"

x intersection y := {z in x: z in y}
also denoted by x * y;

"the intersection of all elements of x"

intersection x := {z in union x: (forall y in x: z in y)}
also used as a quantor intersection x in S /\  A T := intersection {T: x in S /\  A}.
Difference (Differenz)

"the difference of x and y" ("the complement of y in x").

x \ y := {z in x: z not  in y}
also denoted by x - y;
Powerset (Potenzmenge)

"the powerset of x"

P(x) := {y: y subset x}
also denoted by 2x.

Example  Let S := {1, 2, 3, 4, 5}, T := {2, 5, 7}, U := {1, 3, 5, 7, 9}. Then we have
 S intersection T = {2, 5}; S union T = {1, 2, 3, 4, 5, 7}; intersection {S, T, U} = {5}; union {S, T, U} = {1, 2, 3, 4, 5, 7, 9}; P(T) = {0, {2}, {5}, {7}, {2, 5}, {2, 7}, {5, 7}, {2, 5, 7}}.
Let N denote the set of natural numbers and Nn := {x in N: x < n}. Then we have
 union i in N Ni = N; intersection i in N Ni = {};

Remark  Above definitions of union and powerset make use of the general set quantor whose potential problems have been discussed before. Actually, in set theory union and powerset are introduced in a different way: there is an axiom that stipulates the existence of a unary function union with the property that, for every x,
(forall z: z in union x <=> (exists y in x: z in y))
which is equivalent to the definition given above. Based on this axiom, binary union is then defined as x union y := union {x, y}. Likewise, there is an axiom that stipulates the existence of a unary function `P' with the property that, for every x,
(forall y: y in P(x) <=> (forall z in y: z in x))
which is equivalent to the definition given above.

Logic Evaluator  Also the implementation of unary and binary union as well as of powersets is not based on the set quantifier but on set reduction. We can use these functions ( union  is denoted by `++`, P by `Powerset`) by loading a file `set.txt`.

However, binary and unary intersection can be defined with the help of the set quantifier as follows ( intersection  is denoted by `**`, please compare with the mathematical definitions):

We have a number of laws that relate the basic set operations; some of them are listed below.

Proposition 25 (Set Identities) For every A, B, and C we have:
Idempotency, Identity and Domination
 A union A = A, A union 0= A, A intersection A = A, A intersection 0= 0;
Commutativity
 A union B = B union A, A intersection B = B intersection A;
Associativity
 A union (B union C) = (A union B) union C, A intersection (B intersection C) = (A intersection B) intersection C;
Distributivity
 A intersection (B union C) = (A intersection B) union (A intersection C), A union (B intersection C) = (A union B) intersection (A union C);
Cancellation
 A union (A intersection B) = A, A intersection (A union B) = A;
De Morgan
 C\(A union B) = C\A intersection C\B, C\(A intersection B) = C\A union C\B.

Because of associativity, we may write A union B union C respectively A intersection B intersection C without parentheses.

We now argue for the correctness of A union B = B union A.

Proof  Take arbitrary A and B. By definition of =, we have to prove
(1) forall x: x in A union B <=> x in B union A.
Take arbitrary x.
• We prove x in A union B => x in B union A. Assume
(2) x in A union B.
We have to prove x in B union A. By definition of union , we have to prove
(3) x in B \/ x in A.
If x in B, we are done. Thus assume (4) x not  in B. By (2) and definition of union , we have (5) x in A \/ x in B. From (4) and (5), we have x in A and thus (3).
• The proof of x in B union A => x in A union B proceeds analogously.

Many other set identities may be proved with the help of above identities by "equality reasoning" (which relies on the transitivity of =).

Example  For all A, B, C we have:
 (B union A) intersection (C union A) = (B intersection C) union A.
as illustrated by the following  Venn diagram (Venn-Diagramm):
We prove this claim as follows:
 (B union A) intersection (C union A) = (commutativity) (A union B) intersection (A union C) = (distributivity) A union (B intersection C) = (commutativity) (B intersection C) union A.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999