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

TL;DR

This paper analyzes the computational complexity of provability in the logic GLP, showing PSPACE-completeness for variable-free formulas and polynomial-time solvability when certain modalities are excluded.

Contribution

It establishes the complexity classifications of the GLP-provability problem for different classes of variable-free formulas, including PSPACE-completeness and PTIME results.

Findings

GLP-provability for variable-free formulas is PSPACE-complete

For formulas excluding modalities <n>, the problem is in PTIME

Complexity varies with the modal structure of formulas

Abstract

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^n_0 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^n_0 is in PTIME.