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

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)

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

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

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}

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})

("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)

("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|(\$c|:a r c Ù c Î Q):a})

º(definition of Î)

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

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

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

# Ù (\$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))

("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)

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))

("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)))

("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))

("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)

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

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.