fbpx
Wikipedia

Japaridze's polymodal logic

December 18, 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 edit

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

Provability semantics edit

Consider a sufficiently strong first-order theory T such as Peano Arithmetic PA. Define the series T0,T1,T2,... of theories as follows:

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

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

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 Prn('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 T0,T1,T2,... of theories is not the only natural understanding yielding the soundness and completeness of GLP. For instance, each theory Tn 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 edit

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 edit

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 edit

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 edit

  • 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, . 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.

References edit

  1. ^ a b c 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.
  3. ^ a b L. Beklemishev and D. Gabelaia, "Topological completeness of provability logic GLP". Annals of Pure and Applied Logic 164 (2013), pp. 1201–1223.
  4. ^ a b 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.

December 18, 2023
japaridze, polymodal, logic, system, provability, logic, with, infinitely, many, provability, modalities, this, system, played, important, role, some, applications, provability, algebras, proof, theory, been, extensively, studied, since, late, 1980s, named, af. 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 Contents 1 Language and axiomatization 2 Provability semantics 3 Other semantics 4 Computational complexity 5 History 6 Literature 7 ReferencesLanguage and axiomatization editThe 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 lt 0 gt lt 1 gt lt 2 gt are defined by lt n gt 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 lt n gt p n 1 lt n gt pAnd the rules of inference are From p and p q conclude q From p conclude 0 pProvability semantics editConsider a sufficiently strong first order theory T such as Peano Arithmetic PA Define the series T0 T1 T2 of theories as follows T0 is T Tn 1 is the extension of Tn through the additional axioms xF x for each formula F x such that Tn proves all of the formulas F 0 F 1 F 2 For each n let Prn x be a natural arithmetization of the predicate x is the Godel number of a sentence provable in Tn 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 Prn F where F stands for the numeral for the Godel 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 T0 T1 T2 of theories is not the only natural understanding yielding the soundness and completeness of GLP For instance each theory Tn can be understood as T augmented with all true Pn 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 editGLP 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 editThe 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 editGLP 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 editL 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 References edit a b c 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 a b L Beklemishev and D Gabelaia Topological completeness of provability logic GLP Annals of Pure and Applied Logic 164 2013 pp 1201 1223 a b 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 Retrieved from https en wikipedia org w index php title Japaridze 27s polymodal logic amp oldid 1158078197, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.