Linear $ \mathrm{GLP}$-algebras and their elementary theories
Fedor Nikolaevich Pakhomov · Izvestiya Mathematics · 2016
The polymodal provability logic GLP was introduced by Japaridze in 1986. It is the provability logic of certain chains of provability predicates of increasing strength. Every polymodal logic corresponds to a variety of polymodal algebras. Beklemishev and Visser asked whether the elementary theory of the free GLP-algebra generated by the constants 0, 1 is decidable [1]. For every positive integer n we solve the corresponding question for the logics GLP(n) that are the fragments of GLP with n modalities. We prove that the elementary theory of the free GLP(n)-algebra generated by the constants 0, 1 is decidable for all n. We introduce the notion of a linear GLP(n)-algebra and prove that all free GLP(n)-algebras generated by the constants 0, 1 are linear. We also consider the more general case of the logics GLP(alpha) whose modalities are indexed by the elements of a linearly ordered set alpha : we define the notion of a linear algebra and prove the latter result in this case.