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.