Закон двойного отрицания
опущение двойного отрицания формулы / Материал из Википедии — свободной encyclopedia
Зако́н двойно́го отрица́ния — положенный в основу классической логики принцип, согласно которому «если неверно, что неверно А, то А верно». Есть 3 формулировки закона двойного отрицания. В формализованном языке логики высказываний они выражаются формулами:
- — закон введения двойного отрицания;
- — закон снятия двойного отрицания;
- — полный закон двойного отрицания.
В интуиционистской логике выводится лишь закон введения двойного отрицания, закон снятия же не выводится.
В традиционной содержательной математике закон двойного отрицания служит логическим основанием для проведения так называемых доказательств от противного по следующей схеме: из предположения, что суждение А данной математической теории неверно, выводится противоречие в этой теории, затем на основании непротиворечивости теории делается вывод, что неверно «не А», и тогда по закону снятия двойного отрицания заключают, что верно А. В рамках конструктивных рассмотрений, когда действует требование алгоритмической реализуемости обоснования математических суждений, закон снятия двойного отрицания оказывается, вообще говоря, неприемлемым.
Типичным тому примером служит всякое доказательство от противного суждения А, имеющего вид «при всяком х существует у такой, что верно В(х, у)», когда последний шаг, состоящий в применении закона снятия двойного отрицания, оказывается невозможным из-за того, что конструктивное понимание суждения требует для его обоснования построения алгоритма, который по каждому х давал бы конструкцию у такого, что верно В(х, у). Между тем рассуждение с применением закона снятия двойного отрицания не приводит к построению какого бы то ни было алгоритма; более того, искомого в этом случае алгоритма может вообще не существовать (см. также принцип конструктивного подбора).