Math Notes – Quantifying Set Operators
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.
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