Math Notes – Quantifying Set Operators

# Axiom 1: (Èi|false:B[i]) = Æ, (Çi|false:B[i]) = U

Any temporary variables introduced in the theorems are assumed to be distinct.  That is, the temporary variables do not occur as free variables in any other expression.

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

Case: k£i£n º false

(All expressions where k > n are covered with this case)

(Çi|false:~B[i])

º(Axiom 1)

U

º(Negation of the universal set)

~Æ

º(Axiom 1)

~(Èi|false:B[i])

End of Proof Case: k£i£n º false

Case: n=m,m+1

(Given true for n=m, prove true for n=m+1)

(Ç|k£i£m+1:~B[i])

º(Split off term)

(Ç|k£i£m:~B[i])Ç ~B[m+1]

º(deMorgan for two sets)

~(~(Ç|k£i£m:~B[i])È B[m+1])

º(case n=m is true)

~(~~(È|k£i£m:B[i])È B[m+1])

º(Double negative)

~((È|k£i£m:B[i])È B[m+1])

º(Split off term)

~(È|k£i£m+1:B[i])

End of Proof Case: n=m,m+1

End of Proof

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

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

Case: k£i£n º false

(All expressions where k > n are covered with this case)

(Èj|false:(Çi|false:~B[i])ÇB[j])

º(Axiom 1)

Æ

º(Axiom 1)

(Èj|false:B[j])

End of Proof Case: k£i£n º false

Case: n=m,m+1

(Given true for n=m, prove true for n=m+1)

(Èj|k£j£m+1:(Çi|k£i£j-1:~B[i])ÇB[j])

º(Split off term)

(Èj|k£j£m:(Çi|k£i£j-1:~B[i])ÇB[j])

È

((Çi|k£i£m+1-1:~B[i])ÇB[m+1])

º(Arithmetic)

(Èj|k£j£m:(Çi|k£i£j-1:~B[i])ÇB[j])

È

((Çi|k£i£m:~B[i])ÇB[m+1])

º(case n=m is true)

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

È

((Çi|k£i£m:~B[i])ÇB[m+1])

º(Distribute È over Ç)

((Èj|k£j£m:B[j])È(Çi|k£i£m:~B[i]))

Ç

(((Èj|k£j£m:B[j])ÈB[m+1])

º(Theorem 1)

((Èj|k£j£m:B[j])È~(Èi|k£i£m:B[i]))

Ç

(((Èj|k£j£m:B[j])ÈB[m+1])

º(AÈ~A = U)

U

Ç

(((Èj|k£j£m:B[j])ÈB[m+1])

º(Identity of Ç)

(((Èj|k£j£m:B[j])ÈB[m+1])

º(Split off term)

((Èj|k£j£m+1:B[j])

End of Proof Case: n=m,m+1

End of Proof

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