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

F. N. Pakhomov

Izvestiya. Mathematics , Tome 80 (2016) no. 6, pp. 1159-1199

Résumé

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.

Détail

Keywords: provability logics, free algebras, elementary theories, Japaridze logic.
Mots-clés : modal algebras