Георгий Джапаридзе: вклад в логику и теоретическую информатику.

Введение

Георгий Джапаридзе (также Георгие Джапаридзе) — грузинско-американский исследователь в области логики и теоретической информатики. В настоящее время он является профессором на кафедре вычислительных наук Университета Вилланова. Джапаридзе наиболее известен как изобретатель логики вычислимости, циркуэнтного исчисления и полимодальной логики Джапаридзе.

Исследования

В 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. O. Majer, A. V. Pietarinen и T. Tulenheimo, eds. 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. D. Goldin, S. Smolka и P. Wegner, eds. Springer Verlag, Berlin 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, ed., 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 (на русском языке). С. Артемов и Г. Япаридзе, "Об эффективных предикатных логиках доказуемости". Doklady Mathematics 297 (1987), страницы 521–523 (на русском языке). English translation in: Soviet Mathematics Doklady 36, pages 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.