Math Notes – Identity Relations

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.

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.

Axiom 1: a I b º a = b

Theorem 1: dom.I.R = R

(prove LHS = RHS)

(reflexive property of =)

dom.I.R = dom.I.R

º(Definition of set equality)

("x|x Î dom.I.R º x Î dom.I.R)

º(Definition of dom.I.R)

("x|x Î dom.I.R º x Î {a|(\$b|: a I b Ù b Î R):a})

º(definition of Î)

("x|x Î dom.I.R º (\$a|(\$b|: a I b Ù b Î R):a=x))

º(Axiom 1)

("x|x Î dom.I.R º (\$a|(\$b|: a=b Ù b Î R):a=x))

º(one point rule)

("x|x Î dom.I.R º (\$b|: x=b Ù b Î R))

("x|x Î dom.I.R º (\$b| x=b:b Î R))

º(one point rule)

("x|x Î dom.I.R º x Î R)

º(Definition of set equality)

dom.I.R = R

End of Proof

Theorem 2: I = I-1

("a,b|:a =b º a = b)

º(Symmetry of =)

("a,b|:a =b º b = a)

º(Axiom 1)

("a,b|:a I b º b I a)

º(Î of I)

("a,b|:<a,b> ÎIº <b,a> ÎI)

º(definition of inverse)

("a,b|:<a,b> ÎIº <a,b> ÎI-1)

º(("x|z Îr:P) º ("a,b|<a,b> Îr :P[z := <a,b>]))

("x|: x ÎIº x ÎI-1)

º(Definition of set equality)

I = I-1

End of Proof

Theorem 3: ran.I.P = P

(Theorem 1)

dom.I.P = P

º(Theorem 2)

dom.I-1.P = P

ran.I.P = P

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.