arXiv · 2403.17153
Unification in subsystem J$_2$ of provability logic GLB
Abstract
We generalize methods, developed by S. Ghilardi, and apply them to a subsystem J$_2$ of bimodal provability logic GLB. We describe projective formulas in J$_2$ in terms of Kripke semantics and prove that logic J$_2$ has finitary unification type. As an application, we show that admissibility problem for J$_2$ is decidable.
Explore related subjects
Keep this discovery
N. V. Lukashov. 2024-03-25. Unification in subsystem J$_2$ of provability logic GLB. https://arxiv.org/abs/2403.17153
Cite the original work for its findings. Save a collection to share your selection of sources.