关于 GLP-代数的初等理论

存在一种多模态可证性逻辑 $GLP$。我们考虑该逻辑的推广：逻辑 $GLP_{\alpha}$，其中 $\alpha$ 遍历线性有序集并充当模态算子索引集的角色。我们考虑对应于这些多模态逻辑的模态代数簇。我们证明了对于所有有限序数 $n$，自由 $\emptyset$-生成的 $GLP_{n}$-代数的初等理论是可判定的。