Натуральная дедукция: протокол, где каждая строка по правилу

Агата Сомова · старший инспектор

Протокол допроса Ефима. Суд уже установил, что ключ Прохору отдал он, но сам Ефим до сих пор оставляет себе лазейку. Он показал три вещи: если ключ был у Прохора, то дал его либо он сам, либо Рудаков; если дал он, это нарушение устава; если дал Рудаков, тоже нарушение. Вельский скажет, что мы додумали за свидетеля. Перепиши протокол так, чтобы каждый шаг ссылался на правило. Как у Арбениной.

На полях тетради Арбенина написала: «Протокол допроса тоже вывод». В прошлых уроках ты видел системы, где правила говорят про чётные числа и скобки. Теперь правила будут говорить про формулы, знакомые с первого блока: $\wedge$, $\vee$, $\to$, $\neg$.

В блоке «Допросы» вывод проверяли таблицей истинности. Таблица честно отвечает «следует» или «не следует», но не объясняет почему, а на тридцати атомах в ней больше миллиарда строк. Система правил даёт другое: рассуждение по шагам, где каждый шаг можно проверить отдельно. Она называется натуральной дедукцией, потому что повторяет, как люди рассуждают в жизни. Её придумали независимо Герхард Генцен и Станислав Яськовский в 1934 году.