Полимодальная логика Джапаридзе - Japaridzes polymodal logic - Wikipedia

Полимодальная логика Джапаридзе (GLP), это система логика доказуемости с бесконечной доказуемостью модальности. Эта система сыграла важную роль в некоторых приложениях алгебр доказуемости в теория доказательств, и активно изучается с конца 1980-х годов. Он назван в честь Георгий Джапаридзе.

Язык и аксиоматизация

Язык GLP расширяет язык классических логика высказываний включением бесконечных серий [0], [1], [2], ... операторов «необходимости». Их двойственные операторы «возможности» <0>, <1>, <2>, ... определяются как <п>п = ¬[п]¬п.

Все аксиомы GLP - это классические тавтологии и все формулы одной из следующих форм:

  • [п](п → q) → ([п]п → [п]q)
  • [п]([п]п → п) → [п]п
  • [п]п → [п+1]п
  • <п>п → [п+1]<п>п

И правила вывода:

  • Из п и п → q заключить q
  • Из п заключить [0]п

Семантика доказуемости

Считайте «достаточно сильным» теория первого порядка Т Такие как Арифметика Пеано PA. Определите серию Т0,Т1,Т2, ... следующих теорий:

  • Т0 является Т
  • Тп+1 является продолжением Тп с помощью дополнительных аксиом ∀xF(Икс) для каждой формулы F(Икс) такие, что Тп доказывает все формулы F(0), F(1), F(2),...

Для каждого п, пусть Prп(Икс) - естественная арифметизация предиката «Икс это Число Гёделя предложения, доказуемого в Тп.

А реализация это функция *, которая отправляет каждый нелогичный атом а языка GLP в предложение а* языка Т. Он распространяется на все формулы языка GLP, оговаривая, что * коммутирует с булевыми связками и что ([п]F) * является Prп(‘F*'), куда 'F* ’Обозначает (цифру) гёделевское число F*.

An теорема арифметической полноты[1] для GLP утверждает, что формула F доказуемо в GLP тогда и только тогда, когда для каждой интерпретации * предложение F* доказывается в Т.

Вышеупомянутое понимание серии Т0,Т1,Т2, ... теорий - не единственное естественное понимание, обеспечивающее обоснованность и полноту GLP. Например, каждая теория Тп можно понимать как Т дополнен всем истинным ∏п предложения как дополнительные аксиомы. Джордж Булос показал[2] что GLP остается надежным и полным анализом (арифметика второго порядка) в роли базовой теории Т.

Другая семантика

GLP был показан[1] быть неполным относительно любого класса фреймов Крипке.

Естественная топологическая семантика GLP интерпретирует модальности как производные операторы политопологическое пространство. Такие пространства называются GLP-пространствами, если они удовлетворяют всем аксиомам GLP. GLP полон относительно класса всех GLP-пространств.[3]

Вычислительная сложность

Проблема быть теоремой GLP заключается в PSPACE-полный. Таким образом, та же проблема ограничивается только формулами GLP без переменных.[4]

История

GLP под названием GP был представлен Георгий Джапаридзе в своей кандидатской диссертации «Модальные логические средства исследования доказуемости» (Московский Государственный Университет, 1986) и опубликовано двумя годами позже[1] наряду с (а) теоремой о полноте для GLP относительно ее доказуемости интерпретации (впоследствии Беклемишев предложил более простое доказательство той же теоремы[5]) и (b) доказательство того, что шкалы Крипке для GLP не существуют. Беклемишев также провел более обширное исследование моделей Крипке для GLP.[6] Топологические модели GLP изучали Беклемишев, Бежанишвили, Икард и Габелая.[3][7]Разрешимость GLP в полиномиальном пространстве доказал И. Шапировский,[8] а PSPACE-твердость его беспеременного фрагмента доказал Ф. Пахомов.[4] Среди наиболее заметных применений GLP было его использование в теоретико-доказательном анализе. Арифметика Пеано, разрабатывая канонический способ восстановления порядковое обозначение вплоть до ɛ0 из соответствующей алгебры и построение простых комбинаторно независимых утверждений (Беклемишев [9]).

Обширный обзор GLP в контексте логики доказуемости в целом дал Джордж Булос в своей книге «Логика доказуемости».[10]

Литература

Рекомендации

  1. ^ а б c Г. Джапаридзе, «Полимодальная логика доказуемости». Интенсиональная логика и логическая структура теорий. Мецниереба, Тбилиси, 1988, с. 16–48.
  2. ^ Г. Булос, «Аналитическая полнота полимодальной логики Джапаридзе». Анналы чистой и прикладной логики 61 (1993), стр. 95–111.
  3. ^ а б Л. Беклемишев и Д. Габелая, «Топологическая полнота логики доказуемости GLP». Анналы чистой и прикладной логики 164 (2013), стр. 1201–1223.
  4. ^ а б Ф. Пахомов, «О сложности замкнутого фрагмента логики доказуемости Джапаридзе». Архив математической логики 53 (2014), стр. 949–967.
  5. ^ Л. Беклемишев, «Упрощенное доказательство теоремы об арифметической полноте для логики доказуемости GLP». Труды Математического института им. В. А. Стеклова 2011. 274. С. 25–33.
  6. ^ Л. Беклемишев, «Семантика Крипке для логики доказуемости GLP». Анналы чистой и прикладной логики 161, 756–774 (2010).
  7. ^ Л. Беклемишев, Г. Бежанишвили, Т. Икард, “О топологических моделях GLP”. Способы теории доказательства, Ontos Mathematical Logic, 2, ред. Р. Шиндлер, Онтос Верлаг, Франкфурт, 2010 г., стр. 133–153.
  8. ^ И. Шапировский, «PSPACE-разрешимость полимодальной логики Джапаридзе». Успехи в модальной логике 7 (2008), стр. 289-304.
  9. ^ Л. Беклемишев, "Алгебры доказуемости и ординалы теории доказательства, I". Анналы чистой и прикладной логики 128 (2004), стр. 103–123.
  10. ^ Г. Булос, «Логика доказуемости». Издательство Кембриджского университета, 1993.