Math Notes Theory of Relations Part 2

 

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, 3, or 4 is noted.  If there is no reference to part 1,2,3, or part 4 then the theorem reference is on this page.

 

Definition 1: (inverse) <a,b> r <b,a> r-1

 

Theorem 1: ran.r.P = dom.(r-1).P

(Reflexive property of set =)

      ran.r.P = ran.r.P

(definition of set =)

      ("x |: x ran.r.P x ran.r.P)

(definition of ran.r.P)

      ("x |: x ran.r.P x {b |($a |:<a, b> r a P):b})

(definition of )

      ("x |: x ran.r.P ($b |($a |:<a, b> r a P):b=x))

(definition of inverse)

      ("x |: x ran.r.P ($b |($a |:<b, a> r-1 a P):b=x))

(definition of )

      ("x |: x ran.r.P x {b |($a |:<b, a> r-1 a P):b})

(definition of dom.r.P)

      ("x |: x ran.r.P x dom.(r-1).P)

(definition of set =)

      ran.r.P = dom.(r-1).P

End of Proof

 

Theorem 2: ran.(r-1).P = dom.(r).P

(Reflexive property of set =)

      ran.{r-1).P = ran.(r-1).P

(definition of set =)

      ("x |: x ran.{r-1).P x ran.(r-1).P)

(definition of ran.(r-1).P)

      ("x |: x ran.(r-1).P x {b |($a |:<a, b> r-1 a P):b})

(definition of )

      ("x |: x ran.(r-1).P ($b |($a |:<a, b> r-1 a P):b=x))

(definition of inverse)

      ("x |: x ran.(r-1).P ($b |($a |:<b, a> r a P):b=x))

(definition of )

      ("x |: x ran.(r-1).P x {b |($a |:<b, a> r a P):b})

(definition of dom.r.P)

      ("x |: x ran.(r-1).P x dom.r.P)

(definition of set =)

      ran.(r-1).P = dom.r.P

End of Proof

 

Theorem 3: dom.((r-1)-1).P = dom.r.P

(Prove LHS = RHS)

dom.((r-1)-1).P

=(Theorem 1)

ran.(r-1).P

=(Theorem 2)

dom.r.P

End of Proof

 

Theorem 4: ran.((r-1)-1).P = ran.r.P

(Prove LHS = RHS)

ran.((r-1)-1).P

=(Theorem 2)

dom.(r-1).P

=(Theorem 1)

ran.r.P

End of Proof

 

Theorem 5: ran.r. =

(Part 1 Theorem 1)
      dom.(
r-1). =

(Theorem 1)

      ran.r. =

End of Proof

 

Theorem 6: P Q ran.r.P ran.r.Q

(Part 1 Theorem 2)

      P Q dom.(r-1).P dom.(r-1).Q

(Theorem 1)

      P Q ran.r.P ran.r.Q

End of Proof

 

 

Theorem 7: P Q ~ran.r.~P ~ran.r.~Q

(Part 1 Theorem 3)

      P Q ~dom.(r-1).~P ~dom.(r-1).~Q

(Theorem 1)

      P Q ~ran.r.~P ~ran.r.~Q

End of Proof

 

 

Theorem 8: ran.r.(P Q) = ran.r.P ran.r.Q

(Part 1 Theorem 4)

      dom.(r-1).(P Q) = dom.(r-1).P dom.(r-1).Q

(Theorem 1)

      ran.r.(P Q) = ran.r.P ran.r.Q

End of Proof

 

 

Theorem 9: ran.r.(P Q) (ran.r.P ran.r.Q)

(Part 1 Theorem 5)

      dom.(r-1).(P Q) (dom.(r-1).P dom.(r-1).Q)

(Theorem 1)

      ran.r.(P Q) (ran.r.P ran.r.Q)

End of Proof

 

Theorem 10: r AB ran.r.R = ran.r.(R A)

(Prove LHS RHS)

      r AB

(property of inverse)

r-1 BA
(Part 1 Theorem 6)

      dom.(r-1).R = dom.(r-1).(R A)

(Theorem 1)

      ran.r.R = ran.r.(R A)

End of Proof

 

Theorem 11: r AB ran.r.A = ran.r

(given r AB, Prove LHS = RHS)

(definition of ran.r.A)

ran.r.A = {b|($a|:a r b a A):b}

(Definition of set equality)

      ("x|x ran.r.A x {b|($a|:a r b a A):b})

(definition of )

      ("x|x ran.r.A ($b|($a|:a r b a A):x=b))

(r AB a r b a A)

      ("x|x ran.r.A ($b|($a|:a r b true):x=b))

(identity of )

      ("x|x ran.r.A ($b|($a|:a r b):x=b))

(definition of )

      ("x|x ran.r.A x {b|($a|:a r b):b})

(definition of ran.r)

("x|x ran.r.A x ran.r)

(Definition of set equality)

      ran.r.A = ran.r

End of Proof

 

Corollary: r AB ran.r = dom.(r-1)

(given r AB, show LHS = RHS)

(Theorem 11)

ran.r = ran.r.A

(Theorem 1)

ran.r = dom.(r-1).A

(r-1 BA, Part 1 Theorem 7)

ran.r = dom.(r-1)

End of Proof

 

Theorem 12: r AB A P ran.r.P = ran.r

(given r AB A P, prove LHS = RHS)

(property of inverse)

      r-1 BA A P

(Part 1 Theorem 8)

      dom.r-1.P = dom.r-1

(Theorem 1)

      ran.r.P = ran.r

End of Proof

 

Corollary: r AB   ran.r.(R ~R) = ran.r

(given r AB, prove LHS = RHS)

(property of inverse)

      r-1 BA

(Corollary to Part 1 Theorem 8)

      dom.(r-1).(R ~R) = dom.r-1

(Theorem 1)

      ran.r.(R ~R) = ran.r

End of Proof

 

Theorem 13: y ran.r.{x} x r y

(prove LHS RHS)

      y ran.r.{x}

(Definition of ran.r.{x})

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

(Definition of )

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

(One point rule)

     ($a|:a r y a {x})

(Singleton Set Theorem 1)

     ($a|:a r y a = x)

(trading)

     ($a|a r y :a = x)

(One point rule)

     x r y

End of Proof

 

Theorem 14: P ~dom.r ran.r.P =

      P ~dom.r

(definition of )

      ("a|aP: a~dom.r)

(definition of ~)

      ("a|aP: adom.r)

(definition of dom.r)

      ("a|aP: a{x:A |($b:B |: x r b):x})

(definition of )

      ("a|aP: ($x|($b |: x r b):x=a))

(one point rule)

      ("a|aP: ($b |: a r b))

(DeMorgan)

      ("a|aP: ("b |: (a r b)))

(trading)

      ("a|:aP("b |: (a r b)))

(distribute over ")

      ("a|: ("b |: aP(a r b)))

(exchange variables)

      ("b|: ("a |: aP(a r b)))

(DeMorgan, twice)

      ("b|: ($a |: aP (a r b)))

(DeMorgan)

      ($b|: ($a |: aP (a r b)))

(instance ($x|:), contrapositive)

      ($a |: aP (a r x))

(one point rule)

      ($b|($a |: aP (a r x):b=x)

(definition of )

      (x {b|($a |: aP (a r x):b})

(definition of ran.r.P)

      (x ran.r.P)

(definition of )

      ran.r.P =

End of Proof

 

Theorem 15: P dom.r P dom.r.(ran.r.P)

(Prove LHS RHS)

      P dom.r

(PP, PQPRPQR)

      P Pdom.r

(definition of )

      ("s|s P: s Pdom.r)

(definition of )

      ("s|s P: s P s dom.r)

(definition of dom.r)

      ("s|s P: s P s {a|($b|a r b):a})

(definition of )

      ("s|s P: s P ($a|($b|a r b):a=s))

( distributes over $)

      ("s|s P: ($a|($b|a r b s P):a=s))

( is idempotent)

      ("s|s P: ($a|($b| a r b a r b s P):a=s))

(One point rule)

      ("s|s P: ($b| s r b s r b s P))

(existence, P ($x|P))

      ("s|s P: ($b| s r b ($c|:c r b c P)))

(One point rule)

      ("s|s P: ($b| s r b ($d|($c|:c r d c P):d=b)))

(definition of )

      ("s|s P: ($b| s r b b {d|($c|:c r d c P):d}))

(Part 1 definition of ran.r)

      ("s|s P: ($b| s r b b ran.r.P))

(One point rule)

      ("s|s P: ($a|($b| a r b b ran.r.P):a=s))

(definition of )

      ("s|s P: s {a|($b| a r b b ran.r.P):a})

(definition of dom.r.P)

      ("s|s P: s dom.r.(ran.r.P))

(definition of )

      P dom.r.(ran.r.P)

End of Proof

 

Theorem 16: P ran.r P ran.r.(dom.r.P)

(Theorem 15)

P dom.(r-1) P dom.(r-1).(ran.(r-1).P)

(Theorem 1)

P dom.(r-1) P ran.r.(ran.(r-1).P)

(Theorem 2)

P dom.(r-1) P ran.r.(dom. r.P)

(Corollary to Theorem 11)

P ran.r P ran.r.(dom. r.P)

End of Proof

 

References:

 

Brettler, Eli 1999, Course notes and comments from M1090 and M2090 math and logic courses,  http://www.math.yorku.ca/Who/Faculty/Brettler/menu.html

 

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.