Math Notes – Theory of Relations – Part 3
In the following theorems, all relations are subsets of the cross-product A´B, so an implicit assumption in all theorems is
rÍ A´B
In some theorems there will be a reference to the universal set of discourse. The universal set of discourse is denoted by U.
The properties of the identity relation are interesting and useful. The identity relation is denoted by I.
A reference to a theorem from part 1 or part 2 is noted. If there is no reference to part 1 or part 2, then the theorem reference is on this page.
Theorem 1: Given P Ù r, ("a,b|arb Ù a Î P: b Î ran.r.P)
(Reflexive property of Í)
~ran.r.P Í ~ran.r.P
º(definition of Í, definition of complement)
("b|b Ï ran.r.P: b Ï ran.r.P)
º(definition of ran.r.P, definition of Ï)
("b|b Ï ran.r.P: Ø(b Î {x|($a|:arx Ù aÎP):x})
º(definition of Î)
("b|b Ï ran.r.P: Ø($x|($a|:arx Ù aÎP):b=x))
º(one-point rule)
("b|b Ï ran.r.P: Ø($a|:arb Ù aÎP))
º(deMorgan)
("b|b Ï ran.r.P: ("a|:Ø(arb Ù aÎP)))
º(nesting)
("a,b|b Ï ran.r.P: Ø(arb Ù aÎP))
º(trading)
("a,b|arb Ù aÎP:b Î ran.r.P)
End of Proof
Theorem 2: Given P Ù r, ("a,b|:rÙ P Þ ran.r.P)
(Theorem 1)
("a,b|arb Ù a Î P: b Î ran.r.P)
º(trading)
("a,b|:arb Ù a Î P Þ b Î ran.r.P)
º(equivalent predicates)
("a,b|:rÙ P Þ ran.r.P)
End of Proof
Theorem 3: ran.r.P Í R Þ ("a,b|:arb Ù aÎP Þ bÎR)
(prove LHS Þ RHS)
ran.r.P Í R
º(definition of Í)
("b|b Î ran.r.P: b Î R)
º(identity of Ù, Theorem 1)
("b|bÎran.r.P: bÎR) Ù ("a,b|:arb Ù aÎP Þ bÎran.r.P)
º(nesting)
("b|bÎran.r.P: bÎR) Ù ("a|aÎP:("b|:arb Þ bÎran.r.P)
º(trading)
("b|:bÎran.r.P Þ bÎR) Ù ("a|aÎP:("b|:arb Þ bÎran.r.P))
º(distribute over ")
("a|aÎP:("b|:bÎran.r.P Þ bÎR Ù arb Þ bÎran.r.P))
Þ(transitivity of Þ)
("a|aÎP:("b|:arb Þ bÎR))
º(trading)
("a|aÎP:("b|arb : bÎR))
º(nesting)
("a,b|aÎP Ù arb : bÎR))
º(trading)
("a,b|:aÎP Ù arb Þ bÎR))
End of Proof
Theorem 4: ("a,b|:arb Ù a Î P Þ b Î R)Þ ran.r.P Í R
(Prove the contrapositive)
Ø(ran.r.P Í R)
º(definition of Í)
Ø("b|b Î ran.r.P: b Î R)
º(identity of Ù, Theorem 1)
Ø("b|bÎran.r.P: bÎR) Ù ("a,b|:arb Ù aÎP Þ bÎran.r.P)
º(trading)
Ø("b|bÎran.r.P: bÎR) Ù ("a,b|arb Ù aÎP :bÎran.r.P)
Þ(("x|:P)Þ($x:P), monotonicity of Ù)
Ø("b|bÎran.r.P: bÎR) Ù ($a,b|arb Ù aÎP : bÎran.r.P)
º(deMorgan)
($b|bÎran.r.P: bÏR) Ù ($a,b|arb Ù aÎP : bÎran.r.P)
º(nesting)
($b|bÎran.r.P: bÏR) Ù ($a|aÎP:($b|arb : bÎran.r.P)
º(trading)
($b|:bÎran.r.P Ù bÏR) Ù ($a|aÎP:($b|:arb Ù bÎran.r.P)
º(distribute over ")
($a|aÎP:($b|:bÎran.r.P Ù bÏR Ù arb Ù bÎran.r.P)
Þ(a Ù b Þ a, monontonicity of $)
($a|aÎP:($b|:bÏR Ù arb)
º(nesting)
($a,b|aÎP:bÏR Ù arb)
º(trading)
($a,b|aÎP Ù arb:bÏR)
º(deMorgan)
Ø("a,b|aÎP Ù arb:bÎR)
º(trading)
Ø("a,b|>:aÎP Ù arbÞ bÎR)
End of Proof
Theorem 5: ("a,b|:arb Ù a Î P Þ b Î R)º ran.r.P Í R
(Theorem 3)
ran.r.P Í R Þ ("a,b|:rÙ P Þ R)
º(Theorem 4, identity of Ù)
ran.r.P Í R Þ ("a,b|:arb Ù aÎP Þ bÎR) Ù
("a,b|:arb Ù aÎP Þ bÎR) Þ ran.r.P Í R
º((aÞb Ù bÞa) º aºb)
ran.r.P Í R º ("a,b|:arb Ù aÎP Þ bÎR)
End of Proof
Corollary: ("a,b|aÎP: arb Þ b Î R)º ran.r.P Í R
(Theorem 5)
("a,b|:arb Ù a Î P Þ b Î R)º ran.r.P Í R
º(shunting)
("a,b|:aÎP Þ(arb Þ b Î R))º ran.r.P Í R
º(trading)
("a,b|aÎP: arb Þ b Î R)º ran.r.P Í R
End of Proof
Theorem 6: ("a,b|:rÙ P Þ R)º ran.r.P Í R
(Theorem 5)
("a,b|:arb Ù a Î P Þ b Î R) º ran.r.P Í R
º(equivalent predicates)
("a,b|:rÙ P Þ R) º ran.r.P Í R
End of Proof
Theorem 7: ("a|:P Þ R)ºP Í R
(Prove that RHS º LHS)
P Í R
º(Identity Relation Theorem 3)
ran.I.P Í R
º(Theorem 5)
("a,b|:aIb Ù a Î P Þ b Î R)
º((a Ù b Þ c) º (a Þ (b Þ c)), symmetry of Ù)
("a,b|: a Î P Þ (aIb Þ b Î R))
º(trading)
("a,b| a Î P:(aIb Þ b Î R))
º(nesting)
("a| a Î P:("b|:aIb Þ b Î R))
º(trading)
("a| a Î P:("b|aIb :b Î R))
º(definition of identity relation)
("a| a Î P:("b|a=b :b Î R))
º(one point rule)
("a| a Î P:a Î R)
º(trading)
("a|:a Î PÞa Î R)
º(equivalent predicates)
("a|:P Þ R)
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.