Hereditary undecidability of some theories of finite structures

Using a result of Gurevich and Lewis on the word problem for finite semigroups, we give short proofs that the following theories are hereditarily undecidable: (1) finite graphs of vertex-degree at most 3; (2) finite nonvoid sets with two distinguished permutations; (3) finite-dimensional vector spaces over a finite field with two distinguished endomorphisms.

Undecidable Lt theories of topological abelian groups

We prove the hereditary undecidability of the Lt theories of:(1) torsion-free Hausdorff topological abelian groups;(2) locally pure Hausdorff topological abelian groups.

On the undecidability of finite planar cubic graphs

In the March, 1971 issue of this Journal [1] a paper of ours was published purporting to prove the hereditary undecidability of the first-order theory of finite planar graphs. The proof presented there contains an error which is unfortunately “unfixable” by the methods of that paper. The theorem however is true and we demonstrate here a generalization to finite cubic (exactly three edges at each vertex) planar graphs. The method involves coding the halting problem for a Turing machine into the theory of these graphs by considering special printouts of computations. Let us first consider a discussion of the aforementioned mistake and see what can be learned from it.By a graph we will mean a nonempty set V of points together with a set I of unordered pairs of points of V. Each point i = {u, v) ∈ I is an edge of A graph is called finite if ∣V∣ is finite. A graph is said to be planar iff it can be embedded in the plane (i.e., drawn in the plane so that no two edges intersect).In the earlier paper the method of proof was a semantic embedding of certain binary relations into finite planar graphs. The essential idea was, for a given relation, to let the vertices of the graph interpret the field of the relation and the edges represent the related pairs. This method works for arbitrary graphs, but in the planar case has two main difficulties.

On the undecidability of finite planar graphs

In this paper we demonstrate the hereditary undecidability of finite planar graphs. In §2 we introduce the preliminary logical notions used and outline the Rabin–Scott method of semantic embedding. This method is illustrated in §3 by proving the undecidability of the theory of two finite equivalence relations of a special type. In §4 we give a proof of the main theorem by embedding these equivalence relations into finite planar graphs.The basic idea is first to form a graph which codes a pair of these relations and then to take a representative of it and “squish” it to the plane. This “squishing” requires the introduction of crossings; and edges of the original graph become paths in the new one. To distinguish the original edges we place two different types of “diamonds” about crossing points. We can then uncode our new graphs to recover the equivalence relations by means of simple first-order incidence properties.