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

Дано: пять посылок $p \to q$, $q \to r$, $\neg r$, $p \vee s$, $s \to t$. Найти: вывод заключения $t$, то есть последовательность строк, где у каждой указано правило и номера посылок.

Применять правила вывода означает искать в уже выписанных строках пару, совпадающую с шаблоном какого-нибудь правила, и дописывать то, что этот шаблон разрешает. Идти удобно прямым ходом: от посылок к заключению, каждый раз добавляя ровно одну строку. Ответ: заключение $t$ выводится, протокол занимает девять строк, из которых пять посылок и четыре применения правил - гипотетический силлогизм, модус толленс, дизъюнктивный силлогизм и модус поненс. Калькулятор сверху собирает этот протокол и тут же проверяет его перебором: посылки задачи истинны ровно на одном наборе значений из тридцати двух.

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

Дано. Пять посылок, пронумерованных в том порядке, в каком они даны в условии.

Найти. Строку с формулой $t$ и обоснование каждой промежуточной строки.

Шаг 1. Ищем, с чего начать. Правило срабатывает только тогда, когда его шаблону соответствуют целые строки протокола, поэтому сначала смотрим, какие пары вообще стыкуются. Строка 3 короче всех и содержит отрицание, а отрицание следствия - это половина модуса толленса. Вторая половина, импликация с заключением $r$, тоже есть: это строка 2. Но выгоднее сначала связать строки 1 и 2, чтобы отрицание ударило сразу по $p$.

Шаг 2. Гипотетический силлогизм из строк 1 и 2. Две импликации сцеплены общим звеном: заключение первой совпадает с посылкой второй. Значит, промежуточное $q$ можно выбросить:

$$\frac{p \to q,\quad q \to r}{p \to r}.$$

В протокол уходит строка 6: $p \to r$, обоснование - гипотетический силлогизм из строк 1 и 2.

Шаг 3. Модус толленс из строк 6 и 3. Теперь есть импликация $p \to r$ и отрицание её заключения $\neg r$. Правило отрицающего модуса переносит отрицание с конца импликации на начало:

$$\frac{p \to r,\quad \neg r}{\neg p}.$$

Строка 7: $\neg p$, модус толленс из строк 6 и 3.

Шаг 4. Дизъюнктивный силлогизм из строк 4 и 7. Посылка 4 утверждает, что выполняется хотя бы одно из двух, а строка 7 закрывает первую альтернативу. Остаётся вторая:

$$\frac{p \vee s,\quad \neg p}{s}.$$

Строка 8: $s$, дизъюнктивный силлогизм из строк 4 и 7.

Шаг 5. Модус поненс из строк 8 и 5. Условие импликации 5 получено на предыдущем шаге, и правило отделения снимает стрелку:

$$\frac{s,\quad s \to t}{t}.$$

Строка 9: $t$, модус поненс из строк 8 и 5. Цель достигнута, протокол закончен.

Ответ: $t$ выводится из данных посылок за девять строк, четыре из которых получены по правилам вывода; использованы гипотетический силлогизм, модус толленс, дизъюнктивный силлогизм и модус поненс.

Правила вывода: что именно разрешает каждое

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

Буквы $A$, $B$, $C$ здесь метапеременные: вместо них подставляется любая формула, лишь бы подстановка была одинаковой во всех вхождениях. Поэтому модус поненс применим не только к переменным: из $\neg p \to (q \vee r)$ и $\neg p$ он даёт $q \vee r$ целиком. Сами правила разобраны в статьях про модус поненс и модус толленс, а здесь важно другое - их применение к готовому набору посылок.

Главное ограничение: правило работает со строками, а не с кусками формул. Если в протоколе стоит $\neg(p \to q)$, то внутри скобок модус поненс применять нельзя, каким бы подходящим ни выглядел фрагмент. Сначала отрицание нужно снять равносильным преобразованием, и только потом строка станет пригодной для правила.

Второй маршрут к тому же заключению

Вывод не единственный, и это нормально: порядок применения правил свободен. Вместо гипотетического силлогизма можно дважды применить модус толленс. Из строк 2 и 3 получаем $\neg q$, затем из строк 1 и полученного $\neg q$ - тот же самый $\neg p$, после чего дизъюнктивный силлогизм и модус поненс доводят вывод до $t$. Длина протокола та же, девять строк.

Проверяющий засчитывает любой корректный маршрут, поэтому подгонять решение под образец не нужно. Полезнее другое правило выбора: если среди посылок есть отрицание, начинать стоит с него, потому что отрицание отсекает варианты, а импликации сами по себе ничего не утверждают. В калькуляторе сверху переключатель заключения показывает, что по дороге к $t$ честно выводятся и промежуточные формулы $\neg p$ и $s$, а вот $p$ не выводится ни при каком маршруте.

Проверка: одна строка из тридцати двух

У вывода есть семантический двойник: рассуждение корректно, если не существует набора значений переменных, на котором все посылки истинны, а заключение ложно. Переменных пять, наборов $2^5 = 32$, и перебрать их можно механически.

Посылки задачи настолько жёсткие, что выполняются ровно на одном наборе. Строка 3 требует $r = 0$; тогда импликация 2 вынуждает $q = 0$, импликация 1 даёт $p = 0$, дизъюнкция 4 при ложном $p$ требует $s = 1$, а импликация 5 поднимает $t = 1$. Единственный набор, где истинны все пять посылок, это $00011$, и заключение $t$ на нём истинно. Контрпримеров нет, значит вывод верен.

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

Чем это отличается от вывода из аксиом

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

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

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

• Модус поненс применяют в обратную сторону. Из $p \to q$ и $q$ формула $p$ не следует: это утверждение консеквента. Контрпример даёт набор $p = 0$, $q = 1$, на нём обе посылки истинны, а заключение ложно.
• Отрицают условие вместо следствия. Из $p \to q$ и $\neg p$ не выводится $\neg q$. Модус толленс требует отрицания именно заключения импликации, порядок частей в нём не переставляется.
• Правило применяют к части формулы. Внутри $\neg(p \to q)$ или $(p \to q) \vee r$ шаблоны не срабатывают: правило берёт строку целиком.
• Пропускают строку. Переход «$\neg r$, значит $s$» верен по смыслу, но в протоколе между ними три применения правил, и без них решение не засчитают.
• Не указывают номера посылок. Обоснование состоит из двух частей: название правила и номера строк, к которым оно применено; одного названия мало.
• Считают, что вывод обязан быть кратчайшим. Лишние строки не ошибка, если каждая обоснована; ошибка - строка без обоснования.

FAQ

Сколько правил нужно знать для контрольной? Обычно хватает шести: четырёх из таблицы выше плюс упрощение ($A \wedge B$ даёт $A$) и введение конъюнкции (из $A$ и $B$ следует $A \wedge B$). Остальные правила из учебника выводятся через эти и применяются реже.

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

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

Как формализовать словесное рассуждение? Каждому простому утверждению назначить переменную, связки «если ..., то», «или», «не» перевести в $\to$, $\vee$, $\neg$, а затем работать только с формулами. Смысл предложений дальше не нужен: правила вывода не различают, о чём идёт речь.

Коротко

1. Правило вывода дописывает новую строку протокола, когда в нём уже стоят строки, совпадающие с шаблоном правила целиком.
2. Рабочий порядок: выписать посылки под номерами, найти пару под какое-нибудь правило, добавить строку, повторять до заключения.
3. В задаче сработали четыре правила подряд: гипотетический силлогизм дал $p \to r$, модус толленс - $\neg p$, дизъюнктивный силлогизм - $s$, модус поненс - $t$.
4. Обоснование каждой строки состоит из названия правила и номеров посылок; без номеров строка считается необоснованной.
5. Проверка выполняется перебором: посылки истинны только на наборе $00011$, заключение $t$ на нём истинно, контрпримера нет, вывод корректен.