Elementary properties of free lattices II: Decidability of the universal theory

We continue our work on the model theory of free lattices, solving two of the main open problems from our first paper on the subject. Our main result is that the universal (existential) theory of infinite free lattices is decidable. Our second main result is a proof that finitely generated free lattices are positively distinguishable, as for each $n\ge 1$ there is a positive $\mathrm{\exists }\mathrm{\forall }$-sentence true in ${\mathbf{F}}_n$ and false in ${\mathbf{F}}_{n+1}$. Finally, we show that free lattices are first-order rigid in the class of finitely generated projective lattices, and that a projective lattice has the same existential (universal) theory of an infinite free lattice if and only if it has breadth $>4$ (i.e., a single existential sentence is sufficient).