Linear $GLP$-algebras and their elementary theories

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. (paper)