Math Notes – Theory of Relation Conditions
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 an earlier part is noted. If there is no reference to part an earlier part, then the theorem reference is on this page.
Theorem 1: cond.r.Æ = Æ
Prove by showing LHS = RHS)
cond.r.Æ
(definition of cond.r.Æ)
dom.r.Æ – dom.r.~Æ
Æ – dom.r.~Æ
=(property of set difference)
ÆÇ ~dom.r.~Æ
=(zero of Ç)
Æ
End of Proof
Theorem 2: cond.r.R = dom.r - dom.r.~R
(definition of condition)
cond.r.R = dom.r.R – dom.r.~R
=(Relations Part 1 Theorem 14)
cond.r.R = dom.r – dom.r.~R
End of Proof
Theorem 3: R Í Q Þ cond.r.R Í cond.r.Q
(given R Í Q show LHS Í RHS by applying the theorem true Þ P º P)
(Part 1 Theorem 2 and given)
dom.r.R Í dom.r.Q
(Part 1 Theorem 3 and given)
~dom.r.~R Í ~dom.r.~Q
º(identity of Ù)
dom.r.R Í dom.r.Q Ù ~dom.r.~R Í ~dom.r.~Q
Þ(P Í Q Ù R Í S Þ (P Ç R) Í (Q Ç S))
(dom.r.R Ç ~dom.r.~R) Í (dom.r.Q Ç ~dom.r.~Q)
º(definition of set difference)
(dom.r.R - dom.r.~R) Í (dom.r.Q - dom.r.~Q)
º(definition of cond.r.R)
cond.r.R Í cond.r.Q
End of Proof
Theorem 4: cond.r.R Ç cond.r.Q = cond.r.(R Ç Q)
(prove LHS = RHS)
cond.r.R Ç cond.r.Q
=(theorem 2)
dom.r - dom.r.~R Ç dom.r - dom.r.~Q
=((S – R) Ç (S – Q) = S – (R È Q))
dom.r – (dom.r.~R È dom.r.~Q)
dom.r – dom.r.(~R È ~Q)
=(deMorgan)
dom.r – dom.r.~(R Ç Q)
=(theorem 2)
cond.r.(R Ç Q)
End of Proof
Theorem 5: cond.r.R È cond.r.Q Í cond.r.(R È Q)
(prove LHS Í RHS by applying the theorem true Þ P º P)
dom.r.(~R Ç ~Q) Í (dom.r.~R Ç dom.r.~Q)
º(set contrapositive)
~(dom.r.~R Ç dom.r.~Q) Í ~dom.r.(~R Ç ~Q)
(reflexive property of Í)
dom.r Í dom.r
º(identity of Ù)
dom.rÍ dom.r Ù ~(dom.r.~R Ç dom.r.~Q) Í ~dom.r.(~R Ç ~Q)
Þ(P Í Q Ù R Í S Þ (P Ç R) Í (Q Ç S))
dom.r Ç ~(dom.r.~R Ç dom.r.~Q) Í dom.r Ç ~dom.r.(~R Ç ~Q)
º(deMorgan)
dom.rÇ (~dom.r.~R È ~dom.r.~Q) Í dom.rÇ ~dom.r.~(R È Q)
º(distribute Ç over È)
(dom.rÇ ~dom.r.~R) È (dom.rÇ ~dom.r.~Q) Í dom.rÇ ~dom.r.~(R È Q)
º(definition of set difference)
(dom.r - dom.r.~R) È (dom.r - dom.r.~Q) Í dom.r - dom.r.~(R È Q)
º(Theorem 2)
cond.r.R È cond.r.Q Í cond.r.~(R È Q)
End of Proof
Theorem 6: r is a function Þ cond.r.R È cond.r.Q = cond.r.(P È Q)
(prove that LHS = RHS)
cond.r.R È cond.r.Q
=(Theorem 2)
(dom.r – dom.r.~R) È (dom.r – dom.r.~Q)
=((R – P) È (R – Q) = (R – (P Ç Q))
(dom.r – (dom.r.~R Ç dom.r.~Q)
=(Relations Part 4 Theorem 4, given)
(dom.r – dom.r.(~R Ç ~Q)
=(deMorgan)
(dom.r – dom.r.~(R È Q)
=(Theorem 2)
cond.r.(R È Q)
End of Proof
Theorem 7: r is a function Þ dom.r.R = cond.r.R
(prove by showing LHS Þ RHS)
r is a function
Þ(Relations Part 4 Theorem 10, given)
dom.r.R = dom.r.R - dom.r.~R
º(Definition 1)
dom.r.R = cond.r.R
End of Proof
Theorem 8: (dom.r.R Ç dom.r.~R = Æ) º
dom.r.R = cond.r.R
(dom.r.R Ç dom.r.~R = Æ) º
(dom.r.R = dom.r.R – dom.r.~R)
º(Definition 1)
dom.r.R = cond.r.R
End of Proof
Theorem 9: Identity, cond.I.R = R
(prove by showing LHS = RHS)
cond.I.R
=(definition of cond.I.R)
dom.I.R – dom.I.~R
=(Identity Relation Theorem 1)
R - ~R
=(P – Q = P Ç ~Q)
R Ç ~~R
=(~~P = P)
R Ç R
=(idempotency of Ç)
R
End of Proof
Theorem 10: ran.r.(cond.r.R) Í R
(Prove LHS Í RHS by applying the theorem true Þ P º P)
(reflexive property of Í)
ran.r.(cond.r.R) Í ran.r.(cond.r.R)
º(Theorem 2)
ran.r.(cond.r.R) Í ran.r.(dom.r - dom.r.~R)
º(Definition of set difference)
ran.r.(cond.r.R) Í ran.r.(dom.r Ç ~dom.r.~R)
Þ(P Ç Q Í Q, Relations Part 2 Theorem 6, Transitive property of Í
ran.r.(cond.r.R) Í ran.r.(~dom.r.~R)
º(definition of Í)
("x|x Î ran.r.(cond.r.R): x Î ran.r.(~dom.r.~R))
º(Part 1 definition of ran.r.R)
("x|x Î ran.r.(cond.r.R):
x Î {b|($a|:a r b Ù a Î ~dom.r.~R):b})
º(definition of Î)
("x|x Î ran.r.(cond.r.R):
($b|($a|:a r b Ù a Î ~dom.r.~R):b=x))
º(Membership of set complement)
("x|x Î ran.r.(cond.r.R):
($b|($a|:a r b ÙØ(a Î dom.r.~R)):b=x))
º(Part 1 definition of dom.r.~R)
("x|x Î ran.r.(cond.r.R):
($b|($a|:a r b Ù
Ø(a Î {c|($d|:c r d Ù d Î ~R):c})):b=x))
º(definition of Î)
("x|x Î ran.r.(cond.r.R):
($b|($a|:a r b Ù
Ø($c|($d|:c r d Ù d Î ~R):c=a)):b=x))
º(one point rule)
("x|x Î ran.r.(cond.r.R):
($b|($a|:a r b Ù
Ø($d|:a r d Ù d Î ~R)):b=x))
º(one point rule)
("x|x Î ran.r.(cond.r.R):
($a|:a r x ÙØ($d|:a r d Ù d Î ~R)))
º(DeMorgan)
("x|x Î ran.r.(cond.r.R):
($a|:a r x Ù ("d|:Ø(a r d) Ú d Ï ~R)))
º(definition of Ï, P = ~~P)
("x|x Î ran.r.(cond.r.R):
($a|:a r x Ù ("d|:Ø(a r d) Ú d Î R)))
º(Øp Ú q º p Þ q)
("x|x Î ran.r.(cond.r.R):
($a|:a r x Ù ("d|:a r d Þ d Î R)))
Þ(instantiation, d := x)
("x|x Î ran.r.(cond.r.R):
($a|:a r x Ù a r x Þ x Î R))
Þ(modus ponens, monotonicity of $)
("x|x Î ran.r.(cond.r.R):($a|: x Î R))
º(distribute Ù over $)
("x|x Î ran.r.(cond.r.R): x Î R Ù ($a|:true))
Þ(weakening, monotonicity of ")
("x|x Î ran.r.(cond.r.R): x Î R )
º(definition of Í)
ran.r.(cond.r.R) Í 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.