Math Notes Theory of Relation Compositions

 

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

 

      r AB, s AB

 

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: rs = {r,s | ($y|:<r,y> r <y,s> s):<r,s>}

 

Theorem 1: a rs b ($y|:a r y y s b)

(prove LHS RHS)

a rs b

(Set membership)

<a,b> rs

(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.(rs).R = dom.r.(dom.s.R)

(Reflexive property of set =)

      dom.(rs).R = dom.(rs).R

(definition of set =)

      ("x |: x dom.(rs).R x dom.(rs).R)

(definition of dom.(rs).R)

      ("x |: x dom.(rs).R

 x {a|($b|:a (rs) b b R):a})

(definition of )

      ("x |: x dom.(rs).R

 ($a|($b|:a (rs) b b R):a=x))

(Theorem 1)

      ("x |: x dom.(rs).R

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

(one point rule)

      ("x |: x dom.(rs).R

          ($b|:($y|: x r y y s b) b R))

(distribute over $)

      ("x |: x dom.(rs).R

          ($b|:($y|: x r y y s b b R)))

(Variable interchange)

      ("x |: x dom.(rs).R

          ($y|:($b|: x r y y s b b R)))

(distribute over $)

      ("x |: x dom.(rs).R

          ($y|: x r y ($b|: y s b b R)))

(one point rule)

      ("x |: x dom.(rs).R

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

(definition of )

      ("x |: x dom.(rs).R

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

(definition of dom.s.R)

      ("x |: x dom.(rs).R

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

(one point rule)

      ("x |: x dom.(rs).R

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

(definition of )

      ("x |: x dom.(rs).R

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

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

      ("x |: x dom.(rs).R

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

(definition of set equality)

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

End of Proof

 

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

(Part 1 Theorem 7, given rs AB)

      dom.(rs) = dom.(rs).B

(Theorem 2)

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

(Part 1 Theorem 7, given rs AB)

      dom.(rs) = dom.r.(dom.s)

End of Proof

 

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

(Prove LHS = RHS)

      cond.(rs).R

=(definition of cond.(rs).R)

      dom.(rs).R dom.(rs).~R

=(Theorem 2)

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

End of Proof

 

Theorem 5: cond.r.(cond.s.R) cond.(rs).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.(rs).R ~dom.(rs).~R

=(definition of set difference)

      dom.(rs).R - dom.(rs).~R

=(Definition of cond.s.R)

cond.(rs).R

End of Proof

 

Theorem 6: (dom.s.R dom.s.~R =

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

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

(Theorem 5)

cond.r.(cond.s.R) cond.(rs).R

(identity of , P Q Q P P = Q)  

cond.(rs).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.(rs).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.(rs).R

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

cond.(rs).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.