Prawo podwójnego przeczenia

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

$\mathrm{\neg }\mathrm{\neg }p\to p,$

oraz słabego prawa podwójnego przeczenia:

$p\to \mathrm{\neg }\mathrm{\neg }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.	$(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p$	prawo redukcji do absurdu
2.	$[(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p]\to \{p\to [(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p]\}$	prawo poprzedzania
3.	$p\to [(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p]$	reguła odrywania: 1,2
4.	$\{p\to [(\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)\to \mathrm{\neg }\mathrm{\neg }p\}\to \{[p\to (\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)]\to [p\to \mathrm{\neg }\mathrm{\neg }p]\}$	sylogizm Fregego
5.	$[p\to (\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)]\to [p\to \mathrm{\neg }\mathrm{\neg }p]$	reguła odrywania: 3,4
6.	$p\to (\mathrm{\neg }p\to \mathrm{\neg }\mathrm{\neg }p)$	prawo przepełnienia
7.	$p\to \mathrm{\neg }\mathrm{\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 ($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: $\mathrm{\neg }\mathrm{\neg }c=d\ne c.$

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

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

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

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

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

Zobacz też

• intuicjonistyczny rachunek zdań

Bibliografia

• 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.