Undecidability of the elementary theory of the semilattice of GLP-words
Fedor Nikolaevich Pakhomov · Sbornik Mathematics · 2012
The Lindenbaum algebra of Peano arithmetic PA can be enriched by the n-consistency operators which assign, to a given formula, the statement that the formula is compatible with the theory PA extended by the set of all true Pi(n)-sentences. In the Lindenbaum algebra of PA, a lower semilattice is generated from 1 by the n-consistency operators. We prove the undecidability of the elementary theory of this semilattice and the decidability of the elementary theory of the subsemilattice (of this semilattice) generated by the 0-consistency and 1-consistency operators only.