Math Notes – Theory of Relations – Part 4

 

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

 

A reference to a theorem from part 1, part 2, or part 3 is noted.  If there is no reference to an earlier part, then the refered theorem is on this page.

 

Definition 1: A relation r is a function º

 ("b,c,c’ | b r c Ù b r c’ : c = c’) 

 

 

Theorem 1: s Î ran.r.{x} º x r s

(prove by showing LHS º RHS)

      s Î ran.r.{x}

º(definition of ran.r.{x})

      s Î {b|($a|:a r b Ù a Î {x}):b}

º(definition of Î)

($b|($a|:a r b Ù a Î {x}):b=s)

º(Singleton Set Theorem 1)

($b|($a|:a r b Ù a = x):b=s)

º(trading, one point rule)

($b|x r b: b=s)

º(trading, one point rule)

x r s

End of Proof

 

Theorem 2: r is a function Ù ran.r.{x} ¹ÆÞ

      ran.r.{x} is a singleton set

(given r is a function Ù ran.r.{x} ¹Æ,

let s Î ran.r.{x}, prove that ran.r.{x} = {s})

 

(part 1. show {s} Í ran.r.{x})

(given)

s Î ran.r.{x}

º(Singleton Set Theorem 2)

s Í ran.r.{x}

End of Part 1 Proof

 

(part 2. prove ran.r.{x} Í {s})

(proof uses the principal (true Þ P) º P)

(reflexive property of Þ)

      ("t|:t Î ran.r.{x} Þ t Î ran.r.{x})

º(trading)

      ("t|t Î ran.r.{x}: t Î ran.r.{x})

º(theorem 1)

      ("t|t Î ran.r.{x}: x r t)

º(given, theorem 1, identity of Ù)

      ("t|t Î ran.r.{x}: x r t Ù x r s)

Þ(given, axiom 1, monotonicity of ")

      ("t|t Î ran.r.{x}: t = s)

º(Singleton Set Theorem 1)

      ("t|t Î ran.r.{x}: t Î {s})

º(definition of Í)

      ran.r.{x} Í {s}

End of Part 2 Proof

End of Proof

 

Theorem 3: r is a function Þ dom.r.P Ç dom.r.Q Í dom.r.(P Ç Q)

(given r is a function prove LHS Í RHS by applying the theorem true Þ P º P)

(reflexive property of Í)

      dom.r.P Ç dom.r.Q Í dom.r.P Ç dom.r.Q

º(definition of Í)

      ("x | x Î dom.r.P Ç dom.r.Q : x Î dom.r.P Ç dom.r.Q)

º(definition of Ç)

      ("x | x Î dom.r.P Ç dom.r.Q : x Î dom.r.P Ù x Î dom.r.Q)

º(definition of dom.r.P, quantifying variable c is distinct from b)

("x | x Î dom.r.P Ç dom.r.Q :

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

Ù x Î {a|($c|:a r c Ù c Î Q):a})

º(definition of Î)

("x | x Î dom.r.P Ç dom.r.Q :

($a|($b|:a r b Ù b Î P):x=a)

Ù ($a|($c|:a r c Ù c Î Q):x=a))

º(trading in $)

("x | x Î dom.r.P Ç dom.r.Q :

($a|x=a:($b|:a r b Ù b Î P))

Ù ($a|x=a:($c|:a r c Ù c Î Q)))

º(one point rule, x is distinct)

("x | x Î dom.r.P Ç dom.r.Q :

($b|: x r b Ù b Î P) Ù ($c|: x r c Ù c Î Q))

º(distribute Ù over $, c is distinct from b)

("x | x Î dom.r.P Ç dom.r.Q :

($b|: x r b Ù b Î P Ù ($c|: x r c Ù c Î Q)))

º(distribute Ù over $, b is distinct from c)

("x | x Î dom.r.P Ç dom.r.Q :

($b|:($c|:x r b Ù b Î P Ù x r c Ù c Î Q)))

Þ(r is a function Þ b = c)

("x | x Î dom.r.P Ç dom.r.Q :

($b|:($c|: x r b Ù b Î P Ù x r b Ù b Î Q)))

º(symmetric, reflexive properties of Ù

("x | x Î dom.r.P Ç dom.r.Q :

($b|:($c|: x r b Ù b Î P Ù b Î Q)))

º(definition of Ç)

("x | x Î dom.r.P Ç dom.r.Q :

($b|: ($c|: x r b Ù b Î P Ç Q)))

º(Identity of Ú)

("x | x Î dom.r.P Ç dom.r.Q :

($b|:($c|: (x r b Ù b Î P Ç Q) Ú false)))

º(distribute Ú over $)

("x | x Î dom.r.P Ç dom.r.Q :

($b|:(x r b Ù b Î P Ç Q) Ú ($c|:false)))

º(($x|P:false) º false)

("x | x Î dom.r.P Ç dom.r.Q :

($b|:(x r b Ù b Î P Ç Q) Ú false))

º(Identity of Ú)

("x | x Î dom.r.P Ç dom.r.Q :($b|: x r b Ù b Î P Ç Q))

º(one point rule, trading)

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

º(definition of Î)

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

º(definition of dom.r.P)

("x | x Î dom.r.P Ç dom.r.Q :x Î dom.r.(P Ç Q))

º(definition of Í)

dom.r.P Ç dom.r.Q Í dom.r.(P Ç Q))

End of Proof

 

Theorem 4: r is a function Þ dom.r.P Ç dom.r.Q = dom.r.(P Ç Q)

(part 1 theorem 5)

      dom.r.(P Ç Q) Í (dom.r.P Ç dom.r.Q)

(Theorem 3)

      dom.r.P Ç dom.r.Q Í dom.r.(P Ç Q)

º(identity of Ù, P Í Q Ù Q Í P º P = Q)

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

End of Proof

 

Theorem 5: r is a function Þ ran.r.(dom.r.R) Í R

(proof uses the principal (true Þ P) º P)

(given r is a function, prove LHS Í RHS)

(reflexive property of Í)

      ran.r.(dom.r.R) Í  ran.r.(dom.r.R)

º(definition of Í)

      ("y|y Î ran.r.(dom.r.R): y Πran.r.(dom.r.R))

º(definition of ran.r.(dom.r.R))

      ("y|y Î ran.r.(dom.r.R):

 y Π{b|($a|a r b Ù aÎ dom.r.R):b})

º(definition of Î)

      ("y|y Î ran.r.(dom.r.R):

  ($b|($a|a r b Ù aÎ dom.r.R):b=y))

º(trading, one point rule)

      ("y|y Î ran.r.(dom.r.R):

($a|a r y Ù aÎ dom.r.R))

º(definition of dom.r.R)

      ("y|y Î ran.r.(dom.r.R):

($a|a r y Ù aÎ {c|crd Ù d Î R:c}))

º(definition of Î)

      ("y|y Î ran.r.(dom.r.R):

($a|a r y Ù ($c|crd Ù d Î R:c=a)))

º(trading, one point rule)

      ("y|y Î ran.r.(dom.r.R):

($a|a r y Ù ard Ù d Î R))

Þ(definition 1, given)

      ("y|y Î ran.r.(dom.r.R):

($a|a r y Ù ard Ù d Î R Ù y=d))

º(trading, one point rule)

      ("y|y Î ran.r.(dom.r.R):

a r y Ù ary Ù y Î R )

º(a Ù b Þ b, monotonicity of ")

      ("y|y Î ran.r.(dom.r.R): y Î R )

º(definition of Í)

     ran.r.(dom.r.R) Í R

End of Proof

 

Theorem 6: r is a function Ù R Í ran.r Þ ran.r.(dom.r.R) = R

(given r Is a function Ù R Í ran.r, prove LHS = RHS)

(given, Theorem 5)

      ran.r.(dom.r.R) Í R

º(given, Relations Part 2 Theorem 16, identity of Ù)

      ran.r.(dom.r.R) Í R Ù R Í ran.r.(dom.r.R)

º(AÍB Ù BÍA º A = B)

      ran.r.(dom.r.R) = R

End of Proof

 

 

Theorem 7: r is a function Þ dom.r.R Ç dom.r.~R = Æ

(given r is a function,  theorem 4)

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

=(contradiction)

      dom.r.R Ç dom.r.~R = dom.r.Æ

=(Part 1 Theorem 1)

      dom.r.R Ç dom.r.~R = Æ

End of Proof

 

Theorem 8: r is a function Þdom.r.R Í ~dom.r.~R

(prove LHS Þ  RHS)

     r is a function

Þ(Theorem 6)

dom.r.R Ç dom.r.~R = Æ

º(P Ç Q = ƺ P Í ~Q)

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

End of Proof

 

Theorem 9: r is a function Þdom.r.~R Í ~dom.r.R

(prove LHS Þ  RHS)

     r is a function

Þ(Theorem 7)

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

º(Contrapositive)

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

º(~~P = P)

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

End of Proof

 

Theorem 10: r is a function Þ dom.r.R = dom.r.R - dom.r.~R

(prove LHS Þ  RHS)

     r is a function

Þ(Theorem 7)

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

º(P Í Q º P Ç Q = P)

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

º(property 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.