| 词条 | Japaridze's polymodal logic |
| 释义 |
Japaridze's polymodal logic (GLP), is a system of provability logic with infinitely many modal (provability) operators. 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 axiomatizationThe 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:
And the rules of inference are:
Provability semanticsConsider a “sufficiently strong” first-order theory T such as Peano Arithmetic PA. Define the series T0,T1,T2,... of theories as follows:
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 * which 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 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 semanticsGLP 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 w.r.t. the class of all GLP-spaces.[3] Computational complexityThe problem of being a theorem of GLP is PSPACE-complete. So is the same problem restricted to only variable-free formulas of GLP.[4] HistoryGLP, under the name GP, was introduced by Giorgi Japaridze in his PhD thesis "Modal Logical Means of Investigating Provability" (Moscow State University, 1986) and first published in.[1] The completeness theorem for GLP with respect to its provability interpretation was also first proven in.[1] Later, in,[5] Beklemishev came up with a simpler proof of the same theorem. The non-existence of Kripke frames for GLP was shown in.[1] A more extensive study of Kripke models for GLP was conducted by Beklemishev in.[6] Topological models for GLP were studied by Beklemishev, Bezhanishvili, Icard and Gabelaia,.[7][3] 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 system up to {{lang|el|ɛ}}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
References1. ^1 2 3 4 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. ^1 L. Beklemishev and D. Gabelaia, “Topological completeness of provability logic GLP”. Annals of Pure and Applied Logic 164 (2013), pp. 1201–1223. 4. ^1 F. Pakhomov, [https://link.springer.com/article/10.1007%2Fs00153-014-0397-4 “On the complexity of the closed fragment of Japaridze's provability logic”]. Archive for Mathematical Logic 53 (2014), pp. 949–967. 5. ^L. Beklemishev, [https://link.springer.com/article/10.1134%2FS0081543811060046 “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, [https://www.amazon.com/The-Logic-Provability-George-Boolos/dp/0521483255 “The Logic of Provability”.] Cambridge University Press, 1993. 3 : Modal logic|Proof theory|Provability logic |
| 随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。