Исчисление натурального вывода

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

История

Исчисление натурального вывода возникло как реакция на недостатки аксиоматических систем, таких как система Principia Mathematica Бертрана Рассела и Альфреда Норта Уайтхеда. В этих системах доказательства часто были громоздкими и неестественными, так как требовали вывода из небольшого набора аксиом с помощью единственного правила (modus ponens). Генцен и Яськовский независимо друг от друга предложили подход, при котором правила вывода напрямую отражают логические операции, используемые в реальных математических доказательствах.

Герхард Генцен представил систему натурального вывода в своей диссертации 1934 года «Исследования логических выводов» (нем. Untersuchungen über das logische Schließen). Он стремился создать систему, которая была бы «настолько близка к действительным рассуждениям, насколько это возможно». Станислав Яськовский, работавший в то же время, предложил аналогичную систему, основанную на идее «суппозиций» (допущений). Впоследствии натуральный вывод был распространён на интуиционистскую логику, модальную логику и другие неклассические логики.

Основные понятия

Секвенции и суппозиции

В отличие от гильбертовских систем, где доказательство — это последовательность формул, в натуральном выводе доказательство строится в виде дерева или линейной последовательности, где каждая строка может зависеть от некоторого набора допущений (гипотез). Зависимость от допущений обычно обозначается слева от формулы, например: Γ ⊢ A, где Γ — множество допущений, а A — выводимая формула. Такая запись называется секвенцией.

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

Правила вывода в натуральном выводе делятся на два типа для каждой логической связки: правила введения (introduction, I) и правила удаления (elimination, E). Правила введения показывают, как можно получить формулу с данной связкой, а правила удаления — как можно использовать формулу с данной связкой.

Примеры правил для пропозициональной логики

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

Снятие допущений

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

Структура доказательства

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

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

1. A (допущение)
2. A (повторение из строки 1)
3. A → A (→I, снятие допущения A, строки 1-2)

Разновидности

Интуиционистский натуральный вывод

В интуиционистской логике натуральный вывод отличается от классического тем, что в нём отсутствует правило снятия двойного отрицания (¬¬A → A). Вместо этого используется более слабое правило, что приводит к тому, что закон исключённого третьего (A ∨ ¬A) не является теоремой.

Модальный натуральный вывод

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

Натуральный вывод с равенством

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

Применение

Исчисление натурального вывода широко используется в следующих областях:

• Теория доказательств: Является одной из основных систем для изучения структуры доказательств, нормализации и устранения сечений (теорема Генцена об устранении сечений).
• Информатика: Лежит в основе многих систем автоматического доказательства теорем (например, Isabelle, Coq, Agda). В этих системах доказательство строится в стиле натурального вывода, что облегчает его понимание и верификацию.
• Обучение логике: Благодаря своей естественности, натуральный вывод часто используется в учебных курсах по математической логике для обучения студентов формальным доказательствам.
• Семантика естественного языка: Используется в лингвистике для формального представления семантики предложений, особенно в рамках теории типов и грамматики Монтегю.

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

Несмотря на свою естественность, натуральный вывод имеет некоторые недостатки:

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

Связь с другими системами

Натуральный вывод тесно связан с исчислением секвенций (sequent calculus), также разработанным Генценом. Исчисление секвенций является более симметричной системой, где правила введения и удаления заменены на правила введения слева и справа от знака секвенции. Теорема Генцена об устранении сечений устанавливает эквивалентность между натуральным выводом и исчислением секвенций в отношении доказуемости формул.

Источники

1. Генцен, Г. «Исследования логических выводов» (1934).
2. Яськовский, С. «О правилах допущений в формальной логике» (1934).
3. Троелстра, А. С., Швихтенберг, Х. «Основная теория доказательств» (1996).
4. Правниц, Д. «Натуральный вывод: исследование теории доказательств» (1965).