Math Notes Theory of Relations Part 3

 

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

 

      r AB

 

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

 

Theorem 1: Given P r, ("a,b|arb a P: b ran.r.P)

(Reflexive property of )

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

(definition of , definition of complement)

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

(definition of ran.r.P, definition of )

      ("b|b ran.r.P: (b {x|($a|:arx aP):x})

(definition of )

      ("b|b ran.r.P: ($x|($a|:arx aP):b=x))

(one-point rule)

      ("b|b ran.r.P: ($a|:arb aP))

(deMorgan)

      ("b|b ran.r.P: ("a|:(arb aP)))

(nesting)

      ("a,b|b ran.r.P: (arb aP))

(trading)

      ("a,b|arb aP:b ran.r.P)

End of Proof

 

Theorem 2: Given P r, ("a,b|:r P ran.r.P)

(Theorem 1)

      ("a,b|arb a P: b ran.r.P)

(trading)

      ("a,b|:arb a P b ran.r.P)

(equivalent predicates)

      ("a,b|:r P ran.r.P)

End of Proof

 

Theorem 3: ran.r.P R ("a,b|:arb aP bR)

(prove LHS RHS)

      ran.r.P R

(definition of )

      ("b|b ran.r.P: b R)

(identity of , Theorem 1)  

      ("b|bran.r.P: bR) ("a,b|:arb aP bran.r.P)

(nesting)

      ("b|bran.r.P: bR) ("a|aP:("b|:arb bran.r.P)

(trading)

      ("b|:bran.r.P bR) ("a|aP:("b|:arb bran.r.P))

(distribute over ")

       ("a|aP:("b|:bran.r.P bR arb bran.r.P))

(transitivity of )

       ("a|aP:("b|:arb bR))

(trading)

       ("a|aP:("b|arb : bR))

(nesting)

       ("a,b|aP arb : bR))

(trading)

       ("a,b|:aP arb bR))

End of Proof

 

Theorem 4: ("a,b|:arb a P b R) ran.r.P R

(Prove the contrapositive)

      (ran.r.P R)

(definition of )

      ("b|b ran.r.P: b R)

(identity of , Theorem 1)  

      ("b|bran.r.P: bR) ("a,b|:arb aP bran.r.P)

(trading)

      ("b|bran.r.P: bR) ("a,b|arb aP :bran.r.P)

(("x|:P)($x:P), monotonicity of )

      ("b|bran.r.P: bR) ($a,b|arb aP : bran.r.P)

(deMorgan)

      ($b|bran.r.P: bR) ($a,b|arb aP : bran.r.P)

(nesting)

      ($b|bran.r.P: bR) ($a|aP:($b|arb : bran.r.P)

(trading)

      ($b|:bran.r.P bR) ($a|aP:($b|:arb bran.r.P)

(distribute over ")

       ($a|aP:($b|:bran.r.P bR arb bran.r.P)

(a b a, monontonicity of $)

       ($a|aP:($b|:bR arb)

(nesting)

       ($a,b|aP:bR arb)

(trading)

       ($a,b|aP arb:bR)

(deMorgan)

       ("a,b|aP arb:bR)

(trading)

       ("a,b|>:aP arb bR)

End of Proof

     

Theorem 5: ("a,b|:arb a P b R) ran.r.P R

(Theorem 3)

ran.r.P R ("a,b|:r P R)

(Theorem 4, identity of )

ran.r.P R ("a,b|:arb aP bR)

("a,b|:arb aP bR) ran.r.P R

((ab ba) ab)

ran.r.P R ("a,b|:arb aP bR)

End of Proof

 

Corollary: ("a,b|aP: arb b R) ran.r.P R

(Theorem 5)

("a,b|:arb a P b R) ran.r.P R

(shunting)

("a,b|:aP (arb b R)) ran.r.P R

(trading)

("a,b|aP: arb b R) ran.r.P R

End of Proof

 

Theorem 6: ("a,b|:r P R) ran.r.P R

(Theorem 5)

("a,b|:arb a P b R) ran.r.P R

(equivalent predicates)

("a,b|:r P R) ran.r.P R

End of Proof

 

Theorem 7: ("a|:P R)P R

(Prove that RHS LHS)

      P R

(Identity Relation Theorem 3)

      ran.I.P R

(Theorem 5)

("a,b|:aIb a P b R)

((a b c) (a (b c)), symmetry of )  

("a,b|: a P (aIb b R))

(trading)

("a,b| a P:(aIb b R))

(nesting)

("a| a P:("b|:aIb b R))

(trading)

("a| a P:("b|aIb :b R))

(definition of identity relation)

("a| a P:("b|a=b :b R))

(one point rule)

("a| a P:a R)

(trading)

("a|:a Pa R)

(equivalent predicates)

("a|:P 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.