The strength of the Grätzer-Schmidt theorem (Q506962)

The authors analyze the computable and proof theoretic content of notions from lattice theory. They prove that the set of indices of computable lattices that are complete is a \(\Pi^1_1\)-complete set, and prove a similar result for lattices that are algebraic. They construct a computable lattice with a \(\Pi^1_1\)-complete set of compact elements, a computable distributive lattice with a \(\Pi^0_3\)-complete set of compact elements, and show that these results are optimal. Using the framework of reverse mathematics, they show that the Grätzer-Schmidt theorem (every algebraic lattice is isomorphic to the congruence lattice of an algebra) is provable in \(\Pi^1_1\)-\(\text{CA}_0\), while the restriction of the theorem to distributive lattices is provable in \(\text{ACA}_0\), but not in \(\text{RT}^2_2 + \text{WKL}_0\). This work extends and corrects content in an earlier conference paper by the first and the third author [Lect. Notes Comput. Sci. 5635, 59--67 (2009; Zbl 1268.03058)].