582:, 1986) and published two years later 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) and (b) 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
554:. 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.
629:
497:
of theories is not the only natural understanding yielding the soundness and completeness of GLP. For instance, each theory
980:
597:
from the corresponding algebra, and constructing simple combinatorial independent statements (Beklemishev ).
579:
526:
955:
710:
975:
758:
551:
937:
890:
836:
687:
640:
618:
816:
698:
44:
799:
736:
665:
195:
873:
856:
747:
676:
73:
The axioms of GLP are all classical tautologies and all formulas of one of the following forms:
20:
587:
583:
575:
204:
32:
27:. This system has played an important role in some applications of provability algebras in
563:
550:
A natural topological semantics of GLP interprets modalities as derivative operators of a
358:
600:
An extensive survey of GLP in the context of provability logics in general was given by
920:
769:
969:
601:
522:
725:
657:
L. Beklemishev, "On the Craig interpolation and the fixed point properties of GLP".
874:"A simplified proof of arithmetical completeness theorem for provability logic GLP"
677:"A simplified proof of arithmetical completeness theorem for provability logic GLP"
544:
28:
717:
E.V. Dashkov, "On the positive fragment of the polymodal provability logic GLP".
906:
L. Beklemishev, G. Bezhanishvili and T. Icard, "On topological models of GLP".
24:
650:
L. Beklemishev, G. Bezhanishvili and T. Icar, "On topological models of GLP".
630:"A finitary treatment of the closed fragment of Japaridze's provability logic"
857:"On the complexity of the closed fragment of Japaridze's provability logic"
748:"On the complexity of the closed fragment of Japaridze's provability logic"
566:. So is the same problem restricted to only variable-free formulas of GLP.
31:, and has been extensively studied since the late 1980s. It is named after
654:, 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, pp. 133β153.
403:. It extends to all formulas of the language of GLP by stipulating that
661:. S. Feferman et al., eds., College Publications 2010. pp. 49β60.
578:
in his PhD thesis "Modal
Logical Means of Investigating Provability" (
910:, 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, pp. 133β153.
447:
An arithmetical completeness theorem for GLP states that a formula
543:
GLP has been shown to be incomplete with respect to any class of
43:
The language of GLP extends that of the language of classical
817:"The analytical completeness of Japaridze's polymodal logics"
699:"The analytical completeness of Japaridze's polymodal logics"
759:"Interpolation properties for provability logics GL and GLP"
453:
is provable in GLP if and only if, for every interpretation
525:
showed that GLP remains sound and complete with analysis (
51:
of necessity operators. Their dual possibility operators
743:. Metsniereba, Tbilisi, 1988, pp. 16β48 (Russian).
666:"Ordinal completeness of bimodal provability logic GLB"
938:"Provability algebras and proof-theoretic ordinals, I"
619:"Provability algebras and proof-theoretic ordinals, I"
921:"PSPACE-decidability of Japaridze's polymodal logic"
804:
Intensional Logics and
Logical Structure of Theories
770:"PSPACE-decidability of Japaridze's polymodal logic"
741:
Intensional Logics and
Logical Structure of Theories
878:
Proceedings of the
Steklov Institute of Mathematics
837:"Topological completeness of provability logic GLP"
763:
Proceedings of the
Steklov Institute of Mathematics
688:"Topological completeness of provability logic GLP"
681:
Proceedings of the
Steklov Institute of Mathematics
806:. Metsniereba, Tbilisi, 1988, pp. 16β48 (Russian).
726:"Well-orders in the transfinite Japaridze algebra"
831:
829:
437:stands for (the numeral for) the GΓΆdel number of
407:commutes with the Boolean connectives, and that
794:
792:
790:
350:be a natural arithmetization of the predicate
908:Ways of proof theory, Ontos Mathematical Logic
851:
849:
652:Ways of proof theory, Ontos Mathematical Logic
586:, elaborating a canonical way for recovering
8:
891:"Kripke semantics for provability logic GLP"
641:"Kripke semantics for provability logic GLP"
628:L. Beklemishev, J. Joosten and M. Vervoort,
574:GLP, under the name GP, was introduced by
562:The problem of being a theorem of GLP is
786:
473:The above understanding of the series
390:of the language of GLP to a sentence
7:
800:"The polymodal logic of provability"
737:"The polymodal logic of provability"
959:. Cambridge University Press, 1993.
659:Proofs, Categories and Computations
724:D. Fernandez-Duque and J.Joosten,
636:15 (2005), No 4, pp. 447β463.
14:
835:L. Beklemishev and D. Gabelaia,
714:Cambridge University Press, 1993.
686:L. Beklemishev and D. Gabelaia,
670:Lecture Notes in Computer Science
529:) in the role of the base theory
53:<0>,<1>,<2>,...
47:by including the infinite series
23:with infinitely many provability
942:Annals of Pure and Applied Logic
895:Annals of Pure and Applied Logic
841:Annals of Pure and Applied Logic
821:Annals of Pure and Applied Logic
703:Annals of Pure and Applied Logic
692:Annals of Pure and Applied Logic
645:Annals of Pure and Applied Logic
634:Journal of Logic and Computation
623:Annals of Pure and Applied Logic
521:sentences as additional axioms.
384:that sends each nonlogical atom
146:And the rules of inference are:
694:164 (2013), pp. 1201β1223.
194:Consider a sufficiently strong
861:Archive for Mathematical Logic
765:274 (2011), pp. 303β316.
752:Archive for Mathematical Logic
278:through the additional axioms
1:
625:128 (2004), pp. 103β123.
754:53 (2014), pp. 949β967.
732:22 (2014), pp. 933β963.
683:274 (2011), pp. 25β33.
672:6618 (2011), pp. 1β15.
312:proves all of the formulas
776:7 (2008), pp. 289β304.
705:61 (1993), pp. 95β111.
39:Language and axiomatization
17:Japaridze's polymodal logic
997:
843:164 (2013), pp. 1201β1223.
361:of a sentence provable in
730:Logic Journal of the IGPL
956:The Logic of Provability
944:128 (2004), pp. 103β123.
711:The Logic of Provability
606:The Logic of Provability
558:Computational complexity
514:augmented with all true
236:of theories as follows:
925:Advances in Modal Logic
880:274 (2011), pp. 25β33.
863:53 (2014), pp. 949β967.
774:Advances in Modal Logic
580:Moscow State University
527:second-order arithmetic
927:7 (2008), pp. 289-304.
823:61 (1993), pp. 95β111.
552:polytopological space
508:can be understood as
212:. Define the series
190:Provability semantics
19:(GLP) is a system of
897:161, 756β774 (2010).
647:161, 756β774 (2010).
267:is the extension of
397:of the language of
45:propositional logic
719:Mathematical Notes
196:first-order theory
981:Provability logic
721:2012; 91:318β333.
588:ordinal notation
290:for each formula
21:provability logic
988:
960:
951:
945:
936:L. Beklemishev,
934:
928:
919:I. Shapirovsky,
917:
911:
904:
898:
889:L. Beklemishev,
887:
881:
872:L. Beklemishev,
870:
864:
853:
844:
833:
824:
813:
807:
796:
768:I. Shapirovsky,
757:D.S. Shamkanov,
675:L. Beklemishev,
664:L. Beklemishev,
639:L. Beklemishev,
617:L. Beklemishev,
596:
584:Peano arithmetic
576:Giorgi Japaridze
534:
520:
513:
507:
496:
469:
463:
456:
452:
443:
436:
428:
414:
406:
402:
396:
389:
383:
372:
356:
349:
335:
326:
311:
300:
289:
277:
266:
253:
247:
235:
211:
205:Peano Arithmetic
202:
185:
179:
171:
165:
155:
142:
122:
111:
95:
69:
54:
50:
33:Giorgi Japaridze
996:
995:
991:
990:
989:
987:
986:
985:
966:
965:
964:
963:
952:
948:
935:
931:
918:
914:
905:
901:
888:
884:
871:
867:
854:
847:
834:
827:
814:
810:
797:
788:
783:
614:
595:
591:
572:
564:PSPACE-complete
560:
541:
539:Other semantics
530:
519:
515:
509:
506:
498:
494:
487:
480:
474:
465:
464:is provable in
458:
457:, the sentence
454:
448:
438:
430:
422:
416:
408:
404:
398:
391:
385:
381:
370:
362:
351:
343:
337:
331:
313:
310:
302:
291:
279:
276:
268:
265:
256:
249:
246:
240:
233:
226:
219:
213:
207:
198:
192:
181:
175:
167:
157:
151:
125:
114:
98:
77:
56:
55:are defined by
52:
48:
41:
12:
11:
5:
994:
992:
984:
983:
978:
968:
967:
962:
961:
946:
929:
912:
899:
882:
865:
845:
825:
808:
798:G. Japaridze,
785:
784:
782:
779:
778:
777:
766:
755:
744:
735:G. Japaridze,
733:
722:
715:
706:
695:
684:
673:
662:
655:
648:
637:
626:
613:
610:
593:
571:
568:
559:
556:
540:
537:
517:
502:
492:
485:
478:
418:
380:is a function
366:
339:
328:
327:
306:
272:
260:
254:
244:
231:
224:
217:
191:
188:
187:
186:
172:
144:
143:
123:
112:
96:
40:
37:
13:
10:
9:
6:
4:
3:
2:
993:
982:
979:
977:
974:
973:
971:
958:
957:
950:
947:
943:
939:
933:
930:
926:
922:
916:
913:
909:
903:
900:
896:
892:
886:
883:
879:
875:
869:
866:
862:
858:
855:F. Pakhomov,
852:
850:
846:
842:
838:
832:
830:
826:
822:
818:
812:
809:
805:
801:
795:
793:
791:
787:
780:
775:
771:
767:
764:
760:
756:
753:
749:
746:F. Pakhomov,
745:
742:
738:
734:
731:
727:
723:
720:
716:
713:
712:
707:
704:
700:
696:
693:
689:
685:
682:
678:
674:
671:
667:
663:
660:
656:
653:
649:
646:
642:
638:
635:
631:
627:
624:
620:
616:
615:
611:
609:
607:
603:
602:George Boolos
598:
589:
585:
581:
577:
569:
567:
565:
557:
555:
553:
548:
546:
545:Kripke frames
538:
536:
533:
528:
524:
523:George Boolos
512:
505:
501:
491:
484:
477:
471:
468:
461:
451:
445:
441:
434:
426:
421:
412:
401:
394:
388:
379:
374:
369:
365:
360:
355:
347:
342:
334:
324:
320:
316:
309:
305:
298:
294:
287:
283:
275:
271:
263:
259:
255:
252:
243:
239:
238:
237:
230:
223:
216:
210:
206:
201:
197:
189:
184:
178:
173:
170:
164:
160:
154:
149:
148:
147:
141:
137:
133:
129:
124:
121:
117:
113:
110:
106:
102:
97:
93:
89:
85:
81:
76:
75:
74:
71:
68:
64:
60:
46:
38:
36:
34:
30:
26:
22:
18:
976:Proof theory
954:
949:
941:
932:
924:
915:
907:
902:
894:
885:
877:
868:
860:
840:
820:
811:
803:
773:
762:
751:
740:
729:
718:
709:
702:
691:
680:
669:
658:
651:
644:
633:
622:
605:
604:in his book
599:
573:
561:
549:
542:
531:
510:
503:
499:
489:
482:
475:
472:
466:
459:
449:
446:
439:
432:
424:
419:
410:
399:
392:
386:
377:
375:
367:
363:
359:GΓΆdel number
353:
345:
340:
332:
329:
322:
318:
314:
307:
303:
296:
292:
285:
281:
273:
269:
261:
257:
250:
241:
228:
221:
214:
208:
199:
193:
182:
176:
168:
162:
158:
152:
145:
139:
135:
131:
127:
119:
115:
108:
104:
100:
91:
87:
83:
79:
72:
66:
62:
58:
42:
29:proof theory
16:
15:
953:G. Boolos,
815:G. Boolos,
708:G. Boolos,
697:G. Boolos,
378:realization
970:Categories
781:References
612:Literature
301:such that
25:modalities
330:For each
180:conclude
166:conclude
429:, where
203:such as
570:History
357:is the
325:(2),...
590:up to
336:, let
174:From
150:From
134:β <
49:,,,...
321:(1),
317:(0),
86:) β (
495:,...
234:,...
156:and
138:>
130:>
126:<
107:) β
65:= ¬¬
61:>
57:<
427:*')
415:is
248:is
972::
940:.
923:.
893:.
876:.
859:.
848:^
839:.
828:^
819:.
802:.
789:^
772:.
761:.
750:.
739:.
728:.
701:.
690:.
679:.
668:.
643:.
632:.
621:.
608:.
547:.
535:.
470:.
444:.
435:*'
423:('
417:Pr
413:)*
376:A
373:.
338:Pr
282:xF
264:+1
209:PA
161:β
118:β
103:β
90:β
82:β
70:.
35:.
594:0
592:Ι
532:T
518:n
516:Ξ
511:T
504:n
500:T
493:2
490:T
488:,
486:1
483:T
481:,
479:0
476:T
467:T
462:*
460:F
455:*
450:F
442:*
440:F
433:F
431:'
425:F
420:n
411:F
409:(
405:*
400:T
395:*
393:a
387:a
382:*
371:"
368:n
364:T
354:x
352:"
348:)
346:x
344:(
341:n
333:n
323:F
319:F
315:F
308:n
304:T
299:)
297:x
295:(
293:F
288:)
286:x
284:(
280:β
274:n
270:T
262:n
258:T
251:T
245:0
242:T
232:2
229:T
227:,
225:1
222:T
220:,
218:0
215:T
200:T
183:p
177:p
169:q
163:q
159:p
153:p
140:p
136:n
132:p
128:n
120:p
116:p
109:p
105:p
101:p
99:(
94:)
92:q
88:p
84:q
80:p
78:(
67:p
63:p
59:n
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.