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

Материал из Википедии — свободной энциклопедии

Эту статью предлагается объединить с закон исключения третьего.
Пояснение причин и обсуждение — на странице Википедия:К объединению.
Обсуждение длится одну неделю. Дата постановки — 14 апреля года.
Если обсуждение не требуется (очевидный случай) используйте другие шаблоны.

Зако́н двойно́го отрица́ния — положенный в основу классической логики принцип, согласно которому «если неверно, что неверно А, то верно А». Закон двойного отрицания называется также законом снятия двойного отрицания. В формализованном языке логики высказываний закон двойного отрицания выражается формулой $\neg\neg p \rightarrow p$ и в таком виде фигурирует обычно в перечне логических аксиом формальных теорий. В традиционной содержательной математике закон двойного отрицания служит логическим основанием для проведения так называемых доказательств от противного по следующей схеме: из предположения, что суждение А данной математической теории неверно, выводится противоречие в этой теории, затем на основании непротиворечивости теории делается вывод, что неверно «не А», и тогда по закону двойного отрицания заключают, что верно А. В рамках конструктивных рассмотрений, когда действует требование алгоритмической реализуемости обоснования математических суждений, закон двойного отрицания оказывается, вообще говоря, неприемлемым.

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

[править] Другие формулировки

Закон двойного отрицания тесно связан с законом исключённого третьего, а также с так называемым законом Пирса. В определенном смысле все три закона эквивалентны. Так, в интуиционистском исчислении высказываний, где эти законы не являются тавтологиями, каждый из этих двух законов выводим из другого, а добывление любого из них в аксиоматику сразу приводит к классической логике. При этом однако, существуют логики, в которых все три закона неэквивалентны^[1].

[править] Примечания

↑ Zena M. Ariola and Hugo Herbelin. Minimal classical logic and control operators. In Thirtieth International Colloquium on Automata, Languages and Programming , ICALP’03, Eindhoven, The Netherlands, June 30 - July 4, 2003, volume 2719 of Lecture Notes in Computer Science, pages 871–885. Springer-Verlag, 2003.[1]