Two axiom systems for relation algebras.
Chris Brink · Notre Dame Journal of Formal Logic · 1979
It has long been known that, in principle, conversion can be eliminated from the primitive operations of a relation algebra.In [2], and more recently in [1], it is shown that r" is the largest element x such that x r' ^ e τ (r w is the converse of r, e is the identity element, the accent denotes complementation, and the semicolon denotes relative product).This characterization of r w is in fact not a necessary ingredient in the elimination of conversion as a primitive operation.In Definition 2 below conversion is eliminated by axiomatizing a relation algebra in terms of the operation r";s (just as inverses may be eliminated from the definition of a group by using the operation a~l-b).Definition 3 goes one better: it eliminates not only conversion but also complementation, by using the operation r^ s*.Definition 1, taken from [2], is used as standard; it is shown that Definitions 2 and 3 are each equivalent to Definition 1.Also the independence of the axioms in Definitions 2 and 3 is established.Definition 1 A relation algebra is an algebra {R, +, ', , w , e) satisfying the following axioms: Al (R, +, ') is a Boolean algebra A2 (r;s);t=r;(s;t) A3 (r + s);t = r t + s t A4 r e = r A5 r wu = r A6 (r+s) u = r w + s v A7 (r;sΓ = s> w A8 r w ;(r ; s)' + s'=:s'.Note that e = e e = e e = (e e) = e = e by A4, A5 and A7.Also, using the same axioms, we get