Prawo podwójnego przeczenia

Zasugerowano, aby zintegrować ten artykuł z artykułem Prawo podwójnej negacji .

Uzasadnienie:  identyczna tematyka

Prawo podwójnego przeczenia – prawo logiki formalnej. Występuje w formie silnego prawa podwójnego przeczenia:

${\displaystyle \lnot \lnot p\to p,}$

oraz słabego prawa podwójnego przeczenia:

${\displaystyle p\to \lnot \lnot p.}$

Silne prawo podwójnego przeczenia dodane do aksjomatów intuicjonistycznego rachunku zdań tworzy aksjomatykę klasycznego rachunku zdań. Skąd też niejawnie wynika, iż w rachunku intuicjonistycznym jest ono niedowodliwe.

Natomiast Słabe prawo podwójnego przeczenia z kolei jest tezą rachunku intuicjonistycznego:

1.	${\displaystyle (\neg p\to \neg \neg p)\to \neg \neg p}$	prawo redukcji do absurdu
2.	${\displaystyle [(\neg p\to \neg \neg p)\to \neg \neg p]\to \{p\to [(\neg p\to \neg \neg p)\to \neg \neg p]\}}$	prawo poprzedzania
3.	${\displaystyle p\to [(\neg p\to \neg \neg p)\to \neg \neg p]}$	reguła odrywania: 1,2
4.	${\displaystyle \{p\to [(\neg p\to \neg \neg p)\to \neg \neg p\}\to \{[p\to (\neg p\to \neg \neg p)]\to [p\to \neg \neg p]\}}$	sylogizm Fregego
5.	${\displaystyle [p\to (\neg p\to \neg \neg p)]\to [p\to \neg \neg p]}$	reguła odrywania: 3,4
6.	${\displaystyle p\to (\neg p\to \neg \neg p)}$	prawo przepełnienia
7.	${\displaystyle p\to \neg \neg p}$	reguła odrywania: 5,6

Jawny dowód niewyprowadzalności silnego prawa podwójnego przeczenia dostajemy z jednego spośród twierdzeń o pełności dla intuicjonistycznego rachunku zdań, zgodnie z którym formuła zdaniowa jest tezą rachunku intuicjonistycznego wtedy i tylko wtedy, gdy jest ona prawdziwa w dowolnej algebrze Heytinga. Poniżej widzimy algebrę Heytinga (${\displaystyle H=\{0,1\}\times \{0,1,2\}}$ z porządkiem „po współrzędnych”), w której silne prawo podwójnego przeczenia nie zachodzi:

Mianowicie w algebrze tej: ${\displaystyle \neg \neg c=d\neq c.}$

W algebrze tej nie zachodzi także prawo wyłączonego środka (tertium non datur): ${\displaystyle p\vee \neg p.}$

W rzeczy samej, w algebrze tej ${\displaystyle c\vee \neg c=c\vee a=b.}$

Jest to o tyle naturalne, że w intuicjonistycznym rachunku zdań dowodliwa jest formuła ${\displaystyle (p\vee \neg p)\to (\neg \neg p\to p){:}}$

1.	${\displaystyle \neg p\to (\neg \neg p\to p)}$	prawo redukcji do absurdu
2.	${\displaystyle p\to (\neg \neg p\to p)}$	prawo poprzedzania
3.	${\displaystyle {\big (}p\to (\neg \neg p\to p){\big )}\to {\Big [}{\Big (}\neg p\to (\neg \neg p\to p){\Big )}\to {\Big (}p\vee \neg p\to (\neg \neg p\to p){\Big )}{\Big ]}}$	prawo łączenia implikacji
4.	${\displaystyle {\Big (}\neg p\to (\neg \neg p\to p){\Big )}\to {\Big (}p\vee \neg p\to (\neg \neg p\to p){\Big )}}$	reguła odrywania: 2,3
5.	${\displaystyle p\vee \neg p\to (\neg \neg p\to p)}$	reguła odrywania: 1,4

Natomiast w algebrze tej prawdziwe jest słabe prawo wyłączonego środka: ${\displaystyle \neg p\vee \neg \neg p.}$

• intuicjonistyczny rachunek zdań

• Marciszewski, Witold (red.) [1987]. Logika formalna. Zarys encyklopedyczny z zastosowaniem do informatyki i lingwistyki, PWN, Warszawa.
• Marciszewski, Witold (red.) [1988]. Mała encyklopedia logiki, wyd. 2 rozszerzone, Ossolineum, Wrocław (I wyd. 1970).
• Pogorzelski, Witold [1992]. Elementarny słownik logiki formalnej, wyd. Filii UW, Białystok.