Representability is not decidable for finite relation algebras

We prove that there is no algorithm that decides whether a finite relation algebra is representable.

Representability of a finite relation algebra $\mathcal A$ is determined by playing a certain two player game $G({\mathcal A})$ over `atomic $\mathcal A$-networks'. It can be shown that the second player in this game has a winning strategy if and only if $\mathcal A$ is representable.

Let $\tau$ be a finite set of square tiles, where each edge of each tile has a colour. Suppose $\tau$ includes a special tile whose four edges are all the same colour, a colour not used by any other tile. The tiling problem we use is this: is it the case that for each tile $T \in \tau$ there is a tiling of the plane ${\mathbb Z}\times {\mathbb Z}$ using only tiles from $\tau$ in which edge colours of adjacent tiles match and with $T$ placed at $(0,0)$? It is not hard to show that this problem is undecidable.

From an instance of this tiling problem $\tau$, we construct a finite relation algebra $RA(\tau)$ and show that the second player has a winning strategy in $G(RA(\tau))$ if and only if $\tau$ is a yes-instance. This reduces the tiling problem to the representation problem and proves the latter's undecidability.