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

- общее название ряда теорем, позволяющих устанавливать доказуемость импликации в случае, когда дан логический вывод формулы Виз формулы А. В простейшем случае классического, интуиционистского и т. П. Исчислений высказываний Д. Т. Утверждает. Если Г, (из допущений Г, Авыводимо В), то (*) (Г может быть пусто). При наличии кванторов аналогичное утверждение неверно. но не Одна из формулировок Д. Т. Для традиционных исчислений предикатов (классического, интуиционистского и т. П.). Если Г, А|-В, то где означает результат приписывания V -кванторов (см. Квантор )по всем свободным переменным формулы А. В частности, если А- замкнутая формула, Д. Т. Принимает форму (*). Эта формулировка Д. Т. Дает возможность сводить поиск вывода в аксиоматич.

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

Теперь Д. Т. Для традиционных исчислений предикатов уточняется так. Если Г, то где y1, . , у п- полный список переменных, к-рые варьируются для Ав данном выводе. В частности, если никакая свободная переменная из Ане варьируется, то Д. Т. Принимает форму (*). При формулировке соответствующего уточнения Д. Т. Для модальных логик следует считать, что варьирование происходит в правилах введения в заключение импликации и - в посылку. При установлении Д. Т. Для исчислений релевантной импликации (т.