Math Notes Theory of Relations Part 4

 

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.

 

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)

(AB BA 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.