Доклады Российской академии наук. Математика, информатика, процессы управления, 2023, T. 514, № 1, стр. 123-128

1. ВВЕДЕНИЕ

Совместная логика задач и высказываний QHC, рассматриваемая в настоящей работе, введена С.А. Мелиховым [1, 2]. В этой логике каждая переменная и каждая формула имеет один из двух сортов: либо высказывание, либо задача. Формулы сорта высказывание и сорта задача связаны между собой двумя модальностями ? и !. Применив ! к высказыванию $p$, мы получим задачу $!p$, которую можно неформально понимать как “доказать высказывание $p$”. Применив ? к задаче $\alpha $, мы получим высказывание $?\alpha $, которое можно неформально понимать как “задача $\alpha $ имеет решение”. Создание и изучение системы QHC мотивированы неформальным исчислением задач А.Н. Колмогорова и лежат в русле исследований конструктивной семантики Брауэра–Гейтинга–Колмогорова, см., например, [3–6].

Ранее мы установили, что для интуиционистского фрагмента совместной логики задач и высказываний QHC выполнены дизъюнктивное и экзистенциальное свойства [7]. В данной заметке доказаны аналоги теорем Эрбрана и Харропа для логики QHC.

Приведем определение логики QHC, подробно изложенное в [1] и [7]. Язык $\Omega $ логики QHC состоит из множества индивидных переменных $\{ {{x}_{0}},{{x}_{1}},{{x}_{2}}, \ldots \} $, множества константных символов $\{ {{c}_{i}}\,{\text{|}}\,i \in \mathcal{C}\} $ и двух множеств предикатных символов: сорта высказывание $\{ {{P}_{i}}\,{\text{|}}\,i \in \mathcal{P}\} $ и сорта задача $\{ {{\Phi }_{i}}\,{\text{|}}\,i \in \mathcal{T}\} $ ($\mathcal{C},\;\mathcal{P},\;\mathcal{T}$ – некоторые индексные множества). Множество термов логики QHC состоит из переменных $\{ {{x}_{0}},{{x}_{1}},{{x}_{2}}, \ldots \} $ и констант $\{ {{c}_{i}}\,{\text{|}}\,i \in \mathcal{C}\} $. Каждому предикатному символу приписано натуральное число, обозначающее его валентность. Формулы логики QHC сорта высказывание (задача) будем обозначать строчными латинскими (греческими) буквами.

Формула логики QHC определяется следующим образом.

1. Если $P$ ($\Phi $) – предикатный символ сорта высказывание (задача) валентности $n$, ${{t}_{1}}, \ldots ,{{t}_{n}}$ – термы, то $P({{t}_{1}}, \ldots ,{{t}_{n}})$ ($\Phi ({{t}_{1}}, \ldots ,{{t}_{n}})$) – формула сорта высказывание (задача). Такие формулы называются атомарными.

2. 0 – формула сорта высказывание, $ \bot $ – формула сорта задача. (0 и $ \bot $ соответствуют классической и интуиционистской лжи.)

3. Если $p,\;q$ – формулы сорта высказывание, то $(p \wedge q)$, $(p \vee q)$, $(p \to q)$, $\exists x{\kern 1pt} p$, $\forall x{\kern 1pt} p$ – формулы сорта высказывание.

4. Если $\alpha ,\beta $ – формулы сорта задача, то $(\alpha \wedge \beta )$, $(\alpha \vee \beta )$, $(\alpha \to \beta )$, $\exists x{\kern 1pt} \alpha $, $\forall x{\kern 1pt} \alpha $ – формулы сорта задача.

5. Если $p$ – формула сорта высказывание, то $!p$ – формула сорта задача.

6. Если $\alpha $ – формула сорта задача, то $?\alpha $ – формула сорта высказывание.

Схемы аксиом и правила вывода логики QHC следующие. В схемы аксиом вместо переменных по формулам можно подставлять любые формулы соответствующего сорта.

I. Все схемы аксиом и правила вывода классической логики предикатов (в схемах аксиом участвуют переменные по формулам сорта высказывание).

II. Все схемы аксиом и правила вывода интуиционистской логики предикатов (в схемах аксиом участвуют переменные по формулам сорта задача).

III. Дополнительные схемы аксиом и правила вывода, перечисленные ниже.

1. $!(p \to q) \to (!p \to !q)$;

2. $?(\alpha \to \beta ) \to (?\alpha \to ?\beta )$;

3. $\frac{p}{{!p}}$;

4. $\frac{\alpha }{{?\alpha }}$;

5. $?!p \to p$;

6. $\alpha \to !?\alpha $;

7. $\neg !0$.

Как доказано в [7], логика ${\text{QHC}}$ полна относительно семантики типа Крипке с отмеченными мирами. Приведем определение шкалы и модели Крипке логики QHC.

Определение. Пусть $\Omega $ – язык логики QHC. Шкала Крипке этого языка – это набор (W, $ \preccurlyeq ,{\text{Aud}})$, где $(W, \preccurlyeq )$ – непустое частично упорядоченное множество возможных миров, ${\text{Aud}} \subseteq W$ – множество отмеченных миров, и выполнено условие $\forall a \in W\exists b \in W(a \preccurlyeq b \wedge b \in {\text{Aud}}).$ Моделью Крипке логики QHC называется пятерка $\mathcal{K} = (W, \preccurlyeq ,{\text{Aud}},D, \vDash )$, где $(W, \preccurlyeq ,{\text{Aud}})$ – шкала Крипке, D – функция, которая каждому $a \in W$ сопоставляет непустое множество ${{D}_{a}}$. Расширим язык $\Omega $ множеством константных символов для обозначения всех элементов $\bigcup\limits_{a \in W} {{D}_{a}}$ (будем отождествлять эти константные символы и элементы $\bigcup\limits_{a \in W} {{D}_{a}}$). Обозначим этот расширенный язык через $\Omega (D)$. $ \vDash $ – соответствие между мирами (отмеченными мирами) $a \in W$ и замкнутыми атомарными формулами сорта задача (сорта высказывание) языка $\Omega (D)$. При этом выполнены следующие условия:

1. если $a \preccurlyeq b$, то ${{D}_{a}} \subseteq {{D}_{b}}$;

2. если язык $\Omega $ содержит константу c, то она принадлежит любому ${{D}_{a}}$ для $a \in W$;

3. если $\Phi ({{z}_{1}}, \ldots ,{{z}_{n}})$ – атомарная формула сорта задача, ${{z}_{1}}, \ldots ,{{z}_{n}} \in {{D}_{a}}$, $a \vDash \Phi ({{z}_{1}}, \ldots ,{{z}_{n}})$ и $a \preccurlyeq b$, то $b \vDash \Phi ({{z}_{1}}, \ldots ,{{z}_{n}})$ (монотонность);

4. если $a \vDash A({{z}_{1}}, \ldots ,{{z}_{n}})$, то $\{ {{z}_{1}}, \ldots ,{{z}_{n}}\} \subseteq {{D}_{a}}$ (здесь $A$ – некоторый предикатный символ валентности $n$ сорта высказывание или сорта задача языка $\Omega $).

Соответствие $ \vDash $ между мирами множества W и замкнутыми атомарными формулами в соответствующем языке продолжается индукцией по построению формулы до соответствия между мирами и всеми замкнутыми формулами в этом языке. Для любого мира $a \in W$ ($a \in {\text{Aud}}$) полагаем (). Индуктивный переход для классических связок и кванторов определяется поточечно в мирах множества Aud. Индуктивный переход для интуиционистских связок и кванторов определяется в мирах множества W как в шкалах Крипке интуиционистской логики (см., например, [8]). Индуктивный переход для модальностей определяется следующим образом:

Если $w \vDash A$, то будем говорить, что формула $A$ истинна в мире w. Будем говорить, что формула сорта задача (высказывание) истинна в модели Крипке языка $\Omega $, если она истинна в любом мире (отмеченном мире) этой модели Крипке.

Определение 2. Теорией в логике QHC называется множество $\Gamma $ замкнутых формул, содержащее все теоремы логики QHC и замкнутое относительно всех правил вывода логики QHC, кроме, возможно, правила усиления $\frac{p}{{!p}}$. Теория непротиворечива, если она не содержит константы 0.

Замыканием $[\Gamma ]$ множества замкнутых формул $\Gamma $ называется наименьшая по включению теория, содержащая множество $\Gamma $. Множество $\Gamma $ непротиворечиво, если теория $[\Gamma ]$ непротиворечива.

В [7] была доказана следующая теорема о полноте.

Теорема 1. 1) Если замкнутая формула языка $\Omega $ выводима в логике QHC, то она истинна в любой модели Крипке для языка $\Omega $.

2) Для любого непротиворечивого множества замкнутых формул $\Gamma $ логики QHC существуют модель Крипке $\mathcal{K}$ и ее отмеченный мир такие, что в этом мире модели $\mathcal{K}$ истинны все формулы из $\Gamma $.

Как показано в [7], логика QHC является консервативным расширением интуиционистской логики предикатов, и для ее интуиционистской части выполнены следующие дизъюнктивное и экзистенциальное свойства.

Теорема 2. 1) Пусть ${\text{QHC}} \vdash \alpha \vee \beta $. Тогда ${\text{QHC}} \vdash \alpha $ или ${\text{QHC}} \vdash \beta $.

2) Пусть язык $\Omega $ содержит хотя бы одну константу и ${\text{QHC}} \vdash \exists x\alpha $. Тогда для некоторой константы $c$ выполнено ${\text{QHC}} \vdash \alpha [c{\text{/}}x]$.

Эти свойства, рассматриваемые для интуиционистской логики предикатов, могут быть уточнены. Для классической логики предикатов имеет место теорема Эрбрана, которая в некотором смысле является уточнением экзистенциального свойства (см., например, [9]). Кроме того, можно рассматривать вывод из гипотез в интуиционистской логике. Если ввести некоторые ограничения на множество гипотез (они должны быть так называемыми харроповыми формулами), то возможно доказать усиления дизъюнктивного и экзистенциального свойств в интуиционистской логике – теорему Харропа (см., например, [10]). Поскольку логика QHC является расширением как классической, так и интуиционистской логики предикатов, в ней оказывается возможным установить аналоги этих результатов. Соответствующие результаты мы подробно излагаем далее. 

2. АНАЛОГИ ТЕОРЕМЫ ЭРБРАНА ДЛЯ ЛОГИКИ QHC

Для удобства читателя приведем формулировку теоремы Эрбрана для классической логики предикатов в языке без функциональных символов.

Теорема 3. Пусть формула $\exists {{x}_{1}} \ldots \exists {{x}_{n}}\varphi $ выводима в классической логике предикатов, где $\varphi $ – бескванторная формула. Тогда существует конечное множество констант ${{c}_{{1,1}}}, \ldots ,{{c}_{{n,m}}}$, что в классической логике предикатов выводима формула $\varphi [{{c}_{{1,1}}}{\text{/}}{{x}_{1}}$, ..., ${{c}_{{n,1}}}{\text{/}}{{x}_{n}}] \vee \ldots \vee \varphi [{{{{c}_{{\left\{ {1,m} \right\}}}}} \mathord{\left/ {\vphantom {{{{c}_{{\left\{ {1,m} \right\}}}}} {{{x}_{n}}}}} \right. \kern-0em} {{{x}_{n}}}} \ldots {{{{c}_{{\left\{ {n,m} \right\}}}}} \mathord{\left/ {\vphantom {{{{c}_{{\left\{ {n,m} \right\}}}}} {{{x}_{n}}].}}} \right. \kern-0em} {{{x}_{n}}].}}$

Логика ${\text{QHC}}$ является консервативным расширением классической логики предикатов, поэтому для нее автоматически выполнена теорема 3, где $\varphi $ – бескванторная формула сорта высказывание без модальностей. Мы докажем аналоги теоремы 3 для логики QHC, в которых будет рассматриваться более широкий класс формул. Неформально, сначала в формуле идут кванторы существования и модальности, а после них – бескванторная часть. Формальное определение дано ниже.

Определение 3. Определим класс формул $E{{x}_{{Prop}}}$ – экзистенциальные формулы, основанные на формуле сорта высказывание, как минимальный класс, удовлетворяющий следующим условиям:

$ \bullet $ бескванторные формулы сорта высказывание лежат в $E{{x}_{{Prop}}}$;

$ \bullet $ если $p \in E{{x}_{{Prop}}}$, то $\exists xp \in E{{x}_{{Prop}}}$;

$ \bullet $ если $\alpha \in E{{x}_{{Prop}}}$, то $?\alpha \in E{{x}_{{Prop}}}$ и $\exists x\alpha \in E{{x}_{{Prop}}}$;

$ \bullet $ если $\exists xp \in E{{x}_{{Prop}}}$, то $!\exists xp \in E{{x}_{{Prop}}}$.

Иными словами, экзистенциальные формулы, основанные на формуле сорта высказывание p, определены так: сначала идет приставка из кванторов существования и модальностей, а после последнего квантора существования – бескванторная формула сорта высказывание p (т.е. p – ее бескванторная часть).

Аналогично определяются экзистенциальные формулы, основанные на формуле сорта задача $\alpha $ ($\alpha $ – бескванторная часть). Обозначение: $E{{x}_{{Prob}}}$.

Нам понадобится следующая лемма. Будем считать, что язык $\Omega $ содержит хотя бы одну константу.

Лемма 1. 1) ${\text{QHC}} \vdash p \Leftrightarrow {\text{QHC}} \vdash !p$.

2) ${\text{QHC}} \vdash \alpha \Leftrightarrow {\text{QHC}} \vdash ?\alpha $.

Доказательство. 1) Очевидно в силу допустимости правил вывода $\frac{p}{{!p}}$ и $\frac{{!p}}{p}$ (см. [1]).

2) Слева направа выполнено в силу допустимости правила вывода $\frac{\alpha }{{?\alpha }}$. Теперь пусть ${\text{QHC}} \nvdash \alpha $. Тогда найдется модель Крипке $\mathcal{K}$ и ее мир $w$ такие, что $\mathcal{K},w \nvDash \alpha $. Определим модель $\tilde {\mathcal{K}}$ следующим образом: добавим мир u, который будет отмеченным миром, меньшим мира $w$; ${{D}_{u}}$ состоит из констант. Тогда $\tilde {\mathcal{K}},u \nvDash \alpha $, следовательно, $\tilde {\mathcal{K}},u \nvDash ?\alpha $, откуда следует ${\text{QHC}} \nvdash ?\alpha $.

Теорема 4. Пусть имеется экзистенциальная формула, основанная на формуле сорта задача $\alpha $, выводимая в логике QHC. Тогда существуют константы ${{c}_{1}}, \ldots ,{{c}_{n}}$ такие, что в логике QHC выводима формула $\alpha [{{c}_{1}}{\text{/}}{{x}_{1}}, \ldots ,{{c}_{n}}{\text{/}}{{x}_{n}}]$.

Доказательство. Докажем теорему по индукции по длине приставки с кванторами и модальностями. Рассмотрим, с чего начинается экзистенциальная формула, выводимая в логике QHC.

Случай 1: она начинается с модальности ? или !. По лемме 1 можно убрать модальность – получится также выводимая экзистенциальная формула.

Случай 2: она начинается с интуиционистского квантора существования $\exists x\varphi $. Тогда по второму пункту теоремы 2 найдется такая константа c такая, что ${\text{QHC}} \vdash \varphi [c{\text{/}}x]$.

Случай 3: она начинается с классического квантора существования. Так как формула построена на основе формулы сорта задача, то после блока из нескольких кванторов существования обязательно встретится модальность ?. То есть формула имеет вид $\exists {{x}_{1}} \ldots \exists {{x}_{n}}? \ldots \alpha $. Поскольку ${\text{QHC}} \vdash \exists x?\beta \leftrightarrow ?\exists x\beta $ (см. [1]), перекинем модальность вперед и получим такую формулу, также выводимую в логике QHC: $?\exists {{x}_{1}} \ldots \exists {{x}_{n}} \ldots \alpha $. Свели к первому случаю.

Теперь докажем аналог теоремы Эрбрана для экзистенциальных формул, построенных на основе формулы сорта высказывание. Начнем со следующей леммы.

Лемма 2. Пусть имеется формула следующего вида, выводимая в логике QHC: ${\text{QHC}} \vdash \exists {{x}_{1}}...\exists {{x}_{n}}p$. Тогда существуют константы ${{c}_{{1,1}}}, \ldots ,{{c}_{{n,m}}}$ такие, что ${\text{QHC}} \vdash p[{{c}_{{1,1}}}{\text{/}}{{x}_{1}}, \ldots {{c}_{{n,1}}}{\text{/}}{{x}_{n}}] \vee \ldots \vee p[{{c}_{{1,m}}}{\text{/}}{{x}_{1}}, \ldots {{c}_{{n,m}}}{\text{/}}{{x}_{n}}]$.

Доказательство. Доказательство аналогично тому, которое работает в классической логике предикатов. Рассмотрим (возможно, бесконечное) множество формул вида $\neg p[{{c}_{1}}{\text{/}}{{x}_{1}}, \ldots ,{{c}_{n}}{\text{/}}{{x}_{n}}]$ со всеми возможными подстановками констант. Если это множество противоречиво, то противоречие выводится из его конечного подмножества – и тогда выводима дизъюнкция формул с соответствующими подстановками. Если же оно непротиворечиво, то рассмотрим модель Крипке $\mathcal{K}$ и ее отмеченный мир w, в котором все эти формулы истинны. Поменяем множество ${{D}_{w}}$ так, чтобы в нем остались только значения констант. Поскольку формулы бескванторные, то их значения не изменятся. Но при этом $\mathcal{K},w \nvDash \exists {{x}_{1}}...\exists {{x}_{n}}p$, что противоречит условию.

Теперь докажем теорему, верную для любых экзистенциальных формул, основанных на формулах сорта высказывание.

Теорема 5. Пусть имеется экзистенциальная формула, основанная на (бескванторной) формуле сорта высказывание p, выводимая в логике QHC. Обозначим через ${{y}_{1}}, \ldots ,{{y}_{n}}$ переменные, которые стоят в последнем блоке классических кванторов существования (ближайшем к p), а через ${{x}_{1}}, \ldots ,{{x}_{k}}$ – остальные переменные. Тогда существуют константы ${{c}_{1}}, \ldots ,{{c}_{k}}$, ${{d}_{{1,1}}}, \ldots ,{{d}_{{n,m}}}$ такие, что в логике QHC выводима формула $ \vdash p[{{c}_{1}}/{{x}_{1}}, \ldots ,{{c}_{k}}{\text{/}}{{x}_{k}},{{d}_{{1,1}}}{\text{/}}{{y}_{1}}, \ldots ,{{d}_{{n,1}}}{\text{/}}{{y}_{n}}]$ $ \vee \ldots \vee $ $p[{{c}_{1}}{\text{/}}{{x}_{1}}, \ldots ,{{c}_{k}}{\text{/}}{{x}_{k}},{{d}_{{1,m}}}{\text{/}}{{y}_{1}}, \ldots ,{{d}_{{n,m}}}{\text{/}}{{y}_{n}}]$.

Доказательство. Устраняем по очереди кванторы, начиная с внешнего. Пока мы не добрались до последних классических кванторов, применяем теорему 4. Когда же мы до них доберемся, используем лемму 2.

3. АНАЛОГ ТЕОРЕМЫ ХАРРОПА ДЛЯ ЛОГИКИ QHC

Для удобства читателя приведем формулировку теоремы Харропа для интуиционистской логики предикатов.

Определение 4. Определим класс харроповых формул интуиционистской логики предикатов как наименьший класс, удовлетворяющий следующим условиям:

$ \bullet $ атомарные формулы и $ \bot $ харроповы;

$ \bullet $ если $\alpha $ и $\beta $ харроповы, то $\alpha \wedge \beta $ харропова;

$ \bullet $ если $\alpha $ харропова, то $\forall x\alpha $ харропова;

$ \bullet $ если $\alpha $ харропова, $\xi $ произвольная, то $\xi \to \alpha $ харропова.

Теорема 6. Пусть T состоит из замкнутых харроповых формул.

1) Если $T \vdash \alpha \vee \beta $, то $T \vdash \alpha $ или $T \vdash \beta $.

2) Если $T \vdash \exists x\alpha $, то для некоторой константы $c$ выполнено $T \vdash \alpha [c{\text{/}}x]$.

Логика QHC является консервативным расширением интуиционистской логики предикатов и вместе с тем имеет более богатый язык. Поэтому доказательство аналога теоремы Харропа для логики ${\text{QHC}}$ будет иметь свои особенности. В частности, изменится определение харроповой формулы – сначала необходимо определить строго харроповы формулы.

Определение 5. Определим класс строго харроповых формул логики QHC как наименьший класс, удовлетворяющий следующим условиям:

$ \bullet $ атомарные формулы, $0,\; \bot $ строго харроповы;

$ \bullet $ если $\alpha $ и $\beta $ строго харроповы, то $\alpha \wedge \beta $ строго харропова;

$ \bullet $ если $\alpha $ строго харропова, то $\forall x\alpha $ строго харропова;

$ \bullet $ если $\alpha $ строго харропова, $\xi $ произвольная, то $\xi \to \alpha $ строго харропова;

$ \bullet $ если $p$ и $q$ строго харроповы, то $p \wedge q$ строго харропова;

$ \bullet $ если $p$ строго харропова, то $!p$ строго харропова;

$ \bullet $ если $\alpha $ строго харропова, то $?\alpha $ строго харропова.

Определим прямую сумму моделей Крипке следующим образом. Будем считать, что множество константных символов языка $\Omega $ непусто.

Определение 6. Пусть ${{\mathcal{K}}_{1}},\;{{\mathcal{K}}_{2}}$ – 2 модели Крипке, $u \in {{\mathcal{K}}_{1}}$, $v \in {{\mathcal{K}}_{2}}$ – отмеченные миры. Их прямой суммой ${{\mathcal{K}}_{1}} \oplus {{\mathcal{K}}_{2}}$ назовем модель $\mathcal{K}$, состоящую из объединения моделей ${{\mathcal{K}}_{1}}$ и ${{\mathcal{K}}_{2}}$, к которым добавили отмеченный мир w, меньший миров $u$ и $v$. Определим ${{D}_{w}}$ – множество константных символов языка $\Omega $; $w \vDash A(\vec {c}) \Leftrightarrow (u \vDash A(\vec {c})\;{\text{и}}\;v \vDash A(\vec {c}))$, где $A(\vec {c})$ – всевозможные атомарные замкнутые формулы.

В дальнейших леммах рассматривается прямая сумма двух моделей Крипке ${{\mathcal{K}}_{1}},\;{{\mathcal{K}}_{2}}$, $u \in {{\mathcal{K}}_{1}}$, $v \in {{\mathcal{K}}_{2}}$ – их отмеченные миры, w – добавленный отмеченный мир.

Лемма 3. Пусть $A$ – замкнутая строго харропова формула. Тогда $u \vDash A$ и $v \vDash A \Leftrightarrow w \vDash A$.

Доказательство. Доказываем индукцией по построению формулы.

Для атомарных формул утверждение леммы выполнено по определению прямой суммы моделей Крипке; для констант 0 и $ \bot $ утверждение леммы так же выполнено, поскольку 0 и $ \bot $ ложны в каждом мире.

Пусть $A = \alpha \wedge \beta $ (аналогично разбирается случай $A\, = \,p \wedge q$). Тогда $(u \vDash \alpha \wedge \beta ,$ $v \vDash \alpha \wedge \beta )$ $ \Leftrightarrow $ $(u \vDash \alpha ,$ $u \vDash \beta ,v \vDash \alpha ,v \vDash \beta )$ $ \Leftrightarrow $ $(w \vDash \alpha ,w \vDash \beta ) \Leftrightarrow w \vDash \alpha \wedge \beta $.

Пусть $A = \forall x\alpha $. Предположим, что $u \vDash \forall x\alpha $, $v \vDash \forall x\alpha $. Тогда $\forall t \succ w\;\forall d \in {{D}_{t}}$ $t \vDash \alpha [d{\text{/}}x]$. Пусть $c \in {{D}_{w}}$ – константный символ языка $\Omega $. Имеем $u \vDash \alpha [c{\text{/}}x]$, $v \vDash \alpha [c{\text{/}}x]$. В силу того, что $\alpha [c{\text{/}}x]$ – замкнутая строго харропова формула, получаем $w \vDash \alpha [c{\text{/}}x]$. Отсюда $w \vDash \forall x\alpha $. Обратно, если $w \vDash \forall x\alpha $, то $u \vDash \forall x\alpha $ и $v \vDash \forall x\alpha $ по монотонности (см. [7] – для формул сорта задача логики ${\text{QHC}}$ выполнена монотонность отношения истинности).

Пусть $A\, = \,\xi \, \to \,\alpha $. Предположим, что $u \vDash \xi \to \alpha $ и $v \vDash \xi \to \alpha $. Тогда $\forall t \succ w(t \vDash \xi \Rightarrow t \vDash \alpha )$. Предположим, что $w \vDash \xi $. Тогда $v \vDash \xi $ и $u \vDash \xi $ по монотонности. Так как $u \vDash \xi \to \alpha $ и $v \vDash \xi \to \alpha $, имеем $u \vDash \alpha $ и $v \vDash \alpha $. Отсюда $w \vDash \alpha $, так как $\alpha $ – строго харропова формула. Получаем $w \vDash \xi \to \alpha $. Обратно, если $w \vDash \xi \to \alpha $, то $u \vDash \xi \to \alpha $ и $v \vDash \xi \to \alpha $ по монотонности.

Пусть $A = !p$. Предположим, что $u \vDash !p$ и $v \vDash !p$. Тогда $\forall t \succ w(t \in {\text{Aud}} \Rightarrow t \vDash p)$ (мы обозначили через ${\text{Aud}}$ множество отмеченных миров в полученной модели $\mathcal{K}$). В частности, $u \vDash p$ и $v \vDash p$, поскольку $u,v \in {\text{Aud}}$. Так как $p$ – строго харропова формула, имеем $w \vDash p$. Отсюда $\forall t \succcurlyeq w(t \in {\text{Aud}} \Rightarrow t \vDash p)$, то есть $w \vDash !p$. Обратно, если $w \vDash !p$, то $u \vDash !p$ и $v \vDash !p$ по монотонности ($!p$ – формула сорта задача).

Пусть $A = ?\alpha $. Тогда $(u \vDash ?\alpha ,v \vDash ?\alpha )$ $ \Leftrightarrow $ $ \Leftrightarrow $ $(u \vDash \alpha ,v \vDash \alpha )$ $ \Leftrightarrow $ $w \vDash \alpha \Leftrightarrow w \vDash ?\alpha $.

Определение 7. Определим класс харроповых формул логики QHC как наименьший класс, удовлетворяющий следующим условиям:

$ \bullet $ атомарные формулы, $0, \bot $ харроповы;

$ \bullet $ если $\alpha $ и $\beta $ харроповы, то $\alpha \wedge \beta $ харропова;

$ \bullet $ если $\alpha $ харропова, то $\forall x\alpha $ харропова;

$ \bullet $ если $\alpha $ харропова, $\xi $ произвольная, то $\xi \to \alpha $ харропова;

$ \bullet $ если $p$ и $q$ харроповы, то $p \wedge q$ харропова;

$ \bullet $ если $p$ харропова, то $!p$ харропова;

$ \bullet $ если $\alpha $ харропова, то $?\alpha $ харропова;

$ \bullet $ если $p$ строго харропова, $q$ харропова, то $p \to q$ харропова;

$ \bullet $ если $p$ харропова, то $\forall xp$ харропова.

Ясно, что любая строго харропова формула является харроповой. Обратное неверно.

Лемма 4. Пусть $A$ – замкнутая строго харропова формула. Тогда $u \vDash A$ и $v \vDash A \Rightarrow w \vDash A$.

Доказательство. Доказываем индукцией по построению формулы. Проверим только последние два случая индуктивного перехода (все прочие проверяются аналогично тому, как это было сделано в лемме 3).

Пусть $A = p \to q$. Предположим, что $w \vDash p$. Так как $p$ – строго харропова формула, то $u \vDash p$, $v \vDash p$. Так как $u \vDash p \to q$, $v \vDash p \to q$, имеем $u \vDash q$, $v \vDash q$. Так как $q$ – харропова формула, имеем $w \vDash q$. Отсюда $w \vDash p \to q$.

Пусть $A = \forall xp$. Пусть $c \in {{D}_{w}}$ – константный символ языка $\Omega $. Имеем $u \vDash p[c{\text{/}}x]$, $v \vDash p[c{\text{/}}x]$. В силу того, что $p[c{\text{/}}x]$ – замкнутая харропова формула, получаем $w \vDash p[c{\text{/}}x]$. Отсюда $w \vDash \forall xp$.

Наконец, докажем аналоги теоремы Харропа для логики QHC. Определение слабого вывода из гипотез в логике ${\text{QHC}}$ см. в [7].

Теорема 7. Пусть $T$ – множество замкнутых харроповых формул логики ${\text{QHC}}$. Тогда, если $T \vdash \alpha \vee \beta $, то $T \vdash \alpha $ или $T \vdash \beta $.

Доказательство. Предположим, что $T \nvdash \alpha $ и $T \nvdash \beta $. Тогда в силу теоремы 1 о полноте существуют модели ${{\mathcal{K}}_{1}}$, ${{\mathcal{K}}_{2}}$ и их отмеченные миры $u \in {{\mathcal{K}}_{1}}$, $v \in {{\mathcal{K}}_{2}}$, что в этих мирах истинны все формулы из $T$, но при этом $u \nvDash \alpha $, $v \nvDash \beta $. Рассмотрим их прямую сумму ${{\mathcal{K}}_{1}} \oplus {{\mathcal{K}}_{2}}$. Тогда в силу леммы 4 в нижнем мире $w$ будут истинны все формулы из $T$, но $w \nvDash \alpha \vee \beta $.

Теорема 8. Пусть $T$ – множество замкнутых харроповых формул логики QHC. Тогда, если $T \vdash \exists x\alpha $, то существует такая константа $c$, что $T \vdash \alpha [c{\text{/}}x]$.

Доказательство аналогично доказательству теоремы 7. В леммах 3 и 4 надо рассматривать контрмодели для всех формул вида $\alpha [c{\text{/}}x]$ и прямую сумму всех этих моделей.

Замечание 1. Между отношениями слабой выводимости $ \vdash $ и выводимости $ \vdash \,{\text{*}}$ в логике QHC имеется взаимосвязь. Обозначим через ${{T}^{C}}$ (${{T}^{H}}$) множество формул сорта высказывание (задача) из множества формул $T$. Тогда $T \vdash {\kern 1pt} *\alpha \Leftrightarrow {{T}^{H}}$, $!{{T}^{C}} \vdash \alpha $ (см. [7]). Поэтому теоремы 7 и 8 также выполнены, если заменить в их формулировках слабую выводимость $ \vdash $ на выводимость $ \vdash {\kern 1pt} *$.