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.
(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.