Модальный компаньон

В логике , А модальный спутник из суперинтуиционистского (промежуточного) логики L является нормальной модальной логикой , которая интерпретирует L по некоторому каноническому переводу, описанные ниже. Модальные компаньоны обладают различными свойствами исходной промежуточной логики , что позволяет изучать промежуточную логику с помощью инструментов, разработанных для модальной логики.

Перевод Гёделя – МакКинси – Тарского [ править ]

Пусть A - пропозициональная интуиционистская формула. Модальная формула T ( A ) определяется индукцией по сложности A :

${\ Displaystyle T (p) = \ Box p,}$для любой пропозициональной переменной ,${\ displaystyle p}$

${\ Displaystyle Т (\ бот) = \ бот,}$

${\ Displaystyle Т (А \ земля В) = Т (А) \ земля Т (В),}$

${\ Displaystyle Т (А \ лор В) = Т (А) \ лор Т (В),}$

${\ Displaystyle T (от A \ к B) = \ Box (T (A) \ к T (B)).}$

Поскольку отрицание в интуиционистской логике определяется как , мы также имеем${\ displaystyle A \ to \ bot}$

${\ Displaystyle T (\ neg A) = \ Box \ neg T (A).}$

T называется перевод Геделя или Геделя - McKinsey - Тарского перевод . Перевод иногда представляется несколько иначе: например, можно вставить перед каждой подформулой. Все такие варианты доказуемо эквивалентны в S4 .${\ displaystyle \ Box}$

Модальные компаньоны [ править ]

Для любой нормальной модальной логики M , расширяющей S4 , определим ее si-фрагмент ρM как

${\ Displaystyle \ rho M = \ {A \ mid M \ vdash T (A) \}.}$

Si-фрагмент любого нормального расширения S4 является суперинтуиционистской логикой. Модальная логика M является модальным компаньоном суперинтуиционистской логики L if .${\ Displaystyle L = \ rho M}$

У каждой суперинтуиционистской логики есть модальные спутники. Наименьший модальный спутник из L является

${\ Displaystyle \ тау L = \ mathbf {S4} \ oplus \ {T (A) \ mid L \ vdash A \},}$

где обозначает нормальное закрытие. Можно показать, что каждая суперинтуиционистская логика также имеет самого большого модального компаньона , который обозначается σL . Модальная логика M является компаньоном L тогда и только тогда, когда .${\ displaystyle \ oplus}$${\ Displaystyle \ тау L \ substeq M \ substeq \ sigma L}$

Например, S4 сам по себе является наименьшим модальным компаньоном интуиционистской логики ( IPC ). Самым большим модальным компаньоном IPC является логика Гжегорчика Grz , аксиоматизированная аксиомой

${\ Displaystyle \ Box (\ Box (от A \ до \ Box A) \ до A) \ до A}$

над K . Самый маленький модальный компаньон классической логики ( CPC ) - это S5 Льюиса , тогда как его самый большой модальный компаньон - это логика

${\ displaystyle \ mathbf {Triv} = \ mathbf {K} \ oplus (A \ leftrightarrow \ Box A).}$

Еще примеры:

Изоморфизм Блока – Эсакии [ править ]

Набор расширений суперинтуиционистской логики L упорядочены по включению , образует полную решетку , обозначаемый внешн л . Аналогичным образом , множество нормальных расширений модальной логики М является полной решеткой СЛЕДУЮЩИХ М . Сопутствующие операторы ρM , τL и σL можно рассматривать как отображения между решетками Ext IPC и NExt S4 :

${\ Displaystyle \ rho \ двоеточие \ mathrm {NExt} \, \ mathbf {S4} \ to \ mathrm {Ext} \, \ mathbf {IPC},}$

${\displaystyle \tau ,\sigma \colon \mathrm {Ext} \,\mathbf {IPC} \to \mathrm {NExt} \,\mathbf {S4} .}$

Легко видеть, что все три являются монотонными и являются функцией идентичности на Ext IPC . Л. Максимова и В. Рыбаков показали, что ρ , τ и σ на самом деле являются полными , джойн-полными и встречно-полными решеточными гомоморфизмами соответственно. Краеугольным камнем теории модальных спутников является теорема Блока – Эсакия , независимо доказанная Вимом Блоком и Лео Эсакия . Говорится${\displaystyle \rho \circ \tau =\rho \circ \sigma }$

Отображения р и σ взаимно обратной решетки изоморфизмам из Ext МПК и СЛЕДУЮЩИЙ Grz .

Соответственно, σ и ограничение по р к следующему Grz называют изоморфизмом Блок-Esakia . Важное следствие в Блоке-Esakia теорема является простым синтаксическим описанием крупнейших модальных компаньонов: для каждой суперинтуиционистской логики L ,

${\displaystyle \sigma L=\tau L\oplus \mathbf {Grz} .}$

Семантическое описание [ править ]

Перевод Гёделя имеет теоретико-фреймовой аналог. Позвольте быть транзитивным и рефлексивным модальным общим фреймом . Предпорядок R индуцирует отношение эквивалентности${\displaystyle \mathbf {F} =\langle F,R,V\rangle }$

${\displaystyle x\sim y\iff x\,R\,y\land y\,R\,x}$

на F , который определяет точки, принадлежащие одному кластеру. Пусть будет индуцированный фактор частичного порядка (т.е. ρF есть множество классов эквивалентности в ) и положить${\displaystyle \langle \rho F,\leq \rangle =\langle F,R\rangle /{\sim }}$ ${\displaystyle \sim }$

${\displaystyle \rho V=\{A/{\sim }\mid A\in V,A=\Box A\}.}$

Тогда это интуиционистский общий каркас, называемый скелетом из F . Дело каркасного строительства является то , что он сохраняет справедливость по модулю гёделевской перевод: для любой интуиционистской формулы А ,${\displaystyle \rho \mathbf {F} =\langle \rho F,\leq ,\rho V\rangle }$

Справедливо в р F тогда и только тогда , когда Т ( ) действует в F .

Следовательно, si-фрагмент модальной логики M можно определить семантически: если M полон относительно класса C транзитивных рефлексивных общих фреймов, то ρM полон относительно класса .${\displaystyle \{\rho \mathbf {F} ;\,\mathbf {F} \in C\}}$

Самые большие модальные компаньоны также имеют семантическое описание. Для любой интуиционистской общей шкалы пусть σV будет замыканием V относительно булевых операций (двоичное пересечение и дополнение ). Можно показать, что σV замкнута относительно , таким образом, является общей модальной шкалой. Остов сг F изоморфна F . Если L - суперинтуиционистская логика, полная относительно класса C общих фреймов, то ее наибольший модальный компаньон σL полон относительно .${\displaystyle \mathbf {F} =\langle F,\leq ,V\rangle }$${\displaystyle \Box }$${\displaystyle \sigma \mathbf {F} =\langle F,\leq ,\sigma V\rangle }$${\displaystyle \{\sigma \mathbf {F} ;\,\mathbf {F} \in C\}}$

Каркас рамки Крипке сам по себе является рамой Крипке. С другой стороны, σ F никогда не является фреймом Крипке, если F - фрейм Крипке бесконечной глубины.

Теоремы сохранения [ править ]

Ценность модальных компаньонов и теоремы Блока – Эсакии как инструмента для исследования промежуточных логик проистекает из того факта, что многие интересные свойства логик сохраняются некоторыми или всеми отображениями ρ , σ и τ . Например,

• разрешимость сохраняется по ρ , τ и σ ,
• свойство конечной модели сохраняется посредством ρ , τ и σ ,
• табличность сохраняется по ρ и σ ,
• Полнота Крипке сохраняется по р и т ,
• определимость первого порядка на шкалах Крипке сохраняется по р и т .

Другие свойства [ править ]

Каждая промежуточная логика L имеет бесконечное количество модальных компаньонов, и, более того, набор модальных компаньонов L содержит бесконечную убывающую цепочку . Например, состоит из S5 и логики для каждого положительного целого числа n , где - n -элементный кластер. Множество модальных спутников любого L либо счетно , либо имеет мощность континуума . Рыбаков показал , что решетка внешн л может быть встроен в${\displaystyle \rho ^{-1}(L)}$${\displaystyle \rho ^{-1}(\mathbf {CPC} )}$${\displaystyle L(C_{n})}$${\displaystyle C_{n}}$${\displaystyle \rho ^{-1}(L)}$; в частности, у логики есть континуум модальных компаньонов, если у нее есть континуум расширений (это верно, например, для всех промежуточных логик ниже KC ). Неизвестно, верно ли и обратное.

Перевод Гёделя может применяться как к правилам, так и к формулам: перевод правила

${\displaystyle R={\frac {A_{1},\dots ,A_{n}}{B}}}$

это правило

${\displaystyle T(R)={\frac {T(A_{1}),\dots ,T(A_{n})}{T(B)}}.}$

Правило R является допустимым в логике L , если множество теорем L замкнут относительно R . Легко видеть , что R является допустимым в суперинтуиционистских логиках L всякий раз , когда Т ( R ) является допустимым в модальном спутнике L . Обратное не верно вообще, но это имеет место для наибольшего модальных компаньона L .

Ссылки [ править ]

• Александр Чагров и Михаил Захарящев, Модальная логика , т. 35 из Oxford Logic Guides, Oxford University Press, 1997.
• Рыбаков Владимир В. Допустимость правил логического вывода . 136 исследований по логике и основам математики, Elsevier, 1997.