Elementary properties of free lattices III: Undecidability of the full theory

TL;DR

The paper resolves the decidability status of the full first-order theory of infinite free lattices by showing that, for every cardinal $\kappa \ge 3$, the theory of the free lattice $\mathbf F_\kappa$ is undecidable. The authors reduce the known undecidable $\forall\exists$-theory of finite nice bipartite graphs/posets to lattice theories through a translation that uses a FO formula $\Psi(v)$ and a canonical-form analysis of joinands, yielding a lattice sentence $\varphi_*$ that captures the poset property $\varphi$. Central to the argument are canonical joinands, the $E$-relation, and the embedding techniques that connect poset configurations to lattice-theoretic witnesses. A Whitman-based embedding then propagates the undecidability from $\mathbf F_3$ to all $\mathbf F_\kappa$ with $\kappa \ge 3$, thereby resolving major open questions about the model theory of free lattices and their finitely generated cases.

Abstract

In [6] we proved that the universal theory of infinite free lattices is (algorithmically) decidable, leaving open the problem of decidability of the full theory of an (infinite) free lattice. We solve this problem by proving that, for every cardinal $κ\geq 3$, the first-order theory of the free lattice $\mathbf{F}_κ$ is undecidable.

Figures (1)

• Figure 1: Example of embedding of a bipartite poset $Q$ into $F_8$.

Theorems & Definitions (25)

• Theorem 1.1
• Definition 2.1
• Definition 2.2
• Definition 2.4
• Remark 2.5
• Definition 2.6
• Corollary 2.7
• Lemma 3.1
• Lemma 3.2
• Lemma 3.3