The equational form of relation algebra treated here was developed by Alfred Tarski and his students, starting in the 1940s.
[2] Converse and composition distribute over disjunction: B10 is Tarski's equational form of the fact, discovered by Augustus De Morgan, that A • B ≤ C−
The following table shows how many of the usual properties of binary relations can be expressed as succinct RA equalities or inequalities.
Chapter 3.2 of Suppes (1960) contains fewer results, presented as ZFC theorems and using a notation that more resembles that of this entry.
Hence RA proofs are carried out in a manner familiar to all mathematicians, unlike the case in mathematical logic generally.
)[citation needed] Surprisingly, this fragment of FOL suffices to express Peano arithmetic and almost all axiomatic set theories ever proposed.
Hence RA is, in effect, a way of algebraizing nearly all mathematics, while dispensing with FOL and its connectives, quantifiers, turnstiles, and modus ponens.
It is easily shown, e.g. using the method of pseudoelementary classes, that RRA is a quasivariety, that is, axiomatizable by a universal Horn theory.
An RA is a Q-relation algebra (QRA) if, in addition to B1-B10, there exist some A and B such that (Tarski and Givant 1987: §8.4): Essentially these axioms imply that the universe has a (non-surjective) pairing relation whose projections are A and B.
The work of DeMorgan and Peirce came to be known mainly in the extended and definitive form Ernst Schröder gave it in Vol.
Principia Mathematica drew strongly on Schröder's RA, but acknowledged him only as the inventor of the notation.
In 1912, Alwin Korselt proved that a particular formula in which the quantifiers were nested four deep had no RA equivalent.