Определение слова «Дедукции Теорема»

Математическая энциклопедия:

Общее название ряда теорем, позволяющих устанавливать доказуемость импликации в случае, когда дан логический вывод формулы Виз формулы А. В простейшем случае классического, интуиционистского и т. п. исчислений высказываний Д. т. утверждает: если Г, (из допущений Г, Авыводимо В), то (*) (Г может быть пусто). При наличии кванторов аналогичное утверждение неверно: но не Одна из формулировок Д. т. для традиционных исчислений предикатов (классического, интуиционистского и т. п.): если Г, А|-В, то где означает результат приписывания V -кванторов (см. Квантор )по всем свободным переменным формулы А. В частности, если А- замкнутая формула, Д. т. принимает форму (*). Эта формулировка Д. т. дает возможность сводить поиск вывода в аксиоматич. теориях к поиску вывода в исчислении предикатов: формула В выводима из аксиом A1, ...,An тогда и только тогда, когда в исчислении предикатов выводима формула Похожим образом формулируется Д. т. для логик, где имеются связки, "похожие" на кванторы. Так, для модальных логик S4 и S5 Д. т. имеет вид: если Г,то Более тонкие формулы Д. т. получаются, если вводить V-кванторы не по всем свободным переменным, а лишь по тем, к-рые связываются кванторами в процессе вывода. Говорят, что переменная y варьируется для формулы А в данном выводе, если увходит свободно в Аи в рассматриваемом выводе имеется применение правила введения V в заключение импликации (или введения Э в посылку), при к-ром вводится квантор по y, причем посылка этого применения зависит в данном выводе от А. Теперь Д. т. для традиционных исчислений предикатов уточняется так: если Г, то где y1, ... , у п- полный список переменных, к-рые варьируются для Ав данном выводе. В частности, если никакая свободная переменная из Ане варьируется, то Д. т. принимает форму (*). При формулировке соответствующего уточнения Д. т. для модальных логик следует считать, что варьирование происходит в правилах введения в заключение импликации и — в посылку. При установлении Д. т. для исчислений релевантной импликации (т.

Новая философская энциклопедия:

ДЕДУКЦИИ ТЕОРЕМА – метатеоретическое утверждение о формальной логической теории (исчислении) Т, в соответствии с которым существование в исчислении Т вывода логического [ВЫВОД ЛОГИЧЕСКИЙ] формулы В из называемых гипотезами формул А1 А2, ..., Аn (символически: А1 А2, ..., Аn В) означает, что в Т существует также вывод из посылок А1 А2, ..., Аn-1 импликации АnВ (символически: А1 А2, ..., Аn-1 АnВ). Далее дедукции теорема может быть применена снова вплоть до получения утверждения А1.А2...Аn-1.АnВ. Теорема дедукции доказуема для исчислений классической логики, в языке которых используется материальная импликация. В общем случае она имеет силу для любых исчислений в которых доказуемы законы утверждения консеквента А.ВА и самодистрибутивности импликации (А.ВА).АВ.АС. Для исчислении, в которых закон утверждения консеквента, нередко объявляемый парадоксальным, не принимается (см. Релевантная логика [РЕЛЕВАНТНАЯ ЛОГИКА]), нахождение подходящей формулировки теоремы дедукции является проблемой (Сидоренко Е.А. Нормализованные выводы и обобщение теоремы дедукции. – В кн.: Логические исследования, вып. 5. М, 1998).
В естественных рассуждениях теореме дедукции соответствует способ обоснования истинности условных высказываний вида «Если А, то В», при котором такое высказывание считается истинным, когда удается установить выводимость В из А и некоторой совокупности предложений Г, истинность которых считается установленной.
Е.А.Сидоренко

Смотреть другие определения →