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

Теорема о дедукции — это фундаментальное утверждение в математической логике, устанавливающее связь между доказуемостью импликации и отношением логического следования. В своей наиболее общей форме теорема гласит: если из множества посылок \(\Gamma\) и дополнительной гипотезы \(A\) выводима формула \(B\) (то есть \(\Gamma, A \vdash B\)), то из исходного множества посылок \(\Gamma\) выводима импликация \(A \to B\) (то есть \(\Gamma \vdash A \to B\)). Иными словами, теорема формализует интуитивно понятный принцип: чтобы доказать условное утверждение «если A, то B», достаточно временно принять A в качестве допущения и вывести B.

Теорема о дедукции является метатеоремой, то есть утверждением о самой формальной системе, а не теоремой внутри неё. Она играет ключевую роль в теории доказательств, позволяя упрощать построение выводов и обосновывать эквивалентность различных форм записи логических законов. Впервые в явном виде теорема была сформулирована и доказана для исчисления высказываний в работах Альфреда Тарского (1921) и Жака Эрбрана (1930), хотя её неявное использование восходит к трудам Готлоба Фреге и Джузеппе Пеано.

История

Предпосылки и ранние формулировки

Идея, лежащая в основе теоремы о дедукции, была известна ещё в античной логике в виде правила условного доказательства (лат. modus ponens в обратном направлении). Однако формализация этого принципа стала возможной только с развитием математической логики в конце XIX — начале XX века. Готлоб Фреге в своей «Исчислении понятий» (1879) впервые построил аксиоматическую систему логики, где импликация была одной из основных связок, но явного утверждения о связи между выводом и импликацией не сформулировал.

Работы Тарского и Эрбрана

В 1921 году Альфред Тарский в своей докторской диссертации, посвящённой аксиоматике исчисления высказываний, впервые строго доказал теорему о дедукции для классической логики. Он показал, что если формула \(B\) выводима из аксиом и гипотезы \(A\), то формула \(A \to B\) также является теоремой. Независимо от Тарского, в 1930 году Жак Эрбран в своей диссертации «Исследования по теории доказательств» обобщил этот результат на логику первого порядка, сформулировав теорему для систем с кванторами. Эрбран также использовал теорему для доказательства своей знаменитой теоремы (теорема Эрбрана), связывающей выполнимость формул с их пропозициональными сколемами.

Дальнейшее развитие

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

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

Классическое исчисление высказываний

Пусть \(\Gamma\) — множество формул, \(A\) и \(B\) — формулы в языке классического исчисления высказываний. Теорема о дедукции утверждает: \[ \Gamma, A \vdash B \quad \text{тогда и только тогда, когда} \quad \Gamma \vdash A \to B. \] Доказательство обычно проводится индукцией по длине вывода \(B\) из \(\Gamma \cup \{A\}\). Основные шаги:

1. Если \(B\) — аксиома или элемент \(\Gamma\), то \(B\) выводимо из \(\Gamma\), и из аксиомы \(B \to (A \to B)\) по modus ponens получаем \(\Gamma \vdash A \to B\).
2. Если \(B = A\), то \(\Gamma \vdash A \to A\) (тавтология).
3. Если \(B\) получена по правилу modus ponens из \(C\) и \(C \to B\), то по индукционному предположению \(\Gamma \vdash A \to C\) и \(\Gamma \vdash A \to (C \to B)\). Используя аксиому \((A \to (C \to B)) \to ((A \to C) \to (A \to B))\), получаем \(\Gamma \vdash A \to B\).

Логика первого порядка

Для логики первого порядка теорема о дедукции выполняется при условии, что гипотеза \(A\) не содержит свободных переменных, которые связаны кванторами в выводе. Если \(A\) содержит свободную переменную \(x\), а в выводе \(B\) используется правило обобщения (∀-введение) по \(x\), то импликация \(A \to B\) может быть неверна. В таких случаях применяют модифицированную форму: если \(\Gamma, A \vdash B\) и \(A\) замкнута (не содержит свободных переменных), то \(\Gamma \vdash A \to B\).

Обратная теорема

Обратное утверждение (если \(\Gamma \vdash A \to B\), то \(\Gamma, A \vdash B\)) тривиально, так как следует из одного применения modus ponens. Таким образом, теорема устанавливает эквивалентность между выводимостью импликации и выводимостью заключения при добавленной посылке.

Применение

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

Теорема о дедукции позволяет сводить доказательства импликативных формул к доказательствам с дополнительными гипотезами. Например, чтобы доказать закон транзитивности \((A \to B) \to ((B \to C) \to (A \to C))\), достаточно принять \(A \to B\) и \(B \to C\) в качестве гипотез, затем вывести \(A \to C\) (что делается простым цепочкой modus ponens), а затем дважды применить теорему о дедукции.

Связь с исчислением секвенций

В секвенциальном исчислении Генцена теорема о дедукции соответствует правилу введения импликации в правую часть секвенции: \(\frac{\Gamma, A \Rightarrow B}{\Gamma \Rightarrow A \to B}\). Это правило является одним из основных в системах натурального вывода и секвенций.

Теория моделей и полнота

Теорема о дедукции тесно связана с теоремой о полноте для логики первого порядка. Она используется при доказательстве того, что любая логически общезначимая формула является теоремой (полнота по Гёделю). В частности, из теоремы о дедукции следует, что если формула \(A \to B\) общезначима, то из \(A\) логически следует \(B\), и наоборот.

Программирование и искусственный интеллект

В логическом программировании (например, в языке Prolog) теорема о дедукции лежит в основе механизма вывода с возвратом (backward chaining). Правило «если из фактов и правил выводится цель, то можно добавить новое правило» является прямым следствием теоремы. В системах автоматического доказательства теорем (ATP) теорема используется для построения доказательств в стиле натурального вывода.

Примеры

Пример 1: Доказательство тавтологии

Докажем, что \(A \to (B \to A)\) является теоремой. Примем \(A\) в качестве гипотезы. Из аксиомы \(A \to (B \to A)\) (которая является аксиомой в системе Фреге-Лукасевича) по modus ponens получаем \(B \to A\). Применяя теорему о дедукции, получаем \(\vdash A \to (B \to A)\).

Пример 2: Вывод в натуральном исчислении

Пусть даны посылки: \(P \to Q\) и \(Q \to R\). Требуется доказать \(P \to R\). Примем \(P\) в качестве гипотезы. Из \(P\) и \(P \to Q\) по modus ponens получаем \(Q\). Из \(Q\) и \(Q \to R\) получаем \(R\). По теореме о дедукции, \(P \to R\) выводимо из исходных посылок.

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

Интуиционистская логика

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

Модальные логики

В модальных логиках (например, S4, S5) теорема о дедукции требует осторожности. Если в выводе используется правило необходимости (necessitation): из \(\vdash A\) следует \(\vdash \Box A\), то при добавлении гипотезы \(A\) это правило может быть неприменимо. Поэтому для модальных логик часто формулируют «локальную» теорему о дедукции, где импликация заменяется на строгую импликацию.

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

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

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

• Теорема о дедукции является одним из немногих метатеоретических результатов, которые справедливы для большинства «хороших» логических систем (классической, интуиционистской, модальных S4, S5).
• В некоторых аксиоматических системах (например, в системе Гильберта-Аккермана) теорема о дедукции используется для доказательства того, что все тавтологии являются теоремами.
• Обратная теорема (из \(\Gamma \vdash A \to B\) следует \(\Gamma, A \vdash B\)) иногда называется «правилом отделения» (modus ponens) и является тривиальной, но именно её существование делает теорему о дедукции полезной.

Источники

• Тарский А. «Введение в логику и методологию дедуктивных наук». — М.: Издательство иностранной литературы, 1948.
• Эрбран Ж. «Исследования по теории доказательств» (1930).
• Мендельсон Э. «Введение в математическую логику». — М.: Наука, 1976.
• Клини С. К. «Математическая логика». — М.: Мир, 1973.
• Генцен Г. «Исследования логических выводов» (1935).