Теорема дедукции

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

История

Истоки теоремы дедукции восходят к работам древнегреческих философов, в частности к Аристотелю, который сформулировал принцип, известный как «правило отделения» (modus ponens). Однако в явном виде теорема была сформулирована и доказана в рамках современной математической логики.

В начале XX века, в связи с развитием формальных систем, проблема взаимосвязи между импликацией и выводимостью стала одной из центральных. Первое строгое доказательство теоремы дедукции для исчисления высказываний было дано Альфредом Тарским в 1921 году. Независимо от него, в 1930 году Жак Эрбран опубликовал свою версию доказательства, а в 1934 году Герхард Генцен в рамках своего исчисления секвенций (LK) дал элегантное и конструктивное доказательство, которое стало классическим. В 1936 году Алонзо Чёрч включил теорему дедукции в свою монографию «Введение в математическую логику», закрепив её статус как одной из основных метатеорем.

Формулировка

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

Для исчисления высказываний

Пусть Γ — множество формул, A и B — формулы. Тогда:

Прямая теорема дедукции: Если Γ, A ⊢ B, то Γ ⊢ A → B.

Обратная теорема дедукции: Если Γ ⊢ A → B, то Γ, A ⊢ B.

Здесь символ ⊢ обозначает отношение выводимости в данной формальной системе (например, в гильбертовском исчислении).

Для исчисления предикатов

В исчислении предикатов первого порядка теорема дедукции требует дополнительных ограничений, связанных с правилами введения и удаления кванторов. Если в доказательстве B из Γ и A не используются правила, затрагивающие свободные переменные в A (например, правило обобщения по переменной, входящей в A свободно), то теорема остаётся справедливой. В противном случае, прямое применение теоремы может привести к некорректным выводам. Для преодоления этого ограничения вводятся понятия «чистой переменной» и «правила переименования».

Доказательство

Доказательство теоремы дедукции обычно проводится индукцией по длине вывода формулы B из множества посылок Γ ∪ {A}.

Базис индукции

Если длина вывода равна 1, то B является либо аксиомой, либо одной из посылок (Γ или A). Рассматриваются три случая:

1. B — аксиома. Тогда B выводимо из Γ (Γ ⊢ B). По правилу введения импликации, из Γ ⊢ B и того, что A → B является аксиомой (или выводимой формулой), получаем Γ ⊢ A → B.
2. B ∈ Γ. Аналогично предыдущему случаю: Γ ⊢ B, следовательно, Γ ⊢ A → B.
3. B = A. Тогда A → A является тавтологией (или выводимой формулой), следовательно, Γ ⊢ A → A.

Шаг индукции

Предположим, что теорема верна для всех выводов длины меньше n. Пусть вывод B длины n оканчивается применением правила modus ponens к формулам C и C → B, которые имеют меньшую длину вывода. По предположению индукции, Γ ⊢ A → C и Γ ⊢ A → (C → B). Используя аксиому (A → (C → B)) → ((A → C) → (A → B)), по modus ponens дважды получаем Γ ⊢ A → B.

Таким образом, теорема доказана для всех выводов.

Значение и применение

Теорема дедукции имеет фундаментальное значение для математической логики и её приложений.

Упрощение доказательств

Она позволяет сводить задачу доказательства импликации A → B к задаче доказательства B при дополнительном допущении A. Это значительно упрощает построение формальных выводов, так как позволяет использовать все правила вывода, включая те, которые требуют наличия посылок.

Связь с метатеорией

Теорема дедукции является одной из основных метатеорем, наряду с теоремой о полноте и теоремой о корректности. Она устанавливает эквивалентность между двумя фундаментальными понятиями: «логическое следование» (выводимость) и «материальная импликация». Без неё невозможно было бы построить адекватную формальную семантику для многих логических систем.

Применение в программировании

В информатике теорема дедукции лежит в основе метода доказательства программ, известного как «логика Хоара». В этой логике утверждение о программе имеет вид {P} S {Q}, где P — предусловие, S — оператор, Q — постусловие. Теорема дедукции позволяет преобразовывать такие тройки в импликации, что упрощает верификацию программ.

Применение в искусственном интеллекте

В системах автоматического доказательства теорем (например, в резолюционном методе) теорема дедукции используется для преобразования задачи доказательства импликации в задачу поиска противоречия. Если нужно доказать A → B, то добавляют A к посылкам и пытаются вывести B, а затем, используя теорему дедукции, получают импликацию.

Ограничения и обобщения

Теорема дедукции не является универсальной и может не выполняться в некоторых неклассических логиках.

Неклассические логики

• Модальные логики: В модальных логиках, таких как S4 или S5, прямое применение теоремы дедукции может приводить к некорректным результатам из-за особенностей правил, связанных с модальными операторами (□, ◇). Для них разработаны модифицированные версии теоремы.
• Многозначные логики: В некоторых многозначных логиках, где импликация не является «материальной» (например, в логике Лукасевича), теорема дедукции может не выполняться в полном объёме.
• Субструктурные логики: В логиках, где ослаблены структурные правила (например, в линейной логике), теорема дедукции принимает более сложную форму, учитывающую количество использований посылки.

Обобщения

Для логик, где теорема дедукции не выполняется, существуют её обобщения, такие как «теорема дедукции с ограничениями» или «теорема дедукции для секвенций». В исчислении секвенций Генцена теорема дедукции фактически встроена в правила введения импликации справа и слева.

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

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

Источники

1. Чёрч, А. Введение в математическую логику. — М.: Издательство иностранной литературы, 1960. — Т. 1.
2. Мендельсон, Э. Введение в математическую логику. — М.: Наука, 1976.
3. Клини, С. К. Математическая логика. — М.: Мир, 1973.
4. Такеути, Г. Теория доказательств. — М.: Мир, 1978.
5. Генцен, Г. Исследования логических выводов // Математическая теория логического вывода. — М.: Наука, 1967.