Общая характеристика теоремы дедукции
Формы теоремы дедукции и способы их доказательства – это варианты представления одного из фундаментальных результатов теории доказательства, формализующего способ рассуждения, в рамках которого при установлении импликации A→B в качестве необходимого условия вывода используют А.
Введем необходимые для формулировки теоремы дедукции определения.
Пусть Гамма (Г) – это некоторое множество формул, тогда последовательность формул, каждая из которых элемент Г или аксиома, или может быть выведена по правилу modus ponens из более ранних формул, называется выводом из Г.
Формула А, встречающаяся в выводе из множества формул Г, называется выводимой из Г, что обозначается А ⊢ Г.
Теорема дедукции является ключевым результатом в математической логике. Она устанавливает связь между импликацией (логическим следованием) и доказательством в формальной системе.
Формулировка теоремы дедукции может быть следующей: Пусть Γ - множество предположений (предложений) в формальной системе, A и B - предложения, тогда если Γ ∪ {A} ⊢ B, то Γ ⊢ A → B.
Это означает, что если мы можем доказать B при условии, что A верно и предположения в Γ верны, то мы можем сделать вывод, что если все предположения в Γ верны, то A → B также верно. Иными словами, теорема дедукции говорит нам о том, что если мы хотим доказать импликацию A → B, то мы можем добавить A в качестве дополнительного предположения и доказать B при условии, что A верно.
Теорема дедукции является одним из основных инструментов в формальной логике и используется для построения и анализа доказательств в различных областях, таких как математика, философия и информатика. Она позволяет нам разрабатывать строгие и логически обоснованные аргументы и выводы.
Доказательство теоремы дедукции
Если рассматривать теорему дедукции слева направо, она очень проста. Действительно, добавив к выводу из Г импликации A → B формулы A и B, получаем вывод В из Г U {A}. Формула А может быть написана как посылка, а В получена по modus ponens.
Справа налево с помощью индукции доказывается утверждение: если выводом из Г U {A} являются С1, … Сn, то для всех i от 1 до n выводима из Г импликация А → Сi. Индуктивное рассуждение опирается на принцип, который объединяет в себе базу и переход: если выводимы импликации А → С1, … А → С(i-1), то А → Сi тоже выводима.
Рассмотрим следующие случаи:
Сi – аксиома. Тогда вывод импликации включает три шага:
- Ci;
- Ci → (А → Сi) – по аксиоме, что истина может следовать из чего угодно;
- А → Сi – из двух предшествующих шагов по modus ponens.
Сi – посылка, или элемент Г U {A}:
- Сi принадлежит Г – применяется такой же вывод, как для Сi – аксиомы;
- Сi = А. Импликация А → А выводится по теореме о том, что выводимым является закон тождества (т.е. ⊢ A → А).
Ci по правилу modus ponens выводится из формул Cj и Ck, где j $\lt$ i, k $\lt$ i. В таком случае, чтобы можно было применять modus ponens, обязательно, чтобы Ck имело вид Cj → Ci. По индуктивному предположению Г ⊢ (А → Cj) и Г ⊢ (А → Ck), т.е. Г ⊢ (А → (Cj → Ci)). Добавляем далее в вывод аксиому: (А → (Cj → Ci)) → ((А → Cj) → (А → Ci)). Дважды применив modus ponens, получаем то, что требовалось доказать: А → Ci.
Таким образом, разобраны все возможные случаи. Был установлен индукционный принцип; теорема доказана.
Теорема дедукции в неклассических исчислениях
Теорема дедукции в общем случае представляет собой метатеоретическое утверждение, относящееся к формальной логической теории Т. В соответствии с этим утверждением, если в Т существует логический вывод формулы В из гипотез – формул A1 .. An, то в Т (при некоторых ограничениях) существует также вывод An → B из A1 .. A(n-1). Здесь символом → обозначена импликация, фигурирующая в языке Т. Обычно теорему о дедукции формулируют как утверждение, что правомерно перейти от верного для теории утверждения Г, А ⊢ В к верному для этой же теории утверждению Г ⊢ A → B.
Без всякий ограничений эта теорема имеет силу в исчислениях классической логики и вообще в любых пропозициональных исчислениях, в которых доказуемы логические принципы:
- A → .B → А - закон утверждения консеквента;
- (А → .В → С) → .А → В → .А → С – закон самодистрибутивности импликации.
В таких исчислениях можно применять теорему дедукции к утверждению A1 .. A(n-1) ⊢ An → B многократно.
Для естественных рассуждений теорема дедукции выражается с помощью часто применяемого способа обоснования истинности высказываний условного типа «Если А, то В». Это высказывание считают истинным, если удалось установить выводимость В из А и множества предложений Г (в предположении, что их истинность установлена). По сути, здесь неявно используют переход от верного (в некоторой теории, не обязательно фиксированной) Г, А ⊢ В (предполагая, что Г состоит из считающихся истинными утверждений) к Г ⊢ A → B и затем к A → B. Поэтому ясно, что логическая теория, которая описывает какой-либо вид импликации (условной связи, следования), должна удовлетворять теореме дедукции в том или ином смысле.
В неклассических (например, релевантных) исчислениях закон утверждения консеквента не принимается. Поэтому поиск подходящих формулировок теоремы дедукции представляет собой определенную проблему.
Известно, что многие утверждения о выводимости могут быть сформулированы (и доказаны) без ссылок на фиксированную логику. Для этого достаточно опираться лишь на само определение вывода. Вместе с тем такое определение может быть различным. От этого, естественно, будут различными и классы приемлемых утверждений о выводимости, а также классы правил, позволяющих переход от одних утверждений такого типа к другим.
Определение вывода и принимаемая формулировка теоремы дедукции (а формулировки последней также могут быть различными при одинаковом определении вывода) задают различные классы утверждений о выводимости. В этой ситуации теорема дедукции, сохраняя название, выступает в качестве не обычной метатеоремы исчисления, но в качестве правила построения вывода, разрешающего переходить от первого из указанных выводов ко второму. Поэтому правильнее было бы в этих случаях говорить не о теореме, а о принципе дедукции.
