Abstract

Conjecture (1) of [Ma83] is confirmed here by the following result: if $3 \leq \alpha < \omega$, then there is a finite relation algebra of dimension α, which is not a relation algebra of dimension α + 1. A logical consequence of this theorem is that for every finite α ≥ 3 there is a formula of the form $S \subseteq T$ (asserting that one binary relation is included in another), which is provable with α + 1 variables, but not provable with only α variables (using a special sequent calculus designed for deducing properties of binary relations)