# On families of finite graphs with undecidable first-order theory

It is well known that the first order theory of graphs (i.e., an irreflexive and symmetric "edge" relation on a set) is undecidable. The same holds for the first order theory of finite graphs.

I am interested to know about subclasses of finite graphs such that its first-order theory is also known to be undecidable. Any suggestion about where to look for this kind of results? I am particularly interested on any resource (url, survey paper, etc.) gathering results of this kind.

One example of the kind of results I search for is that the first order theory of all finite bipartite graphs with at least three elements is known to be undecidable. Any other subclasses which are also known undecidable?

-
Suggestion 1: Try a citation index using the classic papers for a start. Suggestion 2: There is a small industry proving results in finite undecidability (which classes of finite structures of some type have undecidable f.o. theories); researchers include Jeong, McKenzie, and Valeriote among others. If you are willing to spend half an hour, you might collect references from their papers (or even results) to see which ones might consider subfamilies of finite graphs. Other names include Burris and Idziak. Gerhard "Ask Me About System Design" Paseman, 2011.11.05 –  Gerhard Paseman Nov 5 '11 at 17:40

There are three classic references. Janiczak, A. Undecidability of some simple formalized theories. Fund. Math. 40, (1953). 131–139. It is proved, in particular,that the theory of finite sets with two equivalence relations is undecidable. That result, in turn, was used to prove undecidability of many other theories (by interpreting there the theory of two equivalence relations) including the elementary theory of finite graphs (see, Lavrov, I. A. The effective non-separability of the set of identically true formulae and the set of finitely refutable formulae for certain elementary theories. Algebra i Logika Sem. 2 1963 no. 1, 5–18 and Eršov, Ju. L. New examples of undecidable theories. Algebra i Logika Sem. 5 1966 no. 5, 37–47.) As far as I know this is still the main tool to prove undecidability of elementary theories of finite structures. More modern results about theories of finite graphs (say $k$-regular graphs, etc.), and different methods of proofs, can be found here: Willard, Ross Hereditary undecidability of some theories of finite structures. J. Symbolic Logic 59 (1994), no. 4, 1254–1262.