Правила вывода

У каждой связки ровно два правила, и это не список для зубрёжки

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

forall x: Calgary, гл. 16 «Basic rules for TFL». Генцен, 1934/35 · 24 мин · обновлено 06.09.2026

В рюкзаке у меня зонт и термос.

Отсюда следует, что у меня есть зонт, и это до того просто, что кажется не шагом, а пересказом. Теперь наоборот. Я знаю, что у меня есть зонт, и отдельно знаю, что у меня есть термос. Отсюда следует, что у меня есть зонт и термос.

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

Мысль Генцена

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

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

Что значат буквы в схеме правила

Правило записывают схемой, и в схеме стоят буквы A и B. Понимать их надо правильно, иначе половина выводов не построится. A и B не буквы языка вроде P и Q. Это места, куда подставляют любую формулу, хоть самую длинную.

Пример. Правило ∧I: из A и B получается A ∧ B. Пусть на строке 4 стоит P → Q, а на строке 7 стоит ¬R. Тогда ∧I даёт (P → Q) ∧ ¬R, и читается это так: верно и «если P, то Q», и «не R».

Требование при этом ровно одно: одинаковые места заняты одинаковым, и если A в схеме встретилось дважды, оба раза стоит одна и та же формула. Разными A и B быть не обязаны: из P и P правило ∧I честно даёт P ∧ P. Читается это так: верно P и верно P. Пользы немного, но запрета нет.

Есть и обратная сторона, на которой спотыкаются чаще всего: правило удаления смотрит только на связку, стоящую снаружи. Возьмём строку P → (Q ∧ R), читается она: не бывает так, чтобы P было, а Q и R вместе не выполнялись. Знак ∧ в этой формуле есть, он виден невооружённым глазом, и правило ∧E к ней всё равно неприменимо.

Причина простая: снаружи здесь стоит стрелка, а «и» спрятано внутри скобок, и строка целиком есть стрелка, а не конъюнкция. Чтобы добраться до Q ∧ R, надо сначала убрать стрелку правилом →E, а для этого нужна отдельная строка с P. Приём отсюда получается такой. Прежде чем брать правило, спросите: какая связка стоит в этой строке снаружи? Она и определяет, какие правила к строке применимы.

«И»: два правила

Начнём с той пары, с которой начался урок. Введение, ∧I. Есть строка A, есть строка B, значит можно написать A ∧ B. Словами: зонт есть, термос есть, значит есть зонт и термос.

Удаление, ∧E. Есть строка A ∧ B, значит можно написать A. Или можно написать B. Что именно брать, решает тот, кто строит вывод, и тут стоит остановиться, потому что выбор не безразличен. Если нужна первая часть, берите первую. Если нужны обе, применяйте ∧E дважды, отдельными строками. Одной строкой две вещи не получить: в строке стоит ровно одна формула.

Заметьте и то, чего ∧E не позволяет. Из P ∧ Q нельзя получить P ∧ R, нельзя получить Q ∨ P, нельзя получить «примерно то же самое». Разрешена одна из двух частей, целиком и без изменений: правило убирает связку, а не заменяет её на другую.

Повтор, который берут в долг

Есть правило, которое поначалу выглядит издевательством. Повтор, R. Есть строка A, значит можно написать A ещё раз. Никакой новой мысли в этом нет и не предполагается: формула та же, номер новый. Зачем оно тогда? Затем, что в уроке 12 появятся блоки, и закрывают блок по его последней строке. Бывает, что нужная формула уже стоит выше, а поставить её надо в конец блока. Вот тогда её и повторяют. Пока это единственное правило курса, которое приходится принять в долг, и долг вернётся в следующем уроке.

«Или»: введение, которое выглядит нелепо

Правило ∨I звучит так: есть строка A, значит можно написать A ∨ B, и B при этом любое. На бытовом языке это выглядит дико. «Аня пришла. Значит, Аня пришла или Боря выиграл в лотерею». Возражение возникает сразу: откуда взялась лотерея, о ней речи не было.

Разберём медленно, потому что здесь интуиция даёт уверенный и неверный ответ. Что утверждает «A или B»? Ровно одно: хотя бы одно из двух истинно, а какое именно, связка не сообщает. Значит, чтобы «A или B» было истинным, достаточно истинности A, и наличие B не требуется ни в каком виде.

Проверим на Ане. Аня пришла. Истинно ли «Аня пришла или Боря выиграл в лотерею»? Да, первая часть истинна, и этого хватает. Случая-провала нет. Странность идёт не от логики, а от речи: говоря «или», человек обычно сообщает, что не знает, какая часть верна, а логическое ∨ такого сообщения не несёт. И надо честно сказать, что при этом происходит. Переходя от A к A ∨ B, вы ослабляете утверждение: знали больше, записали меньше.

Зачем ослаблять нарочно, станет ясно через несколько строк.

«Или»: как его убирают

Бытовой случай. Ключи лежат в куртке или в сумке. В куртке их нет, значит, в сумке. Это дизъюнктивный силлогизм, в записи ДС: из A ∨ B и ¬A получается B. Проверьте вслух: «хотя бы одно из двух» плюс «не первое» даёт «второе», и деваться дизъюнкции больше некуда. Порядок ссылок здесь важен: сначала называют строку с «или», потом строку с отрицанием, а в обратном порядке правило не срабатывает.

Теперь видно, зачем ослаблять нарочно. Разберём вывод целиком. Посылки: P и ¬P. Читается это так: идёт дождь, дождя нет. Цель: Q, то есть что угодно.

1. P (посылка).
2. ¬P (посылка).
3. P ∨ Q (∨I 1).
4. Q (ДС 3, 2).

Строки 1 и 2. Посылки, отрицающие друг друга.

Строка 3. Правило ∨I по строке 1. Ослабляем P до P ∨ Q. Буква Q взята с потолка, и правило это прямо разрешает.

Строка 4. Правило ДС по строкам 3 и 2. «P или Q» плюс «не P» даёт Q.

Готово: из противоречия получено произвольное Q, за два шага. Это тот самый ex falso quodlibet из урока 9, теперь не таблицей, а выводом, и ослабление, казавшееся бессмысленным, оказалось единственным способом сдвинуться с места. Запомнить стоит приём, а не пример: ослабляют тогда, когда ослабленное сцепляется с другой посылкой. Сила сама по себе бесполезна, если её не с чем соединить.

Стрелка: половина пары

Удаление, →E. Есть строка A → B, есть строка A, значит можно написать B. Бытовой случай знаком с урока 6: «Если сдам экзамен, поставлю кофе». Экзамен сдан. Значит, кофе будет. Это правило известно под именем modus ponens и есть в каждой системе вывода, какую ни возьми. Порядок ссылок и здесь важен: сначала строка со стрелкой, потом строка с её началом. И требование буквальности: то, что стоит перед стрелкой, обязано совпасть со второй названной строкой знак в знак.

А где же правило введения для стрелки?

Его в этом уроке не будет, и это не забывчивость: чтобы получить «если A, то B», надо что-то сделать с A, а именно допустить его на пробу. Допущение представляет собой отдельную машинерию, и ей посвящён весь следующий урок. Так что таблица правил у нас пока с дыркой, и дырка эта в самом интересном месте.

Разбор по шагам: разобрать, обменять, собрать

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

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

Строки 1 и 2. Посылки, даны условием.

Строка 3. Правило ∧E по строке 1. Из «Аня и Боря» берём «Аня».

Строка 4. Снова ∧E по той же строке 1, но теперь берём вторую часть. Две части дают две строки, иначе никак.

Строка 5. Правило →E по строкам 2 и 3. Стрелка «если Аня, то Вера» плюс «Аня» дают «Вера».

Строка 6. Правило ∧I по строкам 5 и 4. Собираем «Вера» и «Боря» в одну формулу.

Обратите внимание на последнюю строку: порядок ссылок для ∧I безразличен, а порядок частей в результате важен. В цели R стоит первым, значит и в строке 6 оно первое. И заметьте, что вышло с посылкой 1: мы разобрали её на части, а потом одну часть собрали обратно, но уже в другой компании. Это обычная работа вывода: разобрать, обменять, собрать. Почти любой вывод состоит из этих трёх движений.

Порядок строк 3 и 4 можно поменять местами, и вывод от этого не пострадает: строка 4 нигде не опирается на строку 3. А вот строку 5 раньше строки 3 поставить нельзя: она на неё ссылается, а ссылок на будущее не бывает. Отсюда полезное наблюдение о выводах вообще: строгий порядок задан не всеми строками, а только цепочками ссылок. Всё остальное остаётся свободой того, кто пишет.

Почему правилам можно верить

Правило можно придумать любое, вопрос в том, какое имеет право войти в систему. Требование одно и жёсткое: правило никогда не должно вести от истинных строк к ложной. Проверяется оно таблицей, и обычно за две-четыре строки. Возьмём ∨I: надо убедиться, что если A истинно, то A ∨ B истинно при любом B.

Случаев ровно два. Если B истинно, то A ∨ B истинно. Если B ложно, то A ∨ B всё равно истинно, потому что истинно A. Провала нет ни в одном. Теперь возьмём заведомо плохое правило: «из A → B и B получается A». Ищем провал: пусть A ложно, B истинно. Строка A → B истинна, ложное начало стрелку не нарушает. Строка B истинна, а результат, A, ложен. Провал найден за одну строку таблицы, и правило отвергнуто: это подтверждение следствия, форма которого разобрана в уроке 8. Из этого требования и растёт главное обещание системы: всё, что она выводит, действительно следует. Называется это обещание корректностью, а доказывают его в уроке 18.

Что дальше

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

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

Что читать

• forall x: Calgary, гл. 16 «Basic rules for TFL»: Упражнения тут важнее текста: двадцать решённых выводов стоят любого объяснения. Обратите внимание, что там есть и ∨E (правило, которого тренажёр курса не даёт).
• Тренажёр «Построитель вывода» в уроке 12, задачи 1-3: Первые три задачи решаются одними правилами этого урока: →E, разбор и сборка конъюнкции, дизъюнктивный силлогизм. Их можно пройти уже сейчас, не дожидаясь допущений.
• Статья «Relevance Logic» в Stanford Encyclopedia of Philosophy: Про системы, где переход от P и ¬P к произвольному Q запрещён. Читать не обязательно, но полезно увидеть, что недовольство этим переходом представляет собой старую и разработанную позицию, а не наивность. Итог подводит урок 23.