Math Notes – Quantifying Set Operators

The set union operator and the set intersection operator may be used in quantified expressions in a way similar to quantifying either the logical conjunction operator or the logical disjunction operator.  The theorems and techniques are well established.  The references below provide more information on quantifying basic set operators.

Set-based program state concepts (for example, Set-based analysis of if-statements) may refer to a collection or set of related program state spaces.  Each set in the collection may be denoted by a subscript or index.  Thus, a set of state spaces may be denoted as

{i|k£i£n: B[i]}

The theorems on this page are proved using the notation shown above, because the notation is also used in the analysis of programming methods.

# A quantified expression over the union operator has the form

(Èi|k£i£n:B[i]).

# A quantified expression over the intersection operator has the form

(Çi|k£i£n:B[i]).

The meaning of a quantified expression over the union operator is

(Èi|k£i£n:B[i]) = B[k] È B[k+1] È ¼ È B[n].

A quantified expression over the intersection operator has a similar interpretation with the intersection operator in place of the union operator.

# Empty Range

Sometimes the range expression is false, indicating an empty range.  A quantified expression with an empty or false range has the value the identity element.  For set-unions, the identity element is the null set.  For set-intersections, the identity element is the universal set.  Thus:

# Splitting Ranges

The union and intersection operators are symmetric and idempotent, so splitting off a term and splitting a range are both valid operations.

DeMorgan’s law for two sets generalizes to a quantified expression.

# Theorem 1: (deMorgan) (Çi|k£i£n:~B[i]) = ~(Èi|k£i£n:B[i])

DeMorgan’s law also applies to following theorem. The left half of the expression is the union of solutions to an if-statement under certain constraints.  The expression may be simplified by dropping out the set negations.

Theorem 2: (Èj|k£j£n:(Çi|k£i£j-1:~B[i])ÇB[j]) =

(Èj|k£j£n:B[j])

References:

Fejer, Peter and Simovici, Dan A., 1991, Mathematical Foundations of Computer Science, New York, NY: Springer-Verlag

Gries, David and Schneider, Fred B., 1993, A Logical Approach to Discrete Math, New York, NY: Springer-Verlag