Исчисление высказываний
Понятие исчисления
Если в алгебре высказываний изучаются логические операции над множеством логических значений ${0, 1}$ и строятся булевы функции, для которых сделан упор на их семантику (значения булевых функций при разных наборах значений переменных), то исчисление высказываний – это формальная аксиоматическая теория, которая обращает внимание на синтаксис логических формул и правила вывода и на этой основе исследует множество общезначимых формул.
Чтобы задать формальное исчисление, нам надо определить 4 объекта:
-
алфавит – непустое конечное множество символов; конечные последовательности символов алфавита образуют слова исчисления;
-
множество формул исчисления – сюда относятся как истинные, так и ложные формулы, то есть все синтаксически правильные выражения образуют указанное множество формул;
-
аксиомы исчисления – это подмножество множества формул;
-
правила вывода – это отношения между формулами, их может быть несколько.
Если существует правило вывода, которое связывает $m$ формул $\varphi_1, \dots, \varphi_m$ с формулой $\varphi$, то говорят, что существует непосредственный вывод $\varphi$ из $\varphi_1, \dots, \varphi_m$ по соответствующему правилу вывода.
Язык исчисления высказываний. Определение формулы ИВ
Вообще формальным языком в алфавите $A$ называется какое угодно подмножество множества $A^*$ всех слов в этом алфавите. Пустое слово тоже принадлежит этому множеству. Например, в [Белоусов] приводится пример языка арифметических выражений, который построен по принципу исчисления. Можно дополнить этот пример определением языка идентификаторов из [Герасимов, с. 13]: пусть алфавитом ${\tt LettersAndDigits}$ является множество символов ${A, a, B, b, C, c, \dots, Z, z, 0, 1, 2, \dots, 9}$. Определим язык ${\tt Identifiers}$ в этом алфавите как множество всех слов в алфавите ${\tt LettersAndDigits}$, которые начинаются с любого символа, принадлежащего множеству ${A, a, B, b, C, c, \dots, Z, z}$. Например, слова xyz3, Dt0a принадлежат языку ${\tt Identifiers}$, а пустое слово и слово 73abc – нет.
Можно задать язык ${\tt Identifiers}$ и с помощью следующего индуктивного определения:
1) любой символ из ${A, a, B, b, C, c, \dots, Z, z}$ является словом языка ${\tt Identifiers}$;
2) если $\beta$ – слово языка ${\tt Identifiers}$ и $\gamma$ – символ алфавита ${\tt LettersAndDigits}$, то $\beta\gamma$ (т.е. конкатенация $\beta$ и $\gamma$) является словом языка ${\tt Identifiers}$.
Далее определим язык для записи высказываний. Введем множество пропозициональных переменных. Пропозициональная формула (или формула логики высказываний) задается следующим индуктивным определением:
1) любая пропозициональная переменная является пропозициональной формулой;
2) символы 0 и 1 являются пропозициональными формулами и называются истинностными константами;
3) если $A$ и $B$ – пропозициональные формулы, то $\neg A$, $(A \& B)$, $(A \vee B)$ и $(A \to B)$ – пропозициональные формулы;
4) других формул, кроме описанных выше, нет.
Множество всех пропозициональных формул и называется языком логики высказываний.
Замечание. Индуктивный характер определения формул логики высказываний позволяет доказывать утверждения об этих формулах методом индукции по построению.
В первую очередь выполняются операции в скобках, затем все остальные логические операции в порядке старшинства. Порядок старшинства логических операций следующий: $\neg,\;\&,\; \vee,\;\oplus,\;\to,\;\sim$.
Аксиомы и правила вывода ИВ
Существует несколько вариантов подбора аксиом как исходных тождественно истинных формул. Эти наборы эквивалентны в том смысле, что они определяют один и тот же класс выводимых формул.
Приведем основные аксиомы из [ВерещагинШень2]:
-
$A \to (B \to A)$
-
$(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
-
$(A \& B) \to A$
-
$(A \& B) \to B$
-
$A \to (B \to (A \& B))$
-
$A \to (A \vee B)$
-
$B \to (A \vee B)$
-
$(A \to C) \to ((B \to C) \to (A \vee B \to C))$
-
$\neg A \to (A \to B)$
-
$(A \to B) \to ((A \to \neg B) \to \neg A)$
-
$A \vee \neg A$
Эти аксиомы легко запомнить так: 1, 2 – про имликацию (1 - принятую посылку можно вывести из чего угодно, 2 - аналог дистрибутивности импликации), 3, 4, 5 – про конъюнкцию (3, 4 – что можно получить из конъюнкции, 5 – как получить конъюнкцию), 6, 7, 8 – про дизъюнкцию (6, 7 – как получить дизъюнкцию, 8 – что можно вывести из дизъюнкции), 9, 10 – про отрицание, 11 – закон двойного отрицания, от которого отказываются в интуиционистской логике [ВерещагинШень2, с. 58].
Указанные формулы называются схемами аксиом ИВ. При подстановке конкретных формул в какую-либо схему получается частный случай схемы аксиом. Все аксиомы легко проверяются с помощью таблиц истинности либо эквивалентных преобразований алгебры логики.
Основным правилом вывода в ИВ является правило заключения (modus ponens): если $\varphi$ и $\varphi \to \psi$ – выводимые формулы, то $\psi$ – также выводимая формула. Символически это записывается так: \(\frac{\varphi, \varphi \to \psi}{\psi}.\) Например, если высказывания $A \& B$ и $A \& B \to (A \to C)$ выводимы, то высказывание $A \to C$ также выводимо согласно правилу заключения.
Помимо modus ponens, применяют и производные правила вывода, например, modus tollens [Игошин, с. 66].
Выводом в исчислении высказываний называется конечная последовательность формул, каждая из которых есть аксиома или получается из предыдущих по правилу modus ponens.
Доказуемые и выводимые формулы ИВ
Если имеется вывод формулы $F$ из множества гипотез $\Gamma$ (конечная последовательность формул из $\Gamma$, в которой каждая формула – либо аксиома, либо формула из $\Gamma$, либо получена из предыдущих формул по правилу modus ponens), то говорят, что $F$ выводима из $\Gamma$, и пишут $\Gamma \vdash F$. Если $F$ выводима только из аксиом, то говорят, что $F$ доказуема, и пишут $\vdash F$. В таком случае $F$ – теорема ИВ.
В [Степанова], [Игошин, с. 118] и здесь приводятся примеры выводов следующих выводимых формул:
-
$\vdash \varphi \to \varphi$;
-
$\varphi \to \psi,\; \psi \to \chi \vdash \varphi \to \chi$;
-
$\varphi \vdash \neg\neg\varphi$;
-
$\varphi \to \psi \vdash \neg\psi \to \neg\varphi$;
-
$\neg\psi \to \neg\varphi \vdash \varphi \to \psi$;
-
$\varphi \to (\neg \psi \to \neg(\varphi \to \psi))$;
-
$(\varphi \to \psi) \to ((\neg\varphi \to \psi) \to \psi)$;
-
$\neg\neg\varphi \to \varphi$.
В качестве примера рассмотрим вывод $\vdash (\neg A \vee B) \to (A \to B)$.
1) $\neg A \to (A \to B)$ (акс. 9)
2) $B \to (A \to B)$ (акс. 1)
3) $(\neg A \to (A \to B)) \to ((B \to (A \to B)) \to ((\neg A \vee B) \to (A \to B)))$ (акс. 8: $C := A \to B, \; A := \neg A$)
4) $(B \to (A \to B)) \to ((\neg A \vee B) \to (A \to B))$ (m.p. из 1, 3)
5) $(\neg A \vee B) \to (A \to B)$ (m.p. из 2, 4)
В [Лихтарников, с. 62, с. 202], [Игошин], [Корнеева, с. 17], здесь и здесь доказываются производные правила вывода:
-
правило введения конъюнкции $\dfrac{\Gamma \vdash A;\; \Gamma \vdash B}{\Gamma \vdash A\& B}$;
-
правило введения дизъюнкции $\dfrac{\Gamma, A \vdash C; \; \Gamma, B \vdash C}{\Gamma, A \vee B \vdash C}$;
-
правило перестановки посылок $\dfrac{\vdash A \to (B \to C)}{\vdash B \to (A \to C)}$;
-
правило соединения посылок $\dfrac{\vdash A \to (B \to C)}{\vdash A\& B \to C}$;
-
правило разъединения посылок $\dfrac{\vdash A \& B \to C}{\vdash A \to (B \to C)}$
и другие.
Теорема о дедукции
Теорема (о дедукции). Пусть $\Gamma$ – множество формул, $A, B$ – формулы. Тогда $\Gamma \vdash A \to B \Leftrightarrow \Gamma \cup {A} \vdash B$.
Теорема о дедукции утверждает, что понятие посылки в импликации и понятие посылки как элемента множества посылок – это эквивалентные вещи.
Необходимость. Утверждение $\Gamma \vdash A \to B$ означает, что существует последовательность формул, в которой каждая формула либо берется из $\Gamma$, либо получается из предыдущих по правилу вывода, и заканчивается эта последовательность формулой $A \to B$. Продолжим эту последовательность. Поставим следом за ней формулу $A$ и затем формулу $B$, которая получается по правилу $A, A\to B \models B$. Итак, мы получили, что $\Gamma \cup {A} \vdash B$.
Достаточность. Рассмотрим цепочку формул $c_1, c_2, \dots, c_k$, которая является выводом из $\Gamma \cup {A}$. Будем по индукции доказывать, что $\Gamma \vdash A \to c_i$. Рассмотрим 3 случая:
1) $c_i$ – аксиома, тогда она следует из любой посылки;
2) $c_i \in \Gamma \cup {A}$, тогда, если $c_i \in \Gamma$, то цепочка $c_1, \dots, c_i$ будет выводом $c_i$ из $\Gamma$, и поскольку $c_i$ выводима, то по аксиоме 1 выводимо высказывание $A \to c_i$; если $c_i = A$, то получим $A \to A$, это тавтология;
3) $c_i$ получается из предыдущих $c_j, c_k$ по правилу вывода, т.е. $c_k = c_j \to c_i$. По гипотезе индукции высказывания $A \to c_j$ и $A \to c_k$ выводимы из $\Gamma$. Итак, $\Gamma \vdash A \to c_j$, $\Gamma \vdash A \to (c_j \to c_i)$.
По аксиоме 2 $(A \to (c_j \to c_i)) \to ((A \to c_j) \to (A \to c_i))$. Дальше по modus ponens можно оставить только $(A \to c_j) \to (A \to c_i)$. А поскольку $A \to c_j$ у нас уже выведено, то $A \to c_i$ получается по modus ponens. Итак, мы доказали по индукции, что $\Gamma \vdash A \to c_i$ для всех $i$.
В качестве примера применения теоремы дедукции докаже правило “силлогизм”: \((A \to B) \to ((B \to C) \to (A \to C)).\) Непосредственный вывод непростой.
\(\vdash (A \to B) \to ((B \to C) \to (A \to C)) \Leftrightarrow\) \(A \to B \vdash (B \to C) \to (A \to C) \Leftrightarrow\) \(\Leftrightarrow A \to B, B \to C \vdash A \to C \Leftrightarrow\) \(\Leftrightarrow A, A \to B, B \to C \vdash C.\) Вывод: $A,\;A \to B,\;B, \; B\to C,\; C$.
Отметим, что это по смыслу эквивалентно $(A \to B) \& (B \to C) \to (A \to C)$.
Понятие эквивалентных формул ИВ
Спросил меня голос
В пустыне дикой:
-- Много ли в море
Растет земляники?
-- Столько же, сколько
Селедок соленых
Растет на березах
И елках зеленых.
Формулы $\varphi$ и $\psi$ назовем эквивалентными ($\varphi \equiv \psi$), если $\varphi \vdash \psi$ и $\psi \vdash \varphi$. На множестве формул ИВ отношение $\equiv$ есть отношение эквивалентности, т.е. рефлексивное, симметричное и транзитивное отношение.
Можно показать, что при замене любой подформулы на эквивалентную ей формулу получится формула, эквивалентная исходной формуле:
1) если $\varphi \equiv \psi$, то $\vdash\varphi \Leftrightarrow \vdash\psi$;
2) если $\varphi_1 \equiv \psi_1$, $\varphi_2 \equiv \psi_2$, то $\varphi_1 \& \varphi_2 \equiv \psi_1 \& \psi_2$, $\varphi_1 \vee \varphi_2 \equiv \psi_1 \vee \psi_2$, $\varphi_1 \to \varphi_2 \equiv \psi_1 \to \psi_2$, $\neg\varphi_1 \equiv \neg\varphi_1$;
3) если $\varphi$ – формула ИВ, $\psi$ – ее подформула (т.е. подслово формулы, которое в свою очередь является формулой), и пусть $\varphi’$ получается из $\varphi$ путем замены некоторого вхождения $\psi$ на формулу $\psi’$. Тогда если $\psi \equiv \psi’$, то $\varphi \equiv \varphi’$.
Формулировка и доказательство основных законов ИВ
Правило сечения: \(\frac{\Gamma \vdash A \quad \Gamma, A \vdash B}{\Gamma \vdash B}.\)
Ассоциативность дизъюнкции: \((A \vee (B \vee C)) \to ((A \vee B) \vee C).\)
Аксиома 6: $\vdash A \to (A \vee B) \Leftrightarrow A \vdash A \vee B$.
Аналогично $A \vee B \vdash (A \vee B) \vee C$.
По правилу сечения \(\frac{A \vdash A \vee B \quad A, A \vee B \vdash (A \vee B) \vee C}{A \vdash (A \vee B) \vee C}.\)
Аналогично $B \vdash (A \vee B) \vee C$, $C \vdash (A \vee B) \vee C$.
Аксиому 8 можно переформулировать как правило разбора случаев: \(\frac{\Gamma, A \vdash C \quad \Gamma, B \vdash C}{\Gamma, A\vee B \vdash C}.\)
Применяя правило разбора случаев, получим \(\frac{B \vdash (A \vee B) \vee C; \quad C \vdash (A \vee B) \vee C}{B \vee C \vdash (A \vee B) \vee C}.\) Поскольку $A \vdash (A \vee B) \vee C$, то по правилу введения дизъюнкции \(A \vee (B \vee C) \vdash (A \vee B) \vee C.\) Ассоциативность дизъюнкции в одну сторону доказана.
Правило рассуждения от противного: \(\frac{\Gamma, A \vdash B \quad \Gamma, A \vdash B}{\Gamma \vdash \neg A}.\) Следует из акс. 10.
Правило контрапозиции: \((A \to B) \to (\neg B \to \neg A).\)
Закон де Моргана: \(\neg (A \vee B) \leftrightarrow (\neg A \& \neg B).\)
Чтобы доказать эквиваленцию, нужно доказать две импликации.
Заметим, что по правилу контрапозиции $\dfrac{\Gamma,A \vdash B}{\Gamma, B \vdash \neg A}$ из $A \vdash A \vee B$ следует $\neg(A\vee B) \vdash \neg A$.
Далее \(\frac{\frac{B \vdash A \vee B}{\neg (A \vee B) \vdash \neg B};\quad \neg(A \vee B) \vdash \neg A} {\neg(A \vee B) \vdash \neg A \& \neg B}\)
По правилу образования конъюнкции (акс. 5) $\dfrac{\Gamma \vdash A \quad \Gamma \vdash B}{\Gamma \vdash (A \& B)}$
Тогда \(\frac{\neg A, \neg B \vdash \neg(A \vee B)}{\neg A \& \neg B \vdash \neg (A \vee B)}\)
Поскольку $\neg A \& \neg B \vdash \neg A$ (акс. 3) и $\neg A \& \neg B \vdash \neg B$ (акс. 4), то из $\neg A, \neg B \vdash \neg (A \vee B)$ следует, что $\neg A \& \neg B \vdash \neg(A \vee B)$.
Дистрибутивность конъюнкции относительно дизъюнкции и формула замены импликации доказаны в [Судоплатов, с. 24].
Рекомендуется ознакомиться с конспектами лекций МФТИ по исчислению высказываний.
Полнота и непротиворечивость ИВ
Литература
Степанова – Математическая логика. Конспект лекций (2002) [новая версия]
Белоусов – О некоторых методических вопросах преподавания математической логики студентам-программистам (2021)
Герасимов – Курс математической логики и теории вычислимости (2014)
Агарева, Селиванов – Математическая логика и теория алгоритмов (2011)
Гринченков, Потоцкий – Математическая логика и теория алгоритмов для программистов (2010)
Верещагин, Шень – Лекции по математической логике и теории алгоритмов. Часть 2. Языки и исчисления (2012)
Игошин – Математическая логика (2016)
Лихтарников, Сукачева – Математическая логика. Курс лекций. Задачник-практикум и решения (2009)
Судоплатов, Овчинникова – Математическая логика и теория алгоритмов (2010)
Корнеева – Математическая логика. Конспект лекций (2014)
Курс лекций МФТИ по математической логике и теории алгоритмов