Полимодальная логика Джапаридзе (GLP) - это система логики доказуемости с бесконечным множеством модальностей доказуемости . Эта система сыграла важную роль в некоторых приложениях алгебр доказуемости в теории доказательств и широко изучается с конца 1980-х годов. Он назван в честь Георгия Джапаридзе .
Язык и аксиоматизация
Язык GLP расширяет язык классической логики высказываний , включая бесконечные ряды [0], [1], [2], ... операторов необходимости. Их операторы двойной возможности <0>, <1>, <2>, ... определяются как < n > p = ¬ [ n ] ¬ p .
Все аксиомы GLP - это классические тавтологии и все формулы одной из следующих форм:
- [ n ] ( p → q ) → ([ n ] p → [ n ] q )
- [ n ] ([ n ] p → p ) → [ n ] p
- [ n ] p → [ n +1] p
- < n > p → [ n +1] < n > p
И правила вывода:
- Из p и p → q заключаем q
- Из p заключаем [0] p
Семантика доказуемости
Рассмотрим достаточно сильную теорию первого порядка T, такую как арифметика Пеано PA . Определим ряд теорий T 0 , T 1 , T 2 , ... следующим образом:
- T 0 - это T
- T n +1 является расширением T n с помощью дополнительных аксиом ∀ xF ( x ) для каждой формулы F ( x ), такой что T n доказывает все формулы F (0), F (1), F (2), ...
Для каждого n пусть Pr n ( x ) - естественная арифметизация предиката « x - гёделевское число предложения, доказуемого в T n » .
Реализация является функция * , который посылает каждый нелогического атом A языка ГПП в предложение с * на языке Т . Он распространяется на все формулы языка GLP, оговаривая, что * коммутирует с булевыми связками и что ([ n ] F ) * равно Pr n (' F *') , где ' F *' означает (числительное для ) гёделевское число F * .
Арифметическая теорема о полноте [1] для GLP утверждает , что формула F выводима в GLP тогда и только тогда, когда для каждой интерпретации * , предложение Р * доказуемо в T .
Вышеупомянутое понимание ряда теорий T 0 , T 1 , T 2 , ... - не единственное естественное понимание, обеспечивающее надежность и полноту GLP. Например, каждую теорию T n можно понимать как T, дополненную всеми истинными ∏ n предложениями в качестве дополнительных аксиом. Джордж Булос показали [2] , что ГПП остается звук и в комплекте с анализом ( арифметики второго порядка ) в роли теории базовой Т .
Другая семантика
Было показано [1], что GLP неполон по отношению к любому классу фреймов Крипке .
Естественная топологическая семантика GLP интерпретирует модальности как производные операторы политопологического пространства . Такие пространства называются GLP-пространствами, если они удовлетворяют всем аксиомам GLP. GLP полон относительно класса всех GLP-пространств. [3]
Вычислительная сложность
Проблема быть теоремой GLP является PSPACE-полной . Таким образом, та же проблема ограничивается только формулами GLP без переменных. [4]
История
GLP под названием GP был представлен Георгием Джапаридзе в его докторской диссертации «Модальные логические средства исследования доказуемости» ( МГУ , 1986) и опубликован двумя годами позже [1] вместе с (а) теоремой полноты для GLP с относительно его интерпретации доказуемости (впоследствии Беклемишев предложил более простое доказательство той же теоремы [5] ) и (б) доказательство того, что шкалы Крипке для GLP не существуют. Беклемишев также провел более обширное исследование моделей Крипке для GLP. [6] Топологические модели для GLP изучались Беклемишевым, Бежанишвили, Икардом и Габелая. [3] [7] Разрешимость GLP в полиномиальном пространстве была доказана И. Шапировским [8], а PSPACE-трудность ее фрагмента без переменных - Ф. Пахомовым. [4] Среди наиболее известных применений GLP является его применение в доказательстве-теоретический анализ арифметики Пеана , разработки канонического пути для восстановления порядкового обозначения до ɛ 0 из соответствующей алгебры, и построение простых комбинаторных независимых утверждений (Беклемишев [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.
Рекомендации
- ^ a b c Г. Джапаридзе, "Полимодальная логика доказуемости" . Интенсиональная логика и логическая структура теорий. Мецниереба, Тбилиси, 1988, с. 16–48.
- ^ Г. Булос, "Аналитическая полнота полимодальной логики Джапаридзе" . Анналы чистой и прикладной логики 61 (1993), стр. 95–111.
- ^ a b Л. Беклемишев, Д. Габелая, "Топологическая полнота логики доказуемости GLP" . Анналы чистой и прикладной логики 164 (2013), стр. 1201–1223.
- ^ a b Ф. Пахомов, "О сложности замкнутого фрагмента логики доказуемости Джапаридзе" . Архив математической логики 53 (2014), стр. 949–967.
- ^ Л. Беклемишев, "Упрощенное доказательство теоремы арифметической полноты для логики доказуемости GLP" . Труды Математического института им. В. А. Стеклова 2011. 274. С. 25–33.
- ^ Л. Беклемишев, "Семантика Крипке для логики доказуемости GLP" . Анналы чистой и прикладной логики 161, 756–774 (2010).
- ^ Л. Беклемишев, Г. Бежанишвили и Т. Икард, «О топологических моделях GLP». Способы теории доказательства, Ontos Mathematical Logic, 2, ред. Р. Шиндлер, Онтос Верлаг, Франкфурт, 2010 г., стр. 133–153.
- ^ И. Шапировский, "PSPACE-разрешимость полимодальной логики Джапаридзе" . Успехи в модальной логике 7 (2008), стр. 289-304.
- ^ Л. Беклемишев, "Алгебры доказуемости и ординалы теории доказательства, I" . Анналы чистой и прикладной логики 128 (2004), стр. 103–123.
- ^ Г. Булос, "Логика доказуемости". Издательство Кембриджского университета, 1993.