Akademik

теорема дедукции, – одно из важнейших содержательных утверждений математической логики, определяющее связь между логически правильными (аподиктическими) рассуждениями (или умозаключениями, или выводами) и законами (доказуемыми формулами) логики, лежащими в их основе. Прообраз Т. о д. был известен еще стоикам (см. J. B. Mates, Stoic logic, Berk. – Los Ang., 1953) в виде общего принципа связи между выводимостью и импликацией. Как (металогическая) теорема логических исчислений Т. о д. была сформулирована независимо франц. математиком Ж. Эрбраном (1928) и А. Тарским (1930) и доказана Эрбраном (1930) для исчислений, включающих положительное импликативное исчисление высказываний Гильберта [см. Положительная логика, аксиомы 2.1) и 2.2)]. Формулировки Т. о д. зависят, вообще говоря, от того как в том или ином исчислении определяются понятия "выводимость" и "импликация"; поэтому всегда следует иметь в виду тот или иной в а р и а н т Т. о д.

Интуитивно ясным примером Т. о д. для исчисления высказываний может служить следующая ее формулировка: (1) если из аксиом исчисления и к.-л. допущения (гипотезы) А, добавленного к числу аксиом, по правилам исчисления выводимо В, то в этом исчислении доказуемо (выводимо только из аксиом) условие (импликация) A⊃B, означающее, что если доказано А, то доказано и В. Др. словами, данная формулировка Т. о д. означает, что при наличии отношения логич. следования между любой (произвольной) посылкой А и заключением В, доказуемость В релятивизируется условием доказуемости А, или, что то же, доказательство В сводится (см. Сводимость) к доказательству А. Идея такого сведения, являющегося отражением а н а л и т и ч е с к о г о процесса решения матем. и логич. задач, очевидна: после того как установлено, что В является следствием А – на что указывает факт выводимости В из А, – совершенно ясно, что В конечно же будет доказано, если удастся показать, что А – теорема исчисления. Это вытекает из обратного утверждения, отражающего уже с и н т е т и ч е с к у ю часть решения: по правилу modus ponens, если А доказуемая формула, то из A и доказанного в силу Т. о д. утверждения A⊃B следует, что В доказано. Поэтому Т. о д. часто называют обращением modus ponens и, основываясь на указанной взаимной связи между выводимостью и импликацией, формулируют так: (2) необходимым и достаточным условием для категорического утверждения А1, А2, ..., Аn В (т.е. для утверждения о выводимости в нек-ром исчислении по его правилам заключения В из посылок А1, А2, ..., Аn ) является логическая истинность (доказуемость в этом исчислении) условного утверждения А1⊃(А2⊃(...⊃(Аn ⊃B)...)). Эта формулировка Т. о д. фиксирует ту, замеченную еще стоиками, особую роль, к-рую в логике высказываний играют ее законы при определении (проверке) логич. правильности наших рассуждений: относительно любого утверждения о выводимости заключения В из посылок А1, А2, ..., Аn вопрос о его истинности решается разысканием среди законов логики закона А1⊃(А2⊃(...⊃(Аn ⊃B)...)).

Различение понятий "выводимость" и "доказуемость" (соответственно "вывод" и "доказательство") в приведенных выше формулировках Т. о д. восходит к традиц. различению между понятиями "формальная правильность" и "истинность". Пусть В выведено из к.-л. допущений (гипотез) А1, ..., Аm. Доказано ли B? В общем случае очевидно нет, потому что допущения могут быть любыми, в том числе и ложными, а понятие логич. вывода определяется, как правило, так, что из лжи можно вывести любое, в том числе и ложное, заключение. Для того чтобы В было доказано, необходимо, чтобы В следовало из заведомо истинных (или принимаемых за истинные) посылок.

Т. о д. имеет место только для исчислений логистического типа, в к-рых вывод опирается на "абсолютные" допущения (см. Посылка) – аксиомы (или схемы аксиом). Это объясняется, конечно, не наличием слова "доказуема" в приведенных формулировках теоремы [этого может и не быть: напр., С. К. Клини (1952) и А. Чёрч (1956) используют др. терминологию, так что в их формулировках Т. о д. выражает связь между выводимостью одной формулы и выводимостью (же) нек-рой др. формулы], а просто тем, что Т. о д. – это теорема, т.е. утверждение, доказываемое на основе аксиом. В исчислениях без аксиом (в натуральных исчислениях) вместо Т. о д. вводится в качестве основного (или обосновывается в качестве производного) правило введения и м п л и к а ц и и – в нек-ром смысле аналог Т. о д.: если общий принцип (идею), выражаемый Т. о д., рассматривать независимо от того, что это принцип (идея) теоремы, то его можно постулировать в форме правила (Г. Генцен, С. Ящьковский, 1934), к-рое равносильно названным выше аксиомам 2.1) и 2.2) положительной логики.

Лит.: Тарский А., Введение в логику и методологию дедуктивных наук, М., 1948, с. 173–79; Клини С. К., Введение в метаматематику, пер. с англ.. М., 1957, с. 84–91; Чёрч А., Введение в математическую логику, пер. с англ., т. 1, М., 1960, с. 80, 186, 287; Гудстейн Р. Л., Математическая логика, пер. с англ., М., 1961, с. 35–37, 43–44; Новиков П. С., Элементы математической логики, М., 1959, с. 82–85, 221–25; Столл Р. Р., Множества. Логика. Аксиоматические теории, пер. с англ., М., 1968, с. 171–72; Линдон Р., Заметки по логике, пер. с англ., М., 1968, с. 72–73; Herbrand J., Recherches sur la théorie de la démonstration, Warsz., 1930; Pogorzelski W. A., Przegląd twierdzeń о dedukcji dla rachunków zdań, "Studia Logica", 1964, t. 15.