Japaridze's polymodal logic

The language of GLP extends that of the language of classical propositional logic by including the infinite series [0],[1],[2],... of “necessity” operators. Their dual “possibility” operators <0>,<1>,<2>,... are defined by <n>p = ¬[n]¬p.

The axioms of GLP are all classical tautologies and all formulas of one of the following forms:

• [n](p → q) → ([n]p → [n]q)
• [n]([n]p → p) → [n]p
• [n]p → [n+1]p
• <n>p → [n+1]<n>p

And the rules of inference are:

• From p and p → q conclude q
• From p conclude [0]p

Consider a “sufficiently strong” first-order theory T such as Peano Arithmetic PA. Define the series T₀,T₁,T₂,... of theories as follows:

• T₀ is T
• T_n+1 is the extension of T_n through the additional axioms ∀xF(x) for each formula F(x) such that T_n proves all of the formulas F(0), F(1), F(2),...

For each n, let Pr_n(x) be a natural arithmetization of the predicate “x is the Gödel number of a sentence provable in T_n.

A realization is a function * that sends each nonlogical atom a of the language of GLP to a sentence a* of the language of T. It extends to all formulas of the language of GLP by stipulating that * commutes with the Boolean connectives, and that ([n]F)* is Pr_n(‘F*’), where ‘F*’ stands for (the numeral for) the Gödel number of F*.

An arithmetical completeness theorem[1] for GLP states that a formula F is provable in GLP if and only if, for every interpretation *, the sentence F* is provable in T.

The above understanding of the series T₀,T₁,T₂,... of theories is not the only natural understanding yielding the soundness and completeness of GLP. For instance, each theory T_n can be understood as T augmented with all true ∏_n sentences as additional axioms. George Boolos showed[2] that GLP remains sound and complete with analysis (second-order arithmetic) in the role of the base theory T.

GLP has been shown[1] to be incomplete with respect to any class of Kripke frames.

A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of GLP. GLP is complete with respect to the class of all GLP-spaces.[3]

The problem of being a theorem of GLP is PSPACE-complete. So is the same problem restricted to only variable-free formulas of GLP.[4]

GLP, under the name GP, was introduced by Giorgi Japaridze in his PhD thesis "Modal Logical Means of Investigating Provability" (Moscow State University, 1986) and published two years later[1] along with (a) the completeness theorem for GLP with respect to its provability interpretation (Beklemishev subsequently came up with a simpler proof of the same theorem[5]) and (b) a proof that Kripke frames for GLP do not exist. Beklemishev also conducted a more extensive study of Kripke models for GLP.[6] Topological models for GLP were studied by Beklemishev, Bezhanishvili, Icard and Gabelaia.[3][7] The decidability of GLP in polynomial space was proven by I. Shapirovsky,[8] and the PSPACE-hardness of its variable-free fragment was proven by F. Pakhomov.[4] Among the most notable applications of GLP has been its use in proof-theoretically analyzing Peano arithmetic, elaborating a canonical way for recovering ordinal notation up to ɛ₀ from the corresponding algebra, and constructing simple combinatorial independent statements (Beklemishev [9]).

An extensive survey of GLP in the context of provability logics in general was given by George Boolos in his book “The Logic of Provability”.[10]

• L. Beklemishev, "Provability algebras and proof-theoretic ordinals, I". Annals of Pure and Applied Logic 128 (2004), pp. 103–123.
• L. Beklemishev, J. Joosten and M. Vervoort, "A finitary treatment of the closed fragment of Japaridze's provability logic". Journal of Logic and Computation 15 (2005), No 4, pp. 447–463.
• L. Beklemishev, “Kripke semantics for provability logic GLP”. Annals of Pure and Applied Logic 161, 756–774 (2010).
• L. Beklemishev, G. Bezhanishvili and T. Icar, “On topological models of GLP”. Ways of proof theory, Ontos Mathematical Logic, 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, pp. 133–153.
• L. Beklemishev, “On the Craig interpolation and the fixed point properties of GLP”. Proofs, Categories and Computations. S. Feferman et al., eds., College Publications 2010. pp. 49–60.
• L. Beklemishev, “Ordinal completeness of bimodal provability logic GLB”. Lecture Notes in Computer Science 6618 (2011), pp. 1–15.
• L. Beklemishev, “A simplified proof of arithmetical completeness theorem for provability logic GLP”. Proceedings of the Steklov Institute of Mathematics 274 (2011), pp. 25–33.
• L. Beklemishev and D. Gabelaia, “Topological completeness of provability logic GLP”. Annals of Pure and Applied Logic 164 (2013), pp. 1201–1223.
• G. Boolos, "The analytical completeness of Japaridze's polymodal logics". Annals of Pure and Applied Logic 61 (1993), pp. 95–111.
• G. Boolos, “The Logic of Provability”. Cambridge University Press, 1993.
• E.V. Dashkov, “On the positive fragment of the polymodal provability logic GLP”. Mathematical Notes 2012; 91:318–333.
• D. Fernandez-Duque and J.Joosten, “Well-orders in the transfinite Japaridze algebra”. Logic Journal of the IGPL 22 (2014), pp. 933–963.
• G. Japaridze, "The polymodal logic of provability". Intensional Logics and Logical Structure of Theories. Metsniereba, Tbilisi, 1988, pp. 16–48 (Russian).
• F. Pakhomov, “On the complexity of the closed fragment of Japaridze's provability logic”. Archive for Mathematical Logic 53 (2014), pp. 949–967.
• D.S. Shamkanov, “Interpolation properties for provability logics GL and GLP”. Proceedings of the Steklov Institute of Mathematics 274 (2011), pp. 303–316.
• I. Shapirovsky, "PSPACE-decidability of Japaridze's polymodal logic". Advances in Modal Logic 7 (2008), pp. 289–304.