[3][4][5][6] This is a system of modal logic with the "necessity" operators [0],[1],[2],…, understood as a natural series of incrementally weak provability predicates for Peano arithmetic.
In "The polymodal logic of provability"[7] Japaridze proved the arithmetical completeness of this system, as well as its inherent incompleteness with respect to Kripke frames.
GLP has been extensively studied by various authors during the subsequent three decades, especially after Lev Beklemishev, in 2004,[8] pointed out its usefulness in understanding the proof theory of arithmetic (provability algebras and proof-theoretic ordinals).
[9] In the same paper he showed that, on the condition of the 1-completeness of the underlying arithmetical theory, predicate provability logic with non-iterated modalities is recursively enumerable.
[citation needed] Japaridze has cast a similar (and also never answered) challenge to intuitionistic logic,[25] criticizing it for lacking a convincing semantical justification the associated constructivistic claims, and for being incomplete as a result of "throwing out the baby with the bath water".
The positive (negation-free) propositional fragment of intuitionistic logic, however, has been proven to be complete with respect to the computability-logic semantics.
Among Japaridze's contributions is the elaboration of a series of systems of (Peano) arithmetic based on computability logic, named "clarithmetics".
[30][31][32] These include complexity-oriented systems (in the style of bounded arithmetic) for various combinations of time, space and amplitude complexity classes.