Двойного Отрицания Закон

Логический принцип, согласно к-рому "если неверно, что неверно А, то верно Л". Д. о. з. наз. также законом снятия двойного отрицания. В формализованном языке логики высказываний Д. о. з. выражается формулой и в таком виде (или в виде соответствующей аксиом схемы )фигурирует обычно в перечне логич. аксиом формальных теорий. В традиционной содержательной математике Д. о. з. служит логич. основанием для проведения так наз. доказательств от противного в непротиворечивых теориях по следующей схеме: из предположения, что суждение Аданной математич. теории неверно, выводится противоречие в этой теории, затем на основании непротиворечивости теории делается вывод, что неверно "не А", и тогда по Д. о. з. заключают, что верно А. В рамках конструктивных рассмотрений, когда действует требование алгоритмич. эффективности обоснования математич. суждений, Д. о. з. оказывается, вообще говоря, неприемлемым. Типичным тому примером служит всякое доказательство от противного суждения А, имеющего вид "при всяком хсуществует утакой, что верно В( х, у)", когда последний шаг, состоящий в применении Д. о. з., оказывается невозможным из-за того, что конструктивное понимание суждения требует для его обоснования построения алгоритма, к-рый по каждому хдавал бы конструкцию утакого, что верно В( х, у). Между тем рассуждение с применением Д. о. з. не приводит к построению какого бы то ни было алгоритма; более того, искомого в этом случае алгоритма может вообще но существовать (см. также Конструктивного подбора принцип). Д. о. з. тесно связан с исключенного третьего законом, в определенном смысле он даже эквивалентен последнему. Так, в интуиционистском исчислении высказываний каждый из этих двух законов выводим из другого. Лит.:[1] Клини С. К., Введение в метаматематику, пер. о англ., М., 1957. Ф. А. Кабаков.