Japaridze's polymodal logic

Last updated June 02, 2023

Japaridze's polymodal logic (GLP) 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 $[0],[1],[2],...$ of necessity operators. Their dual possibility operators $<0>,<1>,<2>,...$ are defined by $< n > p = \neg[n]\neg p$ .

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

$[n](p \to q) \to ([n] p \to [n] q)$
$[n]([n] p \to p) \to [n] p$
$[n] p \to [n +1] p$
$< n > p \to [n +1]< n > p$

And the rules of inference are:

From $p$ and $p \to q$ conclude $q$
From $p$ conclude $[0] p$

Provability semantics

Consider a sufficiently strong first-order theory $T$ such as Peano Arithmetic $PA$ . Define the series $T 0, T 1, T 2,...$ of theories as follows:

$T 0$ is $T$
$T n +1$ is the extension of $T n$ through the additional axioms $\forall 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 0, T 1, T 2,...$ 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$ .

Other semantics

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]

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.^[4]

History

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 $ɛ 0$ 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]

Literature

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" ^{[ dead link ]}. 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.

Related Research Articles

Gödel's completeness theorem is a fundamental theorem in mathematical logic that establishes a correspondence between semantic truth and syntactic provability in first-order logic.

Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of formal systems of logic such as their expressive or deductive power. However, it can also include uses of logic to characterize correct mathematical reasoning or to establish foundations of mathematics.

<span class="mw-page-title-main">Saul Kripke</span> American philosopher and logician (1940–2022)

Saul Aaron Kripke was an American analytic philosopher and logician. He was Distinguished Professor of Philosophy at the Graduate Center of the City University of New York and emeritus professor at Princeton University. Kripke is considered one of the most important philosophers of the latter half of the 20th century. Since the 1960s, he has been a central figure in a number of fields related to mathematical and modal logic, philosophy of language and mathematics, metaphysics, epistemology, and recursion theory.

Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of provability in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the philosophy of mathematics. The theorems are widely, but not universally, interpreted as showing that Hilbert's program to find a complete and consistent set of axioms for all mathematics is impossible.

Proof theory is a major branch of mathematical logic and theoretical computer science that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. Consequently, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.

<span class="mw-page-title-main">George Boolos</span> American philosopher and mathematical logician

George Stephen Boolos was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology.

In logic and mathematics, second-order logic is an extension of first-order logic, which itself is an extension of propositional logic. Second-order logic is in turn extended by higher-order logic and type theory.

Provability logic is a modal logic, in which the box operator is interpreted as 'it is provable that'. The point is to capture the notion of a proof predicate of a reasonably rich formal theory, such as Peano arithmetic.

In mathematical logic, cointerpretability is a binary relation on formal theories: a formal theory T is cointerpretable in another such theory S, when the language of S can be translated into the language of T in such a way that S proves every formula whose translation is a theorem of T. The "translation" here is required to preserve the logical structure of formulas.

In mathematical logic, a tolerant sequence is a sequence

In mathematical logic, weak interpretability is a notion of translation of logical theories, introduced together with interpretability by Alfred Tarski in 1953.

Kripke semantics is a formal semantics for non-classical logic systems created in the late 1950s and early 1960s by Saul Kripke and André Joyal. It was first conceived for modal logics, and later adapted to intuitionistic logic and other non-classical systems. The development of Kripke semantics was a breakthrough in the theory of non-classical logics, because the model theory of such logics was almost non-existent before Kripke.

Giorgi Japaridze is a Georgian-American researcher in logic and theoretical computer science. He currently holds the title of Full Professor at the Computing Sciences Department of Villanova University. Japaridze is best known for his invention of computability logic, cirquent calculus, and Japaridze's polymodal logic.

In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is weaker than PA but it has the same language, and both theories are incomplete. Q is important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable and essentially undecidable.

In mathematics, Kruskal's tree theorem states that the set of finite trees over a well-quasi-ordered set of labels is itself well-quasi-ordered under homeomorphic embedding.

In mathematical logic, an ω-consistenttheory is a theory that is not only (syntactically) consistent, but also avoids proving certain infinite combinations of sentences that are intuitively contradictory. The name is due to Kurt Gödel, who introduced the concept in the course of proving the incompleteness theorem.

This article gives a sketch of a proof of Gödel's first incompleteness theorem. This theorem applies to any formal theory that satisfies certain technical hypotheses, which are discussed as needed during the sketch. We will assume for the remainder of the article that a fixed theory satisfying these hypotheses has been selected.

A timeline of mathematical logic. See also History of logic.

Sergei Nikolaevich Artemov is a Russian-American researcher in logic and its applications. He currently holds the title of Distinguished Professor at the Graduate Center of the City University of New York where he is the founder and head of its research laboratory for logic and computation. His research interests include proof theory and logic in computer science, optimal control and hybrid systems, automated deduction and verification, epistemology, and epistemic game theory. He is best known for his invention of logics of proofs and justifications.

References

1 2 3 G. Japaridze, "The polymodal logic of provability". Intensional Logics and Logical Structure of Theories. Metsniereba, Tbilisi, 1988, pp. 16–48 (Russian).
↑ G. Boolos, "The analytical completeness of Japaridze's polymodal logics". Annals of Pure and Applied Logic 61 (1993), pp. 95–111.
1 2 L. Beklemishev and D. Gabelaia, "Topological completeness of provability logic GLP". Annals of Pure and Applied Logic 164 (2013), pp. 1201–1223.
1 2 F. Pakhomov, "On the complexity of the closed fragment of Japaridze's provability logic". Archive for Mathematical Logic 53 (2014), pp. 949–967.
↑ 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, "Kripke semantics for provability logic GLP". Annals of Pure and Applied Logic 161, 756–774 (2010).
↑ L. Beklemishev, G. Bezhanishvili and T. Icard, "On topological models of GLP". Ways of proof theory, Ontos Mathematical Logic, 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, pp. 133–153.
↑ I. Shapirovsky, "PSPACE-decidability of Japaridze's polymodal logic". Advances in Modal Logic 7 (2008), pp. 289-304.
↑ L. Beklemishev, "Provability algebras and proof-theoretic ordinals, I". Annals of Pure and Applied Logic 128 (2004), pp. 103–123.
↑ G. Boolos, The Logic of Provability . Cambridge University Press, 1993.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[japaridze1988-1] 1 2 3 G. Japaridze, "The polymodal logic of provability". Intensional Logics and Logical Structure of Theories. Metsniereba, Tbilisi, 1988, pp. 16–48 (Russian).

[2] G. Boolos, "The analytical completeness of Japaridze's polymodal logics". Annals of Pure and Applied Logic 61 (1993), pp. 95–111.

[beklemishev2013-3] 1 2 L. Beklemishev and D. Gabelaia, "Topological completeness of provability logic GLP". Annals of Pure and Applied Logic 164 (2013), pp. 1201–1223.

[pakhomov2014-4] 1 2 F. Pakhomov, "On the complexity of the closed fragment of Japaridze's provability logic". Archive for Mathematical Logic 53 (2014), pp. 949–967.

[5] 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.

[6] L. Beklemishev, "Kripke semantics for provability logic GLP". Annals of Pure and Applied Logic 161, 756–774 (2010).

[7] L. Beklemishev, G. Bezhanishvili and T. Icard, "On topological models of GLP". Ways of proof theory, Ontos Mathematical Logic, 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, pp. 133–153.

[8] I. Shapirovsky, "PSPACE-decidability of Japaridze's polymodal logic". Advances in Modal Logic 7 (2008), pp. 289-304.

[9] L. Beklemishev, "Provability algebras and proof-theoretic ordinals, I". Annals of Pure and Applied Logic 128 (2004), pp. 103–123.

[10] G. Boolos, The Logic of Provability . Cambridge University Press, 1993.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]