On the complexity of the closed fragment of Japaridze's provability logic

الأصل · EN

We consider well-known provability logic GLP. We prove that the GLP-provability problem for variable-free polymodal formulas is PSPACE-complete. For a number n, let Lⁿ₀ denote the class of all polymodal variable-free formulas without modalities <n>, <n+1>,.... We show that, for every number n, the GLP-provability problem for formulas from Lⁿ₀ is in PTIME.