Computer-aided investigations of relation algebras
Peter Jipsen, Bjàrni Jónsson · 1992
This dissertation is a self-contained study of Boolean algebras with a residuated binary operator and a unit element. Such algebras are called unital residuated Boolean algebras, or ur-algebras, and they are natural generalizations of relation algebras. Some background material about Boolean algebras with operators and about discriminator algebras is followed by an algorithm that may be used to construct finite ur-algebras satisfying a finite set of universal sentences or to prove that the sentences have no models. This algorithm has been implemented as a computer program (described briefly in the appendix). The lattice of varieties of ur-algebras, which includes the lattice of varieties of relation algebras, is investigated. It is shown that the variety of all commutative associative ur-algebras is a discriminator variety, whereas this is not the case for the variety of all Euclidean associative ur-algebras. Several varieties that satisfy only weak associativity conditions are shown to have decidable equational theories. On the other hand the equational theory of any variety that contains all totally symmetric relation algebras and is contained in the variety of all commutative relation algebras is undecidable. The main results are about varieties of finite height. A relation algebra is said to be neat if it satisfies the universal sentence $x\le x\circ x$ or $x(x\circ x) = 0.$ It is shown that there are exactly 11 finitely generated join irreducible varieties of height 2 in the lattice of subvarieties of the variety generated by all neat symmetric relation algebras. However there is also an example of a nonfinitely generated variety of height 2, and in the lattice of subvarieties of a certain finitely based variety this example is the only variety of height 2. Finally, it is shown that two equivalence elements in a simple symmetric relation algebra generate a finite subalgebra, and that there exist nonrepresentable absolute retracts in the variety of all symmetric relation algebras. These two results and the results about varieties of height 2 were proved with the assistance of the computer program mentioned above.