Как построить вывод формулы: пошаговое решение

Дано: гильбертовское исчисление высказываний со схемами аксиом A1-A3 и единственным правилом вывода modus ponens. Найти: вывод формулы $A \to A$, то есть последовательность формул, в которой каждая строка обоснована.

Формула $A \to A$ не получается из схем аксиом никакой подстановкой, поэтому её приходится именно выводить: подобрать в схеме A2 подстановку так, чтобы её заключением оказалась цель, а обе посылки взять из схемы A1. Ответ: вывод занимает пять шагов - три вхождения схем аксиом и два применения modus ponens. Самая длинная формула стоит на втором шаге, дальше вывод сжимается к цели. Калькулятор сверху собирает этот протокол и ещё три типовых, показывая обоснование каждой строки.

Решение по шагам

Дано. Схемы аксиом. Буквы $X$, $Y$, $Z$ в них - метапеременные: вместо каждой подставляется любая формула, причём одинаково во всех её вхождениях.

$$\begin{aligned} \text{A1:}\quad & X \to (Y \to X), \\ \text{A2:}\quad & (X \to (Y \to Z)) \to ((X \to Y) \to (X \to Z)), \\ \text{A3:}\quad & (\neg Y \to \neg X) \to ((\neg Y \to X) \to Y). \end{aligned}$$

Правило ровно одно, modus ponens: если в выводе уже стоят формулы $P$ и $P \to Q$, разрешено выписать $Q$.

Найти: вывод $\vdash A \to A$ без гипотез. Отрицаний в цели нет, поэтому схема A3 не понадобится.

Замысел. Последняя строка вывода - это цель. Получить её можно только двумя способами: она либо сама вхождение схемы, либо результат modus ponens. Первый способ отпадает: ни A1, ни A2 не дают $A \to A$. Значит, где-то выше должны стоять формула $P$ и импликация $P \to (A \to A)$. Импликацию с таким заключением умеет давать A2: если взять в ней $X := A$ и $Z := A$, заключение станет $(A \to Y) \to (A \to A)$. Осталось подобрать $Y$ так, чтобы обе посылки оказались аксиомами; подходит $Y := A \to A$.

Шаг 1. Выписываем вхождение схемы A1 при $X := A$, $Y := A \to A$:

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

Шаг 2. Выписываем вхождение схемы A2 при $X := A$, $Y := A \to A$, $Z := A$:

$$\bigl(A \to ((A \to A) \to A)\bigr) \to \bigl((A \to (A \to A)) \to (A \to A)\bigr).$$

Шаг 3. Посылка шага 2 - это в точности формула шага 1, поэтому по modus ponens отделяем заключение:

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

Шаг 4. Снова берём A1, теперь при $X := A$, $Y := A$:

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

Шаг 5. Формула шага 4 совпала с посылкой импликации шага 3, и modus ponens отделяет цель:

$$A \to A.$$

Оформлять вывод принято протоколом в три колонки: номер, формула, обоснование. Обоснование - обязательная часть ответа, без него это просто список формул.

Ответ. Вывод построен и состоит из пяти шагов: строки 1, 2, 4 - вхождения схем аксиом, строки 3 и 5 - применения modus ponens. Последняя формула совпадает с целью, гипотезы не использованы, значит $A \to A$ доказана в исчислении, то есть является его теоремой.

Что считается шагом вывода

Вывод формулы $F$ из множества гипотез $\Gamma$ - это конечная последовательность формул $F_1, F_2, \ldots, F_n$, где $F_n$ совпадает с $F$, а каждая строка получена одним из трёх способов: она вхождение схемы аксиомы, она принадлежит $\Gamma$, либо она получена по modus ponens из двух строк с меньшими номерами. Если $\Gamma$ пусто, вывод называют доказательством, а формулу - теоремой исчисления и пишут $\vdash F$.

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

Формулу и схему важно различать. A1 - не формула, а шаблон с бесконечным числом вхождений: каждая подстановка конкретных формул вместо $X$ и $Y$ даёт свою аксиому. На шагах 1 и 4 разбора стоит одна и та же схема A1 с разными подстановками, и это два разных вхождения, а не повтор.

Как искать вывод: обратный ход от цели

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

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

Полезный ориентир - длина формул. На графике в калькуляторе видно, что вывод не растёт монотонно: на аксиоме A2 длина скачет с 7 до 17 символов, а каждое применение modus ponens её срезает, отбрасывая посылку. Если в черновике формулы только удлиняются, поиск ушёл не туда.

Теорема о дедукции: пять шагов превращаются в два

Теорема о дедукции утверждает: если $\Gamma, A \vdash B$, то $\Gamma \vdash A \to B$. То есть любую формулу разрешено временно добавить в гипотезы, вывести из неё что нужно, а потом свернуть допущение в импликацию.

Для нашей задачи это работает мгновенно. Из гипотезы $A$ формула $A$ выводится за одну строку (она сама гипотеза), значит $A \vdash A$, и по теореме о дедукции $\vdash A \to A$. Весь вывод - две строки вместо пяти; переключатель режима в калькуляторе показывает оба протокола рядом.

Важно понимать, чем за это заплачено. Теорема о дедукции - не новое правило исчисления, а метатеорема о нём: её доказывают индукцией по длине вывода, и в этом доказательстве используются A1, A2 и разобранный выше вывод $A \to A$. Поэтому в контрольной вывод $A \to A$ обычно требуют строить честно: если в условии сказано «только аксиомы и modus ponens», сворачивать допущения нельзя.

Вывод из гипотез: транзитивность импликации

Второй типовой пример - получить $A \to C$ из гипотез $A \to B$ и $B \to C$. Прямой вывод занимает семь шагов: гипотеза $B \to C$, аксиома A1 при $X := B \to C$, $Y := A$, отделение $A \to (B \to C)$, аксиома A2 при $X := A$, $Y := B$, $Z := C$, отделение $(A \to B) \to (A \to C)$, гипотеза $A \to B$ и последний modus ponens.

С теоремой о дедукции та же задача решается почти устно: допускаем $A$, по modus ponens из $A$ и $A \to B$ получаем $B$, из $B$ и $B \to C$ получаем $C$, сворачиваем допущение и получаем $A \to C$. Шесть строк, но ни одной аксиомы - вместо подбора подстановок идёт обычное рассуждение. Оба протокола лежат в калькуляторе под чипом с этой секвенцией.

Выводимость $\vdash$ не стоит путать с семантической истинностью $\vDash$, которую проверяют перебором значений переменных: как это делается, разобрано в задаче как построить таблицу истинности. Таблица показывает, что формула тождественно истинна, но не предъявляет вывод; связывает эти два понятия теорема о полноте, а не сама таблица.

Частые ошибки

• Modus ponens применяют в обратную сторону. Из $B$ и $A \to B$ формула $A$ не следует: это ошибка утверждения консеквента, разобранная в статье про модус поненс. Правило отделяет заключение, зная посылку, и никогда наоборот.
• Несогласованная подстановка в схему. Если в одном вхождении $Y$ заменили на $A \to A$, а в другом на $A$, получится не аксиома, и строка повиснет без обоснования.
• Цель объявляют аксиомой. $A \to A$ похожа на аксиому, но ни одна схема её не даёт. Прежде чем писать «схема A1», подставь буквы и сравни формулы посимвольно.
• Теряются скобки. Импликация правоассоциативна: $A \to A \to A$ читается как $A \to (A \to A)$, а это не то же самое, что $(A \to A) \to A$.
• Вывод подменяют таблицей истинности. Перебор наборов значений доказывает общезначимость, а задание «постройте вывод» требует последовательности строк с обоснованиями.
• Пропущена колонка обоснований или использована теорема о дедукции там, где условие разрешает только аксиомы и modus ponens. Список формул без ссылок на схемы и номера строк не засчитывается, даже если все формулы верные.

FAQ

Чем вывод отличается от доказательства? Доказательство - частный случай вывода, при пустом множестве гипотез. Формула с доказательством называется теоремой исчисления и записывается $\vdash F$; формула, выведенная из гипотез, записывается $\Gamma \vdash F$ и вне этих гипотез ничего не утверждает.

Можно ли построить вывод $A \to A$ короче пяти шагов? В системе со схемами A1, A2 и одним правилом modus ponens убрать из протокола нечего: каждая из пяти строк используется дальше. Два шага получаются только с теоремой о дедукции, которая сама опирается на этот вывод.

Почему в учебниках разные наборы аксиом? Аксиоматика - вопрос удобства, а не истины. У Мендельсона три схемы и modus ponens, у Клини их больше, в натуральном выводе аксиом нет вовсе, зато есть правила введения и удаления связок. Множество выводимых формул при этом одно и то же - все тавтологии классической логики.

Как перенести метод на логику предикатов? Схемы аксиом и modus ponens остаются, добавляются кванторные аксиомы и правило обобщения, а теорема о дедукции получает ограничение: нельзя обобщать по переменной, свободной в допущении. Про значение формулы с кванторами - в статье об интерпретации формулы логики предикатов.

Коротко

1. Вывод - последовательность формул, где каждая строка либо вхождение схемы аксиомы, либо гипотеза, либо результат modus ponens из двух предыдущих; последняя строка и есть цель.
2. Искать вывод нужно от цели назад: раз цель получена по modus ponens, выше стоит импликация с таким заключением, а её даёт схема A2 с подходящей подстановкой.
3. Вывод $A \to A$ занимает пять шагов: A1, A2, modus ponens, A1, modus ponens; вхождений схем три, применений правила два.
4. Оформление - протокол в три колонки: номер, формула, обоснование со схемой и подстановкой или с номерами посылок.
5. Теорема о дедукции сокращает тот же вывод до двух строк, но применять её можно, только если это разрешено условием.