On Elementary Theories of GLP-Algebras

TL;DR

This paper studies generalized polymodal provability logics called GLP-algebras, proving that the elementary theories of free finite-parameter versions are decidable, advancing understanding of their algebraic and logical properties.

Contribution

It introduces and analyzes the elementary theories of free GLP-algebras with finite parameters, establishing their decidability.

Findings

Elementary theories of free GLP_n-algebras are decidable for all finite n.

Generalizations of GLP to indexed modalities are systematically studied.

Decidability results contribute to the understanding of polymodal provability logic algebraic structures.

Abstract

There is a polymodal provability logic $GLP$. We consider generalizations of this logic: the logics $GLP_{\alpha}$, where $\alpha$ ranges over linear ordered sets and play the role of the set of indexes of modalities. We consider the varieties of modal algebras that corresponds to the polymodal logics. We prove that the elementary theories of the free $\emptyset$-generated $GLP_{n}$ -algebras are decidable for all finite ordinals $n$.