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

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

Формальные системы (логика, алгебра, исчисления) дают нам язык, который удивительно хорошо описывает структуру задач реального мира.

Исчисление высказываний не объясняет, почему природа устроена так, а не иначе; оно лишь показывает, как с помощью строгих правил из немногих исходных идей можно получить много нетривиальных следствий, которые потом подтверждаются опытом.

Исчисление высказываний: от философии науки к цифровой инженерии (эссе)#

Помощь в составлении эссе оказала Алиса AI

Почему формализация вообще важна: взгляд Вигнера#

Начнём с большого вопроса: почему математика так хорошо описывает природу? На этот вопрос пытался ответить физик Юджин Вигнер в статье «О непостижимой эффективности математики в естественных науках» (1960).

Вигнер подчёркивал, что математические конструкции, созданные зачастую в отрыве от практики, неожиданно оказываются идеально пригодными для описания широкого класса природных явлений.

Например:

Уравнения Максвелла. Выведенные для известных в XIX веке электрических и магнитных явлений, они позже предсказали существование радиоволн.
Закон всемирного тяготения. Сначала описывал падение тел на Земле, а затем оказался точным инструментом для расчёта орбит планет.

Для нас, изучающих логику, ключевой вывод такой: чтобы использовать эту «эффективность», нужно уметь строго формулировать утверждения и выводить из них следствия. Именно здесь на сцену выходит формальная логика: она даёт однозначный язык и правила вывода, которые позволяют превратить интуитивные идеи в проверяемые утверждения.

Сам факт, что природа так хорошо «ложится» на формальные схемы, — это и есть та самая «непостижимость», о которой говорил Вигнер. А исчисление высказываний — один из самых простых и наглядных инструментов для такой формализации.

Программа Гильберта: стремление к полной формализации математики#

Параллельно с размышлениями о связи математики и реальности в начале XX века развивалась мощная программа по основаниям математики — программа Давида Гильберта.

В чём была суть программы#

Гильберт хотел сделать математику полностью надёжной и прозрачной через полную формализацию:

Формальная система аксиом. Все математические утверждения должны быть записаны как формулы в строго определённом языке.
Чёткие правила вывода. Доказательство — это просто последовательность формул, где каждая следующая получается из предыдущих по формальным правилам.
Доказательство непротиворечивости. Главная цель: доказать, что в такой системе нельзя одновременно вывести утверждение и его отрицание (то есть система не содержит внутренних противоречий).
Полнота. В идеале хотелось бы, чтобы любое истинное утверждение можно было доказать в рамках системы.

Как это связано с нашей темой#

Программа Гильберта напрямую мотивировала развитие математической логики: именно ради этих целей активно исследовались исчисления высказываний и предикатов, формальные доказательства, вопросы разрешимости. Исчисление высказываний здесь — это «пробный полигон»: на нём удобно изучать, как устроены формальные системы, прежде чем переходить к более сложным теориям.

Удар по программе: теоремы Гёделя#

В 1931 году Курт Гёдель доказал свои знаменитые теоремы о неполноте, которые показали принципиальные ограничения формальных систем:

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

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

Проблема разрешимости#

В 1928 году Давид Гильберт и Вильгельм Аккерман в книге «Принципы математической логики» сформулировали задачу, известную как проблема разрешимости (Entscheidungsproblem). Вопрос звучал так: существует ли универсальный алгоритм (эффективная процедура), который для любой заданной формулы в логике первого порядка мог бы за конечное число шагов ответить: «да» (формула общезначима, то есть истинна во всех возможных моделях) или «нет» (не общезначима)? Иными словами, можно ли механически, шаг за шагом, проверять истинность любого математического утверждения, если оно записано в формальном языке?

Гильберт видел в этом ключевой шаг для своей программы по основаниям математики: если такой алгоритм есть, то доказательство теорем сведётся к рутинной механической процедуре — выписал аксиомы, применил правила вывода, и алгоритм сам найдёт доказательство или опровержение.

Кстати, для некоторых частных случаев ответ был положительным. Например, для исчисления высказываний проблему разрешимости решили: там действительно есть эффективный метод (например, построение таблиц истинности). Но Гильберт и Аккерман ставили вопрос шире — для всей логики первого порядка.

Роль работ Тьюринга#

Прорыв случился в 1936 году. Алан Тьюринг опубликовал статью «О вычислимых числах в приложении к проблеме разрешения». Чтобы доказать неразрешимость Entscheidungsproblem, ему пришлось сначала чётко определить, что вообще значит «алгоритм» в математическом смысле. Для этого он ввёл абстрактную модель — машину Тьюринга. Это мысленный эксперимент: устройство с бесконечной лентой, головкой для чтения/записи и таблицей переходов. Ключевая идея: любая интуитивно понятная вычислимая задача может быть смоделирована такой машиной.

Опираясь на эту модель, Тьюринг показал, что проблема разрешимости неразрешима в общем случае. Один из ключевых шагов в его доказательстве связан с так называемой проблемой остановки: можно ли создать алгоритм, который по описанию любой машины Тьюринга и её входным данным определит, остановится ли эта машина или зациклится навсегда? Тьюринг доказал, что такого универсального алгоритма не существует. А поскольку проблему остановки можно свести к проблеме разрешимости, это и показало: не бывает алгоритма, который бы для любой логической формулы гарантированно давал ответ «да» или «нет».

Интересно, что почти одновременно с Тьюрингом аналогичный результат получил Алонзо Чёрч (используя λ-исчисление).

Что это значило#

Результат Тьюринга (и Чёрча) нанёс серьёзный удар по программе Гильберта. Он показал фундаментальное ограничение: в достаточно богатых формальных системах (вроде арифметики натуральных чисел) принципиально не существует механического способа, который бы для всякого утверждения решал, доказуемо оно или нет. Это тесно перекликалось и с теоремами Гёделя о неполноте (1931 год): они уже показали, что в таких системах есть истинные утверждения, которые нельзя доказать внутри самой системы.

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

От слов к символам: Фреге и Буль#

Чтобы формализация работала, нужны чёткие правила. В этом направлении работали два ключевых автора.

Готлоб Фреге развивал строгую систему логики и заложил основы формальных систем. Для темы исчисления высказываний важно, что Фреге показал, как можно строить рассуждения с чёткими правилами вывода, чтобы они были однозначными и воспроизводимыми.

Джордж Буль создал алгебру логики (булеву алгебру), где высказывания — это переменные, а связки («И», «ИЛИ», «НЕ») — операции над ними. Это и есть алгебраический язык исчисления высказываний.

На практике это выглядит так: мы берём простые утверждения и обозначаем их буквами:

$P$: «Система включена»
$Q$: «Дверь открыта»

Тогда сложное утверждение «Система включена и дверь открыта» записывается как $P \,\&\, Q$. А «Система включена или дверь открыта» — как $P\vee Q$.

Важный навык — упрощать такие выражения. Например, с помощью законов де Моргана:

$ \neg (P \,\&\, Q) = \neg P \vee \neg Q $

$ \neg (P \vee Q) = \neg P \,\&\, \neg Q $

Таким образом, Фреге дал «грамматику» формальных рассуждений, а Буль — «арифметику» для высказываний. Вместе они создали аппарат, который позволяет работать с логикой как с точной наукой.

От формул к железу: революция Шеннона#

Следующий шаг — перейти от абстрактных формул к реальным устройствам. Эту связь блестяще показал Клод Шеннон в магистерской диссертации «Символический анализ релейных и переключательных схем» (1938).

Шеннон продемонстрировал, что булева алгебра идеально описывает поведение электрических схем:

Переключатель/контакт — это логическая переменная.
Последовательное соединение контактов — конъюнкция ($A \,\&\, B$): цепь замкнута, только если оба контакта замкнуты.
Параллельное соединение — дизъюнкция ($A \vee B$): цепь замкнута, если хотя бы один контакт замкнут.
Реле с инверсией — отрицание ($\neg A$).

Практический пример#

Представьте схему сигнализации: «Сигнал подаётся, если открыта дверь ИЛИ разбито окно, И при этом система включена».

Обозначим:

$D$: «Дверь открыта»
$W$: «Окно разбито»
$S$: «Система включена»

Формула: $(D \vee W) \,\&\, S$.

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

Именно так формальная логика становится инженерной дисциплиной. Логические вентили (AND, OR, NOT, NAND, NOR) — прямое воплощение булевых операций. Вся цифровая электроника (процессоры, память) построена на этих принципах.

Синтез: как всё это связано#

Давайте соберём картину воедино:

Идея	Автор	Роль в науке и информатике
Математика удивительно хорошо описывает мир	Вигнер	Обоснование ценности формальных моделей: если мир «логичен», формальные системы будут эффективны.
Стремление к полной формализации и доказательству непротиворечивости	Гильберт (с оговоркой Гёделя)	Мотивация для развития математической логики и теории доказательств; фундамент для формальных методов.
Строгие правила вывода и формализация	Фреге	Основа для построения непротиворечивых систем и автоматического вывода.
Алгебра высказываний, операции над истинностными значениями	Буль	Математический аппарат для работы с логическими выражениями и их упрощения.
Применение булевой логики к схемам	Шеннон	Инженерная реализация: логика → схемы → компьютеры.

Мы видим красивую цепочку: философия науки (Вигнер) задаёт вопрос «почему математика работает?», программа Гильберта и логика (Фреге, Буль) даёт инструменты, чтобы эту работу сделать максимально строгой и понятной, а инженерия (Шеннон) показывает, как эти инструменты превращаются в реальные устройства. Исчисление высказываний — это точка пересечения всех трёх направлений.

Мини‑упражнения для закрепления#

Перевод в логику. Дано описание: «Сигнализация срабатывает, если открыта дверь ИЛИ разбито окно, И при этом система включена». Запишите это как формулу и попробуйте её упростить.
Схема по формуле. Дана формула $(A \vee B) \,\&\, \neg C$. Нарисуйте схему из контактов и реле, которая реализует эту логику.
Связь с SAT. Объясните, что задача «найти такие значения переменных, при которых формула истинна» — это и есть задача выполнимости (SAT). Это прямой мост к темам SAT‑солверов, CNF и метода резолюций.

Куда двигаться дальше#

Логика предикатов. Переход от простых высказываний к кванторам и переменным, что нужно для более сложных моделей.
SMT‑солверы. Развитие идей SAT с учётом дополнительных теорий (арифметика, массивы и т. п.).
Нейросимволический ИИ. Современные попытки соединить гибкость нейросетей с жёсткой логикой формальных систем — тема, которая активно развивается сегодня.
Теория доказательств и автоматизация доказательств. Изучение того, как формальные системы используются для проверки математических теорем и программ.

Пример из жизни#

Принципами исчисления высказываний пользуются не только в естественных и технических науках, но и в повседневных делах.

Давайте попробуем придать точную форму житейским рассуждениям.

Краткая справка, что такое вообще исчисление:

Задаётся язык формул, который используется для записи высказываний.
Вводятся аксиомы - исходные формулы, из которых будут выводиться все возможные следствия.
Указываются правила вывода, по которым выводятся новые формулы.

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

Выводить новые формулы можно не только из аксиом, но и из любого множества формул (так называемых гипотез), которые считаются условно истинными.

Пример. Допустим, человек придерживается следующих убеждений: “Если молодой человек и девушка любят друг друга, то они не могут быть не уверены в своих чувствах. Если молодой человек и девушка сожительствуют, то они не уверены в своих чувствах. Если они вступили в брак, то они любят друг друга. Если они не уверены в своих чувствах, то они не вступают в брак.”

Какой вывод он может сделать, если: а) молодой человек и девушка вступили в брак; б) молодой человек и девушка сожительствуют?

Обозначим через $\Gamma$ множество гипотез, которое моделирует систему убеждений, истинных для конкретного человека.

Введем элементарные высказывания:

$a = $ “молодой человек и девушка вступили в брак”
$b = $ “молодой человек и девушка любят друг друга”
$c = $ “молодой человек и девушка сожительствуют”
$d = $ “молодой человек и девушка не уверены в своих чувствах”

Запишем гипотезы:

$b \to \neg d, \;\; c \to d, \;\; a \to b, \;\; d \to \neg a.$

В случае а) добавим к нашему множеству гипотез формулу $a$.

Воспользуемся правилом modus ponens:

$ \dfrac{A \to B, \; A}{B}, $

а также правилом отрицания (modus tollens):

$ \dfrac{A \to B, \; \neg B}{\neg A}. $

Вывод в исчислении высказываний:

$b \to \neg d$ - гипотеза
$c \to d$ - гипотеза
$a \to b$ - гипотеза
$d \to \neg a$ - гипотеза
$a$ - гипотеза
$b$ - MP из 3, 5
$\neg d$ - MP из 1, 6
$\neg c$ - MT из 2, 7

Итак, из гипотез $\Gamma$ (убеждения) и дополнительной гипотезы $a =$ “молодой человек и девушка вступили в брак” вытекает, что:

они любят друг друга ($b$)
они не сожительствуют ($\neg c$)
они не могут быть не уверены в своих чувствах ($\neg d$)

Теперь рассмотрим случай б), когда в качестве гипотезы принята формула $c$.

$b \to \neg d$ - гипотеза
$c \to d$ - гипотеза
$a \to b$ - гипотеза
$d \to \neg a$ - гипотеза
$c$ - гипотеза
$d$ - MP из 2, 5
$\neg a$ - MP из 4, 6
$\neg b$ - MT из 1, 6

Итак, из гипотез $\Gamma$ (убеждения) и дополнительной гипотезы $c =$ “молодой человек и девушка сожительствуют” вытекает, что:

они не вступили в брак ($\neg a$)
они не любят друг друга ($\neg b$)
они не уверены в своих чувствах ($d$)

Из нашего примера видно, как исчисление высказываний помогает механизировать и автоматизировать логические выводы.

Будучи чисто механическим инструментом, исчисление высказываний имеет понятную семантику. Любая формула, выводимая из аксиом в исчислении высказываний, - это тавтология алгебры высказываний. Любая формула, выводимая из гипотез, - это следствие этих гипотез в алгебре высказываний.

С практической точки зрения, исчисление высказываний - удобный инструмент для логического вывода следствий из заданных гипотез.

Схемы аксиом и правило вывода#

В исчислении высказываний описывают множество истинных формул с помощью правил вывода. Буквы, входящие в формулы и обозначающие логические переменные, здесь не заменяют на нули и единицы. Буква в исчислении высказываний означает не любое значение (0 или 1), а любую формулу.

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

$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$

К аксиомам мы еще вернемся, заучивать их наизусть не обязательно.

Основным правилом вывода в исчислении высказываний служит правило заключения (латинское название - modus ponens):

$ \dfrac{A \to B, \; A}{B} $

Данная запись расшифровывается так. Если на место $A$ и $B$ подставить любые формулы, то, если две формулы $A \to B$ и $A$ у нас выведены как истинные, то из них выводится формула $B$.

Если мы приняли, что $A$ влечет $B$, то, зная $A$, заключаем $B$.

Определение. Вывод формулы $A$ - это последовательность формул $A_1, A_2, \ldots, A_n$, в которой $A_n = A$, а все промежуточные формулы $A_i, \, i = 1..n$ - это либо аксиома, либо результат применения правила modus ponens к двум выведенным ранее формулам, т.е. для любого $i = 1..n$ найдутся две формулы $A_j$, $A_k$ ($j < i,\,k < i$) такие, что $A_k = A_j \to A_i$.

Существование возможности вывести формулу $A$ обозначается так: $\vdash A$ (выводимость $A$).

Зачем нужны аксиомы? Почему они именно такие?

В алгебре высказываний мы вводили логические операции с помощью таблиц истинности. В исчислении высказываний, как мы сказали, каждая буква обозначает формулу. Аксиомы нужны для того, чтобы указать, что вообще значат те же значки $\neg, \&, \vee, \to$. То есть мы заходим в ту же науку с другого ракурса - с точки зрения формальной аксиоматической теории.

Что это нам даёт? Иной механизм вывода и обоснования логических следствий, не требующий подстановки на место букв всевозможных значений переменных. Исчисление высказываний похоже на то, как мы рассуждаем (в математике и вообще в жизни). Алгебра высказываний удобнее компьютеру - каждая булева переменная имеет значение 0 или 1. Исчисление высказываний должно помочь нам работать с компьютером (например, делать логические выводы о программном коде).

Аксиомы с импликацией (А1, А2)#

Аксиома 1: $A \to (B \to A)$

Можно назвать её аксиомой добавления посылки (переход к частному случаю).

Давайте внимательно посмотрим на эту формулу. Что она означает? Если $A$ истинно, то, если вдобавок будет выполнено $B$ (частный случай), утверждение $A$ останется в силе. То есть наше первоначальное знание истинности $A$ никуда не исчезает.

Примеры.

Все люди любят спать ($A$). Следовательно, все преподаватели ($B$) любят спать.
Всё на огороде съедобно ($A$). Следовательно, сорняки ($B$) тоже съедобны.
Если злоумышленник решил слить на кого-нибудь компромат ($A$), то он всё равно это сделает, даже если ему заплатят ($B$).

Аксиома 2: $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$

Эта аксиома указывает на возможность провести логический вывод в частном случае ($A$). Назовём её аксиомой транзитивности импликации.

По смыслу аксиома 2 означает следующее. Допустим, мы знаем, что из $A$ и $B$ следует $C$. Тогда, если из $A$ следует $B$ ($A$ “сильнее” $B$), то из $A$ следует $C$.

Примеры.

Летом ($A$) в жару ($B$) быстро потеешь ($C$). Следовательно, если летом жарко ($A \to B$), то летом быстро потеешь ($A\to C$).
Если вода камень точит, то она его мочит. А если вода камень мочит, то он мокрый.

Пусть $A = $ “вода камень точит”, $B = $ “вода камень мочит”, $C = $ “камень мокрый”.

Из того факта, что вода камень точит, напрямую не вытекает, что камень мокрый! Благодаря аксиоме 2 мы знаем, что если $A \to B$ и $B \to C$, то $A \to C$.

Из первых двух аксиом выводится хитрая теорема: $A \to A$.

Она не настолько очевидна. Ведь на месте $A$ может находиться любая формула! А про значок $\to$ в нашей новой теории мы знаем только то, что он функционирует согласно аксиомам 1 и 2. Функционирование теории не обязано автоматически соответствовать нашему опыту! Математическая модель не обязана описывать всё на свете с абсолютной точностью. Только исследуя нашу формальную теорию с помощью математических выводов, нам удастся понять, как она в действительности работает. Включите здоровый скепсис, и пойдём дальше.

Первое правило логики - следить за своими высказываниями.

Давайте построим вывод (доказательство) теоремы $A \to A$. Напомним, что в аксиомах 1, 2 на место букв можно подставить любые формулы.

Согласно аксиоме 1 [$A := A$, $B := A$],

$ A \to (A \to A) $

(эту формулу мы вывели из первой схемы аксиом)

Согласно аксиоме 2 [$A := A$, $B := (A \to A)$, $C := A$],

$ (A \to ((A \to A) \to A)) \to ((A \to (A \to A)) \to (A \to A)) $

Согласно аксиоме 1 [$A := A$, $B := (A \to A)$],

$ A \to ((A \to A) \to A) $

Применяя modus ponens к формулам 2, 3, откусываем заведомо истинную посылку и приходим к следствию:

$ (A \to (A \to A)) \to (A \to A) $

Применяя modus ponens к формулам 1, 4, откусываем истинную посылку и делаем вывод:

$A \to A$

Теорема о дедукции#

Из аксиом 1, 2 получается дополнительное правило вывода - правило введения импликации.

Сперва поясним идею, не обращаясь к формулам.

Вспомните себя, когда вы были абитуриентом и выбирали вуз и направление для поступления. Вы рассуждали: вот поступлю на ИТ-специальность, тогда… И дальше вы делали выводы из своего дополнительного предположения - как будто вы уже поступили на ИТ-специальность.

Вы могли долго фантазировать, рассуждать, предполагать… Но в конечном итоге делали вывод: “если я поступлю туда-то, то мне следует ожидать того-то” - вы делали условное умозаключение.

Пусть $\Gamma$ - это ваши гипотезы, то есть набор предположений. Формула $A$ - это дополнительное предположение (условие), например: “я поступил(а) на ИТ-специальность”. В ходе рассуждений из гипотез $\Gamma,\, A$ вы делаете вывод. Обозначим формулу - результат вывода - через $B$.

Коротко ваш вывод можно записать так: $\Gamma, A \vdash B$.

По правилу введения импликации, отсюда следует такой вывод условного высказывания: $\Gamma \vdash A\to B$.

То есть, если спуститься на землю и оставить в стороне дополнительные допущения (типа $A = $ “я поступил в университет”), вы, однако, обладаете определенным знанием - результатом собственного умозаключения. Вы имеете право сказать слово “если”. Если $A$ (поступлю в университет), то $B$ (буду хорошо учиться).

Коротко правило введения импликации записывается так:

$ \dfrac{\Gamma, A \vdash B}{\Gamma \vdash A \to B} $

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

Правила вывода с импликацией#

modus ponens (с гипотезами), правило введения импликации, правило сечения - расписать алгоритм получения вывода из квазивывода

Правило рассуждения от противного (А10)#

Рассуждением от противного мы пользуемся тогда, когда внезапно приходим к выводу, который не стыкуется с нашими представлениями.

Пример. Покупатель платит в супермаркете на кассе самообслуживания. Он уверен, что отсканировал штрих-коды на всех продуктах. Если всë отсканировано, то автомат примет платеж. Из этих гипотез вытекает, что покупка состоится. Но внезапно автомат подает сигнал ошибки. Это не стыкуется, противоречит нашим представлениям. Значит, они ошибочны.

Программная реализация#

В электронном ресурсе размещён тренажер по исчислению высказываний.

Литература#

Материалы для самостоятельного изучения

Вопросы к коллоквиуму по теме#

Обоснуйте правило удаления импликации.

Обоснуйте правило введения посылки.

Обоснуйте правило транзитивности.

Обоснуйте правило введения конъюнкции.

Обоснуйте правило удаления конъюнкции.

Обоснуйте правило соединения посылок.

Обоснуйте правило разъединения посылок.

Обоснуйте правило введения дизъюнкции.

Обоснуйте правило удаления дизъюнкции (разбор случаев).

Обоснуйте правило исчерпывающего разбора случаев.

Обоснуйте правило введения отрицания (рассуждение от противного).

Обоснуйте правило вывода из противоречия.

Обоснуйте правило навешивания двойного отрицания.

Обоснуйте правило снятия двойного отрицания.

Обоснуйте правило modus tollens.