Expressive Power
The metamathematics of RA are discussed at length in Tarski and Givant (1987), and more briefly in Givant (2006).
RA consists entirely of equations manipulated using nothing more than uniform replacement and the substitution of equals for equals. Both rules are wholly familiar from school mathematics and from abstract algebra generally. Hence RA proofs are carried out in a manner familiar to all mathematicians, unlike the case in mathematical logic generally.
RA can express any (and up to logical equivalence, exactly the) first-order logic (FOL) formulas containing no more than three variables. (A given variable can be quantified multiple times and hence quantifiers can be nested arbitrarily deeply by "reusing" variables.) 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. Because RA can express Peano arithmetic and set theory, Gödel's incompleteness theorems apply to it; RA is incomplete, incompletable, and undecidable. (N.B. The Boolean algebra fragment of RA is complete and decidable.)
The representable relation algebras, forming the class RRA, are those relation algebras isomorphic to some relation algebra consisting of binary relations on some set, and closed under the intended interpretation of the RA operations. 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. In 1950, Roger Lyndon proved the existence of equations holding in RRA that did not hold in RA. Hence the variety generated by RRA is a proper subvariety of the variety RA. In 1955, Alfred Tarski showed that RRA is itself a variety. In 1964, Donald Monk showed that RRA has no finite axiomatization, unlike RA which is finitely axiomatized by definition.
Read more about this topic: Relation Algebra
Famous quotes containing the words expressive and/or power:
“It’s very expressive of myself. I just lump everything in a great heap which I have labeled “the past,” and, having thus emptied this deep reservoir that was once myself, I am ready to continue.”
—Zelda Fitzgerald (1900–1948)
“All goes to show that the soul in man is not an organ, but animates and exercises all the organs; is not a function, like the power of memory, of calculation, of comparison, but uses these as hands and feet; is not a faculty, but a light, is not the intellect or the will, but the master of the intellect and the will; is the background of our being, in which they lie,—an immensity not possessed and that cannot be possessed.”
—Ralph Waldo Emerson (1803–1882)