| Математический сборник |
|
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье) О кванторной версии модальной логики Белнапа–Данна А. В. Грефенштейн, С. О. Сперанский Математический институт им. В. А. Стеклова Российской академии наук, г. Москва
Англоязычная версия:
Sbornik: Mathematics, 2024, Volume 215, Issue 3, Pages DOI: https://doi.org/10.4213/sm9981e 
Реферативные базы данных:
     § 1. ВведениеКванторная интуиционистская логика $\mathsf{QInt}$ играет ключевую роль в конструктивной математике. Среди ее интерпретаций особое место занимают семантика реализуемости по Клини и неформальная интерпретация Брауэра–Гейтинга–Колмогорова (см. [1] и, скажем, [2; гл. 1]). Однако у $\mathsf{QInt}$ имеется определенный недостаток: хотя из каждого вывода $\Phi$ в интуиционистской теории чисел можно извлечь способ верификации $\Phi$, вывод $\neg \Phi$ не дает прямого способа фальсификации $\Phi$, а лишь сводит предположения о верификации $\Phi$ к абсурду1 (см. [3] и [4]). В частности, это влечет отсутствие “негативного дизъюнктивного свойства”: из выводимости $\neg (\Phi \wedge \Psi)$, вообще говоря, не следует выводимость $\neg \Phi$ или $\neg \Psi$. С целью устранения вышеупомянутого недостатка Д. Нельсон предложил обогатить язык $\mathsf{QInt}$ путем добавления “сильного отрицания” $\sim$, которое отвечает непосредственно за фальсификацию, и распространить семантику реализуемости на новый язык (см. [4], а также [5]). Так возникла логика $\mathsf{QN3}$. Затем было описано ее полезное обобщение $\mathsf{QN4}$, которое позволяет работать с противоречивыми данными (см. [6]). При этом $\mathsf{QN3}$ расширяет $\mathsf{QN4}$ путем добавления схемы Далее для любой кванторной логики $\mathsf{Q}L$ мы будем обозначать ее пропозициональную версию2 через $L$. Отметим, что при удалении интуиционистской импликации $\mathsf{N3}$ превращается в сильную трехзначную логику Клини, имеющую алгоритмическую интерпретацию, а $\mathsf{N4}$ – в хорошо известную четырехзначную логику Белнапа–Данна (см. [8; § 64] и [9], [10]).Весьма важную роль в понимании $\mathsf{QInt}$ играет трансляция Гёделя–МакКинси–Тарского из $\mathsf{QInt}$ в модальную логику $\mathsf{QS4}$, т.е. рефлексивно-транзитивное расширение модальной логики $\mathsf{QK}$. Хотелось бы иметь аналогичное понимание логик $\mathsf{QN3}$ и $\mathsf{QN4}$. В пропозициональном случае эта задача была решена С. П. Одинцовым и Х. Вансингом в [11]:
Тем не менее до сих пор ничего не было известно о ситуации в кванторном случае, несмотря на то что конструктивные теории формулируются именно в кванторном языке. Наша цель – разработать кванторную версию $\mathsf{BK}$, доказать для нее и некоторых ее расширений теоремы о сильной полноте относительно подходящей семантики возможных миров, а также обобщить результат о точных вложениях на $\mathsf{QN3}$ и $\mathsf{QN4}$. Мы рассмотрим семантику как с расширяющимися, так и с постоянными носителями. Кроме того, мы обсудим интерполяционные свойства для $\mathsf{QBK}$-расширений. § 2. СинтаксисДля простоты мы ограничимся рассмотрением сигнатур без равенства и без функциональных символов4. Пусть $\sigma$ – сигнатура. Обозначим через $\mathrm{Pred}_{\sigma}$ и $\mathrm{Const}_{\sigma}$ множества всех ее предикатных и константных символов соответственно. Здесь и далее считаем, что $\mathrm{Pred}_{\sigma} \ne \varnothing$. Зафиксируем счетное множество $\mathrm{Var}$, элементы которого будут называться переменными. Обозначим через $\mathrm{Term}_{\sigma}$ множество всех $\sigma$-термов. Таким образом, $\mathrm{Term}_{\sigma} = \mathrm{Var} \cup \mathrm{Const}_{\sigma}$. Наш логический алфавит будет состоять из:
Обозначим через $\mathrm{Form}_{\sigma}$ множество всех $\sigma$-формул. Для каждой $\Phi \in \mathrm{Form}_{\sigma}$ положим
$$
\begin{equation*}
\mathrm{FV}(\Phi):= \{x \in \mathrm{Var} \mid x\ \text{свободна в}\ \Phi\}.
\end{equation*}
\notag
$$
Под $\sigma$-подстановками мы понимаем функции из $\mathrm{Var}$ в $\mathrm{Term}_\sigma$. Если $\mathrm{FV} (\Phi) \subseteq \{x_1, \dots, x_n\}$, то для каждой $\sigma$-подстановки $\lambda$ через $\lambda \Phi$ обозначается результат (одновременной) замены всех свободных вхождений $x_1,\dots,x_n$ в $\Phi$ на $\lambda (x_1),\dots, \lambda (x_n)$ соответственно. В случае, когда
$$
\begin{equation*}
\lambda=\{(x, t)\} \cup \{(y, y) \mid y \in \mathrm{Var}\text{ и }y \ne x\},
\end{equation*}
\notag
$$
где $x \in \mathrm{Var}$ и $t \in \mathrm{Term}_{\sigma}$, мы будем нередко писать $\Phi (x/t)$ вместо $\lambda\Phi$. Наконец, $\sigma$-подстановка $\lambda$ называется основной, если $\lambda (x) \in \mathrm{Const}_{\sigma}$ для всех $x \in \mathrm{Var}$. Для удобства введем следующие сокращения:
Обозначим через $\mathrm{Sent}_{\sigma}$ множество всех $\sigma$-предложений, т.е. $\sigma$-формул без свободных переменных. Произвольные подмножества $\mathrm{Sent}_{\sigma}$ будем называть $\sigma$-теориями. Как обычно, под $\sigma$-структурами понимаются непустые множества с заданными над ними интерпретациями для символов из $\sigma$. Пусть $\mathfrak{A}$ – произвольная $\sigma$-структура, $A$ – ее носитель. Для каждого $\varepsilon \in \sigma$ положим
$$
\begin{equation*}
\varepsilon^{\mathfrak{A}}:=\text{интерпретация }\varepsilon\ \text{в}\ \mathfrak{A}.
\end{equation*}
\notag
$$
Если расширить $\sigma$ до сигнатуры
$$
\begin{equation*}
\sigma_A:=\sigma \cup \{\underline{a} \mid a \in A\},
\end{equation*}
\notag
$$
где $\underline{a}$ суть новые константные символы, то можно будет перейти от самой $\mathfrak{A}$ к ее $\sigma_A$-обогащению $\mathfrak{A}^{\ast}$ такому, что
$$
\begin{equation*}
\underline{a}^{\mathfrak{A}^{\ast}}:=a \quad \text{для любого } \ a\in A.
\end{equation*}
\notag
$$
При этом $\sigma_A$-формулы будут также называться $A$-формулами, а $\sigma_A$-подстановки – $A$-подстановками. Если $\Phi$ – $A$-предложение, мы будем часто писать $\mathfrak{A} \Vdash \Phi$ вместо $\mathfrak{A}^{\ast} \Vdash \Phi$.
§ 3. Гильбертовское исчислениеНаше исчисление для кванторной версии $\mathsf{BK}$ расширяет дедуктивную систему для $\mathsf{BK}$ из [11]. В нем используются следующие схемы аксиом.
Также в нем используются следующие правила вывода.
Обозначим через $\mathsf{QBK}_{\sigma}$ наименьшее множество $\sigma$-формул, содержащее все аксиомы нашего исчисления (в сигнатуре $\sigma$) и замкнутое относительно всех его правил вывода. В дальнейшем, когда выбор $\sigma$ не имеет принципиального значения или же подразумевается логика в целом (без привязки к конкретной сигнатуре), нижний индекс $\sigma$ будет часто опускаться. Утверждение 3.1. $\mathsf{QBK}$ включает схему Крипке Кроме того, $\mathsf{QBK}$ замкнута относительно правила нормализации
Теперь проверим замкнутость относительно правила нормализации. Предположим, что $\Phi$ лежит в $\mathsf{QBK}$. Тогда $\Box \Phi$ также будет лежать в $\mathsf{QBK}$:
Утверждение доказано. Для каждого $\Gamma \subseteq \mathrm{Form}_{\sigma}$ положим
$$
\begin{equation*}
\operatorname{Disj} (\Gamma):=\{\Phi_1 \vee \dots \vee \Phi_n \mid n \in \mathbb{N}\ \text{и}\ \{\Phi_1, \dots, \Phi_n\} \subseteq \Gamma\}.
\end{equation*}
\notag
$$
При этом пустая дизъюнкция отождествляется с $\bot$. Для данных $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ мы пишем5 $\Gamma \vdash \Delta$, если и только если некоторый элемент $\operatorname{Disj} (\Delta)$ можно получить из элементов $\Gamma \,{\cup}\, \mathsf{QBK}_{\sigma}$ с помощью $\mathrm{MP}$, $\mathrm{BR1}$ и $\mathrm{BR2}$. Поскольку тут не применяются модальные правила ($\mathrm{MB}$ и $\mathrm{MD}$), отношение выводимости $\vdash$ имеет локальный характер в том смысле, что оно призвано сохранять истинность в конкретных мирах (см. определение отношения семантического следования в § 4); вместе с тем $\mathrm{MB}$ и $\mathrm{MD}$ будут действовать глобально, т.е. сохранять истинность в моделях, но не в конкретных мирах этих моделей. Разумеется, когда $\Delta = \{\Phi\}$, мы обычно пишем $\Gamma \vdash \Phi$ вместо $\Gamma \vdash \{\Phi\}$. Теорема 3.2 (о дедукции). Для любых $\Gamma \cup \{\Phi\} \subseteq \mathrm{Sent}_{\sigma}$ и $\Psi \in \mathrm{Form}_{\sigma}$ имеем6 Доказательство аналогично случаю классической логики первого порядка. Как и другие логики с сильным отрицанием, $\mathsf{BK}$ не замкнута относительно обычного правила замены (см. [11]). Разумеется, то же самое будет верно для $\mathsf{QBK}$, однако для формального обоснования этого факта нужна подходящая семантика возможных миров, которая появится лишь в § 4. Тем не менее “позитивное” и “слабое” правила замены из [11] можно без особого труда обобщить на кванторный случай. Теорема 3.3 (позитивное правило замены). Пусть $\{\Phi, \Psi, \Theta\} \subseteq \mathrm{Form}_{\sigma}$. Предположим, что $\Phi'$ получается из $\Phi$ заменой некоторых вхождений $\Psi$ на $\Theta$, причем ни одно из этих вхождений не находится в области действия $\sim$. Тогда $\vdash \Psi \leftrightarrow \Theta$ влечет $\vdash \Phi \leftrightarrow \Phi'$. Доказательство. Мы ограничимся рассмотрением случаев, когда $\Phi$ начинается с $\forall$ или $\exists$, так как остальные случаи были фактически рассмотрены С. П. Одинцовым и Х. Вансингом. Кроме того, можно считать, что $\Psi \ne \Phi$, поскольку иначе утверждение тривиально.
Пусть $\Phi = \forall\,x\ \Omega$. Ясно, что части $\Omega$ соответствует $\Omega'$ такая, что $\Phi' = \forall\,x\ \Omega'$. Тогда $\Phi \leftrightarrow \Phi'$ выводится стандартным образом:
Аналогично для $\Phi = \exists\,x\ \Omega$. Теорема доказана. Для удобства в дальнейшем мы будем обозначать применение теоремы 3.3 как $\mathrm{PR}$, от английского “positive replacement”. Теорема 3.4 (слабое правило замены). Пусть $\{\Phi, \Psi, \Theta\} \subseteq \mathrm{Form}_{\sigma}$. Предположим, что $\Phi'$ получается из $\Phi$ заменой некоторых вхождений $\Psi$ на $\Theta$. Тогда $\vdash \Psi \Leftrightarrow \Theta$ влечет $\vdash \Phi \Leftrightarrow \Phi'$. Доказательство. Мы ограничимся рассмотрением случаев, когда $\Phi$ начинается с $\sim$, $\forall$ или $\exists$. Кроме того, можно считать, что $\Psi \ne \Phi$.
Пусть $\Phi = \, \sim \Omega$. Ясно, что части $\Omega$ соответствует $\Omega'$ такая, что $\Phi' = \, \sim \Omega'$. Тогда $\Phi \Leftrightarrow \Phi'$ можно легко вывести:
Пусть $\Phi = \forall\,x\ \Omega$. Значит, части $\Omega$ соответствует $\Omega'$ такая, что $\Phi' = \forall\,x\ \Omega'$. Тогда $\Phi \Leftrightarrow \Phi'$ можно вывести следующим образом:
Аналогично для $\Phi = \exists\,x\ \Omega$. Теорема доказана. Для удобства в дальнейшем мы будем обозначать применение теоремы 3.4 как $\mathrm{WR}$, от английского “weak replacement”. Говорят, что $\sigma$-формула $\Phi$ является негативной нормальной формой или, сокращенно, н.н.ф., если каждое вхождение $\sim$ в $\Phi$ непосредственно предшествует некоторой атомарной подформуле7. Наша ближайшая цель – доказать сильную версию теоремы об н.н.ф. для $\mathsf{QBK}$. Здесь “сильная” указывает на то, что мы будем использовать не $\leftrightarrow$ (как в [13], например), а $\Leftrightarrow$ (ср. [16; утверждение 3.1]). На этом пути полезным оказывается Утверждение 3.5. Следующие схемы выводимы8 в $\mathsf{QBK}$. $\mathrm{A1}$. $\sim \neg \Phi \Leftrightarrow \neg \neg \Phi$. $\mathrm{A2}$. $(\Phi \to \Psi) \Leftrightarrow (\neg \Phi \vee \Psi)$.
(вспомним, что $\neg \Phi$ – сокращение для $\Phi \to \bot$). Теперь выведем $\neg \neg \Phi \to \sim \neg \Phi$:
Таким образом, $\vdash \sim \neg \Phi \leftrightarrow \neg \neg \Phi$ для всех $\Phi \in \mathrm{Form}_{\sigma}$. Наконец, заметим, что
Стало быть, $\vdash \sim \neg \Phi \Leftrightarrow \neg \neg \Phi$ для любой $\Phi \in \mathrm{Form}_{\sigma}$. $\mathrm{A2}$. Понятно, что $(\Phi \to \Psi) \leftrightarrow (\neg \Phi \vee \Psi)$ можно вывести так же, как в классической логике. Покажем выводимость $\sim (\Phi \to \Psi) \leftrightarrow\, \sim (\neg \Phi \vee \Psi)$:
Утверждение доказано. Для каждой $\mathrm{S} \in \{\mathrm{SN1}, \mathrm{SN2}, \mathrm{SN3}, \mathrm{SN6}, \mathrm{SN7}, \mathrm{M1}, \mathrm{M2}\}$ обозначим через $\mathrm{S}^{\ast}$ схему, получающуюся из $\mathrm{S}$ посредством замены $\leftrightarrow$ на $\Leftrightarrow$. Лемма 3.6. $\mathrm{SN1}^{\ast}$, $\mathrm{SN2}^{\ast}$, $\mathrm{SN3}^{\ast}$, $\mathrm{M1}^{\ast}$ и $\mathrm{M2}^{\ast}$ выводимы9 в $\mathsf{QBK}$. Доказательство. $\mathrm{SN1}^{\ast}$. Очевидно, $\sim \sim \sim\Phi \leftrightarrow\, \sim\Phi$ лежит в $\mathsf{QBK}$ (как частный случай $\mathrm{SN1}$).
$\mathrm{SN2}^{\ast}$. Покажем, что $\sim \sim (\Phi \wedge \Psi) \leftrightarrow {\sim (\sim\Phi \, \vee\, \sim \Psi)}$ лежит в $\mathsf{QBK}$:
$\mathrm{SN3}^{\ast}$. Этот случай аналогичен случаю $\mathrm{SN2}^{\ast}$. $\mathrm{M1}^{\ast}$. Покажем, что ${\sim {\neg \Box \Phi}} \leftrightarrow {\sim {\Diamond \neg \Phi}}$ лежит в $\mathsf{QBK}$:
$\mathrm{M2}^{\ast}$. Этот случай аналогичен случаю $\mathrm{M1}^{\ast}$. Лемма доказана. Доказательство. $\mathrm{SN6}^{\ast}$. Покажем, что ${\sim {\sim \forall\,x\ \Phi}} \leftrightarrow {\sim \exists\,x\ \sim\Phi}$ лежит в $\mathsf{QBK}$:
$\mathrm{SN7}^{\ast}$. Этот случай аналогичен случаю $\mathrm{SN6}^{\ast}$. Лемма доказана. Вместе с тем в $\mathrm{SN4}$ нельзя заменить $\leftrightarrow$ на $\Leftrightarrow$ (формально это можно обосновать с помощью подходящей семантики возможных миров). Однако вместо $\mathrm{SN4}$ можно использовать схему формул
$$
\begin{equation}
{\sim (\Phi \to \Psi)} \Leftrightarrow ({\neg \neg \Phi} \, \wedge\, \sim \Psi),
\end{equation}
\tag{SN4$'$}
$$
которую нетрудно получить с помощью результатов выше:
Теперь мы готовы установить следующее. Теорема 3.8 (о негативной нормальной форме, сильная версия). Для любой $\sigma$-формулы $\Phi$ существует н.н.ф. $\overline{\Phi}$ такая, что $\Phi \Leftrightarrow \overline{\Phi} \in \mathsf{QBK}_{\sigma}$. Более того, имеется алгоритм, который по данной $\sigma$-формуле $\Phi$ строит подходящую н.н.ф. $\overline{\Phi}$. Доказательство. Посредством простой индукции по построению $\Phi$, где используются правило $\mathrm{WR}$ и схемы $\mathrm{SN1}^{\ast}$, $\mathrm{SN2}^{\ast}$, $\mathrm{SN3}^{\ast}$, $\mathrm{SN4}'$, $\mathrm{SN6}^{\ast}$, $\mathrm{SN7}^{\ast}$, $\mathrm{M3}$ и $\mathrm{M4}$. При этом $\mathrm{M3}$ и $\mathrm{M4}$ удобно переписать так.
$\mathrm{M3}'$. ${\sim \Box \Phi} \Leftrightarrow {\Diamond \sim\Phi}$. $\mathrm{M4}'$. ${\sim \Diamond \Phi} \Leftrightarrow {\Box \sim\Phi}$. Теорема доказана. Замечание 3.9. Для конструктивных логик Нельсона (пропозициональных или кванторных) аналог теоремы 3.8 не имеет места: там импликация имеет значительно более сложный, интуиционистский характер, и можно получить лишь слабую версию теоремы об н.н.ф. Наконец, под $\mathsf{QBK}$-расширениями будут пониматься надмножества $\mathsf{QBK}$, замкнутые относительно формульных подстановок10 и всех правил вывода (в том числе модальных). Для данного $\mathsf{QBK}$-расширения $L$ положим
$$
\begin{equation*}
\Gamma \vdash_{L} \Delta \quad :\Longleftrightarrow \quad L \cup \Gamma \vdash \Delta.
\end{equation*}
\notag
$$
Если $L$ – $\mathsf{QBK}$-расширение, а $\mathrm{S}_1, \dots,\mathrm{S}_n$ – схемы формул, то через $L\,{+}\, \{\mathrm{S}_1, \dots, \mathrm{S}_n\}$ мы будем обозначать наименьшее $\mathsf{QBK}$-расширение, включающее $L$ и все частные случаи $\mathrm{S}_1$, …, $\mathrm{S}_n$. На самом деле все эти понятия формально зависят от выбора $\sigma$, однако из контекста всегда будет ясно, о какой сигнатуре идет речь, либо мы будем явно писать $L_{\sigma}$ вместо $L$. Нетрудно видеть, что результаты настоящего параграфа останутся верными, если в их формулировках заменить $\mathsf{QBK}$ на произвольное $\mathsf{QBK}$-расширение. § 4. Семантика возможных мировКак обычно, под шкалой понимается упорядоченная пара вида $\mathcal{W} = \langle W, R \rangle$, где $W$ – непустое множество, элементы которого называются возможными мирами, а $R$ – бинарное отношение на $W$. Для данной шкалы $\mathcal{W}$ и двух семейств $\sigma$-структур
$$
\begin{equation*}
\mathscr{A}^+=\langle \mathfrak{A}_w^+\colon w \in W \rangle, \qquad \mathscr{A}^-=\langle \mathfrak{A}_w^-\colon w \in W \rangle
\end{equation*}
\notag
$$
соответствующая упорядоченная тройка
$$
\begin{equation*}
\mathcal{M}=\langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle
\end{equation*}
\notag
$$
называется $\mathsf{QBK}_{\sigma}$-моделью, если для любых $u, v \in W$:
Здесь $A_u^+$ и $A_u^-$ – носители $\sigma$-структур $\mathfrak{A}_u^+$ и $\mathfrak{A}_u^-$ соответственно. Мы будем обычно писать $A_u$ вместо $A_u^+$ (совпадающего с $A_u^-$) и $c^{\mathfrak{A}_u}$ вместо $c^{\mathfrak{A}^+_u}$ (совпадающей с $c^{\mathfrak{A}^-_u}$). Тем не менее стоит помнить, что интерпретации символов из $\mathrm{Pred}_{\sigma}$ в $\mathfrak{A}^+_u$ и $\mathfrak{A}^-_u$ могут существенно различаться. Пусть $\mathcal{M}$ – $\mathsf{QBK}_\sigma$-модель. Далее $R(u)$ будет обозначать $\{v \in W \mid u R v\}$, т.е. образ $\{u\}$ относительно $R$. Для любых $w \in W$ и $A_w$-предложения $\Phi$ определим
$$
\begin{equation*}
\mathcal{M}, w \Vdash^+ \Phi, \qquad \mathcal{M}, w \Vdash^- \Phi
\end{equation*}
\notag
$$
индукцией по построению $\Phi$:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}, w \Vdash^+ P (t_1, \dots, t_n) \quad&\Longleftrightarrow \quad \mathfrak{A}^+_w \Vdash P (t_1, \dots, t_n); \\ \mathcal{M}, w \Vdash^- P (t_1, \dots,t_n) \quad &\Longleftrightarrow \quad \mathfrak{A}^-_w \Vdash P (t_1, \dots,t_n); \\ \mathcal{M}, w \Vdash^+ \Psi \wedge \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{и} \quad \mathcal{M}, w \Vdash^+ \Theta; \\ \mathcal{M}, w \Vdash^- \Psi \wedge \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{или} \quad \mathcal{M}, w \Vdash^- \Theta; \\ \mathcal{M}, w \Vdash^+ \Psi \vee \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{или} \quad \mathcal{M}, w \Vdash^+ \Theta; \\ \mathcal{M}, w \Vdash^- \Psi \vee \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{и} \quad \mathcal{M}, w \Vdash^- \Theta; \\ \mathcal{M}, w \Vdash^+ \Psi \to \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \nVdash^+ \Psi \quad \text{или} \quad \mathcal{M}, w \Vdash^+ \Theta; \\ \mathcal{M}, w \Vdash^- \Psi \to \Theta \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{и} \quad \mathcal{M}, w \Vdash^- \Theta; \\ \mathcal{M}, w \Vdash^+ \bot \quad&\Longleftrightarrow \quad 0 \not= 0; \\ \mathcal{M}, w \Vdash^- \bot \quad&\Longleftrightarrow \quad 0 = 0; \\ \mathcal{M}, w \Vdash^+ \sim \Psi \quad&\Longleftrightarrow \quad \mathcal{M},w \Vdash^- \Psi; \\ \mathcal{M}, w \Vdash^- \sim \Psi \quad&\Longleftrightarrow \quad \mathcal{M},w \Vdash^+ \Psi; \\ \mathcal{M}, w \Vdash^+ {\Box \Psi} \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{для всех} \ {u \in R (w)}; \\ \mathcal{M},w \Vdash^- \Box \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{для некоторого} \ {u \in R (w)}; \\ \mathcal{M}, w \Vdash^+ \Diamond \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Psi \quad \text{для некоторого} \ {u \in R (w)}; \\ \mathcal{M}, w \Vdash^- \Diamond \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Psi \quad \text{для всех} \ {u \in R (w)}; \\ \mathcal{M}, w \Vdash^+ \forall\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ {\Psi (x / \underline{a})} \quad \text{для всех} \ a \in A_w; \\ \mathcal{M},w \Vdash^- \forall\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- {\Psi (x / \underline{a})} \quad \text{для некоторого} \ a \in A_w; \\ \mathcal{M}, w \Vdash^+ \exists\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ {\Psi (x / \underline{a})} \quad \text{для некоторого} \ a \in A_w; \\ \mathcal{M},w \Vdash^- \exists\,x\ \Phi \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- {\Psi (x / \underline{a})} \quad \text{для всех} \ a \in A_w. \end{aligned}
\end{equation*}
\notag
$$
В частности, мы всегда имеем $\mathcal{M}, w \nVdash^+ \bot$ и $\mathcal{M}, w \Vdash^- \bot$. Неформально $\Vdash^+$ отвечает за верифицируемость, а $\Vdash^-$ – за фальсифицируемость. Когда из контекста ясно, о какой модели $\mathcal{M}$ идет речь, мы пишем $w \Vdash^{\circ} \Phi$ вместо $\mathcal{M}, w \Vdash^{\circ} \Phi$, где ${\circ} \in \{+, -\}$. Наконец, запись $\mathcal{W} \Vdash \Phi$ означает, что $\mathcal{M}, w \Vdash^+ \lambda \Phi$ для любых $\mathsf{QBK}_{\sigma}$-модели $\mathcal{M}$ над $\mathcal{W}$, $w \in W$ и $A_w$-подстановки $\lambda$. Семантика для $\mathsf{QBK}$, как и ее пропозициональная версия из [17], являются локально четырехзначными. Точнее, потенциально возможны четыре ситуации:
Первая ситуация соответствует значению “истинно”, вторая – “ложно”, третья – “не определено”, а четвертая – “переопределено”. Замечание 4.1. Модели для $\mathsf{QBK}$ можно воспринимать как “модализированные” версии моделей для кванторной логики Белнапа–Данна (ср. [18]). Хотя в языке последней отсутствуют $\bot$ и $\to$, их можно легко добавить (см. [17; § 4]). Пусть $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$. Говорят, что $\Delta$ семантически следует из $\Gamma$, и пишут $\Gamma \vDash \Delta$, если для любых $\mathsf{QBK}_{\sigma}$-модели $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$, $w \in W$ и основной $A_w$-подстановки $\lambda$
$$
\begin{equation*}
{\mathcal{M}, w \Vdash^+ \Phi} \quad \text{для всех} \ {\Phi \in \Gamma} \quad \Longrightarrow \quad {\mathcal{M}, w \Vdash^+ \lambda \Psi} \quad \text{для некоторой} \ {\Psi \in \Delta}.
\end{equation*}
\notag
$$
По аналогии с $\vdash$, когда $\Delta = \{\Phi\}$, мы обычно пишем $\Gamma \vDash \Phi$ вместо $\Gamma \vDash \{\Phi\}$. Будем называть $\sigma$-формулу $\Phi$ общезначимой, если $\vDash \Phi$. Как легко убедиться, имеет место следующий семантический аналог теоремы о дедукции. Теорема 4.2. Для любых $\Gamma \cup \{\Phi\} \subseteq \mathrm{Sent}_{\sigma}$ и $\Psi \in \mathrm{Form}_{\sigma}$ Наша ближайшая цель – показать, что $\mathsf{QBK}$ корректна относительно семантики выше. Лемма 4.3. Для любой $\Phi \in \mathrm{Form}_{\sigma}$ Другими словами, выводимость $\sigma$-формулы влечет ее общезначимость. Доказательство. Предположим, что $\vdash \Phi$, т.е. существует конечная последовательность $\sigma$-формул такая, что для каждого $i \in \{0, \dots, n\}$ выполнено одно из следующих условий:
Пусть $\mathcal{M}$ – $\mathsf{QBK}_{\sigma}$-модель. Индукцией по $i$ установим, что $\mathcal{M}, w \Vdash^+ \lambda (\Phi_i)$ для всех $w \in W$ и основных $A_w$-подстановок $\lambda$. Если $\Phi_i$ – аксиома классической логики, то можно рассуждать так же, как в классической логике первого порядка. Если $\Phi_i$ – “пропозициональная” аксиома для сильного отрицания, то можно рассуждать так же, как в $\mathsf{BK}$ (см. [11; § 4]). Например, пусть $\Phi_i$ – аксиома типа $\mathrm{SN4}$, т.е. вида
$$
\begin{equation*}
{\sim (\Psi \to \Theta) \leftrightarrow (\Psi \wedge {\sim \Theta})}.
\end{equation*}
\notag
$$
Нам нужно показать, что для любых $w \in W$ и основной $A_w$-подстановки $\lambda$
$$
\begin{equation*}
w \Vdash^+ \lambda \sim (\Psi \to \Theta) \quad \Longleftrightarrow \quad w \Vdash^+ {\lambda (\Psi \wedge {\sim \Theta})}.
\end{equation*}
\notag
$$
Это делается следующим образом:
$$
\begin{equation*}
\begin{aligned} \, w \Vdash^+ \lambda \sim (\Psi \to \Theta) \quad &\Longleftrightarrow \quad w \Vdash^+ {\sim ({\lambda \Psi} \to {\lambda \Theta})} \\ \quad &\Longleftrightarrow \quad w \Vdash^- {\lambda \Psi} \to {\lambda \Theta} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda \Psi} \quad \text{и} \quad w \Vdash^- {\lambda \Theta} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda \Psi} \quad \text{и} \quad w \Vdash^+ {\sim \lambda \Theta} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda \Psi} \wedge {\sim {\lambda \Theta}} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\lambda (\Psi \wedge {\sim \Theta})}. \end{aligned}
\end{equation*}
\notag
$$
Далее рассмотрим “кванторные” аксиомы для сильного отрицания. Пусть $\Phi_i$ – аксиома типа $\mathrm{SN6}$, т.е. вида
$$
\begin{equation*}
{\sim \forall\,x\ \Psi} \leftrightarrow \exists\,x\, \sim \Psi.
\end{equation*}
\notag
$$
Нам нужно показать, что для любых $w \in W$ и основной $A_w$-подстановки $\lambda$
$$
\begin{equation*}
w \Vdash {\lambda \sim \forall\,x\ \Psi} \quad \Longleftrightarrow \quad w \Vdash {\lambda\, \exists\,x\, \sim \Psi}.
\end{equation*}
\notag
$$
Это делается следующим образом:
$$
\begin{equation*}
\begin{aligned} \, w \vDash \lambda \sim \forall\,x\ \Psi \quad &\Longleftrightarrow \quad w \Vdash^+ {\sim \forall\,x\ {\lambda^x_x \Phi}} \\ \quad &\Longleftrightarrow \quad w \Vdash^- \forall\,x\ {\lambda^x_x \Phi} \\ \quad &\Longleftrightarrow \quad w \Vdash^- {(\lambda^x_x \Phi) (x / \underline{a})} \quad \text{для некоторого} \ a \in A_w \\ \quad &\Longleftrightarrow \quad w \Vdash^+ {\sim (\lambda^x_x \Phi) (x / \underline{a})} \quad \text{для некоторого} \ a \in A_w \\ \quad &\Longleftrightarrow \quad w \Vdash^+ \exists\,x\ {\sim {\lambda^x_x \Phi}} \\ \quad &\Longleftrightarrow \quad w \Vdash^+ \lambda \, \exists\,x\ \sim \Psi, \end{aligned}
\end{equation*}
\notag
$$
где $\lambda^x_x$ обозначает $(\lambda \setminus \{(x, {\lambda (x)})\}) \cup \{(x, x)\}$. Аналогично для $\mathrm{SN7}$.
Если $\Phi_i$ – аксиома для $\Box$ либо аксиома связи модальностей, то можно рассуждать так же, как в $\mathsf{BK}$. Если $\Phi_i$ получается из предыдущих $\Phi_j$ и $\Phi_k$ по $\mathrm{MP}$, $\mathrm{BR1}$ или $\mathrm{BR2}$, то можно рассуждать так же, как в классической логике предикатов, а если $\Phi_i$ получается из предыдущей $\Phi_j$ по $\mathrm{MB}$ или $\mathrm{MD}$, то можно рассуждать так же, как в $\mathsf{BK}$. Лемма доказана. Теорема 4.4 (о корректности $\mathsf{QBK}$). Для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ Доказательство. Предположим, что $\Gamma \vdash \Delta$. Значит, найдутся конечное $\Lambda \subseteq \Gamma$ и $\Phi \in \operatorname{Disj} (\Delta)$ такие, что $\Lambda \vdash \Phi$. Отдельно рассмотрим два случая.
Теорема доказана. Пусть $L$ – $\mathsf{QBK}$-расширение. Обозначим через $\vDash_{L}$ релятивизацию $\vDash$ на класс шкал
$$
\begin{equation*}
\mathcal{K}_L:= {\{\mathcal{W} \mid \mathcal{W} \Vdash \Phi\ \text{для всех}\ \Phi \in L\}},
\end{equation*}
\notag
$$
Нетрудно видеть, что результаты настоящего параграфа останутся верными, если в их формулировках заменить $\vdash$ на $\vdash_L$ и $\vDash$ на $\vDash_L$, где $L$ – произвольное $\mathsf{QBK}$-расширение.
§ 5. Теорема о сильной полнотеМы будем называть $\sigma$-теорию $\Gamma$ насыщенной, если:
Здесь первые два условия отвечают за нетривиальность и дедуктивную замкнутость, а третье и четвертое – за обладание “дизъюнктивным” и “экзистенциальным” свойствами. Более того, насыщенные теории обладают другими двумя полезными свойствами. Доказательство аналогично случаю классической логики первого порядка. Для всякого множества $S$ положим
$$
\begin{equation*}
\sigma_S:= \sigma \cup \{\underline{s} \mid s \in S\},
\end{equation*}
\notag
$$
где все $\underline{s}$ суть новые константные символы. Лемма 5.2. Пусть $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ таковы, что $\Gamma \nvdash \Delta$. Тогда для каждого множества $S$ мощности $| \mathrm{Sent}_{\sigma}|$ существует насыщенная $\sigma_S$-теория $\Gamma' \supseteq \Gamma$ такая, что $\Gamma' \nvdash \Delta$. Доказательство аналогично случаю классической логики первого порядка. Теперь зафиксируем какое-нибудь множество $S^{\star}$ мощности $| \mathrm{Sent}_{\sigma} |$. Оно будет играть роль “потенциального универсума” в нашей канонической модели для $\mathsf{QBK}_{\sigma}$. Мы будем называть $S \subseteq S^{\star}$ допустимым, если $| S^{\star} \setminus S | = | S^{\star}|$. Лемма 5.3. Пусть $S \subseteq S^{\star}$ допустимо, а $\Gamma \subseteq \mathrm{Sent}_{\sigma_S}$ и $\Delta \subseteq \mathrm{Form}_{\sigma_S}$ таковы, что $\Gamma \nvdash \Delta$. Тогда существуют допустимое $S' \supseteq S$ и насыщенная $\sigma_{S'}$-теория $\Gamma' \supseteq \Gamma$ такие, что $\Gamma' \nvdash \Delta$. Доказательство. Поскольку $| S^{\star} \setminus S | = | \mathrm{Sent}_{\sigma} |$, можно найти допустимое $S' \supseteq S$ такое, что Более того, мы имеем $| \mathrm{Sent}_{\sigma} | = | \mathrm{Sent}_{\sigma_S} |$, так как $| S | \leqslant | \mathrm{Sent}_{\sigma} |$. Осталось применить лемму 5.2 при $\sigma := \sigma_S$ и $S := S' \setminus S$.
Лемма доказана. Лемма 5.4. Пусть $S \subseteq S^{\star}$ допустимо, а $\Gamma \subseteq \mathrm{Sent}_{\sigma_S}$ и $\Delta \subseteq \mathrm{Form}_{\sigma_S}$ таковы, что $\Gamma \nvdash \Delta$. Тогда существует насыщенная $\sigma_{S^{\star}}$-теория $\Gamma' \supseteq \Gamma$ такая, что $\Gamma' \nvdash \Delta$. Чтобы это доказать, нужно просто применить лемму 5.2 при $\sigma := \sigma_S$ и $S = S^{\star} \setminus S$. Наконец, мы готовы к тому, чтобы адаптировать метод канонических моделей для $\mathsf{QBK}$ и ее расширений. Неформально говоря, нужно естественным образом скомбинировать каноническую модель для $\mathsf{BK}$ из [11; § 4] и каноническую модель для классической кванторной модальной логики (см. [15; § 6]). Мы будем порой опускать индекс $\sigma$, однако из контекста всегда будет ясно, о какой сигнатуре идет речь. Для всякого множества $S$ положим
$$
\begin{equation*}
\mathrm{Sat}_S:= \text{совокупность всех насыщенных}\ \sigma_S \text{-теорий}.
\end{equation*}
\notag
$$
Кроме того, для произвольного множества формул $\Gamma$ обозначим через $\mathrm{Const} ( \Gamma)$ совокупность всех константных символов, встречающихся в элементах из $\Gamma$. Заметим, что для каждой $\Gamma$ из $\mathrm{Sat}_S$ будет верно $\mathrm{Const} (\Gamma) = \mathrm{Const}_{\sigma_S}$: очевидно, $\mathrm{Const}_{\sigma_{S}}$ включает $\mathrm{Const} (\Gamma)$; с другой стороны, для любого $c \in \mathrm{Const}_{\sigma_{S}}$ можно легко построить $\Psi_c \in \mathsf{QBK}_{\sigma_S} \cap \mathrm{Sent}_{\sigma_S}$ такое, что $c$ входит в $\Psi_c$, а потому мы имеем $\mathrm{Const}_{\sigma_{S}} \subseteq \mathrm{Const} (\Gamma)$ (в силу $\mathsf{QBK}_{\sigma_S}\cap \mathrm{Sent}_{\sigma_S} \subseteq \Gamma$). Далее, со всякой насыщенной $\sigma_S$-теорией $\Gamma$ свяжем две $\sigma_S$-структуры, ${(\mathfrak{A}_{\Gamma}^S)}^+$ и ${(\mathfrak{A}_{\Gamma}^S)}^-$, с одним и тем же носителем такие, что все константные символы из $\sigma_S$ интерпретируются в них тождественным образом, и для любого атомарного $\sigma_S$-предложения $\Phi$ выполнено
$$
\begin{equation*}
\begin{aligned} \, {(\mathfrak{A}_{\Gamma}^S)}^+ \Vdash \Phi \quad &:\Longleftrightarrow \quad {\Phi\in \Gamma}, \\ {(\mathfrak{A}_{\Gamma}^S)}^- \Vdash \Phi \quad &:\Longleftrightarrow \quad {\sim \Phi\in \Gamma}. \end{aligned}
\end{equation*}
\notag
$$
Обозначим $\sigma$-обеднения ${(\mathfrak{A}_{\Gamma}^S)}^+ $ и ${( \mathfrak{A}_{\Gamma}^S)}^-$ через $\mathfrak{A}_{\Gamma}^+$ и $ \mathfrak{A}_{\Gamma}^-$ соответственно. Ясно, что любое $A_{\Gamma}$-предложение имеет вид
$$
\begin{equation*}
{\Phi (x_1/\underline{c_1}, \dots, x_n/\underline{c_n})},
\end{equation*}
\notag
$$
где $\{c_1, \dots, c_n\} \subseteq \mathrm{Const} (\Gamma)$; поэтому для удобства мы будем нередко отождествлять его с $\sigma_S$-предложением $\Phi ( x_1/c_1, \dots, x_n/c_n)$. Теперь возьмем
$$
\begin{equation*}
W^{\mathsf{QBK}}:= \bigcup\, \{\mathrm{Sat}_S \mid S\ - \text{допустимое подмножество}\ S^{\star}\}.
\end{equation*}
\notag
$$
Под канонической шкалой для $\mathsf{QBK}$ понимается шкала $\mathcal{W}^{\mathsf{QBK}} = \langle W^{\mathsf{QBK}}, R^{\mathsf{QBK}} \rangle$, где отношение $R^{\mathsf{QBK}}$ определяется стандартным образом11:
$$
\begin{equation*}
R^{\mathsf{QBK}}:= {\{(\Gamma, \Delta) \in W^{\mathsf{QBK}} \times W^{\mathsf{QBK}} \mid \Gamma_{\Box} \subseteq \Delta\}}.
\end{equation*}
\notag
$$
Канонической моделью для $\mathsf{QBK}$ называется
$$
\begin{equation*}
\mathcal{M}^{\mathsf{QBK}}=\langle \mathcal{W}^{\mathsf{QBK}}, {( \mathscr{A}^{\mathsf{QBK}})}^+, {(\mathscr{A}^{\mathsf{QBK}})}^- \rangle,
\end{equation*}
\notag
$$
где
$$
\begin{equation*}
\begin{aligned} \, {(\mathscr{A}^{\mathsf{QBK}})}^+ &:= \langle \mathfrak{A}_{\Gamma}^+ : \Gamma \in W^{\mathsf{QBK}} \rangle,\\ {(\mathscr{A}^{\mathsf{QBK}})}^- &:= \langle \mathfrak{A}_{\Gamma}^- : \Gamma \in W^{\mathsf{QBK}} \rangle. \end{aligned}
\end{equation*}
\notag
$$
Как мы вскоре убедимся, данное построение корректно. Доказательство. Предположим, что $\Gamma R^{\mathsf{QBK}} \Delta$. Пусть $\sigma_S$ – сигнатура $\Gamma$. Ясно, что для любого $c \in \mathrm{Const}_{\sigma_S}$ можно построить $\Psi_c \in \mathsf{QBK}_{\sigma_S} \cap \mathrm{Sent}_{\sigma_S}$ такое, что $c$ входит в $\Psi_c$; тогда $\Box \Psi_c \in \mathsf{QBK}_{\sigma_S} \cap \mathrm{Sent}_{\sigma_S}$ (в силу $\mathrm{RN}$), а потому $\Box \Psi_c \in \Gamma$, откуда получаем $\Psi_c \in \Delta$. Стало быть, $\mathrm{Const} (\Delta)$ включает $\mathrm{Const} (\Gamma)$, которое совпадает с $\mathrm{Const}_{\sigma_S}$. Кроме того, интерпретация символов из $\mathrm{Const}_{\sigma}$ будет, очевидно, сохраняться при переходе от $\mathfrak{A}_{\Gamma}^+$ к $\mathfrak{A}_{\Delta}^+$.
Лемма доказана. Ключевую роль в доказательстве теоремы о сильной полноте играет Лемма 5.6 (о канонической модели для $\mathsf{QBK}$). Для любых $\Gamma \in W^{\mathsf{QBK}}$ и $A_{\Gamma}$-предложения $\Phi$ Доказательство. Применяем индукцию по построению $\Phi$.
Случай, когда $\Phi$ атомарно, тривиален. Пусть $\Phi = \exists\,x\ \Psi$. Сначала рассмотрим верифицируемость:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^+ \exists\,x\ \Psi \quad &\Longleftrightarrow \quad {\mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^+ \Psi (x/\underline{a})} \quad \text{для некоторого} \ {a \in \mathrm{Const} (\Gamma)}\\ \quad &\Longleftrightarrow \quad {\Psi (x / \underline{a}) \in \Gamma} \quad \text{для некоторого} \ {a \in \mathrm{Const} (\Gamma)}\\ &\Longleftrightarrow \quad {\exists\,x\ \Psi} \in \Gamma. \end{aligned}
\end{equation*}
\notag
$$
Тут пояснения требует последняя эквивалентность: прямая импликация получается с помощью $\mathrm{Q2}$, а обратная – с помощью экзистенциального свойства.
Теперь рассмотрим фальсифицируемость:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^- \exists\,x\ \Psi \quad &\Longleftrightarrow \quad \mathcal{M}^{\mathsf{QBK}}, \Gamma \Vdash^- {\Psi (x / \underline{a})} \quad \text{для всех} \ {a \in \mathrm{Const} (\Gamma)} \\ \quad &\Longleftrightarrow \quad {{\sim \Psi (x/\underline{a})} \in \Gamma} \quad \text{для всех} \ {a \in \mathrm{Const} (\Gamma)} \\ &\Longleftrightarrow \quad {\forall\,x\ \sim \Psi} \in \Gamma \\ &\Longleftrightarrow \quad {\sim \exists\,x\ \Psi} \in \Gamma. \end{aligned}
\end{equation*}
\notag
$$
В предпоследней эквивалентности прямая импликация получается с помощью $\mathrm{Q1}$, а обратная – с помощью утверждения 5.1, (ii); последнюю же эквивалентность гарантирует $\mathrm{SN7}$.
Аналогично для $\Phi = \forall\,x\ \Psi$. Остальные случаи разбираются так же, как в $\mathsf{BK}$ (см. [11; § 4] или [17; § 2]), хотя вместо пропозициональной версии леммы о расширении используется лемма 5.3. Лемма доказана. Теорема 5.7 (о сильной полноте $\mathsf{QBK}$). Для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ Доказательство. $\Longrightarrow$. См. теорему 4.4.
$\Longleftarrow$. Предположим, что $\Gamma \nvdash \Delta$. Зафиксируем какое-нибудь допустимое $S \subseteq S^{\star}$ мощности $\aleph_0$ (таким образом, $| S | = | \mathrm{Var} |$). Пусть $\lambda$ – биекция из $\mathrm{Var}$ на $\{ \underline{s} \mid s \in S\}$. Возьмем Легко убедиться, что $\Gamma \nvdash \Delta'$. В силу леммы 5.3 (для $\sigma := \sigma_S$ и $S = S^{\star} \setminus S$) найдется $\Gamma' \in W^{\mathsf{QBK}}$ такая, что $\Gamma \subseteq \Gamma'$ и $\Gamma' \nvdash \Delta'$. Ясно, что $\lambda$ можно воспринимать как основную $A_{\Gamma'}$-подстановку. Значит, в силу леммы 5.6 мы имеем $\mathcal{M}^{\mathsf{QBK}}, \Gamma' \Vdash \Phi$ для всех $\Phi \in \Gamma$ и одновременно $\mathcal{M}^{\mathsf{QBK}}, \Gamma' \nVdash \lambda \Psi$ для всех $\Psi \in \Delta$. Стало быть, $\Gamma \nvDash \Delta$.Теорема доказана. Пусть $L$ – $\mathsf{QBK}$-расширение. Тогда каноническую шкалу для $L$ и каноническую модель для $L$, обозначаемые через $\mathcal{W}^L$ и $\mathcal{M}^L$ соответственно, можно определить так же, как для $\mathsf{QBK}$, но с заменой $\mathrm{Sat}_S$ на
$$
\begin{equation*}
\mathrm{Sat}_S^L:= {\{ \Gamma \in \mathrm{Sat}_S \mid L \cap \mathrm{Sent}_{\sigma_S} \subseteq \Gamma \}}.
\end{equation*}
\notag
$$
Далее, как легко понять, для $L$ будет верен аналог леммы 5.6. Тем не менее аналог теоремы 5.7 может не иметь места, если существуют неканонические модели над $\mathcal{W}^L$, в которых опровергаются формулы из $L$, т.е. когда $\mathcal{W}^L$ не лежит в $\mathcal{K}_L$.
§ 6. Некоторые естественные расширенияИспользуя вариант метода канонических моделей из § 5, нетрудно установить сильную полноту некоторых естественных $\mathsf{QBK}$-расширений (ср. [11; § 4]). Мы рассмотрим два основных типа таких расширений:
Начнем с расширений типа (i). На аксиоматическом уровне исключению “переопределенности” или “неопределенности” соответствуют следующие схемы аксиом. $\mathrm{Exp}$. $\sim\Phi \to (\Phi \to \Psi)$. $\mathrm{ExM}$. ${\Phi}\, \vee\, \sim\Phi$. Здесь $\mathrm{Exp}$ является сокращением для “explosion”, а $\mathrm{ExM}$ – для “excluded middle”. На самом деле достаточно иметь $\mathrm{Exp}$ и $\mathrm{ExM}$ для всех атомарных $\Phi$ и $\Psi$; кроме того, $\mathrm{Exp}$ будет эквивалентна схеме $\sim\Phi \to \neg \Phi$. Положим
$$
\begin{equation*}
\mathsf{QBK}^{\circ}:={\mathsf{QBK} + \{\mathrm{ExM}\}}, \qquad \mathsf{QB3K}:={\mathsf{QBK} + \{\mathrm{Exp}\}}.
\end{equation*}
\notag
$$
Будем называть $\mathsf{QBK}_{\sigma}$-модель $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$: $\bullet$ ${\mathsf{QB3K}}_{\sigma}$-моделью, если для любых $w \in W$ и атомарного $A_w$-предложения $\Phi$
$$
\begin{equation*}
\mathfrak{A}^+_w \nVdash \Phi \quad \text{или} \quad \mathfrak{A}^-_w \nVdash \Phi;
\end{equation*}
\notag
$$
$\bullet$ ${\mathsf{QBK}}^{\circ}_{\sigma}$-моделью, если для любых $w \in W$ и атомарного $A_w$-предложения $\Phi$
$$
\begin{equation*}
\mathfrak{A}^+_w \Vdash \Phi \quad \text{или} \quad \mathfrak{A}^-_w \Vdash \Phi.
\end{equation*}
\notag
$$
Обозначим через $\vDash_{\mathsf{QBK}}^3$ и $\vDash_{\mathsf{QBK}}^{\circ}$ релятивизации $\vDash$ на соответствующие классы моделей. Стоит отметить, что мы избегаем обозначений $\vDash_{\mathsf{QB3K}}$ и $\vDash_{\mathsf{QBK}^{\circ}}$, поскольку иначе возникнет конфликт с тем, как определялось $\vDash_L$ в § 4. Теорема 6.1. Для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ Доказательство. $\Longrightarrow$. Тут рассуждения аналогичны доказательству теоремы 4.4. При этом верифицируемость $\mathrm{Exp}$ во всех $\mathsf{QB3K}_{\sigma}$-моделях устанавливается простой индукцией по построению $\Phi$.
$\Longleftarrow$. Сначала проверим, что $\mathcal{M}^{\mathsf{QB3K}}$ является $\mathsf{QB3K}_{\sigma}$-моделью. Пусть $\Gamma \in W^{\mathsf{QB3K}}$ и $\sigma_S$ – сигнатура $\Gamma$. Рассмотрим произвольное атомарное $A_\Gamma$-предложение $\Phi$; его можно также воспринимать как $\sigma_S$-предложение. Рассуждая от противного, допустим, что $\mathfrak{A}_{\Gamma}^+ \Vdash \Phi$ и $\mathfrak{A}_{\Gamma}^- \Vdash \Phi$, т.е.
$$
\begin{equation*}
\mathcal{M}^{\mathsf{QB3K}}, \Gamma \Vdash^+ \Phi, \qquad \mathcal{M}^{\mathsf{QB3K}}, \Gamma \Vdash^- \Phi.
\end{equation*}
\notag
$$
В силу аналога леммы 5.6 для ${\mathsf{QB3K}}$ это равносильно $\Phi \in \Gamma$ и $\sim\Phi \in \Gamma$. Вместе с тем мы имеем $\sim\Phi \to (\Phi \to \Psi) \in \Gamma$ для всех $\Psi \in \mathrm{Sent}_{\sigma_S}$. Отсюда уже легко получить $\Gamma = \mathrm{Sent}_{\sigma_S}$, что противоречит нетривиальности насыщенных теорий. Далее можно рассуждать так же, как в доказательстве теоремы 5.7.
Теорема доказана. Теорема 6.2. Для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ Доказательство аналогично доказательству теоремы 6.1. Теперь перейдем к рассмотрению расширений типа (ii). Для каждого такого расширения $L$ мы будем предполагать, что:
Тогда теорему о сильной полноте для $L$ можно получить так же, как для $\mathsf{QBK}$. В качестве иллюстрации рассмотрим следующие три схемы аксиом. $\mathrm{D}$. $\Box \Phi \to \Diamond \Phi$. $\mathrm{T}$. $\Box \Phi \to \Phi$. $\mathrm{4}$. $\Box \Phi \to \Box \Box \Phi$. Как и в классической модальной логике, легко показать следующее:
Введем несколько сопутствующих обозначений:
$$
\begin{equation*}
\begin{gathered} \, \mathsf{QBD}:={\mathsf{QBK} + \{\mathrm{D}\}}, \qquad \mathsf{QBT}:={\mathsf{QBK} + \{\mathrm{T}\}}, \qquad \mathsf{QBK4}:={\mathsf{QBK} + \{\mathrm{4}\}}, \\ \mathsf{QBD4}:={\mathsf{QBK} + \{\mathrm{D}, \mathrm{4}\}}, \qquad \mathsf{QBS4}:={\mathsf{QBK} + \{\mathrm{T}, \mathrm{4}\}}. \end{gathered}
\end{equation*}
\notag
$$
Кроме того, для удобства обозначим совокупность всех этих логик через $\mathscr{L}$. Теорема 6.3. Пусть $L \in \mathscr{L}$. Тогда для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ Доказательство аналогично доказательству теоремы 5.7 (с учетом замечаний выше). Разумеется, два типа расширений можно комбинировать. Например, возьмем Стало быть, в $\mathsf{QB3S4}$-моделях должна быть исключена “переопределенность” (как в $\mathsf{QB3K}$), а отношения достижимости должны быть предпорядками (как в $\mathsf{QBS4}$). Обозначим через $\vDash_{\mathsf{QBS4}}^3$ релятивизацию $\vDash$ на такого рода модели. Ясно, что $\mathcal{M}^{\mathsf{QB3S4}}$ окажется $\mathsf{QB3S4}$-моделью. Значит, $\vdash_{\mathsf{QB3S4}}$ совпадет с $\vDash_{\mathsf{QBS4}}^3$, т.е. для $\mathsf{QB3S4}$ будет верна теорема о сильной полноте.Логики $\mathsf{QBS4}$ и $\mathsf{QB3S4}$ будут играть важную роль в § 8, который посвящен точным вложениям кванторных логик Нельсона. § 7. Вариант с постоянными носителямиРассмотрим следующие два варианта схемы Баркан. $\mathrm{Ba}^{\Box}.$ $\forall\,x\ \Box \Phi \to {\Box \forall\,x\ \Phi}$. $\mathrm{Ba}^{\Diamond}.$ ${\Diamond \exists\,x\ \Phi} \to \exists\,x\ \Diamond \Phi$. Заметим, что схема, соответствующая обратной к $\mathrm{Ba}^{\Box}$ импликации, выводима в $\mathsf{QBK}$:
Аналогично получается схема, обратная к $\mathrm{Ba}^{\Diamond}$. Обозначим
$$
\begin{equation*}
\mathsf{QBK}^{\sharp}_{\Box}:=\mathsf{QBK} + \{\mathrm{Ba}^{\Box}\}, \qquad \mathsf{QBK}^{\sharp}_{\Diamond}:=\mathsf{QBK} + \{\mathrm{Ba}^{\Diamond}\}.
\end{equation*}
\notag
$$
Хотя доказательство утверждения ниже полностью аналогично случаю классической кванторной модальной логики, мы приведем его для наглядности.
Аналогичным образом можно показать, что $\mathrm{Ba}^{\Box}$ выводима в $\mathsf{QBK}^{\sharp}_{\Diamond}$. Утверждение доказано. Далее мы будем писать $\mathsf{QBK}^{\sharp}$ вместо $\mathsf{QBK}^{\sharp}_{\Box}$ и $\mathsf{QBK}^{\sharp}_{\Diamond}$, а также $\vdash^{\sharp}$ вместо $\vdash_{\mathsf{QBK}^{\sharp}}$. Кроме того, мы ограничимся рассмотрением не более чем счетных сигнатур, поскольку работа с несчетными сигнатурами порождает некоторые трудности даже для варианта $\mathsf{QK}$ с постоянными носителями (ср. [15; лемма 7.1.2], где в доказательстве существенным образом используется счетность сигнатуры). Будем называть $\mathsf{QBK}_{\sigma}$-модель $\mathcal{M}=\langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ $\mathsf{QBK}^{\sharp}_{\sigma}$-моделью, если $A_u = A_v$ для всех $u, v \in W$. Иными словами, $\mathsf{QBK}^{\sharp}_{\sigma}$-модели суть $\mathsf{QBK}_{\sigma}$-модели с постоянными носителями. На самом деле схема Баркан гарантирует лишь то, что для любых $u, v \in W$ Однако это не принципиально, поскольку для данного $u \in W$ всегда можно перейти к порожденной подмодели с множеством миров $R (u)$. Обозначим через $\vDash^{\sharp}$ релятивизацию $\vDash$ на класс всех $\mathsf{QBK}^{\sharp}_{\sigma}$-моделей.Теорема 7.2 (о корректности для ${\mathsf{QBK}}^{\sharp}_{\sigma}$). Для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ Доказательство аналогично доказательству теоремы 4.4. При этом верифицируемость $\mathrm{Ba}^{\Box}$ (либо $\mathrm{Ba}^{\Diamond}$) во всех $\mathsf{QBK}^{\sharp}_{\sigma}$-моделях устанавливается так же, как в классической кванторной модальной логике. Как и в § 5, зафиксируем какое-нибудь множество $S^{\star}$ мощности $| \mathrm{Sent}_{\sigma} |$. Для сокращения мы будем писать $\sigma_{\star}$ вместо $\sigma_{S^{\star}}$. Возьмем
$$
\begin{equation*}
W^{\sharp}:= \text{совокупность всех насыщенных}\ \sigma_{\star} \text{-теорий}.
\end{equation*}
\notag
$$
Очевидно, $\mathrm{Const} (\Gamma) = \mathrm{Const}_{\sigma_{\star}}$ для всех $\Gamma \in W^{\sharp}$. Под канонической шкалой для $\mathsf{QBK}^{\sharp}$ и канонической моделью для $\mathsf{QBK}^{\sharp}$ понимаются
$$
\begin{equation*}
\mathcal{W}^{\sharp}=\langle W^{\sharp}, R^{\sharp} \rangle, \qquad \mathcal{M}^{\sharp}=\langle \mathcal{W}^{\sharp}, {(\mathscr{A}^{\sharp})}^+, {(\mathscr{A}^{\sharp})}^- \rangle,
\end{equation*}
\notag
$$
где компоненты $R^{\sharp}$, ${(\mathscr{A}^{\sharp})}^+$ и ${( \mathscr{A}^{\sharp})}^-$ определяются так же, как $R^{\mathsf{QBK}}$, ${( \mathscr{A}^{\mathsf{QBK}})}^+$ и ${(\mathscr{A}^{\mathsf{QBK}})}^-$, но с заменой $W^{\mathsf{QBK}}$ на $W^{\sharp}$. Лемма 7.3. Для любых $\Gamma \in W^{\sharp}$ и $\Phi \in \mathrm{Sent}_{\sigma^{\star}}$ Доказательство полностью аналогично случаю классической кванторной модальной логики (см., например, [15; лемма 7.1.2]). Отсюда легко получается Лемма 7.4 (о канонической модели для $\mathsf{QBK}^{\sharp}$). Для любых $\Gamma \in W^{\sharp}$ и $A_{\Gamma}$-предложения $\Phi$ Доказательство. Используем индукцию по построению $\Phi$.
Разумеется, поскольку всем мирам отвечает один и тот же носитель $\mathrm{Const}_{\sigma_{\star}}$, мы не можем использовать лемму 5.3. Тем не менее случаи, когда $\Phi$ не начинается с $\Box$ или $\Diamond$, разбираются так же, как в доказательстве леммы 5.6 (ввиду того, что для них не нужна лемма 5.3). Пусть $\Phi = {\Box \Psi}$. Очевидно, эквивалентность для $\Vdash^+$ следует из леммы 7.3 (и индукционной гипотезы). Рассмотрим теперь фальсифицируемость:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}^{\sharp}, \Gamma \Vdash^- {\Box \Psi}\ \quad \Longleftrightarrow& \quad \text{существует} \ \Delta \in W^\sharp \ \text{такая, что } \Gamma_{\Box} \subseteq \Delta \ \text{и} \ \mathcal{M}^{\sharp}, \Delta \Vdash^- \Psi \\ \quad\Longleftrightarrow& \quad \text{существует} \ \Delta \in W^\sharp \ \text{такая, что } \Gamma_{\Box} \subseteq \Delta \ \text{и} \ \sim \Psi \in \Delta \\ \quad \Longleftrightarrow& \quad {\Diamond \sim \Psi}\in \Gamma \\ \quad \Longleftrightarrow& \quad {\sim {\Box \Psi}}\in \Gamma. \end{aligned}
\end{equation*}
\notag
$$
Здесь предпоследнюю эквивалентность гарантирует лемма 7.3, а последняя следует из того, что $\Diamond \sim \Psi \Leftrightarrow \, \sim {\Box \Psi}$ выводима в $\mathsf{QBK}$:
Аналогично для $\Phi = \Diamond \Psi$. Лемма доказана. Теорема 7.5 (о сильной полноте $\mathsf{QBK}^{\sharp}$). Для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ Доказательство. $\Longrightarrow$. См. теорему 7.2.
$\Longleftarrow$. Предположим, что $\Gamma \nvdash^{\sharp} \Delta$. Зафиксируем какое-нибудь допустимое $S \subseteq S^{\star}$ мощности $\aleph_0$. Пусть $\lambda$ – биекция из $\mathrm{Var}$ на $\{\underline{s} \mid s \in S\}$. Возьмем Ясно, что $\Gamma \nvdash^{\sharp} \Delta'$. В силу леммы 5.4 найдется $\Gamma' \in W^{\sharp}$ такая, что $\Gamma \subseteq \Gamma'$ и $\Gamma' \nvdash^{\sharp} \Delta'$. Очевидно, $\lambda$ можно воспринимать как основную $A_{\Gamma'}$-подстановку. Значит, в силу леммы 7.4 мы имеем $\mathcal{M}^{\sharp}, \Gamma' \Vdash \Phi$ для всех $\Phi \in \Gamma$ и одновременно $\mathcal{M}^{\sharp}, \Gamma' \nVdash \lambda \Psi$ для всех $\Psi \in \Delta$. Стало быть, $\Gamma \nvDash^{\sharp} \Delta$.Теорема доказана. Разумеется, по аналогии с $\mathsf{QBK}$ мы можем рассматривать различные естественные расширения $\mathsf{QBK}^{\sharp}$. В частности, как легко убедиться, для расширений, получающихся из логик из $\mathscr{L}$, $\mathsf{QB3K}$ или $\mathsf{QBK}^{\circ}$ добавлением $\mathrm{Ba}^{\Box}$, будут верны соответствующие теоремы о сильной полноте. § 8. Точное вложение кванторных логик НельсонаПусть $\mathsf{QN4}$ – кванторная версия конструктивной логики Нельсона, $\mathsf{QN3}$ – ее расширение, получающееся путем исключения “переопределенности”, т.е. добавления релятивизации схемы $\mathrm{Exp}$ на язык $\mathsf{QN4}$ (см. [4] и [6], а также [19] и [20]). Напомним, что синтаксически язык $\mathsf{QN4}$ – это просто немодальный фрагмент языка $\mathsf{QBK}$. Однако на семантическом уровне имеются принципиальные различия между $\mathsf{QN4}$ и $\mathsf{QBK}$: $\to$ и $\forall$ верифицируются в $\mathsf{QN4}$ по аналогии с интуиционистской логикой, а не классической, как в $\mathsf{QBK}$. Интуитивно $\mathsf{QN4}$ обогащает кванторную интуционистскую логику $\mathsf{QInt}$ посредством добавления сильного отрицания. Ниже под конструктивными $\sigma$-формулами будут пониматься $\sigma$-формулы в языке $\mathsf{QN4}$, т.е. не содержащие вхождений $\Box$ и $\Diamond$. Негативные нормальные формы в языке $\mathsf{QN4}$ определяются так же, как в $\mathsf{QBK}$. Хорошо известно, что для $\mathsf{QN4}$ имеет место следующий результат, аналогичный теореме 3.8, но со слабой эквивалентностью вместо сильной. Теорема 8.1 (см., например, [20]). Для любой конструктивной $\sigma$-формулы $\Phi$ существует н.н.ф. $\overline{\Phi}$ такая, что $\Phi \leftrightarrow \overline{\Phi} \in \mathsf{QN4}_{\sigma}$. Более того, имеется алгоритм, который по данной конструктивной $\sigma$-формуле $\Phi$ строит подходящую12 н.н.ф. $\overline{\Phi}$. Далее, определим трансляцию $\tau$, которая каждой н.н.ф. в языке $\mathsf{QN4}_{\sigma}$ сопоставляет формулу в языке $\mathsf{QBK}_{\sigma}$:
$$
\begin{equation*}
\begin{aligned} \, \tau (P (t_1, \dots, t_n))&:= \Box P (t_1, \dots, t_n); \\ \tau (\sim P (t_1, \dots, t_n))&:= \, \sim \Diamond P (t_1, \dots, t_n); \\ \tau (\Phi \wedge \Psi)&:= \tau (\Phi) \wedge \tau (\Psi); \\ \tau (\Phi \vee \Psi)&:= \tau (\Phi) \vee \tau (\Psi); \\ \tau (\Phi \to \Psi)&:= \Box (\tau (\Phi) \to \tau (\Psi)); \\ \tau (\bot)&:= \bot; \\ \tau (\sim \bot)&:= \bot \to \bot; \\ \tau (\forall\,x\ \Phi)&:= \Box \forall\,x\ {\tau (\Phi)}; \\ \tau (\exists\,x\ \Phi)&:= \exists\,x\ {\tau (\Phi)}. \end{aligned}
\end{equation*}
\notag
$$
Действие $\tau$ можно естественным образом распространить на множество всех конструктивных $\sigma$-формул: если $\Phi$ не является н.н.ф., то возьмем Формально мы должны были бы писать $\tau_{\sigma}$ вместо $\tau$, однако из контекста всегда будет ясно, о какой сигнатуре идет речь.Ясно, что ограничение $\tau$ на формулы, не содержащие $\sim$, совпадает с трансляцией Гёделя–МакКинси–Тарского, которая точно вкладывает $\mathsf{QInt}$ в модальную логику $\mathsf{QS4}$. Кроме того, $\tau$ можно воспринимать как (кванторное) расширение пропозициональной трансляции, предложенной ранее в [11; п. 7.1]. Замечание 8.2. Если зафиксировать обычный алгоритм приведения конструктивных $\sigma$-формул к н.н.ф., то действие $\tau$ можно описать следующим образом: Говорят, что $\mathsf{QBK}_{\sigma}$-модель $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ является $\mathsf{QN4}_{\sigma}$-моделью, если $R$ – предпорядок на $W$ и для любых $u, v \in W$
$$
\begin{equation*}
u\ R\ v \quad \Longrightarrow \quad {P^{\mathfrak{A}^{\pm}_{u}} \subseteq P^{\mathfrak{A}^{\pm}_{v}}} \quad \text{для всех} \ {P \in \mathrm{Pred}_{\sigma}}.
\end{equation*}
\notag
$$
Далее, $\mathsf{QN4}_{\sigma}$-модель $\mathcal{M}$ называется $\mathsf{QN3}_{\sigma}$-моделью, если для любого $w \in W$
$$
\begin{equation*}
P^{\mathfrak{A}^{+}_{w}} \cap P^{\mathfrak{A}^{-}_{w}}=\varnothing \quad \text{для всех} \ {P \in \mathrm{Pred}_{\sigma}}.
\end{equation*}
\notag
$$
Отношения верифицируемости и фальсифицируемости для $\mathsf{QN4}_{\sigma}$ определяются естественным образом:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}, w \Vdash^+ {P (t_1, \dots, t_n)} \quad\Longleftrightarrow& \quad \mathfrak{A}^+_{w} \Vdash {P (t_1, \dots, t_n)}; \\ \mathcal{M}, w \Vdash^- {P (t_1, \dots,t_n)} \quad\Longleftrightarrow& \quad \mathfrak{A}^-_{w} \Vdash {P (t_1, \dots,t_n)}; \\ \mathcal{M},w \Vdash^+ \Phi \wedge \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi \quad \text{и} \quad \mathcal{M}, w \Vdash^+ \Psi; \\ \mathcal{M},w \Vdash^- \Phi \wedge \Psi \quad\Longleftrightarrow& \quad \mathcal{M},w \Vdash^- \Phi \quad \text{или} \quad \mathcal{M}, w \Vdash^- \Psi; \\ \mathcal{M}, w \Vdash^+ \Phi \vee \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi \quad \text{или} \quad \mathcal{M}, w \Vdash^+ \Psi; \\ \mathcal{M}, w \Vdash^- \Phi \vee \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^- \Phi \quad \text{и} \quad \mathcal{M}, w \Vdash^- \Psi; \\ \mathcal{M},w \Vdash^+ \Phi \to \Psi \quad\Longleftrightarrow& \quad \text{для любого} \ {u \in R (w)}, \text{ если} \ \mathcal{M}, u \Vdash^+ \Phi, \\ &\quad\text{то} \ \mathcal{M},u \Vdash^+ \Psi; \\ \mathcal{M},w \Vdash^- \Phi \to \Psi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi \quad \text{и} \quad \mathcal{M}, w \Vdash^- \Psi; \\ \mathcal{M}, w \Vdash^+ \bot \quad\Longleftrightarrow& \quad 0 \ne 0; \\ \mathcal{M}, w \Vdash^- \bot \quad\Longleftrightarrow& \quad 0 = 0; \\ \mathcal{M}, w \Vdash^+ \sim\Phi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^- \Phi; \\ \mathcal{M}, w \Vdash^- \sim\Phi \quad\Longleftrightarrow& \quad \mathcal{M}, w \Vdash^+ \Phi; \\ \mathcal{M}, w \Vdash^+ \forall\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, u \Vdash^+ \Phi (x / \underline{a})} \quad \text{для всех} \ {u \in R (w)} \ \text{и} \ {a \in A_u}; \\ \mathcal{M},w \Vdash^- \forall\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, w \Vdash^- \Phi (x / \underline{a})} \quad \text{для некоторого} \ {a \in A_w}; \\ \mathcal{M},w \Vdash^+ \exists\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, w \Vdash^+ \Phi (x / \underline{a})} \quad \text{для некоторого} \ {a \in A_w}; \\ \mathcal{M},w \Vdash^- \exists\,x\ \Phi \quad\Longleftrightarrow& \quad {\mathcal{M}, u \Vdash^- \Phi (x / \underline{a})} \quad \text{для всех} \ {u \in R (w)} \ \text{и} \ {a \in A_u}. \end{aligned}
\end{equation*}
\notag
$$
Здесь вместо $\Vdash^+$ и $\Vdash^-$ правильнее было бы писать $\Vdash^+_{\mathsf{QN4}}$ и $\Vdash^-_{\mathsf{QN4}}$, но в дальнейшем из контекста всегда будет ясно, о какой логике идет речь. Заметим, что $\mathcal{M}$ является $\mathsf{QN3}_{\sigma}$-моделью тогда и только тогда, когда не существует таких $w \in W$ и атомарного $A_w$-предложения $\Phi$, что $\mathfrak{A}^+_w \Vdash \Phi$ и $\mathfrak{A}^-_w \Vdash \Phi$ (ср. с определением $\mathsf{QB3K}_{\sigma}$-модели из § 6). Отношения семантического следования для $\mathsf{QN4}$ и $\mathsf{QN3}$ определяются по аналогии с $\vDash_\mathsf{QBK}$ и $\vDash_\mathsf{QBK}^3$; обозначим их через $\vDash_{\mathsf{QN4}}$ и $\vDash_{\mathsf{QN4}}^3$ соответственно. Теорема 8.3 (см. [20] и [19]). Для любых $\Gamma \subseteq \mathrm{Sent}_{\sigma}$ и $\Delta \subseteq \mathrm{Form}_{\sigma}$ где $\vdash_{\mathsf{QN4}}$ и $\vdash_{\mathsf{QN3}}$ обозначают отношения выводимости для $\mathsf{QN4}$ и $\mathsf{QN3}$ соответственно. Пусть $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ – произвольная $\mathsf{QBS4}_{\sigma}$-модель, т.е. $\mathsf{QBK}_{\sigma}$-модель, в которой отношение достижимости рефлексивно и транзитивно. Сопоставим ей тройку
$$
\begin{equation*}
\mathcal{M}':= \langle \mathcal{W}, (\mathscr{A}^+)', (\mathscr{A}^-)' \rangle
\end{equation*}
\notag
$$
такую, что для любых $w \in W$ и атомарного $A_w$-предложения $\Phi$
$$
\begin{equation*}
\begin{aligned} \, {(\mathfrak{A}_w^+)}' \Vdash \Phi \quad&:\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Box \Phi, \\ (\mathfrak{A}_w^-)' \Vdash \Phi \quad&:\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Diamond \Phi. \end{aligned}
\end{equation*}
\notag
$$
При этом мы полагаем ${(A_w)}' = A_w$ для всех $w \in W$. Легко понять, что $\mathcal{M}'$ окажется $\mathsf{QN4}_{\sigma}$-моделью. Более того, если $\mathcal{M}$ – $\mathsf{QB3S4}_{\sigma}$-модель, то $\mathcal{M}'$ будет $\mathsf{QN3}_{\sigma}$-моделью. Следующее утверждение аналогично лемме 14 из [11]. Лемма 8.4. Пусть $\mathcal{M} = \langle \mathcal{W}, \mathscr{A}^+, \mathscr{A}^- \rangle$ – $\mathsf{QBS4_{\sigma}}$-модель. Тогда для любых $w \in W$ и конструктивного $A_w$-предложения $\Phi$ Доказательство. В силу теоремы 8.1 мы можем считать, что $\Phi$ является н.н.ф.
Применяем индукцию по построению $\Phi$. Случай, когда $\Phi$ атомарно, тривиален. Случай, когда $\Phi = \, \sim P (t_1, \dots, t_n)$, немного сложнее:
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}', w \Vdash^+ \sim P (t_1, \dots, t_n) \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^- P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad {(\mathfrak{A}_w^-)}' \Vdash P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^- \Diamond P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \sim \Diamond P (t_1, \dots, t_n) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \tau (\sim P (t_1, \dots, t_n)). \end{aligned}
\end{equation*}
\notag
$$
Пусть $\Phi = \forall\,x\ \Psi.$ Тогда
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}', w \Vdash^+ \forall\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}', u \Vdash^+ {\Psi (x / \underline{a})} \quad \text{для всех} \ u \in R (w) \ \text{и} \ a \in A_u \\ \quad&\Longleftrightarrow \quad \mathcal{M}, u \Vdash^+ {\tau (\Psi (x / \underline{a}))} \quad \text{для всех} \ u \in R (w) \ \text{и} \ a \in A_u \\ \quad&\Longleftrightarrow \quad \mathcal{M}, u \Vdash^+ \tau (\Psi) (x / \underline{a}) \quad \text{для всех} \ u \in R (w) \ \text{и} \ a \in A_u \\ \quad&\Longleftrightarrow \quad \mathcal{M}, u \Vdash^+ \forall\,x\ \tau(\Psi) \quad \text{для всех} \ u \in R (w) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \Box \forall\,x\ \tau(\Psi) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \tau (\Phi). \end{aligned}
\end{equation*}
\notag
$$
Пусть $\Phi = \exists\,x\ \Psi$. Тогда
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}', w \Vdash^+ \exists\,x\ \Psi \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^+ \Psi (x / \underline{a}) \quad \text{для некоторого} \ a \in A_w \\ \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^+ \tau (\Psi (x / \underline{a})) \quad \text{для некоторого} \ a \in A_w \\ \quad&\Longleftrightarrow \quad \mathcal{M}', w \Vdash^+ \tau (\Psi) (x / \underline{a}) \quad \text{для некоторого} \ a \in A_w \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ \exists\,x\ \tau(\Psi) \\ \quad&\Longleftrightarrow \quad \mathcal{M}, w \Vdash^+ {\tau (\Phi)}. \end{aligned}
\end{equation*}
\notag
$$
Остальные случаи разбираются так же, как в $\mathsf{BK}$ (см. [11; § 7]). Лемма доказана. Замечание 8.5. В формулировке леммы 8.4 нельзя заменить $\Vdash^+$ на $\Vdash^-$. Действительно, пусть $\Phi = \Psi \to \Theta$. Тогда, как легко убедиться, однако обратная импликация в общем случае может нарушаться. Аналогичная проблема возникает при $\Phi = \forall\,x\ \Psi$. Отсюда легко получается Теорема 8.6. Для любого конструктивного $\sigma$-предложения $\Phi$ Другими словами, $\tau$ точно вкладывает $\mathsf{QN4}$ в $\mathsf{QBS4}$. Доказательство. В силу теорем о полноте для $\mathsf{QN4}$ и $\mathsf{QBS4}$ нам нужно показать, что
$$
\begin{equation*}
\vDash_{\mathsf{QN4}} \Phi \quad \Longleftrightarrow \quad \vDash_{\mathsf{QBS4}} {\tau (\Phi)}
\end{equation*}
\notag
$$
(см. теоремы 8.3 и 6.3 соответственно).
$\Longrightarrow$. Предположим, что $\vDash_{\mathsf{QN4}} \Phi$. Рассмотрим произвольные $\mathsf{QBS4}_{\sigma}$-модель $\mathcal{M}$ и $w \in W$. Поскольку $\mathcal{M}', w \Vdash^+ \Phi$, мы имеем $\mathcal{M}, w \Vdash^+ \tau (\Phi)$ по лемме 8.4. Стало быть, $\vDash_{\mathsf{QBS4}} {\tau (\Phi)}$. $\Longleftarrow$. Предположим, что $\vDash_{\mathsf{QBS4}} \tau (\Phi)$. Рассмотрим произвольные $\mathsf{QN4}_{\sigma}$-модель $\mathcal{M}$ и $w \in W$. Очевидно, $\mathcal{M}$ можно также рассматривать как $\mathsf{QBS4}_\sigma$-модель; при этом $\mathcal{M}'$ совпадет с $\mathcal{M}$. Значит, поскольку $\mathcal{M}, w \Vdash^+ \tau (\Phi)$, мы имеем $\mathcal{M}, w \Vdash^+ \Phi$ по лемме 8.4. Стало быть, $\vDash_{\mathsf{QN4}} \Phi$. Теорема доказана. Кроме того, имеет место Теорема 8.7. Для любого конструктивного $\sigma$-предложения $\Phi$ Другими словами, $\tau$ точно вкладывает $\mathsf{QN3}$ в $\mathsf{QB3S4}$. Это следует из теоремы 8.6 по модулю теорем о полноте для $\mathsf{QN4}$, $\mathsf{QBS4}$, $\mathsf{QN3}$ и $\mathsf{QB3S4}$. Замечание 8.8. Теоремы 8.6 и 8.7 можно было бы переформулировать в терминах отношений выводимости или семантического следования (с непустыми множествами гипотез). На самом деле такие формулировки окажутся равносильны исходным ввиду теорем о сильной полноте для $\mathsf{QN4}$, $\mathsf{QBS4}$, $\mathsf{QN3}$ и $\mathsf{QB3S4}$. Аналогичный теореме 8.7 результат верен для логики $\mathsf{QN4}^{\circ}$, которая получается из $\mathsf{QN4}$ путем исключения “неопределенности”, т.е. добавления релятивизации схемы $\mathrm{ExM}$ на язык $\mathsf{QN4}$. Точнее, возьмем
$$
\begin{equation*}
\mathsf{QBS4}^{\circ}:=\mathsf{QBS4} + \{\mathrm{ExM}\}.
\end{equation*}
\notag
$$
Тогда $\tau$ будет вкладывать $\mathsf{QN4}^{\circ}$ в $\mathsf{QBS4}^{\circ}$. Формально тут понадобится теорема о сильной полноте для $\mathsf{QN4}^{\circ}$, которую можно доказать по аналогии с теоремой 6.2, пользуясь канонической моделью для $\mathsf{QN4}$. Наконец, все результаты этого параграфа легко релятивизируются на случай постоянных носителей. При этом для $\mathsf{QN4}$-расширений роль схемы Баркан будет играть $\mathrm{CD}$. $\forall\,x\ (\Phi \vee \Psi) \to \Phi \vee \forall\,x\ \Psi$, где $x$ не входит свободно в $\Phi$. Однако такая релятивизация может критиковаться с конструктивной точки зрения, поскольку $\mathrm{CD}$ опровергается в семантике реализуемости по Клини (и тем более по Нельсону). § 9. Интерполяционные свойстваИзвестно, что некоторые расширения классической кванторной модальной логики $\mathsf{QK}$ обладают интерполяционным свойством Крейга (см., например, [21]). В этом параграфе, используя технику из [13; § 2], мы покажем, как результаты об интерполяции для $\mathsf{QK}$-расширений можно переносить на $\mathsf{QBK}$-расширения. Для каждой $\sigma$-формулы $\Phi$ положим
$$
\begin{equation*}
\mathrm{O} (\Phi):= \{\varepsilon \in \sigma \mid\varepsilon\ \text{входит в}\ \Phi\} \cup \mathrm{FV}(\Phi).
\end{equation*}
\notag
$$
Пусть $L$ – $\mathsf{QK}$-расширение. Говорят, что $L$ обладает интерполяционным свойством Крейга или, сокращенно, $\mathrm{CIP}$, если для любых сигнатуры $\sigma$ и $\Phi \to \Psi \in L_{\sigma}$ существует $\Theta \in \mathrm{Form}_{\sigma}$ такая, что
$$
\begin{equation*}
\{\Phi \to \Theta, \Theta \to \Psi\}\subseteq L, \qquad \mathrm{O} (\Theta)\subseteq \mathrm{O} (\Phi) \cap \mathrm{O} (\Psi).
\end{equation*}
\notag
$$
При этом $\Theta$ называют интерполянтом Крейга для $\Phi \to \Psi$ в $L$. Данная терминология будет использоваться также для $\mathsf{QBK}$-расширений. Замечание 9.1. На самом деле включение $\mathrm{FV}(\Phi)$ в $\mathrm{O}(\Phi)$ не имеет принципиального значения, так как при необходимости все свободные переменные $\Phi$ можно будет заменить на новые константные символы. Кроме того, стоит обсудить более тонкую версию $\mathrm{CIP}$ для $\mathsf{QBK}$-расширений (ср. [16; § 4]). В силу теоремы 3.8 мы можем ограничиться рассмотрением н.н.ф. Для данных $\sigma$-н.н.ф. $\Phi$ и $P \in \mathrm{Pred}_{\sigma}$ назовем вхождение $P$ в $\Phi$ позитивным, если оно не находится в области действия $\sim$, и негативным в противном случае. Для каждой $\sigma$-н.н.ф. $\Phi$ положим
$$
\begin{equation*}
\begin{aligned} \, \mathrm{D} (\Phi)&:= \{c \in \mathrm{Const}_{\sigma} \mid c\ \text{входит в}\ \Phi\} \cup \mathrm{FV} (\Phi), \\ \mathrm{P}^+ (\Phi)&:= \{P \in \mathrm{Pred}_{\sigma} \mid P\ \text{входит позитивно в}\ \Phi\}, \\ \mathrm{P}^- (\Phi)&:= \{P \in \mathrm{Pred}_{\sigma} \mid P\ \text{входит негативно в}\ \Phi\}. \end{aligned}
\end{equation*}
\notag
$$
Пусть $L$ – $\mathsf{QBK}$-расширение. Мы будем говорить, что $L$ обладает сильным интерполяционным свойством или, сокращенно, $\mathrm{SIP}$, если для любых сигнатуры $\sigma$ и $\sigma$-н.н.ф. $\Phi \to \Psi$ из $L$ найдется $\sigma$-н.н.ф. $\Theta$ такая, что
$$
\begin{equation*}
\begin{gathered} \, \{\Phi \to \Theta, \Theta \to \Psi\}\subseteq L, \qquad \mathrm{D} (\Theta)\subseteq \mathrm{D} (\Phi) \cap \mathrm{D} (\Psi), \\ \mathrm{P}^+ (\Theta)\subseteq \mathrm{P}^+ (\Phi) \cap \mathrm{P}^+ (\Psi), \qquad \mathrm{P}^- (\Theta)\subseteq \mathrm{P}^- (\Phi) \cap \mathrm{P}^- (\Psi). \end{gathered}
\end{equation*}
\notag
$$
При этом $\Theta$ называется сильным интерполянтом для $\Phi \to \Psi$ в $L$. Легко видеть, что $\mathrm{SIP}$ сильнее $\mathrm{CIP}$: если $L$ обладает $\mathrm{SIP}$, то оно обладает $\mathrm{CIP}$. Очевидно, каждому $\mathsf{QBK}$-расширению $L$ из $\mathscr{L}$ (из формулировки теоремы 6.3) будет соответствовать $\mathsf{QK}$-расширение $\underline{L}$ (без $\mathsf{B}$ в названии). Известно, что все такие $\underline{L}$ обладают $\mathrm{CIP}$ (см. [21]). Наша ближайшая цель – получить $\mathrm{SIP}$ для всех логик из $\mathscr{L}$. Для всякой сигнатуры $\sigma$ положим
$$
\begin{equation*}
\underline{\sigma}:= \sigma \cup \{\underline{P} \mid P \in \mathrm{Pred}_{\sigma}\},
\end{equation*}
\notag
$$
где $\underline{P}$ – новый предикатный символ той же местности, что и $P$. Рассмотрим произвольные $L$ из $\mathscr{L}$ и сигнатуру $\sigma$. Каждой $L_{\sigma}$-модели $\mathcal{M}$ сопоставим $\underline{L}_{\,\underline{\sigma}}$-модель
$$
\begin{equation*}
\underline{\mathcal{M}}:=\langle \mathcal{W}, \underline{\mathscr{A}} \,\rangle,
\end{equation*}
\notag
$$
где $\underline{\mathscr{A}}$ обозначает семейство $\langle \underline{\mathfrak{A}}_{\,w} \colon w \in W \rangle$ такое, что для любого $w \in W$:
Очевидно, $\underline{\mathcal{M}}$ является $\underline{L}_{\,\underline{\sigma}}$-моделью. Более того, для любой $\underline{L}_{\,\underline{\sigma}}$-модели $\mathcal{N}$ существует (единственная) $L_{\sigma}$-модель $\mathcal{M}$ такая, что $\underline{\mathcal{M}} = \mathcal{N}$. Далее, определим трансляцию $\rho$ из множества всех $\sigma$-н.н.ф. в множество всех $\underline{\sigma}$-формул без сильного отрицания следующим образом (ср. [13; § 2] и [16; § 4]):
$$
\begin{equation*}
\begin{aligned} \, \rho (P (t_1, \dots, t_n)) &:= P (t_1, \dots, t_n), \\ \rho (\sim P (t_1, \dots, t_n)) &:= \underline{P} (t_1, \dots, t_n), \\ \rho (\Phi_1 \odot \Phi_2) &:= \rho (\Phi_1) \odot \rho ( \Phi_2), \\ \rho (\bot) &:= \bot, \\ \rho (\sim \bot) &:= \bot \to \bot, \\ \rho (\heartsuit \Phi) &:= \heartsuit \rho (\Phi), \\ \rho ({\mathrm{Q} x}\, \Phi) &:={\mathrm{Q} x}\, \rho (\Phi), \end{aligned}
\end{equation*}
\notag
$$
где $\odot \in \{\wedge, \vee, \to\}$, $\heartsuit \in \{\Box, \Diamond\}$, $\mathrm{Q} \in \{\forall, \exists\}$ и $x \in \mathrm{Var}$. Разумеется, при необходимости действие $\rho$ можно распространить на все $\sigma$-формулы по правилу Формально мы должны были бы писать $\rho_{\sigma}$ вместо $\rho$, однако из контекста всегда будет ясно, о какой сигнатуре идет речь. Лемма 9.2. Для любых $L_{\sigma}$-модели $\mathcal{M}$, $w \in W$ и $\sigma_{A_w}$-предложения $\Phi$ Доказательство. В силу теоремы 3.8 можно считать, что $\Phi$ является н.н.ф. Далее лемма доказывается простой индукцией по построению $\Phi$. Теорема 9.3. Для любой $\sigma$-формулы $\Phi$ Другими словами, $\rho$ точно вкладывает $L$ в $\underline{L}$. Доказательство. В силу теорем о полноте для $L$ и $\underline{L}$ нам нужно показать, что
$$
\begin{equation*}
\vDash_{L} \Phi \quad \Longleftrightarrow \quad \vDash_{\underline{L}} {\tau (\Phi)}
\end{equation*}
\notag
$$
(см. теорему 6.3 и, например, [15; § 6]). Далее можно рассуждать по аналогии с доказательством теоремы 8.6, пользуясь леммой 9.2 вместо леммы 8.4.
Теорема доказана. Отсюда, пользуясь интерполяционными теоремами для $\mathsf{QK}$-расширений, мы можем получить следующий результат. Доказательство. Рассмотрим произвольные $L$ из $\mathscr{L}$ и сигнатуру $\sigma$.
Предположим, что $\sigma$-н.н.ф. $\Phi \to \Psi$ лежит в $L$. В силу теоремы 9.3 мы имеем Поскольку $\underline{L}$ обладает $\mathrm{CIP}$, существует интерполянт Крейга $\Theta$ для $\rho (\Phi) \to \rho (\Psi)$ в $\underline{L}$. Возьмем
$$
\begin{equation*}
\Theta':=\text{результат замены в }\Theta\text{ каждого }\underline{P}\text{ на }\sim P.
\end{equation*}
\notag
$$
Тогда $\Theta'$ – $\sigma$-н.н.ф., причем $\rho (\Theta') = \Theta$. Еще раз применяя теорему 9.3, мы получаем
$$
\begin{equation*}
{\Phi \to \Theta'}\in L, \qquad {\Theta' \to \Psi} \in\ L.
\end{equation*}
\notag
$$
При этом по построению
$$
\begin{equation*}
\begin{aligned} \, \mathrm{D} (\Theta')&= (\mathrm{O} (\Theta') \cap \mathrm{Const}_{\sigma}) \cup \mathrm{FV} (\Theta') \\ &= (\mathrm{O} (\Theta) \cap \mathrm{Const}_{\sigma}) \cup \mathrm{FV} (\Theta) \\ &\subseteq \mathrm{D} (\rho (\Phi)) \cap \mathrm{D} (\rho (\Psi)) = \mathrm{D} (\Phi) \cap \mathrm{D} (\Psi). \end{aligned}
\end{equation*}
\notag
$$
Более того, легко убедиться, что
$$
\begin{equation*}
\mathrm{P}^+ (\Theta)\subseteq \mathrm{P}^+ (\Phi) \cap \mathrm{P}^+ (\Psi), \qquad \mathrm{P}^- (\Theta)\subseteq \mathrm{P}^- (\Phi) \cap \mathrm{P}^- (\Psi).
\end{equation*}
\notag
$$
Значит, $\Theta'$ – сильный интерполянт для $\Phi \to \Psi$ в $L$.
Теорема доказана. Обсудим теперь $\mathsf{QBK}$-расширения типа (i), т.е. $\mathsf{QB3K}$ и $\mathsf{QBK}^{\circ}$. Определим трансляции $\rho^3$ и $\rho^{\circ}$ так же, как $\rho$, но со следующими модификациями (ср. [13; § 2]):
$$
\begin{equation*}
\begin{aligned} \, \rho^3 (\sim P (t_1, \dots, t_n)) &:=\underline{P} (t_1, \dots, t_n) \wedge \neg P (t_1, \dots, t_n), \\ \rho^{\circ} (\sim P (t_1, \dots, t_n)) &:=\underline{P} (t_1, \dots, t_n) \vee \neg P (t_1, \dots, t_n). \end{aligned}
\end{equation*}
\notag
$$
Тогда имеет место Лемма 9.5. Для любых $\mathsf{QB3K}_{\sigma}$-модели $\mathcal{M}$, $w \in W$ и $A_w$-предложения $\Phi$ Аналогично для $\mathsf{QBK}^{\circ}$ и $\rho^{\circ}$. Доказательство. Заметим, что для любой $\mathsf{QB3K}_{\sigma}$-модели $\mathcal{M}$ и атомарного $A_w$-предложения $P (t_1, \dots, t_n)$
$$
\begin{equation*}
\begin{aligned} \, \mathcal{M}, w \Vdash^+ {\sim P (t_1, \dots, t_n)} \quad &\Longleftrightarrow \quad \underline{\mathcal{M}}, w \Vdash {\underline{P} (t_1, \dots, t_n)} \\ \quad &\Longleftrightarrow \quad \underline{\mathcal{M}}, w \Vdash \underbrace{\underline{P} (t_1, \dots, t_n) \wedge \neg P (t_1, \dots, t_n)}_{\rho^3 (\sim P (t_1, \dots, t_n))}. \end{aligned}
\end{equation*}
\notag
$$
Поэтому можно рассуждать так же, как в доказательстве леммы 9.2.
Аналогично для $\mathsf{QBK}^{\circ}$ и $\rho^{\circ}$. Лемма доказана. С другой стороны, при $L \in \{\mathsf{QBK}^{\circ}, \mathsf{QB3K}\}$ нельзя для каждой $\mathsf{QK}_{\underline{\sigma}}$-модели $\mathcal{N}$ найти $L_{\sigma}$-модель $\mathcal{M}$ такую, что $\underline{\mathcal{M}} = \mathcal{N}$. Поэтому нужно действовать чуть более тонко, чем при $L \in \mathscr{L}$. Каждой $\mathsf{QK}_{\underline{\sigma}}$-модели $\mathcal{N} = \langle \mathcal{W}, \mathscr{A} \rangle$ сопоставим $\mathsf{QB3K}_{\sigma}$-модель
$$
\begin{equation*}
\mathcal{N}^3:= \langle \mathcal{W}, \mathscr{A}^{3, +}, \mathscr{A}^{3, -} \rangle,
\end{equation*}
\notag
$$
где $\mathscr{A}^{3, +}$ и $\mathscr{A}^{3, -}$ обозначают семейства $\langle \mathfrak{A}_w^{3, +} : w \in W \rangle$ и $\langle \mathfrak{A}_w^{3, +} : w \in W \rangle$ такие, что для любого $w \in W$:
Очевидно, $\mathcal{N}^3$ является $\mathsf{QB3K}_{\sigma}$-моделью. Аналогично определяется $\mathsf{QBK}^{\circ}_{\sigma}$-модель
$$
\begin{equation*}
\mathcal{N}^{\circ}:= \langle \mathcal{W}, \mathscr{A}^{\circ, +}, \mathscr{A}^{\circ, -} \rangle,
\end{equation*}
\notag
$$
но в последнем пункте нужно заменить $\cap$ на $\cup$: Следующее утверждение будет выполнять роль, обратную к роли леммы 9.5. Лемма 9.6. Для любых $\mathsf{QK}_{\underline{\sigma}}$-модели $\mathcal{N}$, $w \in W$ и $\sigma_{A_w}$-предложения $\Phi$ Аналогично для $\rho^{\circ}$ и $\mathcal{N}^{\circ}$. Доказательство получается простой индукцией по построению $\Phi$. Теорема 9.7. Для любой $\sigma$-формулы $\Phi$ Аналогично для $\mathsf{QBK}^{\circ}$ и $\rho^{\circ}$. Другими словами, $\rho^3$ и $\rho^{\circ}$ точно вкладывают соответственно $\mathsf{QB3K}$ и $\mathsf{QBK}^{\circ}$ в $\mathsf{QK}$. Это следует из лемм 9.6 (в прямую сторону) и 9.5 (в обратную сторону) с учетом теорем о полноте для $\mathsf{QB3K}$, $\mathsf{QBK}^{\circ}$ и $\mathsf{QK}$. Отсюда уже можно получить $\mathrm{CIP}$ для расширений типа (i). Доказательство. Рассмотрим произвольную сигнатуру $\sigma$.
Предположим, что $\Phi \to \Psi \in \mathsf{QB3K}_{\sigma}$. В силу теоремы 9.7 мы имеем Поскольку $\mathsf{QK}$ обладает $\mathrm{CIP}$, существует интерполянт Крейга $\Theta$ для $\rho^3 (\Phi) \to \rho^3 (\Psi)$ в $\mathsf{QB3K}$. Ясно, что $\Theta$ не обязательно имеет вид $\rho^3 (\Theta')$ (так как в $\Theta$ могут встречаться “отдельно стоящие” $\underline{P} (t_1, \dots, t_n)$, не связанные конъюнкцией с $\neg P (t_1, \dots, t_n)$). Возьмем
$$
\begin{equation*}
\begin{aligned} \, \widetilde{\Theta} &:= \text{результат замены в }\Theta \text{ каждой отдельно стоящей} \\ &\qquad \underline{P} (t_1, \dots, t_n)\text{ на }\underline{P} (t_1, \dots, t_n) \wedge {\neg P (t_1, \dots, t_n)}. \end{aligned}
\end{equation*}
\notag
$$
Легко показать, что для любых $\mathsf{QB3K}_{\sigma}$-модели $\mathcal{M}$, $w \in W$ и $A_w$-подстановки $\lambda$
$$
\begin{equation*}
\underline{\mathcal{M}}, w \Vdash \lambda \Theta \quad \Longleftrightarrow \quad \underline{\mathcal{M}}, w \Vdash \lambda \widetilde{\Theta}.
\end{equation*}
\notag
$$
Очевидно, $\widetilde{\Theta} = \rho^3 (\Theta')$ для подходящей $\sigma$-формулы $\Theta'$. С учетом теоремы о корректности для $\mathsf{QK}$ отсюда следует, что для любых $\mathsf{QB3K}_{\sigma}$-модели $\mathcal{M}$, $w \in W$ и $A_w$-подстановки $\lambda$
$$
\begin{equation*}
\underline{\mathcal{M}}, w \Vdash {\lambda (\rho^3 (\Phi) \to \rho^3 ( \Theta'))}, \qquad \underline{\mathcal{M}}, w \Vdash {\lambda (\rho^3 (\Theta') \to \rho^3 (\Psi))},
\end{equation*}
\notag
$$
что в силу леммы 9.5 равносильно
$$
\begin{equation*}
\mathcal{M}, w \Vdash \lambda (\Phi \to \Theta'), \qquad \mathcal{M}, w \Vdash \lambda (\Theta' \to \Psi).
\end{equation*}
\notag
$$
По теореме о полноте для $\mathsf{QB3K}$ последнее означает, что
$$
\begin{equation*}
\Phi \to \Theta'\in \mathsf{QB3K}_{\sigma}, \qquad \Theta' \to \Psi \in\ \mathsf{QB3K}_{\sigma}.
\end{equation*}
\notag
$$
При этом нетрудно проверить, что $\mathrm{O} (\Theta) \subseteq \mathrm{O} ( \Phi) \cap \mathrm{O} (\Psi)$. Значит, $\Theta'$ – интерполянт Крейга для $\Phi \to \Psi$ в $\mathsf{QB3K}$.
Аналогично рассуждаем в случае $\mathsf{QBK}^{\circ}$. Теорема доказана. Замечание 9.9. Логики $\mathsf{QB3K}$ и $\mathsf{QBK}^{\circ}$ не обладают $\mathrm{SIP}$. Действительно, в случае $\mathsf{QB3K}$ возьмем где $P$ – какой-нибудь $n$-местный предикатный символ. Тогда $\Phi \to \Psi \in \mathsf{QB3K}$, но у $\Phi \to \Psi$ нет сильного интерполянта в $\mathsf{QB3K}$. В случае $\mathsf{QBK}^{\circ}$ можно взять Тогда $\Phi \to \Psi \in \mathsf{QBK}^{\circ}$, но у $\Phi \to \Psi$ нет сильного интерполянта в $\mathsf{QBK}^{\circ}$. Разумеется, доказательство теоремы 9.8 легко модифицировать с тем, чтобы получить $\mathrm{CIP}$ для $\mathsf{QB3S4}$, например. 
Цитирование в формате AMSBIB
\RBibitem{GreSpe24} |
|
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Обратная связь: |
Пользовательское соглашение
|
Регистрация посетителей портала |
Логотипы |
|