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

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

Перевод Гёделя – McKinsey – Тарского

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

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

$T(\bot )=\bot ,$

$T(A\land B)=T(A)\land T(B),$

$T(A\lor B)=T(A)\lor T(B),$

$T(A\to B)=\Box (T(A)\to T(B)).$

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

$T(\neg A)=\Box \neg T(A).$

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

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

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

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

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

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

$\tau L=\mathbf {S4} \oplus \{T(A)\mid L\vdash A\},$

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

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

$\Box (\Box (A\to \Box A)\to A)\to A$

над К. ​Наименьшим модальным компаньоном классической логики ( Льюиса , как тогда CPC) является S5 ее самым большим модальным компаньоном является логика

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

Еще примеры:

л	τL	σL	другие товарищи L
МПК	С4	Грз	S4.1 , Дум , ...
КС	С4.2	Гр.2	С4.1.2 , ...
ЛК	С4.3	Гр.3	С4.1.3 , С4.3Дум , ...
КТК	С5	Трив	см. ниже

Блока

Множество расширений суперинтуиционистской логики , упорядоченное по включению, образует полную решетку , обозначаемую Ext L. L Аналогично множество нормальных расширений модальной логики M представляет собой полную решетку NExt M . Операторы-компаньоны ρM , τL и σL можно рассматривать как отображения между решетками Ext IPC и NExt S4 :

$\rho \colon \mathrm {NExt} \,\mathbf {S4} \to \mathrm {Ext} \,\mathbf {IPC} ,$

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

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

Отображения ρ и σ являются обратными решеточными изоморфизмами Ext Grz IPC и NExt . взаимно

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

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

Семантическое описание

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

$x\sim y\iff x\,R\,y\land y\,R\,x$

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

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

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

A допустимо в ρ F тогда и только тогда, когда ( A ) допустимо в F. T

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

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

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

сохранения

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

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

Другая недвижимость

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

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

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

это правило

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

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

Ссылки

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