Натуральная дедукция

Математики не проверяют теоремы перебором всех случаев - они ДОКАЗЫВАЮТ их. «Сумма углов треугольника равна 180°» доказывается рассуждением, а не измерением всех треугольников. Натуральная дедукция - формализация того, как люди на самом деле рассуждают.

• **Proof assistants:** Coq, Lean, Isabelle используют правила, похожие на натуральную дедукцию, для верификации программ и доказательств
• **Компиляторы:** Система типов - это логика, где типы = утверждения, программы = доказательства (соответствие Карри-Ховарда)
• **Юриспруденция:** Судебные аргументы строятся как цепочки выводов: факты → применение закона → заключение

Натуральная дедукция

**Натуральная дедукция** - это система формальных доказательств, имитирующая естественное человеческое рассуждение. В отличие от таблиц истинности (проверка всех случаев), здесь мы **строим доказательство** шаг за шагом, применяя правила вывода.

**Герхард Генцен** (1934) создал натуральную дедукцию как формализацию математического рассуждения. Каждая логическая связка имеет два правила: **введение** (как получить) и **удаление** (как использовать).

Доказательство начинается с **посылок** (данных) и заканчивается **заключением**. По пути мы можем делать **допущения** (временные предположения), которые потом «закрываются» правилами введения импликации или отрицания.

Правила введения

**Правила введения** говорят, как **получить** формулу с данной связкой. Чтобы ввести конъюнкцию A ∧ B, нужно иметь и A, и B. Чтобы ввести дизъюнкцию A ∨ B, достаточно иметь A или B.

**Введение импликации (→I):** Чтобы доказать A → B, допустим A и выведем B. Тогда закрываем допущение и получаем A → B. Это соответствует: «Если бы A было истинно, то B было бы истинно».

**Ключевая идея →I:** Мы не утверждаем, что A истинно! Мы говорим: «ЕСЛИ БЫ A было истинно, ТО B было бы истинно». Допущение - это гипотетический мир, который мы исследуем, а потом покидаем.

Правила удаления

**Правила удаления** говорят, как **использовать** формулу с данной связкой. Modus ponens (→E) - самое важное: имея A → B и A, получаем B. Из конъюнкции A ∧ B можно извлечь A или B.

**Удаление дизъюнкции (∨E)** - самое сложное правило. Имея A ∨ B, мы не знаем, какая часть истинна. Поэтому нужно рассмотреть оба случая: допустить A, вывести C; допустить B, вывести C. Тогда C в любом случае.

**Ex falso quodlibet** (из лжи следует всё): если мы получили противоречие (⊥), можно вывести любую формулу. Это не баг, а фича - противоречивые посылки делают систему бесполезной, что и отражает правило.

Стратегия доказательства

**Стратегия «от цели»:** Смотрим на заключение и спрашиваем: «Какое правило введения даёт такую формулу?» Если цель A → B - допускаем A и доказываем B. Если цель A ∧ B - доказываем A и B отдельно.

**Эвристики:** 1) Начни с введения главной связки цели. 2) Используй все посылки - они даны не зря. 3) При A ∨ B в посылках - рассмотри случаи. 4) Если застрял - попробуй доказательство от противного.

**Проверка доказательства:** Каждая строка должна быть либо посылкой, либо допущением, либо получена правилом из предыдущих. Все допущения должны быть закрыты к концу. Нельзя ссылаться на закрытые допущения.

Ключевые идеи

• **Введение** - как получить формулу с данной связкой (∧I, ∨I, →I, ¬I)
• **Удаление** - как использовать формулу с данной связкой (∧E, ∨E, →E, ¬E)
• **Допущения** - гипотетические миры, которые нужно закрыть
• **Стратегия от цели** - смотри на главную связку заключения
• **Ex falso** - из противоречия следует что угодно

Связанные темы

Натуральная дедукция - основа формальных доказательств:

• Доказательство от противного — Специальная техника с использованием ¬I
• Импликация — →I и →E - ключевые правила для работы с импликацией
• Modus ponens — →E - это формализация modus ponens

Вопросы для размышления

• Почему правило удаления дизъюнкции (∨E) сложнее остальных?
• Как бы вы объяснили ex falso quodlibet интуитивно?
• Если бы вы проектировали язык программирования, как бы типы соответствовали логическим связкам?

Связанные уроки

• comp-18-type-checking
• ml-03