Go up to 3 Sets, Relations, and Functions
Go forward to 3.2 Tuples
|
Go up to 3 Sets, Relations, and Functions Go forward to 3.2 Tuples |
|
The formula x in y is read as
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 <=> (forall z: z in x <=> z in y).
Furthermore, we have a "minimal" set:
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.
{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.
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.,
The binary predicatejoin(T0,join(T1, ...,join(Tn-1,{}))) = {T0, T1, ..., Tn-1}.
= also denotes set equality (we will see later how
we can define a corresponding predicate ourselves).
Sets have an important "ordering" relationship:
x subset y : <=> (forall z in x: z in y).
The subset relationship is an ordering in the following sense.
Furthermore, we have the following relationship between equality and the subset predicate:
x = y <=> (x subset y /\ y subset x).
(1) forall z: z in x <=> z in y.We have to prove x subset y /\ y subset 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.
(1) forall z in x: z in y; (2) forall z in y: z in x.
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:
{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}.
{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.
{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.
{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())
set.addElement(element.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:
"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}.
"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}.
"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;
"the powerset of x"
P(x) := {y: y subset x}also denoted by 2x.
Let N denote the set of natural numbers and Nn := {x in N: x < n}. 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}}.
union i in N Ni = N; intersection i in N Ni = {};
(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.
A union A = A, A union 0= A, A intersection A = A, A intersection 0= 0;
A union B = B union A, A intersection B = B intersection A;
A union (B union C) = (A union B) union C, A intersection (B intersection C) = (A intersection B) intersection C;
A intersection (B union C) = (A intersection B) union (A intersection C), A union (B intersection C) = (A union B) intersection (A union C);
A union (A intersection B) = A, A intersection (A union B) = A;
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) forall x: x in A union B <=> x in B union A.Take arbitrary x.
(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).
as illustrated by the following Venn diagram (Venn-Diagramm):
(B union A) intersection (C union A) = (B intersection C) union A.
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.
