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

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

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

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

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

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

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

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

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

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

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

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

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

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

Вышеупомянутое понимание серии Т₀,Т₁,Т₂, ... теорий - не единственное естественное понимание, обеспечивающее обоснованность и полноту 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 было его использование в теоретико-доказательном анализе. Арифметика Пеано, разрабатывая канонический способ восстановления порядковое обозначение вплоть до ɛ₀ из соответствующей алгебры и построение простых комбинаторно независимых утверждений (Беклемишев ^[9]).

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

Литература

Л. Беклемишев, "Алгебры доказуемости и ординалы теории доказательства, I". Анналы чистой и прикладной логики 128 (2004), стр. 103–123.
Л. Беклемишев, Й. Йостен и М. Вервурт, «Финальная обработка закрытого фрагмента логики доказуемости Джапаридзе». Журнал логики и вычислений 15 (2005), № 4, стр. 447–463.
Л. Беклемишев, «Семантика Крипке для логики доказуемости GLP». Анналы чистой и прикладной логики 161, 756–774 (2010).
Л. Беклемишев, Г. Бежанишвили, Т. Икар, “О топологических моделях GLP”. Способы теории доказательства, Ontos Mathematical Logic, 2, ред. Р. Шиндлер, Онтос Верлаг, Франкфурт, 2010 г., стр. 133–153.
Л. Беклемишев, “Об интерполяции Крейга и свойствах неподвижной точки GLP”. Доказательства, категории и вычисления. С. Феферман и др., Редакторы, College Publications, 2010. стр. 49–60.
Л. Беклемишев, «Порядковая полнота бимодальной логики доказуемости GLB». Конспект лекций по информатике 6618 (2011), стр. 1–15.
Л. Беклемишев, «Упрощенное доказательство теоремы об арифметической полноте для логики доказуемости GLP». Труды Математического института им. В. А. Стеклова 2011. 274. С. 25–33.
Л. Беклемишев и Д. Габелая, «Топологическая полнота логики доказуемости GLP». Анналы чистой и прикладной логики 164 (2013), стр. 1201–1223.
Г. Булос, «Аналитическая полнота полимодальной логики Джапаридзе». Анналы чистой и прикладной логики 61 (1993), стр. 95–111.
Г. Булос, «Логика доказуемости». Издательство Кембриджского университета, 1993.
Е.В. Дашков, “О положительном фрагменте полимодальной логики доказуемости GLP”. Математические заметки 2012; 91: 318–333.
Д. Фернандес-Дуке и Х. Йостен, «Хорошие порядки в трансфинитной алгебре Джапаридзе». Логический журнал IGPL 22 (2014), стр. 933–963.
Г. Джапаридзе, «Полимодальная логика доказуемости». Интенсиональная логика и логическая структура теорий. Мецниереба, Тбилиси, 1988, с. 16–48.
Ф. Пахомов, «О сложности замкнутого фрагмента логики доказуемости Джапаридзе». Архив математической логики 53 (2014), стр. 949–967.
Шамканов Д.С., «Интерполяционные свойства для логик доказуемости GL и GLP». Труды Математического института им. В. А. Стеклова 2011. 274. С. 303–316.
И. Шапировский, «PSPACE-разрешимость полимодальной логики Джапаридзе». Успехи в модальной логике 7 (2008), стр. 289–304.