Теорема дедукции для классических и неклассических исчислений.

Abstract

Как известно, в классической логике под теоремой дедукции имеется в виду утверждение, согласно которому выводимость в соответствующем исчислении формулы $В$ из посылок $\varGamma$ и $А$ (символически: $\varGamma, A\vdash B$) означает, что в этом исчислении существует вывод импликации $A\rightarrow B$ из $\varGamma$, т.е. имеет силу $\varGamma\vdash A \rightarrow B $. Эвристическая значимость указанной теоремы достаточно высока, так как она позволяет, в частности, сводить проблему вывода формул вида $A_1\rightarrow. ...\rightarrow.A_n\rightarrow B$ из посылок $\varGamma$ к менее сложной проблеме вывода $В$ из посылок $\varGamma, A_1, ..., A_n.$

Чтобы более ясно сформулировать основные цели данной работы, напомним определение логического вывода из посылок, которое мы будем называть стандартным.