Исчисление высказываний

Понятие исчисления

Если в алгебре высказываний изучаются логические операции над множеством логических значений ${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]:

1. $A \to (B \to A)$

2. $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

3. $(A \& B) \to A$

4. $(A \& B) \to B$

5. $A \to (B \to (A \& B))$

6. $A \to (A \vee B)$

7. $B \to (A \vee B)$

8. $(A \to C) \to ((B \to C) \to (A \vee B \to C))$

9. $\neg A \to (A \to B)$

10. $(A \to B) \to ((A \to \neg B) \to \neg A)$

11. $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)

Курс лекций МФТИ по математической логике и теории алгоритмов