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

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

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

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

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

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

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

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

(given 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: 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

# <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. dom.r

º(Corollary to Theorem 8)

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

("x| : x Ï dom. x Î dom.r.R Ú x Î dom.r.~R)

º(symmetry and associativity of Ú)

("x| : (x Ï dom. x Î dom.r.~R) Ú x Î dom.r.R)

º(DeMorgan)

("x| : Ø(x Î dom. x Ï dom.r.~R) Ú x Î dom.r.R)

("x| x Î dom. 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. ~dom.r.~R Í ~dom.r.~R

Þ(P Í Q Ù R Í S Þ (P Ç R) Í (Q Ç S))

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