Unification in subsystem J$_2$ of provability logic GLB
Logic
2024-03-27 v1
Abstract
We generalize methods, developed by S. Ghilardi, and apply them to a subsystem J of bimodal provability logic GLB. We describe projective formulas in J in terms of Kripke semantics and prove that logic J has finitary unification type. As an application, we show that admissibility problem for J is decidable.
Keywords
Cite
@article{arxiv.2403.17153,
title = {Unification in subsystem J$_2$ of provability logic GLB},
author = {N. V. Lukashov},
journal= {arXiv preprint arXiv:2403.17153},
year = {2024}
}
Comments
In Russian, 20 pages