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

 

      rÍ A´B, sÍ 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)

º(definition of 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}))

º(definition of dom.s.R)

      ("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})

º(definition of dom.r.(dom.s.R))

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

=(definition of 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)

=(Definition of cond.s.R)

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

=(definition of set difference)

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

=(Condition Theorem 4)

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

=(Definition of cond.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

=(Definition of cond.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.