Japaridze's polymodal logic


Japaridze's polymodal logic is a system of provability logic with infinitely many provability modalities. This system has played an important role
in some applications of provability algebras in proof theory, and has been extensively studied since the late 1980s. It is named after Giorgi Japaridze.

Language and axiomatization

The language of GLP extends that of the language of classical propositional logic by including the infinite series of necessity operators. Their dual possibility operators are defined by.
The axioms of GLP are all classical tautologies and all formulas of one of the following forms:
And the rules of inference are:
  • From and conclude
  • From conclude

Provability semantics

Consider a sufficiently strong first-order theory such as Peano Arithmetic.
Define the series of theories as follows:
  • is
  • is the extension of through the additional axioms for each formula such that proves all of the formulas
For each, let be a natural arithmetization of the predicate
is the Gödel number of a sentence provable in.
A realization is a function that sends each nonlogical atom of
the language of GLP to a sentence of the language of. It extends to all formulas
of the language of GLP by stipulating that commutes with the Boolean connectives, and
that is, where
stands for the Gödel number of.
An arithmetical completeness theorem for GLP states that a formula is provable in GLP if and only if, for every interpretation, the sentence is provable in.
The above understanding of the series of theories is not the only natural understanding yielding the soundness and completeness of GLP. For instance, each theory can be understood as augmented with all true sentences as additional axioms. George Boolos showed that GLP remains sound and complete with analysis in the role of the base theory.

Other semantics

GLP has been shown 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.

Computational complexity

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

History

GLP, under the name GP, was introduced by Giorgi Japaridze in his PhD thesis "Modal Logical Means of Investigating Provability" and published two years later along with the completeness theorem for GLP with respect to its provability interpretation and a proof that Kripke frames for GLP do not exist. Beklemishev also conducted a more extensive study of Kripke models for GLP.
Topological models for GLP were studied by Beklemishev, Bezhanishvili, Icard and Gabelaia.
The decidability of GLP in polynomial space was proven by I. Shapirovsky, and the PSPACE-hardness of its variable-free fragment was proven by F. Pakhomov. 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 .
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.

Literature

  • L. Beklemishev, . Annals of Pure and Applied Logic 128, pp. 103–123.
  • L. Beklemishev, J. Joosten and M. Vervoort, . Journal of Logic and Computation 15, No 4, pp. 447–463.
  • L. Beklemishev, . Annals of Pure and Applied Logic 161, 756–774.
  • 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, . Lecture Notes in Computer Science 6618, pp. 1–15.
  • L. Beklemishev, . Proceedings of the Steklov Institute of Mathematics 274, pp. 25–33.
  • L. Beklemishev and D. Gabelaia, . Annals of Pure and Applied Logic 164, pp. 1201–1223.
  • G. Boolos, . Annals of Pure and Applied Logic 61, pp. 95–111.
  • G. Boolos, 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, "". Logic Journal of the IGPL 22, pp. 933–963...
  • G. Japaridze, . Intensional Logics and Logical Structure of Theories. Metsniereba, Tbilisi, 1988, pp. 16–48.
  • F. Pakhomov, . Archive for Mathematical Logic 53, pp. 949–967.
  • D.S. Shamkanov, . Proceedings of the Steklov Institute of Mathematics 274, pp. 303–316.
  • I. Shapirovsky, . Advances in Modal Logic 7, pp. 289–304.