Linear $\mathrm{GLP}$-algebras and their elementary theories

The polymodal provability logic $\mathrm{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 $\mathrm{GLP}$-algebra generated by the constants $\mathbf{0}$, $\mathbf{1}$ is decidable [1]. For every positive integer $n$ we solve the corresponding question for the logics $\mathrm{GLP}_n$ that are the fragments of $\mathrm{GLP}$ with $n$ modalities. We prove that the elementary theory of the free $\mathrm{GLP}_n$-algebra generated by the constants $\mathbf{0}$, $\mathbf{1}$ is decidable for all $n$. We introduce the notion of a linear $\mathrm{GLP}_n$-algebra and prove that all free $\mathrm{GLP}_n$-algebras generated by the constants $\mathbf{0}$, $\mathbf{1}$ are linear. We also consider the more general case of the logics $\mathrm{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.