| Математический сборник |
|
|
|
|
|
Эта публикация цитируется в 7 научных статьях (всего в 7 статьях) Предикатный вариант совместной логики задач и высказываний А. А. Оноприенко Математический институт им. В. А. Стеклова Российской академии наук, г. Москва
Англоязычная версия:
Sbornik: Mathematics, 2022, Volume 213, Issue 7, Pages DOI: https://doi.org/10.4213/sm9608e 
Реферативные базы данных:
     § 1. ВведениеВ настоящей работе мы рассматриваем логику $\mathrm{QHC}$ – объединенную логику задач и высказываний, введенную С. А. Мелиховым (см. [1], [2]). В этой логике каждая переменная и каждая формула имеют один из двух сортов: высказывание либо задача. Формулы сорта высказывание и сорта задача связаны между собой двумя модальностями: ? и !. Применив ! к высказыванию $p$, мы получим задачу $!p$ – “доказать высказывание $p$”. Наоборот, применив ? к задаче $\alpha$, мы получим высказывание $?\alpha$ – “задача $\alpha$ имеет решение”. Семантика пропозиционального фрагмента логики $\mathrm{QHC}$ – логики $\mathrm{HC}$ – подробно изучена автором в [3]. В этой работе рассмотрены HC-алгебры Линденбаума, семантика типа Крипке с двумя множествами миров, а также семантика типа Крипке с отмеченными1 мирами. Шкалы последнего типа возникли в работе [4] в качестве моделей для интуиционистской эпистемической логики $\mathrm{IEL}^+$. Автором настоящей работы была показана полнота логики HC относительно каждого из этих типов моделей, свойство конечных моделей, а также консервативность логики HC относительно логики $\mathrm{IEL}^+$ (если понимать модальность $\mathbf K$ как $!?$). Система $\mathrm{QHC}$ вдохновлена неформальным исчислением задач А. Н. Колмогорова и лежит в русле исследований конструктивной семантики Брауэра–Гейтинга–Колмогорова (см. [5]–[22]). Комбинируя модальности ! и ? логики $\mathrm{QHC}$, можно получить производные модальности. Модальность $?!$, обозначаемую как $\Box$ и примененную к высказыванию $p$, можно понимать как высказывание “существует доказательство высказывания $p$” или “$p$ доказуемо”. Модальность !?, обозначаемую как $\nabla$ и примененную к задаче $\alpha$, можно понимать как задачу “доказать, что задача $\alpha$ имеет решение”. Дальнейшее итерирование базовых модальностей ! и ? не дает ничего нового, поскольку в логике $\mathrm{QHC}$ доказуемы формулы $!p\leftrightarrow\,!?!p$ и $?\alpha\leftrightarrow\,?!?\alpha$ (см. [1]). В некотором смысле модальность $\Box$ соответствует классическому пониманию понятия знания об истинности высказывания, а модальность $\nabla$ – интуиционистскому пониманию. Основываясь на аксиомах и правилах вывода логики $\mathrm{QHC}$, несложно доказать (см., например, [1]), что модальность $\Box$ удовлетворяет следующим принципам: $(1^{\Box})$ $\Box p\to p$; $(2^{\Box})$ $\Box p\to \Box\Box p$; $(3^{\Box})$ $\cfrac{p}{\Box p}$; $(4^{\Box})$ $\Box(p\to q)\to(\Box p\to \Box q)$. Модальность $\nabla$ удовлетворяет следующим принципам: $(1^{\nabla})$ $\alpha\to\nabla\alpha$; $(2^{\nabla})$ $\nabla\nabla\alpha\to\nabla\alpha$; $(3^{\nabla})$ $\nabla\bot\to\bot$; $(4^{\nabla})$ $\nabla(\alpha\to\beta)\to(\nabla\alpha\to\nabla\beta)$. Аксиомы и правила вывода $(1^{\Box})-(4^{\Box})$ в классической логике предикатов с модальностью $\Box$ образуют логику $\mathrm{QS4}$ (это предикатный вариант логики $\mathrm{S4}$). В [1] было показано, что $\mathrm{QHC}$ – консервативное расширение логики $\mathrm{QS4}$. Аксиомы $(1^{\nabla})$–$(4^{\nabla})$ в интуиционистской логике предикатов с модальностью $\nabla$ образуют логику, названную С. А. Мелиховым в [1] логикой $\mathrm{QH4}$. Интуиционистская модальная логика, содержащая аксиомы $(1^{\nabla})$, $(2^{\nabla})$ и $(4^{\nabla})$, впервые возникла в работе Р. Голдблатта [23], который исследовал логику оператора локализации на топосе. Оператор на гейтинговой алгебре с аналогичными свойствами также возник в работе А. Г. Драгалина [24], который называл его “оператором пополнения” (для таких операторов в англоязычной литературе закрепился термин nucleus). Впоследствии эта логика была переоткрыта М. Фэтлоу и М. Мендлером и получила название lax logic. В статье [25] был изучен пропозициональный вариант PLL, в [26] – предикатный вариант QLL этой логики. При добавлении аксиомы $(3^{\nabla})$ рассматриваемая логика называется соответственно $\mathrm{PLL}^+$ или $\mathrm{QLL}^+$. В работе [26] построены модели типа Крипке для логик $\mathrm{QLL}$ и $\mathrm{QLL}^+$. Эти модели имеют достаточно сложную структуру: они содержат непустое множество возможных миров, два отношения достижимости, отображение, сопоставляющее миру некоторое подмножество миров, а также множество “миров, подверженных ошибкам” (только для логики QLL). Изучением логики QLL занимался также П. Акцель (см. [27]), еще один тип семантики QLL был построен Р. Голдблаттом (см. [28]), Д. Рогозин исследовал лямбда-исчисление, связанное с этой логикой и некоторыми другими близкими к ней логиками (см. [29]). С. Артёмов и Т. Протопопеску провели глубокий анализ интуиционистской логики знания и построили три формальные системы: $\mathrm{IEL}^-$, $\mathrm{IEL}$ и $\mathrm{IEL}^+$. Системы $\mathrm{IEL}$ и $\mathrm{IEL}^+$ оказались совпадающими соответственно с логиками $\mathrm{PLL}$ и $\mathrm{PLL}^+$. В работе [4] построены модели Крипке с отмеченными мирами для логики $\mathrm{IEL}^+$, которые лежат в основе семантики логики $\mathrm{QHC}$ в настоящей работе. Автором настоящей работы было показано в [3], что пропозициональная логика $\mathrm{HC}$ является консервативным расширением логики $\mathrm{PLL}^+$. Логику $\mathrm{PLL}^+$ С. А. Мелихов обозначал как $\mathrm{H4}$, в дальнейшем мы будем придерживаться этого обозначения. В настоящей работе доказывается, что $\mathrm{QHC}$ является консервативным расширением предикатной логики $\mathrm{QH4}$, а также строятся модели Крипке с отмеченными мирами логик $\mathrm{QHC}$ и $\mathrm{QH4}$. Одним из возможных приложений логики $\mathrm{QHC}$ является построение на ее основе различных стандартных теорий, которое лучше согласуется с интуитивным пониманием. С. А. Мелихов приводит аксиоматизацию элементарной геометрии Тарского, формализованную в рамках $\mathrm{QHC}$, и аргументирует это тем, что сам Евклид рассматривал постулаты и аксиомы (см. [2]). На основе $\mathrm{QHC}$ становится возможным более ясно описать логическую структуру теории Евклида и избавиться от скрытых гипотез и возникающих из них парадоксов. Показано, что эта теория содержит (в некотором точном смысле) элементарную геометрию Тарского (см. [30]) как классическую часть и конструктивную версию геометрии Тарского, предложенную М. Бисоном (см. [31]), как интуиционистскую часть. В настоящей работе предлагается семантика Крипке предикатной логики $\mathrm{QHC}$, доказывается ее корректность и полнота. Кроме того, показана консервативность $\mathrm{QHC}$ над интуиционистской модальной предикатной логикой $\mathrm{QH4}$ (для пропозициональных вариантов этих логик консервативность была показана в [3]). Показаны дизъюнктивное и экзистенциальное свойства $\mathrm{QHC}$, а именно если интуиционистская формула $\alpha\vee\beta$ выводима в $\mathrm{QHC}$, то $\alpha$ или $\beta$ выводима в $\mathrm{QHC}$; если интуиционистская формула $\exists\, x\ \alpha(x)$ выводима в $\mathrm{QHC}$, то $\alpha(c)$ выводима в $\mathrm{QHC}$ для некоторой константы $c$ (но необходимо, чтобы сигнатура содержала хотя бы одну константу). § 2. Логика $\mathrm{QHC}$Сигнатура $\Omega$ логики $\mathrm{QHC}$ состоит из множества константных символов $c_1, c_2,\dots$ и двух множеств предикатных символов: VarProp – множество предикатных символов сорта высказывание и VarProb – множество предикатных символов сорта задача; язык логики $\mathrm{QHC}$ с сигнатурой $\Omega$ будем называть языком $\Omega$. Каждому предикатному символу приписывается натуральное число, которое обозначает его валентность. Будем обозначать предикатные символы сорта высказывание строчными латинскими буквами ($p(x,y,z),q(x),\dots$), а предикатные символы сорта задача – строчными греческими буквами ($\alpha(x),\beta(x,y),\dots$). Так же будем обозначать формулы логики $\mathrm{QHC}$ соответствующих сортов. Формулы неизвестного сорта будем обозначать заглавными греческими буквами: $A,B,\Phi,\Psi,\dots$ . Для простоты рассматриваем логику $\mathrm{QHC}$ в языке без функциональных символов, а лишь с предикатными и константными. Термами $\mathrm{QHC}$ являются индивидные переменные $x_1, x_2, \dots$ и константы $c_1,c_2,\dots$ (они ни к какому сорту не принадлежат, интуитивно можно считать, что это “объекты”, которые могут встречаться в формулировках высказываний и задач). Каждая формула $\mathrm{QHC}$ имеет либо сорт высказывание, либо сорт задача. Формулы логики $\mathrm{QHC}$ строятся из атомарных формул при помощи стандартных классических и интуиционистских связок $\wedge$, $\vee$, $\to$, $\leftrightarrow$, $\neg$, классических и интуиционистских кванторов $\exists$, $\forall$ и модальностей $?$ и $!$ с соответствующими ограничениями на валентность, при этом атомарные формулы определяются, как в стандартной логике предикатов. Аналогично пропозициональному фрагменту логики $\mathrm{QHC}$ – логике $\mathrm{HC}$ (см. [3]) – связки и кванторы не меняют сорт формулы, а модальности – меняют. Классические истину и ложь будем обозначать как $0$ и $1$, а интуиционистские истину и ложь – как $\top$ и $\bot$ соответственно. Аксиомы и правила вывода логики $\mathrm{HC}$ следующие. I. Все аксиомы и правила вывода классической пропозициональной логики. В схемы аксиом вместо переменных можно подставлять любые формулы сорта высказывание (возможно, содержащие модальности $\text{? и !).}$ II. Все аксиомы и правила вывода интуиционистской пропозициональной логики. В схемы аксиом вместо переменных можно подставлять любые формулы сорта задача (возможно, содержащие модальности $\text{? и !).}$ III. Дополнительные аксиомы (точнее, схемы аксиом) и правила вывода, перечисленные ниже: 1) $!(p\to q)\to(!p\to \,!q)$; 2) $?(\alpha\to\beta)\to (?\alpha\to\,?\beta)$; 3) $\cfrac{p}{!p}$; 4) $\cfrac{\alpha}{?\alpha}$; 5) $?!p\to p$; 6) $\alpha\to\,!?\alpha$; 7) $\neg!0$. Правила вывода 3) и 4) называются правилами усиления. Логика $\mathrm{QHC}$ является расширением логики $\mathrm{HC}$. В схемы аксиом логики $\mathrm{QHC}$ можно подставлять любые формулы сорта высказывание (задача), возможно, содержащие кванторы. Кроме того, к аксиомам и правилам вывода логики $\mathrm{QHC}$ добавляются следующие аксиомы и правила вывода: 8) $\forall\, v \ A(v)\to A(t)$; 9) $A(t)\to\exists\, v\ A(v)$. Предполагается, что в этих двух схемах аксиом подстановки $t$ вместо $v$ корректны. Отметим, что поскольку $A$ – формула сорта высказывание или сорта задача, то фактически мы имеем четыре схемы аксиом. Правила Бернайса: 10) $\cfrac{A\to B}{A\to\forall\, x \ B}$; 11) $\cfrac{B\to A}{\exists\, x \ B\to A}$. Предполагается, что в этих двух правилах вывода $x$ не является параметром формулы $A$. Аналогично предыдущему, поскольку $A, B$ – формулы одного сорта (сорта высказывание или сорта задача), мы имеем четыре правила вывода. Определение 1. Вывод в логике $\mathrm{QHC}$ – это конечная последовательность формул $\Phi_1,\dots,\Phi_n$ такая, что для каждого $i = 1, \dots, n$ формула $\Phi_i$ либо является аксиомой логики $\mathrm{QHC}$, либо получена из одной или двух предыдущих формул этого списка по одному из правил вывода (по правилу modus ponens, или по одному из правил Бернайса, или по одному из правил усиления). Формула $\Phi$ выводима в логике $\mathrm{QHC}$ (является теоремой логики $\mathrm{QHC}$), если существует вывод, оканчивающийся формулой $\Phi$. Обозначение: $\vdash\Phi$. Определение 2. Квазивывод формулы $\Phi$ из гипотез $\Gamma$ – это конечная последовательность формул $\Phi_1,\dots,\Phi_n$ такая, что для каждого $i = 1, \dots, n$ формула $\Phi_i$ либо является аксиомой логики $\mathrm{QHC}$, либо гипотезой, либо получена из одной или двух предыдущих формул по одному из правил вывода. Для данного квазивывода $\Phi_1,\dots,\Phi_n$ и для каждого $i=1,\dots,n$ определим по индукции множество $\Delta(\Phi_i)\subseteq\Gamma$: 1) если $\Phi_i$ – аксиома, то $\Delta(\Phi_i)=\varnothing$; 2) если $\Phi_i$ – гипотеза, то $\Delta(\Phi_i)=\{\Phi_i\}$; 3) если $\Phi_i$ получена по правилу modus ponens из $\Phi_k$ и $\Phi_l$, то 4) если $\Phi_i$ получена по одному из правил Бернайса, 10) или 11), или же по одному из правил усиления, 3) или 4), из $\Phi_k$, то $\Delta(\Phi_i)=\Delta(\Phi_k)$. Неформально $\Delta(\Phi_i)$ – множество гипотез, от которых зависит формула $\Phi_i$, получающаяся при выводе. Определение 3. Вывод формулы $\Phi$ из гипотез $\Gamma$ – это квазивывод $\Phi$ из $\Gamma$, в котором любое применение правил Бернайса, 10) или 11), к формуле $\Phi_i$ связывает переменную, не входящую свободно ни в одну из формул множества $\Delta(\Phi_i)$. Формула $\Phi$ выводима из $\Gamma$, если существует вывод из $\Gamma$, оканчивающийся формулой $\Phi$. Обозначение: $\Gamma\vdash^*\Phi$. Определение 4. Слабый квазивывод формулы $\Phi$ из гипотез $\Gamma$ – это конечная последовательность формул $\Phi_1,\dots,\Phi_n$ такая, что для каждого $i = 1, \dots, n$ формула $\Phi_i$ либо является теоремой логики $\mathrm{QHC}$, либо гипотезой, либо получена из двух предыдущих формул этого списка по правилу modus ponens или по одному из правил Бернайса. Аналогичным образом определяются множество $\Delta(\Phi_i)$ для данного слабого квазивывода и понятие слабого вывода формулы $\Phi$ из множества гипотез $\Gamma$. Тот факт, что существует слабый вывод формулы $\Phi$ из множества гипотез $\Gamma$, обозначается как $\Gamma\vdash\Phi$. Если $\Gamma$ и $\Delta$ – два множества формул, то будем писать $\Gamma\vdash\Delta$ ($\Gamma\vdash^*\Delta$), если $\Gamma\vdash\Phi$ ($\Gamma\vdash^*\Phi$) для любой формулы $\Phi\in\Delta$. Теорема 1 (о дедукции). Пусть $\Gamma$ – некоторое множество формул, $\Phi,\Psi$ – формулы одного сорта. Пусть $\Gamma\cup\{\Phi\}\vdash\Psi$. Тогда $\Gamma\vdash\Phi\to\Psi$. Теорема доказывается методом, изложенным в [32] – индукцией по длине вывода. § 3. Корректность логики $\mathrm{QHC}$ относительно моделей Крипке с отмеченными мирамиПусть $\Omega$ – язык логики QHC. Шкала Крипке с отмеченными мирами этого языка – это набор $\mathcal K=(W,\preccurlyeq,\mathrm{Aud})$, где $(W,\preccurlyeq)$ – частично упорядоченное множество, $\mathrm{Aud}\subseteq W$ и выполнено свойство
$$
\begin{equation*}
\forall\, a\in W \ \exists\, b\in W \ (a\preccurlyeq b\wedge b\in\mathrm{Aud}).
\end{equation*}
\notag
$$
Модель Крипке логики QHC с отмеченными мирами – это шкала Крипке с функцией $D$, которая каждому $a\in W$ сопоставляет непустое множество $D_a$, а также с оценкой атомов $\models$. Предполагается, что если $a\preccurlyeq b$, то $D_a\subseteq D_b$ (интуитивно, $D_a$ – множество объектов, построенных к моменту времени $a$ и доступных для исследования; условие $a\preccurlyeq b\Rightarrow D_a\subseteq D_b$ означает, что обнаруженные объекты не исчезают в будущем). Если язык $\Omega$ содержит константу $c$, то ей сопоставляется объект $\overline c\in D_{a}$ для любого $a\in W$. В дальнейшем мы будем отождествлять $c$ и $\overline c$. Оценка атомов $\models$ – это некоторое соответствие между множеством $W$ и множеством всех атомов вида $A(x_1,\dots,x_n)$, где $A$ есть $n$-местный предикатный символ сигнатуры $\Omega$, а $x_1,\dots,x_n\in\bigcup_{a\in W}D_a$. Запись $a\models A(x_1,\dots,x_n)$ прочитывается стандартным образом: “$A(x_1,\dots,x_n)$ истинно в $a$”. На соответствие $\models$ налагается ограничение: атомы сорта задача могут быть истинны или ложны в любом мире множества $W$, но атомы (и другие формулы) сорта высказывание могут быть истинны или ложны только в мирах из множества $\mathrm{Aud}$. Кроме того, соответствие $\models$ обладает таким свойством: если $a\models A(x_1,\dots,x_n)$, то $\{x_1,\dots,x_n\}\subseteq D_a$, и если $A(x_1,\dots,x_n)$ – атом сорта задача и $a\preccurlyeq b$, то $b\models A(x_1,\dots,x_n)$ (т.е. для атомов сорта задача выполнена монотонность). Определим отношение истинности для всех остальных формул QHC индукцией по построению формулы. Для классических связок $\wedge$, $\vee$, $\rightarrow$, $\neg$ оценка определяется поточечно в мирах множества $\mathrm{Aud}$. Для интуиционистских связок $\wedge$, $\vee$, $\rightarrow$, $\neg$ оценка определяется в мирах множества $W$, как в обычных шкалах Крипке. Для модальностей оценка определяется так же, как в моделях Крипке логики HC с отмеченными мирами:
$$
\begin{equation*}
\begin{aligned} \, &a\models\,?\alpha \Leftrightarrow a\models\alpha \quad \text{(для }a\in\mathrm{Aud}), \\ &a\models\,!p \Leftrightarrow \forall\, b\in\mathrm{Aud}\ (a\preccurlyeq b \Rightarrow b\models p)\quad \text{(для }a\in W). \end{aligned}
\end{equation*}
\notag
$$
Определим истинность для классических кванторов $\exists$ и $\forall$ ($a\in\mathrm{Aud}$):
$$
\begin{equation*}
\begin{aligned} \, &a\models\exists\, x \ p(x) \Leftrightarrow (\exists\, v\in D_a)\ a\models p(v), \\ &a\models\forall\, x \ p(x) \Leftrightarrow (\forall\, v\in D_a)\ a\models p(v). \end{aligned}
\end{equation*}
\notag
$$
Наконец, определим истинность для интуиционистских кванторов $\exists$ и $\forall$ ($a\in W$):
$$
\begin{equation*}
\begin{aligned} \, &a\models\exists\, x \ \alpha(x) \Leftrightarrow \exists\, v\in D_a \ a\models \alpha(v), \\ &a\models\forall\, x \ \alpha(x) \Leftrightarrow \forall\, b\succcurlyeq a \ \forall\, v\in D_b \ b\models \alpha(v). \end{aligned}
\end{equation*}
\notag
$$
Доказательство проводится стандартной индукцией по построению формулы $\alpha$. Формула сорта задача (высказывание) истинна в модели $\mathcal K$, если она истинна в любом мире множества $W$ ($\mathrm{Aud}$) этой модели. Теорема 2 (корректность). Если замкнутая формула языка $\Omega$ выводима в логике $\mathrm{QHC}$, то она истинна в любой модели Крипке для языка $\Omega$. Доказательство. Докажем более общее утверждение: если формула выводима в QHC, то ее универсальное замыкание истинно в любой модели Крипке. Очевидно, достаточно проверить, что универсальное замыкание любой аксиомы истинно в любой модели Крипке и что правила вывода сохраняют это свойство. Для аксиом и правил вывода логики $\mathrm{HC}$ это следует из корректности $\mathrm{HC}$ относительно моделей Крипке с отмеченными мирами (см. [3]), поскольку модели Крипке логики $\mathrm{QHC}$ с отмеченными мирами являются обогащением таковых моделей логики $\mathrm{HC}$. Тот факт, что modus ponens сохраняет указанное свойство формул, очевиден. Осталось проверить это для новых аксиом и правил вывода 8)–11). Для их классических вариантов корректность устанавливается непосредственно по определению, а для интуиционистских доказательство имеется в [32; теорема 53]. Теорема доказана. Пример 1 (модель Крипке с отмеченными мирами). Классическую логику иногда понимают как логику, в которой все высказывания делятся на истинные и ложные. В интуиционистской логике помимо истинных и ложных высказываний имеются также неустановленные, которые могут стать истинными или ложными спустя время. Поскольку в математике имеются недоказуемые и неопровержимые утверждения, второй подход представляется более удовлетворительным. Покажем, что логика $\mathrm{QHC}$ предусматривает эту возможность. Изобразим шкалу Крипке логики $\mathrm{QHC}$, в которой отношение порядка $\preccurlyeq$ обозначено стрелками (если $x\preccurlyeq y$, то стрелка ведет из $x$ в $y$), а множество отмеченных миров $\mathrm{Aud}$ равно $\{b,c\}$:
Зададим на этой шкале оценку переменных: $b\models p$, $c\nvDash p$. Отсюда получаем $b\models\,!p$, $c\models\,!\neg p$. Таким образом, находясь в мире $a$, выше него имеем два мира, в одном из которых строится доказательство $p$, а в другом строится доказательство $\neg p$. § 4. Выводимость из гипотез в логике $\mathrm{QHC}$Отметим несколько простых свойств отношений выводимости $\vdash$ и $\vdash^*$ из гипотез в логике $\mathrm{QHC}$. Лемма 2. 1) Пусть $\Gamma$ – множество формул сорта задача и $\Gamma\vdash\alpha$. Тогда $?\Gamma\vdash\,?\alpha$. 2) Пусть $\Gamma$ – множество формул сорта высказывание и $\Gamma\vdash p$. Тогда $!\Gamma\vdash\,!p$. Доказательство. Докажем п. 1). Из того, что $\Gamma\vdash\alpha$, следует, что существует конечное множество формул $\beta_1,\dots,\beta_n\in\Gamma$ таких, что $\{\beta_1,\dots,\beta_n\}\vdash\alpha$. Применяя несколько раз теорему о дедукции 1, имеем Равносильным образом получаем Получаем, что $\beta_1\wedge\dots\wedge\beta_n\to\alpha$ – теорема логики $\mathrm{QHC}$. Следовательно, $?(\beta_1\wedge\dots\wedge\beta_n\to\alpha)$ также является теоремой логики $\mathrm{QHC}$. Далее, так как $?\beta_1,\dots,?\beta_n\in\,?\Gamma$, имеем Кроме того, из того, что $?(\beta_1\wedge\dots\wedge\beta_n\to\alpha)$ – теорема логики $\mathrm{QHC}$, получаем
$$
\begin{equation*}
?\Gamma\vdash\,?\beta_1\wedge\dots\wedge\,?\beta_n\to\,?\alpha
\end{equation*}
\notag
$$
(здесь была применена аксиома $?(\beta\to\gamma)\to(?\beta\to\,?\gamma)$, а также теорема $\mathrm{QHC}$ $?(\beta\wedge\gamma)\leftrightarrow(?\beta\wedge\,?\gamma)$, доказанная в [1]). Наконец, применив modus ponens, получаем $?\Gamma\vdash\,?\alpha$. Доказательство п. 2) аналогично: в логике $\mathrm{QHC}$ имеется аксиома $!(p\to q)\to(!p\to\,!q)$, а $!(p\wedge q)\leftrightarrow(!p\wedge\,!q)$ является теоремой логики $\mathrm{QHC}$. Лемма доказана. Отметим, что имеет место консервативность: при слабом выводе формулы сорта задача можно оставить среди гипотез только формулы сорта задача; при слабом выводе формулы сорта высказывание можно оставить среди гипотез только формулы сорта высказывание. Определение 5. Для множества формул $\Gamma$ обозначим через $\Gamma^C$ множество формул сорта высказывание из $\Gamma$, а через $\Gamma^H$ – множество формул сорта задача из $\Gamma$. Лемма 3. Справедливы следующие равносильности: 1) $\Gamma\vdash\alpha\Leftrightarrow\Gamma^H\vdash\alpha$; 2) $\Gamma\vdash p\Leftrightarrow\Gamma^C\vdash p$. В обоих пунктах следование справа налево очевидно, а доказательство следования слева направо проводится несложной индукцией по построению вывода. Также отметим связь между отношениями $\vdash$ и $\vdash^*$. Лемма 4. Справедливы следующие равносильности: 1) $\Gamma\vdash^*\alpha\Leftrightarrow \Gamma^H,!\Gamma^C\vdash\alpha$; 2) $\Gamma\vdash^*p\Leftrightarrow\,?\Gamma^H,?!\Gamma^C\vdash p$. Доказательство. Следование справа налево в 1) и 2) очевидно: гипотезы правой части получаются по правилам усиления из гипотез левой. Следование слева направо для 1) и 2) докажем совместной индукцией по построению выводов. Ясно, что достаточно рассмотреть шаг индукции с применением правил усиления. 1) Пусть $\alpha$ получена по правилу усиления $\cfrac{p}{!p}$, тогда $\alpha=\,!p$. Значит, $\Gamma\vdash p$. По предположению индукции для п. 2) леммы 3 имеем $?\Gamma^H,?!\Gamma^C\vdash p$. Тогда $!?\Gamma^H,!?!\Gamma^C\vdash \,!p$ по лемме 2. Так как в логике $\mathrm{QHC}$ имеет место равносильность $!?!q\leftrightarrow \,!q$, получаем 2) Пусть $p$ получена по правилу усиления $\cfrac{\alpha}{?\alpha}$, тогда $p=\,?\alpha$. Значит, $\Gamma\vdash\alpha$. По предположению индукции для п. 1) леммы 3 имеем $\Gamma^H,!\Gamma^C\vdash\alpha$. Тогда $?\Gamma^H,?!\Gamma^C\vdash\,?\alpha$ по лемме 2, что и требовалось. Лемма доказана. Лемма 5. Пусть $\Gamma$ – некоторое множество формул. 1) Если $\Gamma\nvdash\alpha$ для некоторой формулы $\alpha$ сорта задача, то $\Gamma\nvdash \bot$. 2) Если $\Gamma\nvdash p$ для некоторой формулы $p$ сорта высказывание, то $\Gamma\nvdash 0$. Справедливость леммы следует из того, что формулы $\bot\to\alpha$, $0\to p$ являются теоремами $\mathrm{QHC}$: $\bot\to\alpha$ – интуиционистская тавтология для любой формулы $\alpha$ сорта задача, $0\to p$ – классическая тавтология для любой формулы $p$ сорта высказывание. Определение 6. Множество замкнутых формул $\Gamma$ некоторого языка будем называть теорией в логике $\mathrm{QHC}$, если оно содержит все теоремы логики $\mathrm{QHC}$, замкнуто относительно слабой выводимости (если $\Gamma\vdash\Phi$, то $\Phi\in\Gamma$) и $?\Gamma^H\subseteq\Gamma^C$. Теория непротиворечива, если она не содержит констант $0$ и $\bot$. Замыканием $[\Gamma]$ множества замкнутых формул $\Gamma$ будем называть наименьшую по включению теорию, содержащую это множество. Замечание 1. Пусть имеется некоторое множество $\Gamma$, состоящее из формул логики $\mathrm{QHC}$. Отметим, что для получения его замыкания $[\Gamma]$ необходимо проделать следующие действия: 1) добавить к $\Gamma$ все теоремы логики $\mathrm{QHC}$, получив множество $\Gamma_1$; 2) замкнуть $\Gamma_1$ относительно интуиционистских правил Бернайса и modus ponens, получив множество $\Gamma_2$; 3) рассмотреть множество $\Gamma_3=\,?\Gamma_2^H\cup\Gamma_2$ и замкнуть его относительно классических правил Бернайса и modus ponens. Ясно, что получившееся в результате множество является наименьшей по включению теорией, содержащей $\Gamma$. Лемма 6. Пусть $\Gamma$ – теория в логике $\mathrm{QHC}$. Тогда если $\Gamma\nvdash0$, то $\Gamma\nvdash \bot$. Доказательство. Предположим, что $\Gamma\vdash\bot$. Значит, $\bot\in\Gamma$. В силу того, что $?\Gamma^H\subseteq\Gamma^C$, получаем $\Gamma\vdash\,?\bot$. Кроме того, $?\bot\to0$ – теорема $\mathrm{QHC}$ (см., например, [1]). Далее по modus ponens получаем $\Gamma\vdash0$. Лемма доказана. Из леммы 6 следует, что для непротиворечивости теории достаточно потребовать только отсутствие константы 0 среди теорем данной теории. Лемма 7. Пусть $\Gamma$ – некоторое множество формул, $p$ – формула сорта высказывание, $\beta$ – формула сорта задача. Тогда: 1) $\beta\in[\Gamma]\Leftrightarrow\Gamma\vdash\beta$; 2) $p\in[\Gamma]\Leftrightarrow\,?\Gamma^H\cup\Gamma^C\vdash p$. Доказательство. В обоих пунктах импликация справа налево очевидна. Докажем, что имеет место следование слева направо.
1) Пусть $\beta\in[\Gamma]$. Согласно замечанию 1 это означает, что либо $\beta$ является теоремой логики $\mathrm{QHC}$, либо имеется слабый вывод формулы $\beta$ из $\Gamma$. В обоих случаях, пользуясь леммой 3, получаем $\Gamma\vdash\beta$. 2) Пусть $p\in[\Gamma]$. Рассмотрим множество $\Gamma_1$, которое получается из $\Gamma$ добавлением всех теорем логики $\mathrm{QHC}$, и множество $\Gamma_2$, которое получается из $\Gamma_1$ замыканием относительно интуиционистских правил Бернайса и modus ponens. Согласно замечанию 1 получаем, что либо $p$ является теоремой логики $\mathrm{QHC}$, либо имеется слабый вывод формулы $p$ из $?\Gamma_2^H\cup\Gamma_2$. В обоих случаях, пользуясь леммой 3, получаем $?\Gamma_2^H\cup\Gamma_2^C\vdash p$. Поскольку $\Gamma^H\vdash\Gamma_2^H$ и $\Gamma^C\vdash\Gamma_2^C$, окончательно получаем Лемма доказана. § 5. Полнота логики $\mathrm{QHC}$ относительно моделей Крипке с отмеченными мирамиВ доказательстве теоремы о полноте мы будем следовать общей канве работы [32], пользуясь идеями из [4]. Пусть имеется язык $L_M$, содержащий счетное множество константных символов $M$. Определение 7. Множество формул $\Gamma$ языка $L_M$ называется $M$-насыщенным, если: 1) $\Gamma$ – непротиворечивая теория (в логике $\mathrm{QHC}$); 2) $\Gamma$ обладает свойством дизъюнктивности: если $A\vee B\in\Gamma$, то $A\in\Gamma$ или $B\in\Gamma$ (здесь $A$ и $B$ – формулы одного сорта); 3) $\Gamma$ обладает свойством экзистенциальности: если $\exists\, v \ A(v)\in\Gamma$, то $A(c)\,{\in}\,\Gamma$ для некоторой константы $c\in M$. Замечание 2. 1) Если $\Gamma$ – теория, то $\Gamma\vdash \varphi$ равносильно $\varphi\in\Gamma$. 2) Если теория $\Gamma$ является $M$-насыщенной, то ее классический фрагмент $\Gamma^{C}$ является полной теорией по отношению к формулам сорта высказывание: для любой формулы $p$ сорта высказывание либо $p\in\Gamma$, либо $\neg p\in\Gamma$ (но не оба варианта сразу в силу $0\notin\Gamma$). Это следует из того, что $p\vee\neg p$ – теорема $\mathrm{QHC}$, а $\Gamma$ обладает свойством дизъюнктивности. Лемма 8. Пусть $M$ – не более чем счетное множество констант, $M'$ – его расширение счетным множеством дополнительных констант $\{c_1,c_2,\dots\}$. Пусть $\Gamma$ – теория в логике $\mathrm{QHC}$, $p$ – формула языка $L_M$ сорта высказывание и $\Gamma\nvdash p$. Тогда существует $M'$-насыщенная теория $\Gamma'$ языка $L_{M'}$ такая, что $\Gamma\subseteq\Gamma'$ и $p\notin\Gamma'$. Доказательство. Приведем набросок доказательства. Аналогичное утверждение для интуиционистского исчисления предикатов доказано в [32]. Рассматривается последовательность всех экзистенциальных формул языка $L_{M'}$
$$
\begin{equation*}
\exists\, v_0\ \Psi_0(v_0), \quad \exists\, v_1\ \Psi_1(v_1), \quad \exists\, v_2\ \Psi_2(v_2), \quad\dots
\end{equation*}
\notag
$$
и последовательность всех дизъюнктивных формул языка $L_{M'}$
$$
\begin{equation*}
\Psi_0\vee\Psi'_0, \ \Psi_1\vee\Psi'_1, \ \Psi_2\vee\Psi'_2, \ \dots\,.
\end{equation*}
\notag
$$
Определим множество формул $\Gamma_n$ для каждого $n$ следующим образом. Множество $\Gamma_0$ совпадает с множеством $\Gamma$. Далее, для каждого четного $n$ в последовательности экзистенциальных формул найдем первую еще не рассмотренную формулу $\exists\, v\ \Psi(v)$ такую, что $\Gamma_n\vdash\exists\, v\ \Psi(v)$. Пусть $c$ – константа, которая не встречается в формулах из $\Gamma_n$ и формуле $\exists\, v\ \Psi(v)$. Положим $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi(c)\}$. Для каждого нечетного $n$ в последовательности дизъюнктивных формул найдем первую еще не рассмотренную формулу $\Psi\vee\Psi'$ такую, что $\Gamma_n\vdash\Psi\vee\Psi'$. Если $\Gamma_n\cup\{\Psi\}\nvdash p$, то положим $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi\}$. В противном случае положим $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi'\}$. Наконец, пусть $\Gamma_{n+1}=[\widetilde\Gamma_{n+1}]$. Положим $\Gamma'=\bigcup_{n=0}^{\infty}\Gamma_n$ и покажем, что $\Gamma'\nvdash p$. Достаточно доказать, что $\Gamma_n\nvdash p$ для любого $n$. Рассуждаем индукцией по $n$. Действительно, для $n=0$ это следует из условия леммы. Теперь пусть для некоторого $n$ имеет место $\Gamma_n\nvdash p$. Докажем, что $\Gamma_{n+1}\nvdash p$. Предположим противное: пусть $\Gamma_{n+1}\vdash p$. Поскольку $\Gamma_{n+1}$ – теория, это означает, что $p\in\Gamma_{n+1}$. В силу леммы 7 имеем
$$
\begin{equation*}
?\widetilde\Gamma^H_{n+1}\cup\widetilde\Gamma^C_{n+1}\vdash p.
\end{equation*}
\notag
$$
Рассмотрим два случая. Пусть $n$ четно. Тогда $\widetilde\Gamma_{n+1}=\Gamma_n\cup\{\Psi(c)\}$, причем $\Gamma_n\vdash\exists\, v\ \Psi(v)$, а константа $c$ не встречается в $\exists\, v\ \Psi(v)$ и формулах из $\Gamma_n$. Пусть $\Psi(c)$ имеет сорт высказывание. Тогда в силу $\widetilde\Gamma^C_{n+1}=\{\Psi(c)\}\cup\Gamma^C_n$ и $\widetilde\Gamma^H_{n+1}=\Gamma^H_{n}$, применяя теорему о дедукции 1, получаем Поскольку $\Gamma_n$ – теория, то $?\Gamma^H_n\subseteq\Gamma_n$, и получаем Заменим в этом выводе каждое вхождение константы $c$ на переменную $u$, которая не встречается ни в одной из формул данного вывода. Несложно показать, что тогда получим $\Gamma_n\vdash\Psi(u)\to p$. Применяя правило Бернайса, имеем $\Gamma_n\vdash\exists\, v\ \Psi(v)\to p$, а так как $\Gamma_n\vdash\exists\, v\ \Psi(v)$, получаем $\Gamma_n\vdash p$, что противоречит предположению $\Gamma_n\nvdash p$.Пусть $\Psi(c)$ имеет сорт задача. Поскольку $\widetilde\Gamma^C_{n+1}=\Gamma^C_n$ и $?\widetilde\Gamma^H_{n+1}=\,?\Gamma^H_n\cup\{?\Psi(c)\}$, то, применяя теорему о дедукции 1, получаем Поскольку $\Gamma_n$ – теория, то $?\Gamma^H_n\subseteq\Gamma_n$, и получаем Заменим в этом выводе каждое вхождение константы $c$ на переменную $u$, которая не встречается ни в одной из формул данного вывода. Получим ${\Gamma_n\vdash\,?\Psi(u)\to p}$. Применяя правило Бернайса, имеем $\Gamma_n\vdash\exists\, v\ ?\Psi(v)\to p$. Поскольку $?\exists\, x\ \alpha(x)\leftrightarrow\exists\, x\ ?\alpha(x)$ – теорема логики $\mathrm{QHC}$ (доказана в [1]), имеем Так как $\Gamma_n\vdash\exists\, v\ \Psi(v)$ и так как $\Gamma_n$ – теория, получаем и далее получаем $\Gamma_n\vdash p$, что противоречит предположению $\Gamma_n\nvdash p$.Пусть $n$ нечетно. Тогда $\Gamma_n\vdash\Psi\vee\Psi'$. Обозначим
$$
\begin{equation*}
\Delta=[\Gamma_n\cup\{\Psi\}], \qquad \Delta'=[\Gamma_n\cup\{\Psi'\}].
\end{equation*}
\notag
$$
Ясно, что достаточно показать, что из $\Delta\vdash p$ и $\Delta'\vdash p$ следует $\Gamma_n\cup\{\Psi\vee\Psi'\}\vdash p$, и так как $\Gamma_n\vdash\Psi\vee\Psi'$, получаем противоречие с $\Gamma_n\nvdash p$. Разберем наиболее трудный случай: $\Psi\vee\Psi'$ имеет сорт задача. Тогда по лемме 7 имеем
$$
\begin{equation*}
?\Gamma^H_n\cup\Gamma^C_n\cup\{?\Psi\}\vdash p, \qquad ?\Gamma^H_n\cup\Gamma^C_n\cup\{?\Psi'\}\vdash p.
\end{equation*}
\notag
$$
По теореме о дедукции 1 получаем
$$
\begin{equation*}
?\Gamma^H_n\cup\Gamma^C_n\vdash\,?\Psi\to p, \qquad ?\Gamma^H_n\cup\Gamma^C_n\vdash\,?\Psi'\to p.
\end{equation*}
\notag
$$
Поскольку $\Gamma_n$ – теория, то $?\Gamma^H_n\subseteq\Gamma_n$, и получаем $\Gamma_n\vdash\,?\Psi\to p$ и $\Gamma_n\vdash\,?\Psi'\to p$. В силу того, что $(q_1\to r)\to((q_2\to r)\to(q_1\vee q_2\to r))$ – аксиома логики $\mathrm{QHC}$, имеем Далее, $?(\alpha\vee\beta)\leftrightarrow(?\alpha\,\vee\,?\beta)$ – теорема $\mathrm{QHC}$ (доказана в [1]), и мы получаем Так как $\Gamma_n\vdash\Psi\vee\Psi'$ и $\Gamma_n$ – теория, получаем $\Gamma_n\vdash\,?(\Psi\vee\Psi')$, откуда получаем $\Gamma_n\vdash p$, что противоречит предположению $\Gamma_n\nvdash p$. Итак, было показано, что $\Gamma'\nvdash p$. Ясно, что $\Gamma'$ содержит все теоремы логики $\mathrm{QHC}$. Доказательство замкнутости $\Gamma'$ относительно слабой выводимости, дизъюнктивного и экзистенциального свойств $\Gamma'$ проводится аналогично доказательству подобной теоремы из [32]. Покажем, что $?\Gamma'^H\subseteq\Gamma'^C$. Действительно, если $\alpha\in\Gamma'^H$, то для некоторого $n$ $\alpha\in\Gamma^H_n$, и так как $\Gamma_n$ – теория, получаем $?\alpha\in\Gamma^C_n$, т.е. $?\alpha\in\Gamma'$. Таким образом, $\Gamma'$ – теория. Наконец, это непротиворечивая теория в силу леммы 5 (напомним, что для непротиворечивости теории достаточно проверить, что $\Gamma'\nvdash0$). Лемма 8 доказана. Определение 8. $M$-насыщенная теория $\Gamma$ рефлексивна, если $\Gamma_{?}\subseteq\Gamma$, где $\Gamma_{?}=\{\alpha\mid\,?\alpha\in\Gamma\}$. Лемма 9. Пусть $\Gamma$ – некоторая теория, $\Gamma\nvdash p$ и $\Delta=[\Gamma_?\cup\Gamma]$. Тогда $\Delta\nvdash p$. Доказательство. Доказываем от противного: пусть $\Delta\vdash p$. По лемме 7 имеем Поскольку $?\Gamma_?\subseteq\Gamma^C$, имеем $?\Gamma^H,\Gamma^C,\Gamma_?\vdash p$. Так как $\Gamma$ – теория, то $?\Gamma^H\subseteq\Gamma^C$ и $\Gamma^C,\Gamma_?\vdash p$. Поскольку $\Gamma_?$ – множество формул сорта задача, по лемме 3 имеем $\Gamma^C\vdash p$, откуда приходим к противоречию с $\Gamma\nvdash p$. Лемма доказана. Лемма 10. Пусть $M$ – не более чем счетное множество констант, $M'$ – его расширение счетным множеством дополнительных констант $\{c_1,c_2,\dots\}$. Тогда для любой $M$-насыщенной теории $\Gamma$, если $\Gamma\nvdash p$, то существует рефлексивная $M'$-насыщенная теория $\Delta$ такая, что $\Gamma\subseteq\Delta$ и $\Delta\nvdash p$. Доказательство. Пусть $M=M_0\subseteq M_1\subseteq M_2\subseteq\dots\subseteq M'$, где $M_{i+1}$ – расширение $M_i$ счетным числом констант и $M'=\bigcup_{i=0}^{\infty}M_i$. Определим последовательность теорий $\Gamma^0,\Gamma^1,\Gamma^2,\dots$, где $\Gamma^i$ – $M_i$-насыщенная теория, следующим образом. Пусть $\Gamma_0=\Gamma$. Для $n\geqslant0$ пусть
$$
\begin{equation*}
\Gamma^{n+1}\text{ - такая }M_{n+1}\text{-насыщенная теория, что } \Gamma'_n=\Gamma^n_{?}\cup\Gamma^n\subseteq\Gamma^{n+1}\text{ и }\Gamma^{n+1}\nvdash p.
\end{equation*}
\notag
$$
(Это возможно, так как из $\Gamma^n\nvdash p$ следует $\Gamma'_n\nvdash p$ по лемме 9. Далее расширим $\Gamma'_n$ до $M_{n+1}$-насыщенной теории $\Gamma_{n+1}$, пользуясь леммой 8.) Положим Ясно, что $\Delta$ – теория. Покажем, что $\Delta$ обладает свойством дизъюнктивности. Пусть $\psi_1\vee\psi_2\in\Delta$. Тогда $\psi_1\vee\psi_2\in\Gamma^n$ для некоторого $n\geqslant0$. Поскольку $\Gamma^n$ обладает свойством дизъюнктивности, то либо $\psi_1\in\Gamma^n$, либо $\psi_2\in\Gamma^n$. Отсюда получаем $\psi_1\in\Delta$ или $\psi_2\in\Delta$. Покажем, что $\Delta$ обладает свойством экзистенциальности. Пусть $\exists\, v\ \psi(v)\,{\in}\,\Delta$. Тогда $\exists\, v\ \psi(v)\in\Gamma^n$ для некоторого $n\geqslant0$. Поскольку $\Gamma^n$ обладает свойством экзистенциальности, то $\psi(c)\in\Gamma^n$ для некоторой константы $c\in M_n\subseteq M'$. Отсюда получаем $\psi(c)\in\Delta$. Покажем, что $\Delta$ рефлексивна, т.е. $\Delta_{?}\subseteq\Delta$. Действительно, пусть $\alpha\in\Delta_{?}$. Тогда $?\alpha\in\Delta$, т.е. $?\alpha\in\Gamma^n$ для некоторого $n$. Следовательно, $\alpha\in\Gamma^n_{?}$ и $\alpha\in\Gamma^{n+1}$, т.е. $\alpha\in\Delta$. Осталось показать, что $\Delta\nvdash p$. Действительно, в противном случае $p\in\Gamma^n$ для некоторого $n$; противоречие. Отсюда заключаем, что $\Delta\nvdash p$. Лемма доказана. Лемма 11. Пусть $M$ – не более чем счетное множество констант, $M'$ – его расширение счетным множеством дополнительных констант $\{c_1,c_2,\dots\}$. Тогда для любой теории $\Gamma$ и формулы $p$ в языке $L_M$, если $\Gamma\nvdash\,!p$, то существует рефлексивная $M'$-насыщенная теория $\Delta$ такая, что $\Gamma^H\subseteq\Delta$ и $p\notin\Delta$. Доказательство. Рассмотрим множество формул $\Gamma'=\Gamma^H\cup\,?\Gamma^H$. Покажем, что $\Gamma'\nvdash p$. Действительно, предположим противное: $\Gamma'\vdash p$. Тогда по лемме 3 получаем, что $?\Gamma^H\vdash p$. Отсюда по лемме 2 имеем $!?\Gamma^H\vdash\, !p$. Поскольку $\alpha\to\,!?\alpha$ – аксиома логики $\mathrm{QHC}$, имеем $\Gamma^H\vdash\,!?\Gamma^H$, и в конечном итоге получаем $\Gamma^H\vdash\,!p$, что противоречит условию $\Gamma\nvdash\,!p$. Следовательно, $\Gamma'\nvdash p$. Отсюда по лемме 10 найдется рефлексивная $M'$-насыщенная теория $\Delta$, содержащая $\Gamma'$ (а значит, и $\Gamma^H$), такая, что $p\notin\Delta$, что и требовалось. Лемма доказана. Теорема 3. Если $M$-насыщенная теория $\Gamma$ языка $L_M$ является рефлексивной, то существуют модель Крипке $\mathcal K=(W,\preccurlyeq,\mathrm{Aud},D,\models)$ с отмеченными мирами и ее отмеченный мир $x$ такие, что для любой формулы $\alpha$ сорта задача языка $L_M$ выполнено а для любой формулы $p$ сорта высказывание языка $L_M$ выполнено Доказательство. Построим модель Крипке с отмеченными мирами $\mathcal K$ следующим образом. Определим последовательность множеств констант $M_0, M_1, M_2, \dots$ индуктивно: $M_0=M$, а $M_{i+1}$ получается добавлением к $M_i$ счетного множества новых констант. Пусть $W$ – семейство всех теорий $\Delta$ таких, что: 1) $\Delta$ состоит из замкнутых формул некоторого языка $L_{M_i}$; 2) $\Delta$ является $M_i$-насыщенной; 3) $\Gamma^H\subseteq\Delta$. Для $\Delta_1,\Delta_2\in W$ положим $\Delta_1\preccurlyeq\Delta_2\rightleftharpoons\Delta_1^H\subseteq\Delta_2^H$; $\Delta\in\mathrm{Aud}$ тогда и только тогда, когда $\Delta$ рефлексивна. Далее, пусть $\Delta\in W$ является $M_i$-насыщенной теорией. Тогда полагаем $D_{\Delta}=M_i$, и если $A(c_1,\dots,c_n)$ – атомарная формула с константами $c_1,\dots,c_n\in M_i$, то положим
$$
\begin{equation*}
\Delta\models A(c_1,\dots,c_n)\rightleftharpoons A(c_1,\dots,c_n)\in\Delta.
\end{equation*}
\notag
$$
Проверим, что мы действительно получили модель Крипке с отмеченными мирами. Ясно, что $\preccurlyeq$ – частичный порядок на $W$ и что $\mathrm{Aud}\subseteq W$. Далее,
$$
\begin{equation*}
\forall\,\Delta_1\in W\ \exists\,\Delta_2\in W\ (\Delta_1\preccurlyeq\Delta_2\wedge\Delta_2\in\mathrm{Aud})
\end{equation*}
\notag
$$
выполнено в силу леммы 10 (в качестве $p$ можно взять, например, $0$). Кроме того, для атомов сорта задача выполнена монотонность отношения истинности $\models$ (так как $\Delta_1\preccurlyeq\Delta_2\Leftrightarrow\Delta_1^H\subseteq\Delta_2^H$). Наконец, из построения следует, что
$$
\begin{equation*}
\Delta_1\preccurlyeq\Delta_2\Rightarrow D_{\Delta_1}\subseteq D_{\Delta_2}.
\end{equation*}
\notag
$$
Таким образом, построена модель Крипке с отмеченными мирами $\mathcal K= {(W,\preccurlyeq, \mathrm{Aud},D,\models)}$. Докажем, что для любого $\Delta\in W$ выполнено следующее: если $\Delta$ является $M_i$-насыщенным, то для любой замкнутой формулы $A$ языка $L_{M_i}$ (при этом если $A$ – формула сорта высказывание, то рассматриваем данную равносильность только для $\Delta\in\mathrm{Aud}$). Тогда утверждение теоремы будет немедленно получено, если положить $x=\Gamma$.Доказательство проводится индукцией по построению формулы $A$. Для атомарных формул это выполнено по определению $\models$. Доказательство случая индуктивного перехода с использованием интуиционистских связок и кванторов проводится методом, изложенным в [32] для интуиционистского исчисления предикатов. Приведем данное рассуждение в самом трудном случае – в случае индуктивного перехода для кванторов. Пусть дана формула $\alpha(x)$ с единственной свободной переменной $x$. Тогда в силу того, что $\alpha(c)$ – замкнутая формула для любой константы $c$, имеем следующую цепочку равносильностей:
$$
\begin{equation*}
\Delta\models\exists\, x\ \alpha(x)\Leftrightarrow\exists\, c\in D_{\Delta} \ (\Delta\models\alpha(c))\Leftrightarrow\exists\, c\in D_{\Delta}\ (\alpha(c)\in\Delta)\Leftrightarrow \exists\, x\ \alpha(x)\in\Delta.
\end{equation*}
\notag
$$
Последний равносильный переход слева направо имеет место в силу того, что $\Delta$ замкнута относительно слабой выводимости, а справа налево – в силу того, что $\Delta$ обладает свойством экзистенциальности. Рассмотрим следующую цепочку равносильностей для квантора всеобщности:
$$
\begin{equation*}
\begin{aligned} \, &\Delta\models\forall\, x\ \alpha(x)\Leftrightarrow\forall\,\Delta'\succcurlyeq\Delta\ \forall\, c\in D_{\Delta'}\ (\Delta'\models\alpha(c)) \\ &\qquad \Leftrightarrow \forall\,\Delta'\succcurlyeq\Delta\ \forall\, c\in D_{\Delta'} \ (\alpha(c)\in\Delta')\Leftrightarrow\forall\, x\ \alpha(x)\in\Delta. \end{aligned}
\end{equation*}
\notag
$$
В обосновании нуждается только последний равносильный переход. Действительно, импликация справа налево выполнена в силу замкнутости $\Delta$ относительно слабой выводимости. Докажем импликацию слева направо. Пусть
$$
\begin{equation*}
\forall\,\Delta'\succcurlyeq\Delta\ \forall\, c\in D_{\Delta'} \ (\alpha(c)\in\Delta'),
\end{equation*}
\notag
$$
но при этом условие $\forall\, x\ \alpha(x)\in\Delta$ не выполнено. Следовательно, $\Delta\nvdash\forall\, x\ \alpha(x)$. Тогда $\Delta\nvdash\alpha(c)$ для любой константы $c\notin D_{\Delta}$. Действительно, в противном случае, заменив все вхождения константы $c$ на переменную $u$, не встречающуюся в этом выводе, получим вывод из $\Delta$ формулы $\alpha(u)$, после чего получим $\Delta\vdash\forall\, u\ \alpha(u)$, что противоречит предположению $\Delta\nvdash\forall\, x\ \alpha(x)$. Пусть $\Delta$ – $M_i$-насыщенная теория, тогда для $c\in M_{i+1}\setminus M_i$ имеем $\Delta\nvdash\alpha(c)$. В силу леммы 8 существует $M_{i+2}$-насыщенная теория $\Delta'$ такая, что $\Delta\preccurlyeq\Delta'$ и $\alpha(c)\notin\Delta'$, что противоречит изначальному предположению. Доказательство случаев индуктивного перехода с использованием классических связок и кванторов проводится еще более простым рассуждением (или можно определить “порядок” на отмеченных мирах как $\Delta^1\preccurlyeq_{\text{клас.}}\Delta^2$, если $\Delta^1=\Delta^2$, а затем просто повторить доказательство в интуиционистском случае). Осталось доказать случаи индуктивного перехода с применением модальностей. Пусть $?\alpha\in\Delta$ (при этом $\Delta\in\mathrm{Aud}$, так как $?\alpha$ имеет сорт высказывание). Так как $\Delta$ – рефлексивная теория, $\alpha\in\Delta$. По предположению индукции $\Delta\models\alpha$. Отсюда получаем $\Delta\models\,?\alpha$ по определению $\models$. Пусть $\Delta\models\,?\alpha$. Тогда $\Delta\models\alpha$ по определению $\models$. По предположению индукции $\alpha\in\Delta$. Отсюда $?\alpha\in\Delta$ в силу того, что $\Delta$ – теория. Пусть $!p\in\Delta$. Необходимо доказать, что $\Delta\models\,!p$, т.е.
$$
\begin{equation*}
\forall\,\Delta'\in\mathrm{Aud}\ (\Delta\preccurlyeq\Delta'\Rightarrow\Delta'\models p).
\end{equation*}
\notag
$$
Рассмотрим произвольное $\Delta'\in\mathrm{Aud}$, $\Delta'\succcurlyeq\Delta$. Поскольку $!p\in\Delta$, имеем $!p\in\Delta'$ ($!p$ имеет сорт задача). Так как $\Delta'$ – теория, то $?!p\in\Delta'$. Так как $?!p\,{\to}\, p$ – теорема $\mathrm{QHC}$, то $p\in\Delta'$. По предположению индукции это означает, что $\Delta'\models p$. Отсюда получаем $\Delta\models\,!p$. Пусть $!p\notin\Delta$. Если $\Delta$ является $M_i$-насыщенной теорией, то по лемме 11 найдется рефлексивная $M_{i+1}$-насыщенная теория $\Delta'$ такая, что $\Delta^H\subseteq\Delta'$ и $p\notin\Delta'$. Таким образом, мы нашли рефлексивную теорию $\Delta'\succcurlyeq\Delta$ такую, что $\Delta'\nvDash p$. Это означает, что $\Delta\nvDash\,!p$. Теорема 3 доказана. Теорема 4. Для любой непротиворечивой теории $\Gamma$ логики $\mathrm{QHC}$ существуют модель Крипке $\mathcal K$ и ее отмеченный мир $x$ такие, что в этом мире данной модели $\mathcal K$ истинны все формулы из $\Gamma$. Доказательство. Пусть $\Gamma$ – непротиворечивая теория логики $\mathrm{QHC}$ в сигнатуре $\Omega$. Тогда $\Gamma\nvdash0$. В силу леммы 8 существует $M$-насыщенное множество формул $\Gamma'$ сигнатуры $\Omega'$, полученной добавлением к $\Omega$ счетного множества дополнительных констант, такое, что $\Gamma\subseteq\Gamma'$. В силу леммы 10 существует рефлексивное $M'$-насыщенное множество формул $\Gamma''$ сигнатуры $\Omega''$, полученной добавлением к $\Omega'$ счетного множества дополнительных констант, такое, что $\Gamma'\subseteq\Gamma''$. По теореме 3 существует модель Крипке с отмеченными мирами $\mathcal K$, в одном из миров которой истинны все формулы множества $\Gamma''$. Так как $\Gamma\subseteq\Gamma''$, то $\mathcal K$ – модель Крипке для множества $\Gamma$. Теорема доказана. Из этой теоремы получаем такое следствие. Теорема 5 (о полноте $\mathrm{QHC}$ относительно моделей Крипке с отмеченными мирами). Если формула $A$ сорта задача (сорта высказывание) языка $\Omega$ истинна в любом мире (отмеченном мире) любой модели Крипке с отмеченными мирами для языка $\Omega$, то $A$ выводима в $\mathrm{QHC}$. § 6. Модели логики $\mathrm{QH4}$ и консервативностьЛогика $\mathrm{QH4}$ – предикатный вариант пропозициональной модальной логики $\mathrm{H4}$. Логика $\mathrm{H4}$ рассматривалась С. Н. Артёмовым и Т. Протопопеску в [4] как эпистемическая интуиционистская логика с модальностью знания $\mathbf K$ и обозначалась в этой работе как $\mathrm{IEL}^+$. В этой же работе были построены модели логики $\mathrm{H4}$ с отмеченными мирами, доказана теорема о корректности и полноте. В работе [3] было отмечено свойство конечных моделей для данного класса моделей логики $\mathrm{H4}$, а также доказано, что логика $\mathrm{HC}$ является консервативным расширением логики $\mathrm{H4}$. В работе [4], а также в ее журнальной версии [22] рассматривались логики $\mathrm{IEL}^-$ и $\mathrm{IEL}$ – более слабые системы, родственные логике $\mathrm{IEL}^+$. В работе Й. Су и К. Сано [33] изучена семантика типа Крипке предикатных вариантов логик $\mathrm{IEL}^-$ и $\mathrm{IEL}$ – логик $\mathrm{QIEL}^-$ и $\mathrm{QIEL}$. В этой работе была доказана теорема о полноте обеих логик $\mathrm{QIEL}^-$ и $\mathrm{QIEL}$ относительно семантики Крипке. Метод работы [33] основывался на построении исчисления секвенций для этих логик и рассмотрении множества насыщенных секвенций в качестве модели Крипке. Ниже приведено доказательство теоремы о полноте логики $\mathrm{QIEL}^+$ (или логики $\mathrm{QH4}$) иным способом, а именно рассмотрением интуиционистских насыщенных теорий. Это доказательство близко к доказательству теоремы о полноте пропозициональной логики $\mathrm{IEL}^+$ относительно семантики Крипке (см. [4]). Термами логики $\mathrm{QH4}$ являются индивидные переменные и константы. Язык логики $\mathrm{QH4}$ содержит интуиционистские связки $\wedge,\vee,\to,\leftrightarrow,\neg$, кванторы $\forall$, $\exists$ и модальность $\nabla$, а также предикатные символы только одного сорта (в отличие от логики $\mathrm{QHC}$). Стандартным образом определяется понятие формулы логики $\mathrm{QH4}$. Аксиомы и правила вывода логики $\mathrm{QH4}$ состоят из аксиом и правил вывода интуиционистского исчисления предикатов, а также следующих схем аксиом: $(1^{\nabla})$ $\alpha\to\nabla\alpha$; $(2^{\nabla})$ $\nabla\nabla\alpha\to\nabla\alpha$; $(3^{\nabla})$ $\nabla\bot\to\bot$; $(4^{\nabla})$ $\nabla(\alpha\to\beta)\to(\nabla\alpha\to\nabla\beta)$. Для логики $\mathrm{QH4}$ можно определить понятие вывода, квазивывода из гипотез и вывода из гипотез аналогичным образом, как это было сделано для логики $\mathrm{QHC}$. Опишем модели Крипке с отмеченными мирами логики $\mathrm{QH4}$. Пусть $\Omega$ – язык логики QH4 (без функциональных символов). Шкала Крипке с отмеченными мирами этого языка – набор $\mathcal K=(W,\preccurlyeq,\mathrm{Aud})$, где $(W,\preccurlyeq)$ – частично упорядоченное множество, $\mathrm{Aud}\subseteq W$ и выполнено свойство
$$
\begin{equation*}
\forall\, a\in W\ \exists\, b\in W\ (a\preccurlyeq b\wedge b\in\mathrm{Aud}).
\end{equation*}
\notag
$$
Модель Крипке логики $\mathrm{QH4}$ с отмеченными мирами – шкала Крипке с функцией $D$, которая каждому $a\in W$ сопоставляет непустое множество $D_a$, а также оценкой атомов $\models$. Предполагается, что если $a\preccurlyeq b$, то $D_a\subseteq D_b$. Если язык $\Omega$ содержит константу $c$, то ей сопоставляется объект $\overline c\in D_{a}$ для любого $a\in W$ (мы отождествляем $c$ и $\overline c$). Оценка атомов $\models$ – некоторое соответствие между множеством $W$ и множеством всех атомов вида $A(x_1,\dots,x_n)$, где $A$ есть $n$-местный предикатный символ сигнатуры $\Omega$, а $x_1,\dots,x_n\in\bigcup_{a\in W}D_a$. Запись $a\models A(x_1,\dots,x_n)$ прочитывается стандартным образом: “$A(x_1,\dots,x_n)$ истинно в $a$”. Соответствие $\models$ обладает таким свойством: если $a\models A(x_1,\dots,x_n)$, то $\{x_1,\dots,x_n\}\subseteq D_a$, и если $A(x_1,\dots,x_n)$ – атомарная формула и $a\preccurlyeq b$, то $b\models A(x_1,\dots,x_n)$ (т.е. для атомов имеет место монотонность). Отношение истинности для остальных формул логики $\mathrm{QH4}$ определяется индукцией по построению формулы. Для связок $\wedge,\vee,\to,\leftrightarrow,\neg$ и кванторов $\forall$, $\exists$ индуктивный переход в определении отношения истинности осуществляется так же, как и в моделях Крипке интуиционистского исчисления предикатов. Определим отношение истинности в индуктивном переходе для модальности $\nabla$:
$$
\begin{equation*}
a\models\nabla\varphi\Leftrightarrow\forall\, b\in W\ (a\preccurlyeq b\wedge b\in\mathrm{Aud}\Rightarrow b\models\varphi).
\end{equation*}
\notag
$$
Аналогично лемме 1 можно показать, что монотонность имеет место не только для атомов, но и для любых формул. Теорема 6 (корректность). Если замкнутая формула языка $\Omega$ выводима в $\mathrm{QH4}$, то она истинна в любой модели Крипке логики $\mathrm{QH4}$ для языка $\Omega$. Для доказательства этой теоремы, как и в теореме 2, следует проверить, что если формула истинна в $\mathrm{QH4}$, то ее универсальное замыкание истинно в любой модели Крипке. Ясно, что достаточно проверить, что универсальное замыкание любой аксиомы истинно в любой модели Крипке и что правила вывода сохраняют это свойство. Для аксиом и правил вывода интуиционистского исчисления предикатов это уже проверено в теореме 2. Для дополнительных аксиом $\mathrm{QH4}$ доказательство имеется в [4] (ясно, что модели логики $\mathrm{QH4}$ являются обогащением моделей логики $\mathrm{H4}$). Как и раньше, рассматриваем $M$-насыщенные теории, но только не в логике $\mathrm{QHC}$, а в логике $\mathrm{QH4}$ (с тем отличием, что для $M$-насыщенных теорий в логике $\mathrm{QH4}$ отсутствует требование $?\Gamma^H\subseteq\Gamma^C$). Напомним: $\Gamma\vdash\varphi$ означает, что существует вывод $\varphi$ из гипотез $\Gamma$; $[\Gamma]$ означает наименьшую по включению теорию, содержащую $\Gamma$. Определение 9. $M$-насыщенная теория $\Gamma$ в логике $\mathrm{QH4}$ рефлексивна, если $\Gamma_{\nabla}\subseteq\Gamma$, где $\Gamma_{\nabla}=\{\varphi\mid\nabla\varphi\in\Gamma\}.$ Лемма 12. Пусть $M$ – не более чем счетное множество констант, $M'$ – его расширение счетным множеством дополнительных констант $\{c_1,c_2,\dots\}$. Тогда для любого множества формул $\Gamma$ и формулы $\beta$ в языке $L_M$ если $\Gamma\nvdash\nabla\beta$, то существует рефлексивная $M'$-насыщенная теория $\Delta$ такая, что $\Gamma\subseteq\Delta$ и $\Delta\nvdash\beta$. Доказательство. Доказательство данной леммы очень близко к доказательству леммы 10. Положим
$$
\begin{equation*}
M=M_0\subseteq M_1\subseteq M_2\subseteq\dots\subseteq M',
\end{equation*}
\notag
$$
где $M_{i+1}$ – расширение $M_i$ счетным числом констант и $M'=\bigcup_{i=0}^{\infty}M_i$. Далее отметим, что если $\Sigma\nvdash\nabla\varphi$, то $\Sigma_{\nabla}\nvdash\nabla\varphi$ (доказательство этого факта имеется в [4; лемма 5] и в [3; лемма 7]). Аналогично лемме 8, для любого множества формул $\Gamma$ и формулы $\alpha$ языка $M$ если $\Gamma\nvdash\alpha$, то существует такая $M'$-насыщенная теория $\Gamma'$, расширяющая $\Gamma$, что $\Gamma'\nvdash\alpha$ ($M'$ – расширение $M$ счетным множеством дополнительных констант). Определим последовательность теорий $\Gamma^0,\Gamma^1,\Gamma^2,\dots$ следующим образом. Пусть $\Gamma^0=[\Gamma]$ и
$$
\begin{equation*}
\Gamma^{n+1}\text{ - такая }M_{n+1}\text{-насыщенная теория, что } \Gamma^n_{\nabla}\subseteq\Gamma^{n+1}\text{ и }\Gamma^{n+1}\nvdash\beta.
\end{equation*}
\notag
$$
Таким образом, мы имеем следующую цепочку включений:
$$
\begin{equation*}
\Gamma^0\subseteq \Gamma^0_{\nabla}\subseteq\Gamma^1\subseteq \Gamma^1_{\nabla}\subseteq\Gamma^2\subseteq \Gamma^2_{\nabla}\subseteq\dotsb.
\end{equation*}
\notag
$$
Положим Докажем, что $\Delta$ обладает всеми необходимыми свойствами. В [3; лемма 7] имеется доказательство аналогичного утверждения, но для логики $\mathrm{H4}$, а не $\mathrm{QH4}$. Ясно, что подобными рассуждениями можно показать, что $\Delta$ – теория, $\Delta_{\nabla}\,{\subseteq}\,\Delta$, $\Delta\nvdash\beta$ и $\Delta$ обладает свойством дизъюнктивности. Осталось показать, что $\Delta$ обладает свойством экзистенциальности. Действительно, пусть $\exists\, v\ \varphi(v)\in\Delta$. Тогда $\exists\, v\ \varphi(v)\in\Gamma^n$ для некоторого $n>0$. Поскольку $\Gamma^n$ – $M_n$-насыщенная теория, то $\varphi(c)\in\Gamma^n$ для некоторой константы $c$. Отсюда получаем $\varphi(c)\in\Delta$. Лемма доказана. Теорема 7. Если множество формул $\Gamma$ языка $L_M$ является $M$-насыщенной теорией, то существует модель Крипке $\mathcal K=(W,\preccurlyeq,\mathrm{Aud},D,\models)$ с отмеченными мирами логики $\mathrm{QH4}$ такая, что для любой формулы $A$ языка $L_M$ выполнено Доказательство. Построим модель Крипке логики $\mathrm{QH4}$ следующим образом (как в теореме 3). Определим последовательность множеств констант $M_0,M_1,M_2,\dots$ индуктивно: $M_0=M$, а $M_{i+1}$ получается добавлением к $M_i$ счетного множества новых констант. Пусть $W$ – семейство всех теорий $\Delta$ таких, что: 1) $\Delta$ состоит из замкнутых формул некоторого языка $L_{M_i}$; 2) $\Delta$ является $M_i$-насыщенной; 3) $\Gamma\subseteq\Delta$. Для $\Delta_1,\Delta_2\in W$ положим $\Delta_1\preccurlyeq\Delta_2\rightleftharpoons\Delta_1\subseteq\Delta_2$; $\Delta\in\mathrm{Aud}$ тогда и только тогда, когда $\Delta$ рефлексивна. Далее, пусть $\Delta\in W$ является $M_i$-насыщенной теорией. Тогда полагаем $D_{\Delta}=M_i$, и если $A(c_1,\dots,c_n)$ – атомарная формула с константами $c_1,\dots,c_n\in M_i$, то положим
$$
\begin{equation*}
\Delta\models A(c_1,\dots,c_n)\rightleftharpoons A(c_1,\dots,c_n)\in\Delta.
\end{equation*}
\notag
$$
Проверим, что мы действительно получили модель Крипке логики $\mathrm{QH4}$. Ясно, что $\preccurlyeq$ – частичный порядок на $W$ и что $\mathrm{Aud}\subseteq W$. Покажем, что
$$
\begin{equation*}
\forall\,\Delta_1\in W\ \exists\,\Delta_2\in W\ (\Delta_1\preccurlyeq\Delta_2\wedge\Delta_2\in\mathrm{Aud}).
\end{equation*}
\notag
$$
Возьмем произвольное $\Delta_1\in W$. Пусть $\Delta_1$ – $M_i$-насыщенная теория. Так как $\Delta$ непротиворечива, то $\Delta\nvdash\nabla\bot$ и по лемме 12 найдется такая рефлексивная $M_{i+1}$-насыщенная теория $\Delta_2$, что $\Delta_1\subseteq\Delta_2$ и $\bot\notin\Delta_2$. Таким образом, найдена нужная теория $\Delta_2$. Кроме того, для атомов выполнена монотонность отношения истинности $\models$ (так как $\Delta_1\preccurlyeq\Delta_2\Leftrightarrow\Delta_1\subseteq\Delta_2$). Наконец, из построения следует, что
$$
\begin{equation*}
\Delta_1\preccurlyeq\Delta_2\Rightarrow D_{\Delta_1}\subseteq D_{\Delta_2}.
\end{equation*}
\notag
$$
Таким образом, построена модель Крипке с отмеченными мирами $\mathcal K= (W,\preccurlyeq,\mathrm{Aud},D,\models)$. Докажем, что для любого $\Delta\in W$ выполнено следующее: если $\Delta$ является $M_i$-насыщенным, то для любой формулы $A$ языка $L_{M_i}$ Доказательство проводится индукцией по построению формулы $A$. Для атомарных формул это выполнено по определению $\models$. Для связок и кванторов доказательство проводится методом, изложенным в [32] (случай индуктивного перехода с применением кванторов разобран нами в теореме 3). Осталось доказать случай индуктивного перехода с применением модальности $\nabla$. Пусть $\nabla\varphi\in\Delta$. Необходимо доказать, что $\Delta\models\nabla\varphi$, т.е. $\forall\,\Delta'\supseteq\Delta$ если $\Delta'$ рефлексивна, то $\Delta'\models\varphi$. Действительно, возьмем рефлексивную теорию $\Delta'\supseteq\Delta$. Так как $\nabla\varphi\in\Delta$, имеем $\nabla\varphi\in\Delta'$. Так как $\Delta'$ рефлексивна, имеем $\varphi\in\Delta'$. По предположению индукции $\Delta'\models\varphi$. Следовательно, $\Delta\models\nabla\varphi$. Пусть $\nabla\varphi\notin\Delta$. По лемме 12 существует рефлексивная теория $\Delta'\supseteq\Delta$ такая, что $\varphi\notin\Delta'$. По предположению индукции $\Delta'\nvDash\varphi$. Следовательно, $\Delta\nvDash\nabla\varphi$. Теорема доказана. Теорема 7 имеет два важных следствия. Теорема 8 (полнота $\mathrm{QH4}$). Для любого непротиворечивого множества формул $\Gamma$ логики $\mathrm{QH4}$ существует модель Крипке $\mathcal K$ логики $\mathrm{QH4}$ такая, что в любом мире модели $\mathcal K$ истинны все формулы из $\Gamma$. Доказательство проводится аналогично доказательству теоремы 4. Теорема 9 (консервативность). Логика $\mathrm{QHC}$ – консервативное расширение логики $\mathrm{QH4}$. Доказательство. Рассмотрим формулу $\varphi$, не выводимую в логике $\mathrm{QH4}$. Согласно теореме 8 найдется контрмодель Крипке $\mathcal K$ логики $\mathrm{QH4}$ для формулы $\varphi$. Пусть $\widetilde\varphi$ получена из формулы $\varphi$ заменой всех символов $\nabla$ на $!?$. Контрмодель Крипке логики $\mathrm{QHC}$ для формулы $\widetilde\varphi$ совпадает с $\mathcal K$, поскольку истинность формул в языке логики $\mathrm{QH4}$ согласованна в обеих моделях (см. доказательство теоремы 5 в [3] для пропозициональных вариантов этих логик; ясно, что для кванторов определение истинности также согласованно).
Теорема доказана. § 7. Дизъюнктивное и экзистенциальное свойстваИзложение этого параграфа во многом близко к [32]. Пусть $T$ – некоторая непротиворечивая теория в логике $\mathrm{QHC}$. Будем говорить, что теория $T$ обладает дизъюнктивным свойством, если из $\alpha\vee\beta\in T$ следует $\alpha\in T$ или $\beta\in T$ (здесь $\alpha,\beta$ – произвольные формулы сорта задача). Теория $T$ обладает экзистенциальным свойством, если из $\exists\, x\ \alpha(x)\in T$ следует, что существует такая константа $c$, что $\alpha(c)\in T$ (здесь $\alpha$ – произвольная формула сорта задача). Ясно, что имеет смысл говорить об экзистенциальности теории, если ее язык содержит хотя бы одну константу. Пусть имеются две модели Крипке с отмеченными мирами
$$
\begin{equation*}
\mathcal K_1=(W_1, \preccurlyeq_1, \mathrm{Aud}_1,D_1,\models_1), \qquad \mathcal K_2=(W_2,\preccurlyeq_2,\mathrm{Aud}_2,D_2,\models_2)
\end{equation*}
\notag
$$
логики $\mathrm{QHC}$, причем $W_1\cap W_2=\varnothing$. Их суммой называется такая модель $\mathcal K=(W,\preccurlyeq, \mathrm{Aud},D,\models)$, что:
Сумма моделей $\mathcal K_1$ и $\mathcal K_2$ обозначается как $\mathcal K_1+\mathcal K_2$. Ясно, что для любой формулы $A$ имеет место
$$
\begin{equation*}
(\mathcal K_1+\mathcal K_2)\models A\Leftrightarrow (\mathcal K_1\models_1 A\text{ и }\mathcal K_2\models_2 A).
\end{equation*}
\notag
$$
(Здесь $\mathcal K\models A$ означает, что формула $A$ сорта задача (сорта высказывание) истинна в любом мире (отмеченном мире) модели Крипке $\mathcal K$.) Отсюда следует, что сумма двух моделей теории также является моделью теории. Сумма $\sum_{i\in I}\mathcal K_i$ любого семейства моделей Крипке $\{\mathcal K_i\mid i\in I\}$ определяется аналогично. В этом случае если каждое $\mathcal K_i$ ($i\in I$) является моделью теории $T$, то сумма $\sum_{i\in I}\mathcal K_i$ также является моделью этой теории. Для модели Крипке с отмеченными мирами $\mathcal K=(W,\preccurlyeq,\mathrm{Aud}, D,\models)$ языка $L_M$, где $M\ne\varnothing$, определим модель $\mathcal K'=(W',\preccurlyeq',\mathrm{Aud}',D',\models')$ следующим образом:
Ясно, что в результате применения операции $'$ получается модель Крипке с отмеченными мирами. Теорема 10. Если класс моделей теории $T$ замкнут относительно операции $'$, то теория $T$ обладает дизъюнктивным и экзистенциальным свойствами. Доказательство. Рассуждения не отличаются от доказательства аналогичной теоремы для интуиционистского исчисления предикатов (см. [32]). Приведем набросок доказательства. Покажем, что $T$ обладает дизъюнктивным свойством. В самом деле, если $T\nvdash \alpha$ и $T\nvdash\beta$, то найдутся контрмодели Крипке $\mathcal K_1$ и $\mathcal K_2$ для $\alpha$ и $\beta$ соответственно. Тогда $\mathcal K=(\mathcal K_1+\mathcal K_2)'$, являющаяся по условию моделью теории $T$, является контрмоделью для $\alpha\vee\beta$. Покажем, что $T$ обладает экзистенциальным свойством. В самом деле, если $T\nvdash\alpha(c)$ для любой константы $c\in M$, то для любой константы $c\in M$ найдется такая контрмодель Крипке с отмеченными мирами $\mathcal K_c$ теории $T$, что $\mathcal K_c\nvDash A(c)$. Тогда $\mathcal K=(\sum_{c\in M}\mathcal K_c)'$, являющаяся по условию моделью теории $T$, является контрмоделью для $\exists\, x\ \alpha(x)$. Теорема доказана. Следствие. Если сигнатура $\Omega$ содержит хотя бы одну константу, то $\mathrm{QHC}$ (в этой сигнатуре) обладает дизъюнктивным и экзистенциальным свойствами. Поскольку класс моделей $\mathrm{QHC}$ в сигнатуре $\Omega$ замкнут относительно операции $'$, для завершения доказательства осталось применить теорему 10. Мы установили дизъюнктивное свойство для $\mathrm{QHC}$ только в случае, если сигнатура $\Omega$ содержит хотя бы одну константу. Это ограничение несущественно, как показывает следующая теорема. Доказательство не отличается от доказательства аналогичной теоремы из [32]. Замечание 3. В силу консервативности логики $\mathrm{QHC}$ относительно логики $\mathrm{QH4}$ для логики $\mathrm{QH4}$ также имеют место дизъюнктивное и экзистенциальное свойства. БлагодарностиАвтор выражает благодарность своему научному руководителю Л. Д. Беклемишеву за неоценимую помощь на всех этапах работы над статьей. Автор также благодарит рецензента за ценные замечания и указание на работу [33], близкую к результатам § 6. Автор является победителем конкурса стипендиатов Фонда развития теоретической физики и математики ``БАЗИС'' и выражает благодарность жюри и спонсорам конкурса.
Цитирование в формате AMSBIB
\RBibitem{Ono22} |
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|
Обратная связь: |
Пользовательское соглашение
|
Регистрация посетителей портала |
Логотипы |
|