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 A is determined by playing a certain two player game G(A) over 'atomic A-networks'. It can be shown that the second player in this game has a winning strategy if and only if 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 is an element of tau there is a tiling of the plane Z x 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.