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|kin:~B[i]) = ~(i|kin:B[i])

Case: kin 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: kin false

 

Case: n=m,m+1

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

(|kim+1:~B[i])

(Split off term)

(|kim:~B[i]) ~B[m+1]

(deMorgan for two sets)

~(~(|kim:~B[i]) B[m+1])

(case n=m is true)

~(~~(|kim:B[i]) B[m+1])

(Double negative)

~((|kim:B[i]) B[m+1])

(Split off term)

~(|kim+1:B[i])

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

End of Proof

 

Theorem 2: (j|kjn:(i|kij-1:~B[i])B[j]) =

(j|kjn:B[j])

Case: kin 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: kin false

 

Case: n=m,m+1

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

(j|kjm+1:(i|kij-1:~B[i])B[j])

(Split off term)

(j|kjm:(i|kij-1:~B[i])B[j])

((i|kim+1-1:~B[i])B[m+1])

(Arithmetic)

(j|kjm:(i|kij-1:~B[i])B[j])

((i|kim:~B[i])B[m+1])

(case n=m is true)

(j|kjm:B[j])

((i|kim:~B[i])B[m+1])

(Distribute over )

((j|kjm:B[j])(i|kim:~B[i]))

(((j|kjm:B[j])B[m+1])

(Theorem 1)

((j|kjm:B[j])~(i|kim:B[i]))

(((j|kjm:B[j])B[m+1])

(A~A = U)

U

(((j|kjm:B[j])B[m+1])

(Identity of )

(((j|kjm:B[j])B[m+1])

(Split off term)

((j|kjm+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