Натуральный вывод

Таблица выносит приговор, вывод показывает дорогу

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

forall x: Calgary, гл. 15 «The very idea of natural deduction». Генцен, 1934/35 · 22 мин · обновлено 06.09.2026

На доске формула, и в ней десять разных букв, а вопрос к ней простой: бывает ли она ложной? Способ ответить у нас уже есть: выписать таблицу истинности и просмотреть все строки подряд. Метод честный и не требует ни капли изобретательности.

Строк будет 1024.

Это не преувеличение. Каждая новая буква удваивает число случаев: одна буква даёт две строки, две буквы дают четыре, три дают восемь. Десять букв дают 1024 строки. Вечер уйдёт, и это ещё лучший из плохих исходов: двадцать букв дают больше миллиона строк, тридцать больше миллиарда.

Но главная неприятность не в размере. Досчитанная таблица говорит одно слово: «да» или «нет», а на вопрос, почему да, она молчит. Этот модуль строит второй инструмент, который не перебирает случаи вовсе: он предъявляет дорогу от посылок к заключению по шагам, и каждый шаг назван по имени.

Цена перебора

Посчитаем рост честно, на маленьких числах. Одна буква даёт два случая: истинна или ложна. Добавили вторую, и каждый прежний случай раздвоился, стало четыре, а третья буква даёт восемь. Правило простое: n букв дают 2ⁿ строк, где 2ⁿ читается «два в степени n».

Числа отсюда выходят такие. Четыре буквы дают 16 строк, это ещё лист бумаги. Десять букв дают 1024 строки, двадцать больше миллиона, тридцать больше миллиарда. Двадцать условий в расписании смен или в договоре встречаются постоянно, и это не выдумка для устрашения.

Возражение напрашивается: пусть считает машина. Машина и правда считает быстро, и до какого-то размера это работает. Только вопрос «выполнима ли формула» и есть та самая задача, на которой Стивен Кук в 1971 году впервые доказал NP-полноту. Что стоит за этим словом, объясняет теория сложности, и в курс этот разговор не входит. Урок 20 назовёт результат и на том остановится. Здесь достаточно одного: способа, который был бы быстрым сразу для всех формул, никто не предъявил.

Второй довод: таблицы кончаются

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

Таких миров бесконечно много, и перебрать их нельзя ни за вечер, ни за век, ни машиной. И это не лень исследователей: в 1936 году Чёрч и Тьюринг независимо доказали, что общего механического способа проверить следование в логике первого порядка не существует. Одно утешение всё же есть, и оно как раз про вывод. Если заключение действительно следует, машина рано или поздно вывод найдёт, а если не следует, может искать вечно. Отсюда простое следствие: там, где таблицы кончаются, вывод остаётся единственным инструментом. Подробности ждут урока 20, а здесь важно только, что модуль IV строится не от скуки.

Третий довод: путь вместо приговора

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

Его можно проверить по частям. Каждая строка проверяется отдельно от прочих, и ошибка ищется не во всём рассуждении, а в одной строке.

В нём видно место поломки. Если в выводе ошибка, она сидит в конкретной строке, и на эту строку можно показать пальцем. Таблица на вопрос «где именно я не прав» не отвечает никак.

Его куски переносятся. Доказав однажды переход от «если A, то B» и «не B» к «не A», им пользуются во всех дальнейших выводах, и заново он не строится.

Его можно понять. Вывод объясняет, почему следует, а не только что следует. Человек, прочитавший вывод, уносит с собой приём, а не факт.

Аналогия. Таблица выдаёт справку «доехать можно», а вывод выдаёт маршрут: улицы, повороты, номер автобуса.

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

Как выглядит вывод

Договоримся о записи, дальше она понадобится в каждом уроке модуля. Вывод представляет собой столбик пронумерованных строк, и в каждой строке три вещи. Номер задаёт счёт сверху вниз, чтобы на строку можно было сослаться. Формула показывает, что на этой строке получено. Обоснование называет правило и номера строк, из которых оно взято.

Первые строки обычно ничем не обоснованы: это посылки, они даны условием. В обосновании так и пишут: «посылка». Такая запись придумана не сразу. Правила парами придумал Герхард Генцен в 1934-1935 годах, а привычный нам столбик с блоками появился позже: его предложил Фредерик Фитч в 1950-е.

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

Одну деталь записи стоит увидеть заранее: часть строк бывает сдвинута вправо и отчёркнута вертикальной чертой. Черта означает, что эти строки живут внутри допущения, то есть предположения, взятого на пробу. Такие блоки появятся в уроке 12, и без них вывод остаётся половиной инструмента. Пока достаточно знать, что сдвиг вправо не украшение: он часть обоснования, ведь строка внутри блока опирается на допущение, а строка вне блока не опирается.

Разбор по шагам: цепочка из трёх посылок

Разберём один вывод целиком, не пропуская ничего. Уговор такой: если придёт Аня, придёт и Боря, а если придёт Боря, придёт и Вера. Аня придёт. Хотим получить: придут и Боря, и Вера.

Сначала ключ перевода: пусть P обозначает «Аня придёт», Q обозначает «Боря придёт», R обозначает «Вера придёт». Тогда посылки записываются так. Первая, P → Q, читается: не бывает так, чтобы Аня пришла, а Боря нет. Вторая, Q → R, читается: не бывает так, чтобы Боря пришёл, а Вера нет. Третья, просто P, означает «Аня придёт». Цель записывается как Q ∧ R и читается: Боря пришёл и Вера пришла.

1. P → Q (посылка).
2. Q → R (посылка).
3. P (посылка).
4. Q (→E 1, 3).
5. R (→E 2, 4).
6. Q ∧ R (∧I 4, 5).

Теперь то же самое словами, по одной строке. Строки 1-3. Посылки. Обосновывать их нечем и не нужно: они даны условием задачи.

Строка 4. Правило →E, оно же modus ponens. Берём строку 1 («если P, то Q») и строку 3 («P»). Получаем Q. Словами: уговор про Аню и Борю плюс приход Ани дают приход Бори.

Строка 5. То же правило →E, но теперь по строкам 2 и 4. Строка 4 нам не была дана, мы её только что добыли. Ссылаться на добытое разрешено, в этом весь смысл цепочки.

Строка 6. Правило ∧I. Из двух отдельных строк, 4 и 5, собирается одна: Q ∧ R.

Заключение стоит на строке 6, и путь к нему виден целиком: ни один шаг не оставлен без имени, у каждого есть правило и ссылки. Соблазн сократить тут велик: из уговоров и прихода Ани сразу видно, что придут все. Зачем расписывать четыре строки?

Затем, что «видно» проверить нельзя, а проверить можно только названное правило и названные строки. Как только в выводе появляется шаг без имени, проверка на этом месте останавливается, и дальше начинается доверие. Есть и практическая причина: в шести строках сокращение безобидно, в тридцати оно прячет ошибку. Ошибки как раз и заводятся там, где рука пошла быстрее головы. Правила →E и ∧I здесь только применены, а откуда они берутся и почему им можно верить, разбирает урок 11.

Правило ничего не понимает

У правил вывода есть свойство, которое поначалу раздражает, а потом оказывается главным их достоинством: правило смотрит на устройство формулы и больше ни на что. Правило →E требует буквально следующего: одна строка вида «стрелка», вторая строка, совпадающая с началом стрелки знак в знак. Не «по смыслу то же самое». Не «почти то же». Знак в знак.

Возьмём случай, где разница видна. На строке 1 стоит P → Q, то есть не бывает так, чтобы P, а Q нет. На строке 3 стоит Q ∧ P, то есть верно и Q, и P. Человек скажет: но ведь Q ∧ P содержит P, значит стрелку применить можно. Правило скажет: нет. Перед стрелкой стоит P, а на строке 3 стоит Q ∧ P, и это другая формула.

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

Тому, кто привык рассуждать словами, первые выводы кажутся мучительно мелочными. Это ощущение проходит, и проходит быстро. Остаётся другое: привычка замечать, что шаг, казавшийся одним, на деле состоял из трёх.

Два знака, которые нельзя путать

У нас теперь два разных способа сказать «отсюда следует», и знаки у них разные. Знак ⊨ говорит о случаях. Запись «P → Q, P ⊨ Q» читается так: нет ни одного случая, где обе посылки истинны, а Q ложно. Проверяется это таблицей. Знак ⊢ говорит о выводе. Запись «P → Q, P ⊢ Q» читается так: из этих посылок Q выводимо, то есть существует столбик строк вроде того, что мы только что построили. Вопросы эти разные до основания: первый спрашивает обо всех случаях сразу, второй о существовании одной конкретной записи.

Слить их в один соблазнительно, и делать этого нельзя. Вот почему. Представьте, что кто-то добавил в систему правило: «из A → B и B получается A». Выглядит невинно, а это подтверждение следствия, то есть форма, у которой есть контрпример. С таким правилом ⊢ начнёт выдавать то, что по ⊨ не следует. Знак ⊢ зависит от набора правил: меняем правила, и меняется ответ, а знак ⊨ не зависит ни от чего, кроме значений истинности. То, что для нашей системы оба знака дают один и тот же ответ, не заложено ни в записи, ни в определениях. Это две отдельные теоремы, и разбирает их урок 18.

Ещё одна запись пригодится в уроке 12. Слева от ⊢ иногда не стоит ничего вовсе: «⊢ A». Читается это так: A выводимо без всяких посылок. Такое A истинно при любых значениях букв, а вывод его добывает из воздуха, точнее, из одних только правил. Звучит странно, а делается просто: берут допущение, доводят его до конца и закрывают, а как именно, покажет урок 12.

Асимметрия, вывернутая наизнанку

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

У вывода всё зеркально.

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

Практический порядок отсюда получается такой. Если кажется, что следует, ищите вывод. Если кажется, что не следует, ищите строку-контрпример. И ещё одно, для честности: пока вывод найден, но не проверен, он ничего не закрывает. Найти и проверить не одно и то же.

Что дальше

Правил вывода у нас пока два, и взялись они ниоткуда. Урок 11 разбирает весь набор и показывает, что он не случаен. У каждой связки ровно два правила: как её получить и как ею воспользоваться. Урок 12 добавляет допущение, без которого вывод остаётся игрушкой, и это самое трудное место курса. Там же стоит тренажёр, который проверяет каждый ваш шаг и не пропускает неточных ссылок. Урок 13 разбирает один длинный вывод целиком, вместе с двумя тупиками, в которые пришлось зайти по дороге.

Вопросы для самопроверки

Что читать

• forall x: Calgary, гл. 15 «The very idea of natural deduction»: Там объяснено, зачем натуральный вывод понадобился рядом с таблицами. Читается легко и почти без символов, и прочесть его полезно до урока 11, а не после.
• Герхард Генцен, «Untersuchungen über das logische Schließen», 1935: Работа, с которой начался натуральный вывод. Читать целиком не нужно и трудно. Стоит открыть ради одного: увидеть, что приём, которым мы пользуемся, придуман один раз и довольно недавно.
• Тренажёр «Построитель вывода» в уроке 12: Заглянуть в него можно уже сейчас, чтобы увидеть запись живьём. Решать задачи пока рано: правила разбираются в уроках 11 и 12.