Длинное доказательство целиком

Вместе с двумя тупиками, в которые пришлось зайти по дороге

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

forall x: Calgary, гл. 17 «Constructing proofs». Де Морган, «Формальная логика», 1847 · 28 мин · обновлено 06.09.2026

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

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

Задача

Условие бытовое. Мне говорят: «Неверно, что будет дождь или снег». Что отсюда следует? Понятно что: дождя не будет и снега не будет. С этим согласится каждый, и в этом вся трудность: согласиться легко, а собирать доказательство не из чего, потому что шаг кажется одним и неделимым.

Ключ перевода такой. Пусть P означает «будет дождь», а Q означает «будет снег». Посылка записывается как ¬(P ∨ Q) и читается: неверно, что будет дождь или снег. Цель записывается как ¬P ∧ ¬Q и читается: дождя не будет и снега не будет.

Это половина закона де Моргана: целиком закон говорит, что «ни то, ни другое» и «не то и не это» значат одно и то же. Названы законы по Огастесу де Моргану, хотя известны были и раньше, в частности Уильяму Оккаму в XIV веке. Инструменты у нас те же, что были: правила уроков 11 и 12, ничего нового.

Тупик первый: вперёд от посылки

Почти каждый начинает одинаково: смотрит на посылку и пробует хоть что-нибудь из неё добыть. Ход разумный: посылка у нас одна, других строк нет вовсе, начинать больше не с чего. Переберём по очереди все правила, какие есть.

Правило ∧E убирает «и», а снаружи в ¬(P ∨ Q) стоит отрицание, а не «и», так что оно не подходит. ДС требует строки вида «A или B», но снаружи опять отрицание: вся формула есть «не», а «или» спрятано внутри скобок, и он тоже не подходит. Правила →E и МТ требуют строки со стрелкой, а стрелки нет ни одной, так что не подходят и они. Правило ∨I работает от любой строки, и применить его можно. Получим, например, строку ¬(P ∨ Q) ∨ P, читается она: либо неверно, что дождь или снег, либо дождь. Формула законная и совершенно бесполезная, потому что уводит от цели, а не к ней.

¬E. Вот единственное правило, которое всерьёз берётся за отрицание, и требует оно пары: строки ¬A и строки A. У нас есть ¬(P ∨ Q), значит, для пары нужна строка P ∨ Q, то есть «будет дождь или снег». Её нет. Тупик: из посылки не сделать ни одного полезного шага вперёд.

Тренажёр урока 12 в этом месте отвечает коротко и по делу. На ∧E он скажет, что убрать «и» можно только из конъюнкции, а на ДС ответит, что нужна строка вида A ∨ B. Отказы эти стоит прочитать внимательно, а не отмахнуться, потому что каждый из них называет, чего именно не хватает, и тем самым подсказывает следующий шаг.

Вывод отсюда не «задача нерешаема», а другой: начинать надо не с посылки. Это первый приём урока, и добыт он неудачей: тупик не пропал даром, а сузил поиск вдвое.

Приём: смотреть на цель

Развернёмся и посмотрим на то, куда идём. Цель: ¬P ∧ ¬Q. Какая связка стоит в ней снаружи? Знак «и», а вводит «и» правило ∧I. Значит, последним шагом вывода будет ∧I, и для него нужны две строки: ¬P и ¬Q.

Задача только что развалилась на две поменьше, и каждая из них есть подцель. Продолжим тем же приёмом: у подцели ¬P снаружи стоит отрицание, а вводит отрицание правило ¬I, значит, надо открыть блок, допустить P и дойти до ⊥. То же самое с подцелью ¬Q: блок, допущение Q, ⊥.

Посмотрите, что произошло. Мы не написали ни одной строки вывода, а план готов целиком: два блока и сборка в конце. Приём этот работает почти всегда, и формулируется он одной фразой. Какая связка стоит в цели снаружи, такое правило введения и понадобится последним.

Тупик второй: ⊥ не складывается

Начинаем первый блок: открываем его и допускаем P. Что доступно внутри? Строка с посылкой стоит снаружи, но блок закрывает выход, а не вход. Итак, внутри блока у нас две строки: P и ¬(P ∨ Q).

Цель внутри блока есть ⊥, а даёт ⊥ правило ¬E: из формулы и её отрицания. Строка с отрицанием есть, строка без отрицания есть. Готово? Нет. И вот здесь спотыкаются даже те, кто всё понял.

Правило ¬E требует, чтобы под отрицанием стояла в точности та же формула, что и во второй строке. У нас под отрицанием стоит P ∨ Q, а во второй строке стоит просто P, и это разные формулы. Тренажёр на такую попытку отвечает прямо: нужны формула и её отрицание. Не «похожая формула». Не «формула, которая в ней содержится».

Тупик второй: пара не складывается, ⊥ не получается, блок не закрывается. Здесь очень хочется сказать: но ведь и так понятно, что противоречие есть. Понятно человеку, а правило понимает только совпадение знак в знак, и в этом его единственное достоинство: понимающее правило понимало бы иногда неправильно.

Подогнать формулу под правило

Выход из второго тупика короткий, и это самый поучительный момент модуля. Раз правилу нужна строка P ∨ Q, надо её раздобыть, а у нас есть P и есть правило, которое из A делает A ∨ B при любом B. Это ∨I, то самое правило, что в уроке 11 выглядело нелепой поблажкой: «Идёт дождь, значит идёт дождь или Луна из сыра».

Вот здесь оно и окупается. Из P получаем P ∨ Q, и вторую часть выбираем не с потолка, а нарочно: именно Q, чтобы формула совпала с той, что стоит под отрицанием. Теперь пара складывается: строка P ∨ Q и строка ¬(P ∨ Q) совпадают знак в знак, и правило ¬E даёт ⊥.

Приём стоит запомнить в общем виде. Если правило не подходит к строкам, посмотрите, нельзя ли подогнать строку под правило. Чаще всего подгоняют именно ослаблением: сильная строка правилу не подходит, а ослабленная подходит, потому что правило требует совпадения, а не силы.

Вывод целиком

Теперь всё складывается, и вывод пишется без остановок.

1. ¬(P ∨ Q) (посылка)
2. │ P (допущение)
3. │ P ∨ Q (∨I 2)
4. │ ⊥ (¬E 3, 1)
5. ¬P (¬I 2, 4)
6. │ Q (допущение)
7. │ P ∨ Q (∨I 6)
8. │ ⊥ (¬E 7, 1)
9. ¬Q (¬I 6, 8)
10. ¬P ∧ ¬Q (∧I 5, 9)

Разберём построчно, ничего не пропуская. Строка 1. Посылка стоит вне блоков и потому доступна везде до конца вывода.

Строка 2. Открываем блок и допускаем P. Так требует подцель ¬P: допускать надо то же самое без отрицания.

Строка 3. Правило ∨I по строке 2: ослабляем P до P ∨ Q. Вторая часть взята не случайно, а ради совпадения с посылкой.

Строка 4. Правило ¬E по строкам 3 и 1: формула P ∨ Q и её отрицание дают ⊥. Заметьте, что строка 1 лежит снаружи блока и это разрешено.

Строка 5. Закрываем блок правилом ¬I: допустили P, дошли до ⊥, значит ¬P. Строка стоит уже вне блока и на допущение не опирается.

Строка 6. Открываем второй блок и допускаем Q. Первый блок закрыт, его строки 2-4 недоступны, и они нам больше не нужны.

Строка 7. Правило ∨I по строке 6. На этот раз Q ослабляем до P ∨ Q. Формула та же, только Q попало во вторую часть, а не в первую.

Строка 8. Правило ¬E по строкам 7 и 1, и снова ⊥.

Строка 9. Закрываем второй блок правилом ¬I. Получаем ¬Q вне блока.

Строка 10. Правило ∧I по строкам 5 и 9. Обе доступны: они на нулевой глубине. Собираем цель.

Возникает законный вопрос: нельзя ли сэкономить и провести оба доказательства в одном блоке? Нельзя, и причина в устройстве блока: он закрывается одним допущением и даёт снаружи одну строку, так что, допустив P, мы получим ¬P и больше ничего. Строка ¬Q требует своего допущения, а второе допущение внутри первого блока открыло бы вложенный блок, и закрытие дало бы стрелку, а это не то, что нужно.

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

Почему нельзя написать «аналогично»

Строки 6-9 повторяют строки 2-5 буква в букву, и разница только в том, что вместо P стоит Q. В человеческом тексте здесь пишут «аналогично для второй части», и это законное сокращение: читатель проверит сам, если захочет. В формальном выводе так нельзя: строки должны быть выписаны все. Причина не в занудстве: вывод проверяется механически, сверяются правило и ссылки, а слово «аналогично» проверке не поддаётся, потому что проверять в нём нечего.

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

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

Приёмы поиска, собранные вместе

Соберём в одно место всё, что показал этот вывод. Первый: смотреть на цель. Какая связка стоит в цели снаружи, такое правило введения и понадобится последним: «и» значит ∧I, стрелка значит →I, отрицание значит ¬I. Второй: при цели со стрелкой начинать с допущения. Почти без исключений: допускают левую часть и идут к правой.

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

Пятый: подгонять строку под правило. Если не складывается ¬E, сделайте из имеющейся строки ту формулу, которая стоит под отрицанием: ослабление через ∨I держат в системе ровно для этого. Шестой: проверять доступность вслух. Больше всего испорченных выводов получается из-за ссылки на строку внутри закрытого блока.

Первый приём работает только при верном чтении формулы: связка снаружи в ¬P ∧ ¬Q есть «и», а не «не», хотя отрицаний в записи два. Ошибка чтения ведёт к правилу, которое не сработает, и тупик получается на ровном месте, так что, прежде чем выбирать правило, полезно вслух назвать, какая связка стоит снаружи. Приёмы эти не алгоритм: они сужают перебор, а не отменяют его. Механического способа найти вывод не существует, и в уроке 20 будет сказано, почему именно.

Честный итог

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

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

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

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

А дальше курс сворачивает в сторону, потому что логика высказываний упирается в потолок: она не видит слов «все» и «некоторые». Самое известное рассуждение в истории (про Сократа и смертность) нашему аппарату не по зубам, и урок 14 начинается ровно с этого. Что с потолком сделали в 1879 году, разбирает весь модуль V.

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

Что читать

• forall x: Calgary, гл. 17 «Constructing proofs»: Главный источник практики. Двадцать решённых задач стоят любого объяснения, и это не фигура речи: умение находить вывод берётся повторением, а не пониманием правил.
• Тренажёр «Построитель вывода» в уроке 12, второй заход: Те же семь задач после этого урока проходятся иначе, а седьмая из них и есть та самая, которую мы сейчас разобрали. Полезно засечь время на первой попытке и на второй: разница показывает, что именно приобретается практикой.
• Open Logic Project, раздел о натуральном выводе: Открытый учебник под лицензией CC BY 4.0, уровень «после вводного курса». Те же правила изложены строго, вместе с доказательствами о самой системе. Открывать стоит после урока 18, а не сейчас.