Естественный вывод

Curry-Howard correspondence: каждое доказательство - это программа, каждый тип - это теорема. Правило →I соответствует lambda-abstraction. Правило →E соответствует вызову функции. В Lean4 `have h : A := proof` - это буквально →I. `exact h` или `apply` - это →E. Lean4 верифицировал теорему Кеплера о паковке сфер (400 лет математической истории) через те же семь правил Генцена, которые изучаются в этом уроке.

• **Lean4 / Coq (формальная верификация)**: proof assistants используют Natural Deduction напрямую - тип-чекер проверяет доказательства так же как компилятор проверяет типы; в 2023 Lean4 верифицировал теорему Кеплера
• **Hindley-Milner type inference (GHC, Rust)**: алгоритм выведения типов - это поиск доказательства в системе типов через правила intro/elim; exhaustiveness check в match/switch - это ∨E
• **Верификация ML-систем**: Brunel et al. (2023) верифицировали корректность backpropagation в Coq через Natural Deduction - формальные гарантии для нейросетей как следующий шаг safety-critical AI

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

В 2023 году Lean4 верифицировал теорему Кеплера о плотнейшей упаковке сфер - результат, который математики доказывали 400 лет. Внутри Lean4 нет магии: только семь правил Natural Deduction Герхарда Генцена (1935). Каждая логическая связка имеет ровно два правила - **introduction** (как построить формулу) и **elimination** (как использовать доказанную формулу).

Правило →I - сердце системы. Чтобы доказать «если дождь, то улица мокрая», предполагается дождь и показывается мокрая улица. Предположение временное - оно исчезает, когда правило применяется. Curry-Howard correspondence делает это буквальным: →I в Lean4 соответствует lambda-abstraction. `fun (h : Rain) => show Wet street from h` - это ровно то же, что →I.

∨E - это proof by cases. Его аналог в Haskell: `case either of { Left a -> ... ; Right b -> ... }`. Тип-чекер GHC при exhaustiveness check буквально применяет ∨E: если оба случая ведут к одному типу, результат имеет этот тип. Hindley-Milner type inference - это поиск доказательства в системе типов через те же правила introduction/elimination.

Гипотетические доказательства

Некоторые теоремы недостижимы прямыми правилами. Нужны вложенные гипотезы - субдоказательства под временными предположениями. Это не трюк: это формализация того, как математики рассуждают тысячи лет. В Coq каждый `have h : A := proof` открывает субдоказательство под гипотезой h - ровно →I.

Гипотезы - это scope. Всё что доказано внутри scope [φ] зависит от φ. Когда →I применяется, scope закрывается - зависимость упаковывается в импликацию. Rust borrow checker делает то же самое: lifetime'ы - это переменные, связанные scope'ами. Компилятор применяет аналог →I когда проверяет что заимствование не выходит за пределы области действия.

В **интуиционистской логике** RAA не принимается: чтобы доказать φ, нужно его построить - показать свидетеля, написать программу нужного типа. Отрицание ¬φ там означает «φ → ⊥» (из φ следует противоречие), а не просто «φ не доказана». Это принципиальное расхождение: классическая логика допускает p ∨ ¬p для любого p - интуиционистская нет. Coq, Agda, Lean4 - конструктивны по умолчанию, RAA нужно импортировать явно.

Brunel et al. (2023) формально верифицировали корректность backpropagation в Coq - без RAA, чисто конструктивно. Каждый шаг градиентного спуска доказан как правильный вывод. Это не академическая игра: верификация ML-систем через proof assistants становится требованием для safety-critical AI.

Корректность и полнота

Система вывода может быть красивой и при этом бесполезной - если доказывает что-то ложное (некорректная), или не доказывает что-то истинное (неполная). Natural Deduction Генцена для FOL корректна и полна: ⊢ и ⊨ совпадают. Это нетривиальный результат: правила вывода (синтаксис) точно соответствуют семантике через все возможные интерпретации.

Гёдель 1930 года - теорема о **полноте**: FOL полна, всё семантически верное доказуемо. Гёдель 1931 года - теоремы о **неполноте**: арифметика (PA) не полна, есть истинные недоказуемые утверждения. Это не противоречие. FOL - язык. Арифметика - конкретная теория на этом языке, намного более богатая.

**Curry-Howard correspondence** - не метафора. Это изоморфизм: тип в системе типов = формула в логике; программа = доказательство; вычисление = нормализация доказательства. →I соответствует lambda-abstraction. →E соответствует применению функции. ∧ соответствует произведению типов. ∨ соответствует сумме типов. В Lean4 и Coq этот изоморфизм встроен в ядро: type-checker - это proof-checker.

Полнота FOL означает: proof assistant на Natural Deduction в принципе достаточен. Но теорема Чёрча добавляет: нет алгоритма, который всегда находит доказательство. Поэтому Lean4 и Coq - интерактивные: человек ведёт стратегию, машина проверяет каждый шаг. Lean4 верифицировал теорему Кеплера не потому что «умнее» математика - а потому что проверил все 10 000 шагов доказательства без единой ошибки.

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

• **Introduction** строит формулы: ∧I (оба компонента), ∨I (один из), →I (из гипотезы - импликация), ⊥ нет intro
• **Elimination** извлекает информацию: →E (modus ponens), ∧E (проекция), ∨E (case analysis), ⊥E (ex falso)
• **Гипотетическое доказательство**: субдоказательство под гипотезой [φ] - scope закрывается через →I; RAA - классический (не конструктивный) метод
• **Корректность**: всё доказуемое истинно (⊢ φ ⟹ ⊨ φ); **Полнота**: всё истинное доказуемо (⊨ φ ⟹ ⊢ φ) - для FOL обе выполнены
• Curry-Howard: →I = lambda, →E = применение функции; type-checker в Lean4/Coq - это proof-checker над теми же правилами

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

Natural Deduction - мост между логикой, теорией типов и верификацией программ:

• Предикатная логика первого порядка — Формулы FOL - объекты, над которыми работают правила intro/elim
• Пропозициональная логика — Связки ∧, ∨, →, ¬ получают свои intro/elim правила как фундамент
• Резолюция — Альтернативный движок: автоматический вывод без гипотетических субдоказательств

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

• Curry-Howard: тип A → B = доказательство A → B = функция из A в B. Что соответствует типу A × B? А A + B? А типу Void?
• Почему Coq конструктивен по умолчанию и RAA нужно импортировать явно? Какие теоремы нельзя доказать без RAA - и что это означает для верифицированных программ?
• Теорема Гёделя о полноте говорит что FOL полна. Теорема Чёрча говорит что общезначимость FOL неразрешима. Как эти два результата совмещаются? Что из этого следует для proof assistants?

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

• ml-02 — FOL-формулы - объекты, над которыми работают правила вывода
• ml-01 — Пропозициональные связки ∧, ∨, → - основа intro/elim правил
• ml-04 — Резолюция - альтернативный, алгоритмический движок вывода
• ml-15 — Модальная логика расширяет Natural Deduction операторами необходимости
• plt-06-lambda-calculus