Закон подвійного заперечення

Зако́н подві́йного запере́чення — принцип, що покладений в основу класичної логіки, згідно з яким «якщо неправильно, що неправильно А, то А правильно». Закон подвійного заперечення називається законом зняття подвійного заперечення. Формалізованою мовою логіки висловлювань закон подвійного заперечення може бути виражений формулою

${\displaystyle \neg (\neg A)\rightarrow A}$

і в такому вигляді фігурує, зазвичай, в переліку логічних аксіом формальних теорій. У традиційній змістовній математиці закон подвійного заперечення служить логічною підставою для проведення так званих доведень від супротивного за наступною схемою: з припущення, що судження А цієї математичної теорії є неправильним, виводиться суперечність у цій теорії, потім на підставі несуперечності теорії робиться висновок, що неправильним є «не А», тоді за законом подвійного заперечення укладають те, що А є правильним. У рамках конструктивних поглядів, коли діє вимога алгоритмічної реалізованості обґрунтування математичних суджень, закон подвійного заперечення виявляється, взагалі кажучи, неприйнятним.

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