Math Notes Theory of Relations Part 1

 

In the following theorems, all relations are subsets of the cross-product BC, 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.

 

 

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

Definition 2. dom.r = {a:A |($b:B |: a r b):a}

Definition 3.ran.r.p = {b:B |($a:A |: a r b a P):b}

Definition 4.dom.r.Q = {a:A |($b:B |: a r b b Q):a}

Definition 5. Identity: I = {s,t | s = t:<s,t>}

 

Any temporary variables introduced in the theorems are assumed to be distinct.  That is, the temporary variables do not as free variables in any other expression.

 

Theorem 1: dom.r. =

(prove LHS = RHS by applying the theorem true P P)

(reflexive property of =)

      dom.r. = dom.r.

(definition of set =)

      ("x|: x dom.r.ƺ x dom.r.)

(definition 4 of dom.r.)

("x|: x dom.r.ƺ x {a|($b|:a r b b ):a})

(Definition of )

("x|: x dom.r.ƺ ($a|($b|:a r b b ):x=a})

(property of )

("x|: x dom.r.ƺ ($a|($b|:a r b false):x=a})

(zero of )

("x|: x dom.r.ƺ ($a|($b|:false):x=a})

(($x|P:false) false)

("x|: x dom.r.ƺ ($a|false:x=a})

(empty range of $)

("x|: x dom.r.ƺ false)

(property of )

      ("x|: x dom.r.ƺ x )

(definition of set =)

      dom.r. =

End of Proof

 

Theorem 2: R Q dom.r.R dom.r.Q

(given R Q, prove that P P LHS RHS,

This will prove LHS RHS by applying the theorem true P P)

(reflexive property of )

      dom.r.R dom.r.R

(definition of )

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

(definition of dom.r.R)

      ("x|x dom.r.R : x {a|($b|:a r b b R):a})

(Definition of )

("x|x dom.r.R : ($a|($b|:a r b b R):x=a))

(trading in $)

("x|x dom.r.R : ($a|x=a:($b|:a r b b R)))

(R Q, definition of , monotonicity of ", $,

(pq) (r p r q)))

("x|x dom.r.R : ($a|x=a:($b|:a r b b Q)))

(trading in $)

("x|x dom.r.R : ($a|($b|:a r b b Q):x=a))

(Definition of )

("x|x dom.r.R : x {a|($b|:a r b b Q):a})

(definition of dom.r.Q)

      ("x|x dom.r.R : x dom.r.Q)

(definition of )

      dom.r.R dom.r.R

End of Proof

 

Theorem 3: R Q ~dom.r.~R ~dom.r.~Q

(Prove by showing LHS RHS)

      R Q

(Set Contrapositive)

      ~Q ~R

(Theorem 2)

      dom.r.~Q dom.r.~R

(Set Contrapositive)

      ~dom.r.~R ~dom.r.~Q

End of Proof

 

Theorem 4: dom.r.(P Q) = dom.r.P dom.r.Q

(reflexive property of =)

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

(Definition of set equality)

      ("x|x dom.r.(P Q) x dom.r.(P Q))

(Definition of dom.r.(P Q))

      ("x|x dom.r.(P Q) x {a|($b|:a r b b (P Q)):a})

(definition of )

      ("x|x dom.r.(P Q) ($a|($b|:a r b b (P Q)):x=a))

(trading in $)

      ("x|x dom.r.(P Q) ($a|x=a:($b|:a r b b (P Q))))

(Definition of )

("x|x dom.r.(P Q) ($a|x=a:($b|:a r b (b P b Q))))

(Distribute over )

("x|x dom.r.(P Q)

($a|x=a:($b|:(a r b b P) (a r b b Q))))

(Distribute over $)

("x|x dom.r.(P Q)

($a|x=a:($b|:a r b b P) ($b|:a r b b Q)))

(Distribute over $)

("x|x dom.r.(P Q)

($a|x=a: ($b|:a r b b P)) ($a|x=a:($b|:a r b b Q)))

(trading in $)

("x|x dom.r.(P Q)

($a|($b|:a r b b P:b):x=a) ($a|($b|:a r b b Q):x=a))

(definition of )

("x|x dom.r.(P Q)

x {a|($b|:a r b b P:b):x} x {a|($b|:a r b b Q:b):x})

(Definition of dom.r.P)

("x|x dom.r.(P Q) x dom.r.P x dom.r.Q)

(Definition of )

("x|x dom.r.(P Q) x (dom.r.P dom.r.Q))

(Definition of set equality)

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

End of Proof

 

Theorem 5: dom.r.(P Q) (dom.r.P dom.r.Q)

(prove LHS RHS by applying the theorem true P P)

((P Q) P and theorem 2)

      dom.r.(P Q) dom.r.P

((P Q) Q and theorem 2)

      dom.r.(P Q) dom.r.Q

(identity of )

      dom.r.(P Q) dom.r.P dom.r.(P Q) dom.r.Q

(P Q R S (P R) (P R)

      (dom.r.(P Q) dom.r.(P Q)) (dom.r.P dom.r.Q)

(idempotency of )

      dom.r.(P Q) (dom.r.P dom.r.Q)

End of Proof

 

Theorem 6: r AB dom.r.R = dom.r.(R B)

(given r AB, prove LHS = RHS)

(definition of dom.r.R)

dom.r.R = {a|($b|:a r b b R):a}

(Definition of set equality)

      ("x|x dom.r.R x {a|($b|:a r b b R):a})

(definition of )

      ("x|x dom.r.R ($a|($b|:a r b b R):x=a))

(r AB x r y y B)

      ("x|x dom.r.R ($a|($b|:a r b b R b B):x=a))

(definition of )

      ("x|x dom.r.R ($a|($b|:a r b b R B):x=a))

(definition of )

      ("x|x dom.r.R x {a|($b|:a r b b R B):x=a})

(definition of dom.r.R)

("x|x dom.r.R x dom.r.(R B))

(Definition of set equality)

dom.r.R = dom.r.(R B)

End of Proof

 

Theorem 7: r AB dom.r.B = dom.r

(given r AB, prove LHS = RHS)

(definition of dom.r.B)

dom.r.B = {a|($b|:a r b b B):a}

(Definition of set equality)

      ("x|x dom.r.B x {a|($b|:a r b b B):a})

(definition of )

      ("x|x dom.r.B ($a|($b|:a r b b B):x=a))

(r AB a r b b B)

      ("x|x dom.r.B ($a|($b|:a r b true):x=a))

(identity of )

      ("x|x dom.r.B ($a|($b|:a r b):x=a))

(definition of )

      ("x|x dom.r.B x {a|($b|:a r b):a})

(definition of dom.r)

("x|x dom.r.B x dom.r)

(Definition of set equality)

      dom.r.B = dom.r

End of Proof

 

Theorem 8: r AB B R dom.r.R = dom.r

(given r AB B R prove LHS = RHS)

      dom.r.R

=(Theorem 6)

      dom.r.(R B)

=( B R (B R R B = B))

      dom.r.B

=(Theorem 7)

      dom.r

End of Proof

 

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

(B (U = R ~R), Theorem 8)

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

End of Proof

 

Theorem 9: dom.r.R dom.r

(prove LHS RHS)

(R R ~R, Theorem 2)

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

(Theorem 8)

      dom.r.R dom.r

End of Proof

 

Theorem 10: <x,y> r x dom.r

(prove LHS RHS)

      <x,y> r

(p[a:=x] ($a|p:a=x)

($b|<x,b> r:b=y)

(monotonicity of $)

($b|<x,b> r)

(p[a:=x] ($a|p:a=x)

($a|($b|<a,b> r):a=x)

(definition of )

x {a|($b|<a,b> r):a}

(definition of dom.r)

x dom.r

End of Proof

 

Theorem 11: (dom.r - dom.r.~R) dom.r.R

(prove by showing LHS RHS)

(Reflexive property of )

      dom.r dom.r

(Corollary to Theorem 8)

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

(Definition of )

      ("x| x dom.r : x dom.r.(R ~R))

(Theorem 4)

      ("x| x dom.r : x (dom.r.R dom.r.~R))    

(Definition of )

      ("x| x dom.r : x dom.r.R x dom.r.~R)  

(Trading in ")

      ("x| : x dom.r x dom.r.R x dom.r.~R)

(symmetry and associativity of )

      ("x| : (x dom.r x dom.r.~R) x dom.r.R)

(DeMorgan)

      ("x| : (x dom.r x dom.r.~R) x dom.r.R)

(Trading in ")

      ("x| x dom.r x dom.r.~R : x dom.r.R)

(Set difference)

      ("x| x (dom.r - dom.r.~R) : x dom.r.R)

(Definition of )

      dom.r - dom.r.~R dom.r.R

End of Proof

 

Theorem 12: (dom.r - dom.r.~R) (dom.r.R dom.r.~R)

(Prove by showing LHS RHS by applying the theorem true P P)

(Theorem 11)

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

(P Q = P ~Q, P ~Q ~Q)

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

(identity of )

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

(P Q R S (P R) (Q S))

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

(idempotency of )

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

(definition of set difference)

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

End of Proof

 

Theorem 13: (dom.r.R - dom.r.~R) (dom.r dom.r.~R)

(Theorem 9)

      dom.r.R dom.r

(reflexive property of )

      ~dom.r.~R ~dom.r.~R

(identity of )

      dom.r.R dom.r ~dom.r.~R ~dom.r.~R

(P Q R S (P R) (Q S))

      dom.r.R ~dom.r.~R dom.r ~dom.r.~R

(definition of set difference)

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

End of Proof

 

Theorem 14: (dom.r.R - dom.r.~R) = (dom.r dom.r.~R)

(theorem 12)

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

(theorem 13)

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

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

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

End of Proof

 

Theorem 15: (dom.r.R dom.r.~R = )

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

(prove LHS RHS)

       dom.r.R dom.r.~R =

(P Q = ƺ P ~Q)

dom.r.R ~dom.r.~R

(P Q P = P Q)

dom.r.R = dom.r.R ~dom.r.~R

(definition of set difference)

dom.r.R = dom.r.R - dom.r.~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.