Натуральное исчисление

Натуральное исчисление — это раздел математической логики, изучающий формальные системы, в которых доказательства строятся с помощью правил вывода, непосредственно отражающих естественные («натуральные») способы человеческих рассуждений. В отличие от аксиоматических систем (например, гильбертовского исчисления), где доказательство представляет собой последовательность формул, начинающуюся с аксиом, в натуральном исчислении основное внимание уделяется введению и устранению логических связок и кванторов. Основоположниками данного подхода считаются немецкий логик Герхард Генцен (1934 год) и польский логик Станислав Яськовский (1934 год, независимо от Генцена).

История возникновения

Предпосылки создания

В начале XX века, после работ Готлоба Фреге и Бертрана Рассела, математическая логика развивалась преимущественно в рамках аксиоматических систем. Однако такие системы были громоздкими: доказательства даже простых утверждений (например, A → A) требовали длинных цепочек формул, а сами правила вывода (часто только modus ponens) плохо соответствовали интуитивным шагам рассуждений. Возникла потребность в формализме, который бы точнее моделировал реальные математические доказательства.

Работы Генцена и Яськовского

В 1934 году Герхард Генцен в своей диссертации «Исследования логических выводов» предложил систему натурального исчисления (нем. Naturliches Schliessen). Он стремился создать систему, которая была бы «настолько близка к действительным рассуждениям, насколько это возможно». Одновременно, независимо от Генцена, Станислав Яськовский разработал аналогичную систему, опубликовав её в 1934 году в работе «О правилах допущений в формальной логике».

Генцен ввёл ключевое понятие — правила введения и устранения для каждой логической связки. Например, правило введения импликации (→I) позволяет заключить A → B, если из допущения A выведено B. Это напрямую соответствует методу доказательства «предположим A, тогда...». Правило устранения импликации (→E) — это классический modus ponens: из A и A → B следует B.

Развитие и влияние

Натуральное исчисление быстро стало одним из основных инструментов в теории доказательств. В 1935 году Генцен доказал теорему об устранении сечения (Hauptsatz) для своего исчисления, что стало фундаментальным результатом. Теорема утверждает, что любое доказательство, использующее правило сечения (аналог леммы), может быть преобразовано в доказательство без него, что делает выводы «чистыми» и позволяет анализировать их структуру. Впоследствии натуральное исчисление было расширено на интуиционистскую логику, модальные логики, логику предикатов высших порядков и другие неклассические логики.

Основные понятия и структура

Секвенции и выводы

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

Генценовская версия натурального исчисления часто формулируется через секвенции — выражения вида Γ ⊢ A, где Γ — множество (или список) допущений, а A — выводимая формула. Однако в классическом изложении (например, у Д. Правеца) выводы записываются в виде дерева, где допущения явно помечаются и снимаются.

Правила вывода

Каждая логическая связка имеет два типа правил: введение (I) и устранение (E). Для пропозициональной логики (логики высказываний) правила выглядят следующим образом:

Конъюнкция (∧)

• Введение (∧I): Из A и B можно заключить A ∧ B.
• Устранение (∧E): Из A ∧ B можно заключить A (или B).

Дизъюнкция (∨)

• Введение (∨I): Из A можно заключить A ∨ B (или B ∨ A).
• Устранение (∨E): Из A ∨ B, A → C и B → C можно заключить C. Это правило моделирует разбор случаев.

Импликация (→)

• Введение (→I): Если из допущения A выведено B, то можно заключить A → B, сняв допущение A.
• Устранение (→E): Из A и A → B следует B (modus ponens).

Отрицание (¬)

В классическом натуральном исчислении отрицание часто определяется через константу ложь (⊥). Тогда ¬A — это A → ⊥.

• Введение (¬I): Если из допущения A выведено ⊥, то можно заключить ¬A (сняв A).
• Устранение (¬E): Из A и ¬A следует ⊥.

Для классической логики добавляется правило снятия двойного отрицания (DNE): Из ¬¬A можно заключить A. В интуиционистской логике это правило отсутствует.

Пример доказательства

Докажем формулу A → A (закон тождества) в натуральном исчислении:

1. Допускаем A (гипотеза).
2. Из A (шаг 1) по правилу →I (введение импликации) заключаем A → A, снимая допущение A.

Дерево вывода: `` [A]¹ ──── A → A (→I, 1) ` Здесь [A]¹ — допущение, снятое на шаге →I`.

Классификация и варианты

Пропозициональное и предикатное исчисление

• Пропозициональное натуральное исчисление работает только с высказываниями и логическими связками.
• Предикатное натуральное исчисление добавляет правила для кванторов: ∀ (всеобщность) и ∃ (существование). Правила введения и устранения кванторов учитывают ограничения на свободные переменные (например, правило ∀I требует, чтобы переменная не была свободной в допущениях).

Интуиционистское и классическое

• Интуиционистское натуральное исчисление: не содержит правила снятия двойного отрицания. В нём нельзя доказать закон исключённого третьего (A ∨ ¬A) в общем виде.
• Классическое натуральное исчисление: включает DNE или эквивалентное правило (например, reductio ad absurdum в классической форме).

Системы с явными и неявными допущениями

В оригинальной системе Генцена допущения явно помечаются и снимаются. В альтернативных версиях (например, в системе Фитча) допущения записываются в виде вложенных столбцов, что визуально упрощает отслеживание области действия гипотез.

Применение

В математике и теории доказательств

Натуральное исчисление широко используется для формализации математических доказательств. Оно лежит в основе многих систем автоматического доказательства теорем (например, Isabelle, Coq, Lean). В этих системах пользователь строит доказательство, применяя правила введения и устранения, что интуитивно понятно математикам.

В информатике

• Проверка корректности программ: Натуральное исчисление применяется в системах формальной верификации (например, в языке F*).
• Логическое программирование: Идеи натурального исчисления повлияли на разработку языков программирования с зависимыми типами.
• Обработка естественного языка: Алгоритмы, основанные на натуральном исчислении, используются для анализа логической структуры текстов.

В философии и лингвистике

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

Критика и ограничения

Сложность поиска доказательств

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

Неоднозначность представления

Деревья вывода в натуральном исчислении могут быть громоздкими для сложных доказательств. Существуют компактные линейные нотации (например, в стиле Фитча), но они менее наглядны.

Проблема с правилом сечения

Хотя теорема Генцена об устранении сечения решает проблему избыточности, в практических системах (например, в Coq) правило сечения всё равно используется как лемма, что может усложнять анализ доказательств.

Связь с другими исчислениями

Исчисление секвенций

Генцен разработал исчисление секвенций (LK) как альтернативу натуральному исчислению, более удобную для доказательства теоремы об устранении сечения. В исчислении секвенций правила симметричны: есть правила введения связок как слева, так и справа от ⊢. Натуральное исчисление и исчисление секвенций эквивалентны по выразительной силе, но различаются по структуре доказательств.

Гильбертовское исчисление

В отличие от натурального исчисления, гильбертовское исчисление использует небольшое количество аксиом и только одно правило вывода (modus ponens). Доказательства в нём длиннее и менее интуитивны, но оно удобно для метаматематических исследований (например, для доказательства непротиворечивости).

Интересные факты

• Генцен разработал натуральное исчисление в возрасте 24 лет, будучи ассистентом Давида Гильберта.
• Термин «натуральное исчисление» (нем. Naturliches Schliessen) был введён самим Генценом, чтобы подчеркнуть его близость к естественным рассуждениям.
• В 1936 году Генцен доказал непротиворечивость арифметики Пеано с помощью трансфинитной индукции до ординала ε₀, используя методы, основанные на его исчислении секвенций.
• Система Coq, один из самых мощных ассистентов доказательства, использует вариант натурального исчисления, называемый «исчислением индуктивных конструкций».

Источники

• Gentzen, G. (1935). "Untersuchungen über das logische Schließen". Mathematische Zeitschrift, 39(1), 176–210.
• Jaskowski, S. (1934). "On the Rules of Suppositions in Formal Logic". Studia Logica, 1, 5–32.
• Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell.
• Troelstra, A. S., & Schwichtenberg, H. (2000). Basic Proof Theory (2nd ed.). Cambridge University Press.
• Непейвода, Н. Н. (2005). Прикладная логика. Ижевск: Институт компьютерных исследований.