Приглашаем посетить сайт
Дедукции теорема
ДЕДУКЦИИ ТЕОРЕМА (от лат. deductio - выведение) - утверждение о свойствах логической теории. Д. т. гласит: «Если имеется вывод Г, А (- В, то имеется также и вывод Г J- А -> В, где -> - знак импликации, Г - произвольное (возможно пустое) множество формул языка теории, А, В - произвольные формулы языка теории». Название «Д. т .» принадлежит Д. Гильберту и П. Бернайсу Hubert D., Bernays P. Grundlagen der Mathematik. Berlin, 1934), однако доказательство теоремы встречается еще раньше в работе Эрбрана (Herbrand /. Recherches sur la theorie de la demonstration // Travaux de la Societe des Sciences et des Letters de Varsovie. Classe III. Sciences Mathematiques et Physiques. № 33. 1930).
Д. т. позволяет использовать при построении выводов и доказательств вспомогательное правило: «Если необходимо вывести или доказать импликативную формулу, то достаточно осуществить вспомогательный вывод, в котором в качестве дополнительного допущения принимается антецедент этой формулы, а обосновывается ее консеквент». Обычно такой дополнительный вывод построить значительно проще.
Доказательство Д. т. осуществляется методом возвратной математической индукции. Цель доказательства - показать, как вспомогательный вывод Г, А |- В может быть на каждом шаге вывода перестроен в вывод Г \-А -> В. При этом стандартное доказательство основывается на использовании следующих дедуктивных принципов: «утверждение консеквента» А - > ( В - > А ) и «самодистрибутивность импликации» ( А - > ( В - > А)) - > ( А -» В) -> (А - С), а также «закон тождества» А -> А, получаемый из этих аксиом. Поскольку указанные формулы включаются в аксиоматику интуиционистской логики, доказательство Д. т. для этой логической теории и более сильных (включая классическую логику) является стандартным. Однако далеко не во всех логических теориях принимаются эти дедуктивные принципы. В ряде исчислений неклассической логики доказательство соответствующей формы Д. т. оказывается нетривиальной процедурой. Для некоторых теорий, напр. для отвергающих импликативную формулировку закона тождества, Д. т. доказать невозможно.
Д.В. Зайцев