Math Notes – Theory of Relation Compositions

In the following theorems, all relations are subsets of the cross-product B´C, so an implicit assumption in all theorems is

A´B, 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.

A reference to a theorem from part 1, 2 or 3 is noted.  If there is no reference to part 1,2  or part 3, then the theorem reference is on this page.

Definition 1: r·s = {r,s | (\$y|:<r,y> ÎrÙ <y,s> Îs):<r,s>}

Theorem 1: a r·s b º (\$y|:a r y Ù y s b)

(prove LHS º RHS)

a r·s b

º(Set membership)

<a,b> Îr·s

º(definition 1)

<a,b> Î {r,s | (\$y|r r y Ù y s s):<r,s>}

º(definition of Î)

(\$r,s | (\$y|r r y Ù y s s):<r,s>=<a,b>)

º(One point rule)

(\$y|a r y Ù y s b)

# End of Proof

Theorem 2: dom.(r·s).R = dom.r.(dom.s.R)

(Reflexive property of set =)

dom.(r·s).R = dom.(r·s).R

º(definition of set =)

("x |: x Î dom.(r·s).R º x Î dom.(r·s).R)

("x |: x Î dom.(r·s).R º

# x Î {a|(\$b|:a (r·s) b Ù b Î R):a})

º(definition of Î)

("x |: x Î dom.(r·s).R º

# (\$a|(\$b|:a (r·s) b Ù b Î R):a=x))

º(Theorem 1)

("x |: x Î dom.(r·s).R º

(\$a|(\$b|:(\$y|: a r y Ù y s b)Ù b Î R):a=x))

º(one point rule)

("x |: x Î dom.(r·s).R º

(\$b|:(\$y|: x r y Ù y s b)Ù b Î R))

º(distribute Ù over \$)

("x |: x Î dom.(r·s).R º

(\$b|:(\$y|: x r y Ù y s b  Ù b Î R)))

º(Variable interchange)

("x |: x Î dom.(r·s).R º

(\$y|:(\$b|: x r y Ù y s b  Ù b Î R)))

º(distribute Ù over \$)

("x |: x Î dom.(r·s).R º

(\$y|: x r y Ù (\$b|: y s b Ù b Î R)))

º(one point rule)

("x |: x Î dom.(r·s).R º

(\$y|: x r y Ù (\$a|(\$b|: a s b Ù b Î R):a=y)))

º(definition of Î)

("x |: x Î dom.(r·s).R º

(\$y|: x r y Ù y Î {a|(\$b|: a s b Ù b Î R):a}))

("x |: x Î dom.(r·s).R º

(\$y|: x r y Ù y Î dom.s.R))

º(one point rule)

("x |: x Î dom.(r·s).R º

(\$a|(\$y|: a r y Ù y Î dom.s.R):a=x))

º(definition of Î)

("x |: x Î dom.(r·s).R º

x Î {a|(\$y|: a r y Ù y Î dom.s.R):a})

("x |: x Î dom.(r·s).R º

x Î dom.r.(dom.s.R))

º(definition of set equality)

dom.(r·s).R = dom.r.(dom.s.R)

End of Proof

Theorem 3: dom.(r·s) = dom.r.(dom.s)

(Part 1 Theorem 7, given r·sÎ A´B)

dom.(r·s) = dom.(r·s).B

º(Theorem 2)

dom.(r·s) = dom.r.(dom.s.B)

º(Part 1 Theorem 7, given r·sÎ A´B)

dom.(r·s) = dom.r.(dom.s)

End of Proof

Theorem 4: cond.(r·s).R = dom.r.(dom.s.R) - dom.r.(dom.s.~R)

(Prove LHS = RHS)

cond.(r·s).R

dom.(r·s).R – dom.(r·s).~R

=(Theorem 2)

dom.r.(dom.s.R) – dom.r.(dom.s.~R)

End of Proof

Theorem 5: cond.r.(cond.s.R) Í cond.(r·s).R

(Prove LHS Í RHS)

cond.r.(cond.s.R)

cond.r.(dom.s.R – dom.s.~R)

=(definition of set difference)

cond.r.(dom.s.R Ç ~dom.s.~R)

cond.r.(dom.s.R) Ç cond.r.(~dom.s.~R)

(dom.r.(dom.s.R) - dom.r.(~dom.s.R))

Ç (dom.r.(~dom.s.~R) - dom.r.(~~dom.s.~R))

=(definition of set difference)

(dom.r.(dom.s.R) Ç ~dom.r.(~dom.s.R))

Ç (dom.r.(~dom.s.~R) Ç ~dom.r.(~~dom.s.~R))

=(~~P = P)

(dom.r.(dom.s.R) Ç ~dom.r.(~dom.s.R))

Ç (dom.r.(~dom.s.~R) Ç ~dom.r.(dom.s.~R))

Í(P Ç Q Í P)

dom.r.(dom.s.R) Ç ~dom.r.(dom.s.~R)

=(Theorem 2)

dom.(r·s).R Ç ~dom.(r·s).~R

=(definition of set difference)

dom.(r·s).R - dom.(r·s).~R

cond.(r·s).R

End of Proof

Theorem 6: (dom.s.R Ç dom.s.~R = Æ Ù

dom.r.(dom.s.R) Ç dom.r.(~dom.s.R) = Æ) Þ

cond.(r·s).R Í cond.r.(cond.s.R)

(given dom.s.R Ç dom.s.~R = ÆÙ dom.r.(dom.s.R) Ç dom.r.(~dom.s.R) = Æ,

prove that LHS Í RHS)

cond.(r·s).R

=(Theorem 4)

dom.r.(dom.s.R) - dom.r.(dom.s.~R)

=(property of set difference)

dom.r.(dom.s.R) Ç ~dom.r.(dom.s.~R)

Í(P Ç Q Í P)

dom.r.(dom.s.R)

=(Condition Theorem 8, given)

cond.r.(cond.s.R)

End of Proof

Corollary to Theorem 6: (dom.s.R Ç dom.s.~R = ÆÙ

dom.r.(dom.s.R) Ç dom.r.(~dom.s.R) = Æ) Þ

cond.(r·s).R = cond.r.(cond.s.R)

(given dom.s.R Ç dom.s.~R = ÆÙ dom.r.(dom.s.R) Ç dom.r.(~dom.s.R) = Æ,

prove that LHS = RHS)

(Theorem 6, given)

cond.(r·s).R Í cond.r.(cond.s.R)

(Theorem 5)

cond.r.(cond.s.R) Í cond.(r·s).R

º(identity of Ù, P Í Q Ù Q Í P º P = Q)

cond.(r·s).R = cond.r.(cond.s.R)

End of Proof

Theorem 7: r is a function Ù s is a function Þ

cond.r.(cond.s.R) = cond.(r·s).R

(given r is a function Ùs is a function, Prove LHS = RHS)

cond.r.(cond.s.R)

=(Condition Theorem 7, given)

dom.r.(dom.s.R)

=(theorem 2)

dom.(r·s).R

=(Condition Theorem 7, the composite of two functions is a function)

cond.(r·s).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.