Жорджи Жапаридзенің ғылыми еңбектері мен логикадағы жаңа бағыттары

Кіріспе

Георгий Джапаридзе (кейде Георгий Джапаридзе деп те жазылады) – логика және теориялық информатика саласындағы грузин-американдық зерттеуші. Қазіргі уақытта Вилланова университетінің Есептеу ғылымдары факультетінде толық профессор атағын иеленеді. Джапаридзе есептеу логикасын, циркуенттік есептеуді және Джапаридзенің полимодальдық логикасын ойлап тапқанымен әйгілі.

Зерттеу

1985–1988 жылдары Жапаридзе GLP жүйесін жасады, ол Жапаридзедің полимодальдық логикасы ретінде белгілі. Бұл модальдық логика жүйесі, Пеано арифметикасы үшін инкрементті түрде әлсіздейтін дәлелдемелік предикаттардың табиғи қатары ретінде түсіндірілетін «қажеттілік» операторларымен ([0],[1],[2]) жабдықталған. «Дәлелдемелік полимодальдық логика» еңбегінде Жапаридзе осы жүйенің арифметикалық толықтығын, сондай-ақ Крипке кадрларына қатысты толық еместігін дәлелдеді. GLP кейінгі үш онжылдық бойына әртүрлі авторлар тарапынан кеңінен зерттелді, әсіресе 2004 жылы Лев Беклемишев оның арифметиканың дәлелдеме теориясын түсінудегі пайдалылығын көрсеткеннен кейін (дәлелдемелік алгебралар және теориялық ординалдар). Жапаридзе сондай-ақ дәлелдемелік логиканың бірінші реттік (предикат) нұсқаларын зерттеді. Ол осы логиканың бір айнымалы фрагментінің аксиоматизациясын жасады және оның арифметикалық толықтығы мен шешілгіштігін дәлелдеді. Сол мақалада ол негізгі арифметикалық теорияның 1-толықтығы болған жағдайда, қайталанбаған модальдықтары бар предикаттық дәлелдемелік логика рекурсивті түрде саналатынын көрсетті. Studia Logica 50-де ол модальдық емес сандық белгілері бар предикаттық дәлелдемелік логика үшін де солай істеді. 1992–1993 жылдары Жапаридзе түсіндірілімділік логикасынан туындайтын түсіндірілімділік, төзімділік және ко-төзімділік ұғымдарын жасады. Ол ко-төзімділіктің 1-консервативтілікке, ал төзімділіктің 1-тұрақтылыққа тең екенін дәлелдеді. Бұл, 1-консервативтіліктің метаматематикалық мағынасына қатысты ұзақ жылдар бойы ашық қалған мәселеге жауап болды. Осы зерттеу бағытында Жапаридзе төзімділік (1993) және арифметикалық иерархияның (1994) модальдық логикасын құрастырды және олардың арифметикалық толықтығын дәлелдеді. 2002 жылы Жапаридзе «Міндеттер логикасын» енгізді, ол кейіннен оның Абстрактілік ресурстық семантикасының бір бөлігіне, ал екінші жағынан – Есептеу логикасының фрагментіне айналды. Жапаридзе 2003 жылы Есептеу логикасын құрғандығымен және оның дамуына үлес қосқандығымен танымал. Бұл – ұзақ мерзімді зерттеу бағдарламасы және «дәстүрлі түрде шындықтың формальды теориясы болғаннан гөрі, (интерактивті) есептеудің формальды теориясы ретінде логиканы қайта дамыту» үшін семантикалық платформа. 2006 жылы Жапаридзе циркуенттік есептеуді, формулалар немесе тізбектер сияқты дәстүрлі және жалпылама ағаш тәрізді құрылымдардың орнына циркуенттер деп аталатын граф стиліндегі құрылымдарды қолдайтын дәлелдемелік тәсіл ретінде ұсынды. Бұл жаңа дәлелдемелік тәсіл кейіннен есептеу логикасының әртүрлі фрагменттерін «бағындыруға» сәтті қолданылды, олар әйтпесе секвенттік есептеу немесе Гилберт стиліндегі жүйелер сияқты дәстүрлі дәлелдемелік жүйелерді пайдалана отырып, барлық аксиоматизациялау әрекеттеріне қарсы тұрды. Ол сондай-ақ тәуелсіздікке бейім логиканың таза пропозициялық фрагментін (анықтау және) аксиоматизациялау үшін де қолданылды. Циркуенттік есептеудің пайда болуымен бірге тиісті «абстрактілік ресурстық семантика» ұсынылды. Семантикасы бар циркуенттік есептеуді, сызықтық логикадан айырмашылығы, ресурстарды бөлісуді есепке алуға мүмкіндік беретін ресурстардың логикасы ретінде қарастыруға болады. Осылайша, Жапаридзе оны сызықтық логикаға тиімді балама ретінде ұсынды, соңғысын ресурстық логика ретінде жеткілікті экспрессивті де, толық та емес деп бірнеше рет сынады. Алайда, бұл шақыру сызықтық логика қауымдастығы тарапынан көбінесе назарсыз қалды, оған жауап берілген жоқ. Жапаридзе интуиционистік логикаға ұқсас (және жауап алынбаған) сын айтты, оны сенімді семантикалық негіздемесі болмағандықтан сынға алды, бұл конструктивтік талаптарға зиян келтірді және «ванна суымен бірге баланы да тастау» салдарынан толық емес. Гейтингтің интуиционистік логикасы, оның толық жалпылығы бойынша, есептеу логикасының семантикасына қатысты дұрыс, бірақ толық емес екені дәлелденді. Интуиционистік логиканың оң (негациясыз) пропозициялық фрагменті есептеу логикасының семантикасына қатысты толық екені дәлелденді. «Есептеу логикасының CL12 жүйесі туралы» еңбегінде, есептеу логикасы платформасында Жапаридзе уақыт пен кеңістіктің күрделіліктері туралы дәстүрлі ұғымдарды интерактивті есептеулерге жалпылады және мұндай есептеулер үшін күрделілік өлшемінің үшінші түрін енгізді, ол «амплитудалық күрделік» деп аталды. Жапаридзенің еңбектерінің бірі – «клархиметрия» деп аталатын есептеу логикасына негізделген (Пеано) арифметика жүйелерінің сериясын жасау. Бұларға уақыт, кеңістік және амплитудалық күрделік кластарының әртүрлі комбинациялары үшін шешілген арифметика стиліндегі күрделікке бағытталған жүйелер кіреді.

During 1985–1988 Japaridze elaborated the system GLP, known as Japaridze's polymodal logic. This is a system of modal logic with the "necessity" operators [0],[1],[2], , understood as a natural series of incrementally weak provability predicates for Peano arithmetic. In "The polymodal logic of provability" Japaridze proved the arithmetical completeness of this system, as well as its inherent incompleteness with respect to Kripke frames. GLP has been extensively studied by various authors during the subsequent three decades, especially after Lev Beklemishev, in 2004, pointed out its usefulness in understanding the proof theory of arithmetic (provability algebras and proof theoretic ordinals). Japaridze has also studied the first order (predicate) versions of provability logic. He came up with an axiomatization of the single variable fragment of that logic, and proved its arithmetical completeness and decidability. In the same paper he showed that, on the condition of the 1 completeness of the underlying arithmetical theory, predicate provability logic with non iterated modalities is recursively enumerable. In Studia Logica 50 he did the same for the predicate provability logic with non modalized quantifiers. In 1992–1993, Japaridze came up with the concepts of cointerpretability, tolerance and cotolerance, naturally arising in interpretability logic. He proved that cointerpretability is equivalent to 1 conservativity and tolerance is equivalent to 1 consistency. The former was an answer to the long standing open problem regarding the metamathematical meaning of 1 conservativity. Within the same line of research, Japaridze constructed the modal logics of tolerance (1993) and of the arithmetical hierarchy (1994), and proved their arithmetical completeness. In 2002 Japaridze introduced "the Logic of Tasks", which later became a part of his Abstract Resource Semantics on one hand, and a fragment of Computability Logic (see below) on the other hand. Japaridze is best known for founding Computability Logic in 2003 and making subsequent contributions to its evolution. This is a long term research program and a semantical platform for "redeveloping logic as a formal theory of (interactive) computability, as opposed to the formal theory of truth that it has more traditionally been". In 2006 Japaridze conceived cirquent calculus as a proof theoretic approach that manipulates graph style constructs, termed cirquents, instead of the more traditional and less general tree like constructs such as formulas or sequents. This novel proof theoretic approach was later successfully used to "tame" various fragments of computability logic, which had otherwise stubbornly resisted all axiomatization attempts using the traditional proof systems such as sequent calculus or Hilbert style systems. It was also used to (define and) axiomatize the purely propositional fragment of independence friendly logic. The birth of cirquent calculus was accompanied with offering the associated "abstract resource semantics". Cirquent calculus with that semantics can be seen as a logic of resources that, unlike linear logic, makes it possible to account for resource sharing. As such, it has been presented as a viable alternative to linear logic by Japaridze, who repeatedly has criticized the latter for being neither sufficiently expressive nor complete as a resource logic. This challenge, however, has remained largely unnoticed by the linear logic community, which never responded to it. Japaridze has cast a similar (and also never answered) challenge to intuitionistic logic, criticizing it for lacking a convincing semantical justification the associated constructivistic claims, and for being incomplete as a result of "throwing out the baby with the bath water". Heyting's intuitionistic logic, in its full generality, has been shown to be sound but incomplete with respect to the semantics of computability logic. The positive (negation free) propositional fragment of intuitionistic logic, however, has been proven to be complete with respect to the computability logic semantics. In "On the system CL12 of computability logic", on the platform of computability logic, Japaridze generalized the traditional concepts of time and space complexities to interactive computations, and introduced a third sort of a complexity measure for such computations, termed "amplitude complexity". Among Japaridze's contributions is the elaboration of a series of systems of (Peano) arithmetic based on computability logic, named "clarithmetics". These include complexity oriented systems (in the style of bounded arithmetic) for various combinations of time, space and amplitude complexity classes.

Өмірбаяны және академиялық мансабы

Георгий Жапаридзе 1961 жылы Грузияның Тбилиси қаласында (сол кездегі КСРО) дүниеге келген. 1983 жылы Тбилиси мемлекеттік университетін бітірген, 1987 жылы Мәскеу мемлекеттік университетінен философия ғылымдарының докторы дәрежесін, ал 1998 жылы Пенсильвания университетінен екінші доктор дәрежесін (компьютер ғылымдары бойынша) алған. 1987–1992 жылдары Жапаридзе Грузия Ғылым академиясының Философия институтында аға ғылыми қызметкер болып жұмыс істеді. 1992–1993 жылдары Амстердам университетінде (математика және компьютер ғылымдары кафедрасы) докторант болып тағылымдамадан өтті. 1993–1994 жылдары Нотр-Дам университетінде (философия кафедрасы) қонақ профессор болып жұмыс істеді. Ол Вилланова университетінің факультетіне (компьютер ғылымдары кафедрасы) қосылды. Жапаридзе сондай-ақ Қытайдағы Сямен университетінде (2007) және Шандонг университетінде (2010–2013) қонақ профессор болып жұмыс істеді.

Марапаттар

1982 жылы "Детерминизм және ерік бостандығы" атты еңбегі үшін Жапаридзе Грузия ғылым академиясының ең үздік студенттік ғылыми жұмысы үшін медалін алды, ол жыл сайын елі бойынша бір ғана студентке беріледі. 2015 жылы ол Вилланова университетінен жыл сайын бір ғана оқытушыға табыс етілетін үздік факультеттік ғылыми-зерттеу сыйлығын алды. Жапаридзе түрлі гранттар мен стипендиялардың иегері болды, оның ішінде АҚШ Ұлттық ғылым қоры, Вилланова университеті және Шандонг университетінен алған ғылыми гранттар, Голландия үкіметінің докторантурадан кейінгі тағылымдамасы, Индиана университетінің Смуллиан стипендиясы (пайдаланылмаған) және Пенсильвания университетінің деканының стипендиясы бар.

Байланысты әдебиеттер

Ф. Пахомов, "Жапаридзенің дәлелдеу логикасының жабық фрагментінің күрделілігі туралы". Математикалық логика мұрағаты 53 (2014), 949–967 беттер. Д. Фернандес Дуке және Дж. Жостен, "Трансфинитті Жапаридзе алгебрасындағы жақсы реттелулер". IGPL логикалық журналы 22 (2014), 933–963 беттер. В. Сюй, "Жапаридзенің IF логикасына қатысты тәсілімен шақырылған пропозициялық жүйе". IGPL логикалық журналы 22 (2014), 982–991 беттер. И. Шапировский, "Жапаридзенің полимодальдық логикасының PSPACE шешілмелігі". Модальдық логикадағы жетістіктер 7 (2008), 289–304 беттер. Л. Д. Беклемишев, Ж. Ж. Жостен және М. Вервоорт, "Жапаридзенің дәлелдеу логикасының жабық фрагментін шектеулі қарастыру". Логика және есептеу журналы 15(4) (2005), 447–463 беттер. Г. Булос, "Жапаридзенің полимодальдық логикасының аналитикалық толықтығы". Таза және қолданбалы логиканың жылнамалары 61 (1993), 95–111 беттер.

Таңдалған жарияланымдар

Г. Жапаридзе, "Өздігінен құрастырылған арифметика I: Құрылым және толықтық". Logical Methods in Computer Science 12 (2016), 3-шық, 8-ші мақала, 1–59 беттер. Г. Жапаридзе, "Өздігінен құрастырылған арифметика II: Дұрыстық". Logical Methods in Computer Science 12 (2016), 3-шық, 12-ші мақала, 1–62 беттер. Г. Жапаридзе, "Арифметикаға кіріспе II". Information and Computation 247 (2016), 290–312 беттер. Г. Жапаридзе, "Арифметикаға кіріспе III". Annals of Pure and Applied Logic 165 (2014), 241–252 беттер. Г. Жапаридзе, "Компьютерлік логикадағы қайталануларды циркулянтты есептеу арқылы шектеу, II бөлім". Archive for Mathematical Logic 52 (2013), 213–259 беттер. Г. Жапаридзе, "Компьютерлік логикадағы қайталануларды циркулянтты есептеу арқылы шектеу, I бөлім". Archive for Mathematical Logic 52 (2013), 173–212 беттер. Г. Жапаридзе, "Компьютерлік логиканың тармақталған қайталануының жаңа бейнесі". Applied Mathematics Letters 25 (2012), 1585–1589 беттер. Г. Жапаридзе, "Конструктивті жүйелердің логикалық негізі". Journal of Logic and Computation 22 (2012), 605–642 беттер. Г. Жапаридзе, "Негізгі қайталанулардың негізгі логикасын ажырату". Annals of Pure and Applied Logic 163 (2012), 377–389 беттер. Г. Жапаридзе, "Арифметикаға кіріспе I". Information and Computation 209 (2011), 1312–1354 беттер. Г. Жапаридзе, "Компьютерлік логикадағы формулалардан циркуенттерге дейін". Logical Methods in Computer Science 7 (2011), 2-ші шық, 1-ші мақала, 1–55 беттер. Г. Жапаридзе, "Компьютерлік логикадағы ауыстыру операторлары". Theoretical Computer Science 412 (2011), 971–1004 беттер. Г. Жапаридзе, "Компьютерлік логикаға негізделген қолданбалы теорияларға қарай". Journal of Symbolic Logic 75 (2010), 565–601 беттер. Г. Жапаридзе, "Алгоритмдік азайтудың көптеген түсініктері және екі логикасы". Studia Logica 91 (2009), 1–24 беттер. Г. Жапаридзе, "Бастапқыда ойын семантикасы болды". Games: Unifying Logic, Language and Philosophy. О. Майер, А. В. Пиетаринен және Т. Туленхеймо, ред. Springer 2009, 249–350 беттер. Г. Жапаридзе, "Компьютерлік логикадағы ретті операторлар". Information and Computation 206 (2008), 1443–1475 беттер. Г. Жапаридзе, "Циркулянтты есептеуді тереңдету". Journal of Logic and Computation 18 (2008), 983–1028 беттер. Г. Жапаридзе, "Пропозициялық деңгейдегі компьютерлік логиканың интуиционистік фрагменті". Annals of Pure and Applied Logic 147 (2007), 187–227 беттер. Г. Жапаридзе, "Интерактивті Тьюринг азайтуының логикасы". Journal of Symbolic Logic 72 (2007), 243–276 беттер. Г. Жапаридзе, "Интуициялық есептеу логикасы". Acta Cybernetica 18 (2007), 77–113 беттер. Г. Жапаридзе, "Шындықтан есептеуге дейін II". Theoretical Computer Science 379 (2007), 20–52 беттер. Г. Жапаридзе, "Шындықтан есептеуге дейін I". Theoretical Computer Science 357 (2006), 100–135 беттер. Г. Жапаридзе, "Циркулянтты есептеуге және абстрактілік ресурстық семантикаға кіріспе". Journal of Logic and Computation 16 (2006), 489–532 беттер. Г. Жапаридзе, "Компьютерлік логика: өзара әрекеттесудің формалды теориясы". Interactive Computation: The New Paradigm. Д. Голдин, С. Смолка және П. Вегнер, ред. Springer Verlag, Берлин 2006, 183–223 беттер. Г. Жапаридзе, "Пропозициялық есептеу логикасы II". ACM Transactions on Computational Logic 7 (2006), 331–362 беттер. Г. Жапаридзе, "Пропозициялық есептеу логикасы I". ACM Transactions on Computational Logic 7 (2006), 302–330 беттер. Г. Жапаридзе, "Компьютерлік логикаға кіріспе". Annals of Pure and Applied Logic 123 (2003), 1–99 беттер. Г. Жапаридзе, "Міндеттердің логикасы". Annals of Pure and Applied Logic 117 (2002), 261–293 беттер. Г. Жапаридзе, "Элементар міндеттердің пропозициялық логикасы". Notre Dame Journal of Formal Logic 41 (2000), No. 2, 171–183 беттер. Г. Жапаридзе және Д. ДеДжонг, "Дәлелдік логикасы". In: Handbook of Proof Theory, S. Buss, ред., North Holland, 1998, 475–545 беттер. Г. Жапаридзе, "Сызықтық логика тілі үшін конструктивті ойын семантикасы". Annals of Pure and Applied Logic 85 (1997), 87–156 беттер. Г. Жапаридзе, "Pi 1 консервативтілік логикасының арифметикалық толықтығының қарапайым дәлелі". Notre Dame Journal of Formal Logic 35 (1994), 346–354 беттер. Г. Жапаридзе, "Арифметикалық иерархияның логикасы". Annals of Pure and Applied Logic 66 (1994), 89–112 беттер. Г. Жапаридзе, "Біршама түсініктіліктің жалпыланған түсінігі және тиісті модальдық логика". Annals of Pure and Applied Logic 61 (1993), 113–160 беттер. Г. Жапаридзе, "Сызықтық төзімділіктің логикасы". Studia Logica 51 (1992), 249–277 беттер. Г. Жапаридзе, "Модальданбаған сандық белгілермен дәлелдеу логикасын болжау". Studia Logica 50 (1991), 149–160 беттер. Г. Жапаридзе, "Дәлелдіктің шешілетін және саналатын предикат логикасы". Studia Logica 49 (1990), 7–21 беттер. С. Артемов пен Г. Жапаридзе, "Крипкінің шекті модельдері және дәлелдену логикасының предикаттары". Journal of Symbolic Logic 55 (1990), 1090–1098 беттер. Г. Жапаридзе, "Дәлелдендірудің полимодальдық логикасы". Intensional Logics and Logical Structure of Theories. Metsniereba, Tbilisi, 1988, 16–48 беттер (орыс тілінде). С. Артемов пен Г. Жапаридзе, "Дәлелдіктің тиімді предикат логикалары туралы". Dokady Mathematics 297 (1987), 521–523 беттер (орыс тілінде). Ағылшын тіліне аудармасы: Soviet Mathematics Doklady 36, 478–480 беттер.

G. Japaridze, "Build your own clarithmetic I: Setup and completeness". Logical Methods is Computer Science 12 (2016), Issue 3, paper 8, pages 1–59. G. Japaridze, "Build your own clarithmetic II: Soundness". Logical Methods is Computer Science 12 (2016), Issue 3, paper 12, pages 1–62. G. Japaridze, "Introduction to clarithmetic II". Information and Computation 247 (2016), pages 290 312. G. Japaridze, "Introduction to clarithmetic III". Annals of Pure and Applied Logic 165 (2014), pages 241 252. G. Japaridze, "The taming of recurrences in computability logic through cirquent calculus, Part II". Archive for Mathematical Logic 52 (2013), pages 213 259. G. Japaridze, "The taming of recurrences in computability logic through cirquent calculus, Part I". Archive for Mathematical Logic 52 (2013), pages 173 212. G. Japaridze, "A new face of the branching recurrence of computability logic". Applied Mathematics Letters 25 (2012), pages 1585 1589. G. Japaridze, "A logical basis for constructive systems". Journal of Logic and Computation 22 (2012), pages 605 642. G. Japaridze, "Separating the basic logics of the basic recurrences". Annals of Pure and Applied Logic 163 (2012), pages 377 389. G. Japaridze, "Introduction to clarithmetic I". Information and Computation 209 (2011), pages 1312 1354. G. Japaridze, "From formulas to cirquents in computability logic". Logical Methods is Computer Science 7 (2011), Issue 2, Paper 1, pages 1–55. G. Japaridze, "Toggling operators in computability logic". Theoretical Computer Science 412 (2011), pages 971 1004. G. Japaridze, "Towards applied theories based on computability logic". Journal of Symbolic Logic 75 (2010), pages 565 601. G. Japaridze, "Many concepts and two logics of algorithmic reduction". Studia Logica 91 (2009), pages 1–24. G. Japaridze, "In the beginning was game semantics". Games: Unifying Logic, Language and Philosophy. O. Majer, A. V. Pietarinen and T. Tulenheimo, eds. Springer 2009, pages 249 350. G. Japaridze, "Sequential operators in computability logic". Information and Computation 206 (2008), pages 1443 1475. G. Japaridze, "Cirquent calculus deepened". Journal of Logic and Computation 18 (2008), pages 983 1028. G. Japaridze, "The intuitionistic fragment of computability logic at the propositional level". Annals of Pure and Applied Logic 147 (2007), pages 187 227. G. Japaridze, "The logic of interactive Turing reduction". Journal of Symbolic Logic 72 (2007), pages 243 276. G. Japaridze, "Intuitionistic computability logic". Acta Cybernetica 18 (2007), pages 77–113. G. Japaridze, "From truth to computability II". Theoretical Computer Science 379 (2007), pages 20–52. G. Japaridze, "From truth to computability I". Theoretical Computer Science 357 (2006), pages 100 135. G. Japaridze, "Introduction to cirquent calculus and abstract resource semantics". Journal of Logic and Computation 16 (2006), pages 489 532. G. Japaridze, "Computability logic: a formal theory of interaction". Interactive Computation: The New Paradigm. D. Goldin, S. Smolka and P. Wegner, eds. Springer Verlag, Berlin 2006, pages 183 223. G. Japaridze, "Propositional computability logic II". ACM Transactions on Computational Logic 7 (2006), pages 331 362. G. Japaridze, "Propositional computability logic I". ACM Transactions on Computational Logic 7 (2006), pages 302 330. G. Japaridze, "Introduction to computability logic". Annals of Pure and Applied Logic 123 (2003), pages 1–99. G. Japaridze, "The logic of tasks". Annals of Pure and Applied Logic 117 (2002), pages 261 293. G. Japaridze, "The propositional logic of elementary tasks". Notre Dame Journal of Formal Logic 41 (2000), No. 2, pages 171 183. G. Japaridze and D. DeJongh, "The logic of provability". In: Handbook of Proof Theory, S. Buss, ed., North Holland, 1998, pages 475 545. G. Japaridze, "A constructive game semantics for the language of linear logic". Annals of Pure and Applied Logic 85 (1997), pages 87–156. G. Japaridze, "A simple proof of arithmetical completeness for Pi 1 conservativity logic". Notre Dame Journal of Formal Logic 35 (1994), pages 346 354. G. Japaridze, "The logic of arithmetical hierarchy". Annals of Pure and Applied Logic 66 (1994), pages 89–112. G. Japaridze, "A generalized notion of weak interpretability and the corresponding modal logic". Annals of Pure and Applied Logic 61 (1993), pages 113 160. G. Japaridze, "The logic of linear tolerance". Studia Logica 51 (1992), pages 249 277. G. Japaridze, "Predicate provability logic with non modalized quantifiers". Studia Logica 50 (1991), pages 149 160. G. Japaridze, "Decidable and enumerable predicate logics of provability". Studia Logica 49 (1990), pages 7–21. S. Artemov and G. Japaridze, "Finite Kripke models and predicate logics of provability". Journal of Symbolic Logic 55 (1990), pages 1090 1098. G. Japaridze, "The polymodal logic of provability". Intensional Logics and Logical Structure of Theories. Metsniereba, Tbilisi, 1988, pages 16–48 (Russian). S. Artemov and G. Japaridze, "On effective predicate logics of provability". Dokady Mathematics 297 (1987), pages 521 523 (Russian). English translation in: Soviet Mathematics Doklady 36, pages 478 480.