Дедукции теорема

- общее название ряда теорем, позволяющих устанавливать доказуемость импликации [img: http://localhost:8080/file/020507-23.jpg] в случае, когда дан логический вывод формулы Виз формулы А. В простейшем случае классического, интуиционистского и т. п. исчислений высказываний Д. т. утверждает: если Г, [img: http://localhost:8080/file/020507-24.jpg] (из допущений Г, Авыводимо В), то [img: http://localhost:8080/file/020507-25.jpg] (*) (Г может быть пусто). При наличии кванторов аналогичное утверждение неверно: [img: http://localhost:8080/file/020507-26.jpg] но не [img: http://localhost:8080/file/020507-27.jpg] Одна из формулировок Д. т. для традиционных исчислений предикатов (классического, интуиционистского и т. п.): если Г, А|-В, то [img: http://localhost:8080/file/020507-28.jpg] где [img: http://localhost:8080/file/020507-29.jpg] означает результат приписывания V -кванторов (см. Квантор)по всем свободным переменным формулы А. В частности, если А- замкнутая формула, Д. т. принимает форму (*). Эта формулировка Д. т. дает возможность сводить поиск вывода в аксиоматич. теориях к поиску вывода в исчислении предикатов: формула В выводима из аксиом A1,...,An тогда и только тогда, когда в исчислении предикатов выводима формула [img: http://localhost:8080/file/020507-30.jpg] Похожим образом формулируется Д. т. для логик, где имеются связки, "похожие" на кванторы. Так, для модальных логик S4 и S5 Д. т. имеет вид: если Г, [img: http://localhost:8080/file/020507-31.jpg] то [img: http://localhost:8080/file/020507-32.jpg] Более тонкие формулы Д. т. получаются, если вводить V-кванторы не по всем свободным переменным, а лишь по тем, к-рые связываются кванторами в процессе вывода. Говорят, что переменная y варьируется для формулы А в данном выводе, если увходит свободно в Аи в рассматриваемом выводе имеется применение правила введения V в заключение импликации (или введения Э в посылку), при к-ром вводится квантор по y, причем посылка этого применения зависит в данном выводе от А. Теперь Д. т. для традиционных исчислений предикатов уточняется так: если Г, [img: http://localhost:8080/file/020507-33.jpg] то [img: http://localhost:8080/file/020507-34.jpg] где y1,..., у п- полный список переменных, к-рые варьируются для Ав данном выводе. В частности, если никакая свободная переменная из Ане варьируется, то Д. т. принимает форму (*). При формулировке соответствующего уточнения Д. т. для модальных логик следует считать, что варьирование происходит в правилах введения [img: http://localhost:8080/file/020507-35.jpg] в заключение импликации и [img: http://localhost:8080/file/020507-36.jpg] - в посылку. При установлении Д. т. для исчислений релевантной импликации (т. Если Ане варьируется в данном выводе, то Д. т. принимает форму (*), а если Аварьируется, то Д. т. принимает вид: если А, Г|- В, то [img: http://localhost:8080/file/020507-40.jpg] где t- константа "истина" (или конъюнкция формул ([img: http://localhost:8080/file/020507-41.jpg]) для всех пропозициональных переменных р, выходящих в Л, Г, В).