Math Notes Singleton Sets

 

Axiom 1: {a} = {x|x=a:x}.

 

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: b {a} b = a

(prove LHS RHS)

b {a}

(axiom 1)

b {x|x=a:x}

(definition of )

($x|x=a:b=x)

(one point rule)

b = a

End of Proof

 

Corollary: x {x}

(reflexive property of =)

x = x

(Theorem 1)

x {x}

End of Proof 

 

Theorem 2: a P {a} P

(prove RHS LHS)

{a} P

(definition of )

("x|x {a}: x P)

(Theorem 1)

("x|x = a: x P)

(one point rule)

a P

End of Proof

 

Theorem 3: {a} P {a} Q {a} (P Q)

(Prove by showing LHS RHS)

     {a} P {a} Q

(Theorem 2)

     a P a Q

(definition of )

     a (P Q)

(Theorem 2)

     a (P Q)

End of Proof

 

Theorem 4: {x} B {x} ~B

(prove LHS RHS)

({x} B)

(Theorem 2)

(x B)

(definition of not )

x B

(complement)

x ~B

(Theorem 2)

{x} ~B

End of Proof

 

 

References:

 

Dijkstra, Edsgar W. and Scholten, Carel S. 1990 Predicate Calculus and Program Semantics, New York, NY: Springer-Verlag

 

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

 

Ganong, Rick 1999, Course notes and comments from M1090 and M2090 math and logic courses, http://www.math.yorku.ca/Who/Faculty/Ganong

 

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

 

Hu Sze-Tsen, 1963, Elements of Modern Algebra, San Francisco: Holden-Day, Inc.