Math Notes – Theory of Relations – Part 1

 

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

 

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 ", $,

(pÞq) Þ (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Í A´B Þ dom.r.R = dom.r.(R Ç B)

(given rÍ A´B, 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Í A´B º 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Í A´B Þ dom.r.B = dom.r

(given rÍ A´B, 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Í A´B Ù 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Í A´B Ù B Í R Þ dom.r.R = dom.r

(given rÍ A´B Ù 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Í A´B Þ  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.