On the positive fragment of the polymodal provability logic GLP
Evgenij Vladimirovich Dashkov · Mathematical Notes · 2012
The fragment of the polymodal provability logic GLP in the language with connectives ┬, Λ, and 〈 n 〉 for all n ∈ ω is considered. For this fragment, a deductive system is constructed, a Kripke semantics is proposed, and a polynomial bound for the complexity of a decision procedure is obtained.