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

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:

x = y <=> (forallz: z in x <=> z in y).

Furthermore, we have a "minimal" set:

Because of Axiomexistsx:forally:ynot inx.

0:=suchx:forally:ynot inx.

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

{is a term that denotes the set of all theT_{0},T_{1}, ...,T_{n-1}}

As a special case, we have {} =xin {T_{0},T_{1}, ...,T_{n-1}} <=> (x=T_{0}\/x=T_{1}\/ ... \/x=T_{n-1}).

1,i.e., 1 in0, {1, 2},a,

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.,

The binary predicate`join`

(T_{0},`join`

(T_{1}, ...,`join`

(T_{n-1},`{}`

))) = {T_{0},T_{1}, ...,T_{n-1}}.

`=`

also denotes set equality (we will see later how
we can define a corresponding predicate ourselves).
Sets have an important "ordering" relationship:

xsubsety: <=> (forallzinx:ziny).

The subset relationship is an ordering in the following sense.

**Minimum (Kleinstes Element)****Reflexivity (Reflexivität)****Antisymmetry (Antisymmetrie)****Transitivity (Transitivität)**

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

x=y<=> (xsubsety/\ysubsetx).

- We prove
`x`=`y`=> (`x`subset`y`/\`y`subset`x`). Assume`x`=`y`, i.e., by definition of `=',(1)

We have to prove**forall**`z`:`z`in`x`<=>`z`in`y`.`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
- We prove (
`x`subset`y`/\`y`subset`x`) =>`x`=`y`. Assume`x`subset`y`/\`y`subset`x`, i.e., by definition of ` subset '

We prove(1) **forall**`z`in`x`:`z`in`y`;(2) **forall**`z`in`y`:`z`in`x`.`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).

- We prove

**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:

{The value of this term is the set of all elementsxinS: A}.

We callxin {x in S: A} <=> (xinS/\A).

{is {1, 2, 3, 4, 6, 8, 10}.xinS:x<= 3 \/xis even}

**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

{such that, for everyx:A},

**Generalization** The set quantifier is often used in a more
general form. Let `T`_{x} be a term with free variable `x`,
`S` be a term, and `A` be a proposition. Then the term

{denotes the set of all values ofT_{x}:xinS/\A}

{Ify: (existsxinS:y=T_{x}/\A)}.

{2*is usually interpreted asx: 1 <=x<=5}

{2*(wherex:xinN/\ 1 <=x<=5}

{denotes in assignment [x+y: 1 <=x<=5}

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

`set`

(xinS:A,T) = {T_x:xinS/\A}.

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

{with the meaningZ_{x, y}:xinS/\yinT/\A}

{Again, the formulaz: (existsxinS,yinT:z=Z_{x, y}/\A)}.

{is usually interpreted asx+y: 1 <=x<= 3 /\ 0 <=y<= 2}

{Its value is the same as that of the termx+y:xinN/\yinN/\ 1 <=x<= 3 /\ 0 <=y<= 2}.

{which is the sets: (existsxinN,yinN:s=x+y/\ 1 <=x<= 3 /\ 0 <=y<= 2)}.

{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()) set.addElement(element.eval()); Context.end(); } return set; } }

The evaluation of the Java term `(new SetTerm(`

results in the set
{`x`, `S`,
`A`, `T`)).eval()`T`_{x}: `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 sets^{3}:

*Union (Vereinigung)*"the union of

`x`and`y`"`x`union`y`:= {`z`:`z`in`x`\/`z`in`y`}`x`+`y`;"the union of all elements of

`x`"**union**`x`:= {`z`: (**exists**`y`in`x`:`z`in`y`)}**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`}`x`*`y`;"the intersection of all elements of

`x`"**intersection**`x`:= {`z`in**union**`x`: (**forall**`y`in`x`:`z`in`y`)}**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`}`x`-`y`;*Powerset (Potenzmenge)*"the powerset of

`x`"**P**(`x`) := {`y`:`y`subset`x`}^{x}.

Let

SintersectionT= {2, 5};SunionT= {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}}.

union_{i in N}N_{i}=N;intersection_{i in N}N_{i}= {};

(which is equivalent to the definition given above. Based on this axiom, binary union is then defined asforallz:zinunionx<=> (existsyinx:ziny))

(which is equivalent to the definition given above.forally:yinP(x) <=> (forallziny:zinx))

**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.

**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`.

(1)Take arbitraryforallx:xinAunionB<=>xinBunionA.

- We prove
`x`in`A`union`B`=>`x`in`B`union`A`. Assume(2)

We have to prove`x`in`A`union`B`.`x`in`B`union`A`. By definition of union , we have to prove(3)

If`x`in`B`\/`x`in`A`.`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 =).

as illustrated by the following

( BunionA) intersection (CunionA)= ( BintersectionC) unionA.

We prove this claim as follows:

( BunionA) intersection (CunionA)= (commutativity) ( AunionB) intersection (AunionC)= (distributivity) Aunion (BintersectionC)= (commutativity) ( BintersectionC) unionA.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999