Z Wikipedii, wolnej encyklopedii
Prawo podwójnego przeczenia – prawo logiki formalnej . Występuje w formie silnego prawa podwójnego przeczenia :
¬
¬
p
→
p
,
{\displaystyle \lnot \lnot p\to p,}
oraz słabego prawa podwójnego przeczenia :
p
→
¬
¬
p
.
{\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.
(
¬
p
→
¬
¬
p
)
→
¬
¬
p
{\displaystyle (\neg p\to \neg \neg p)\to \neg \neg p}
prawo redukcji do absurdu
2.
[
(
¬
p
→
¬
¬
p
)
→
¬
¬
p
]
→
{
p
→
[
(
¬
p
→
¬
¬
p
)
→
¬
¬
p
]
}
{\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.
p
→
[
(
¬
p
→
¬
¬
p
)
→
¬
¬
p
]
{\displaystyle p\to [(\neg p\to \neg \neg p)\to \neg \neg p]}
reguła odrywania: 1,2
4.
{
p
→
[
(
¬
p
→
¬
¬
p
)
→
¬
¬
p
}
→
{
[
p
→
(
¬
p
→
¬
¬
p
)
]
→
[
p
→
¬
¬
p
]
}
{\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.
[
p
→
(
¬
p
→
¬
¬
p
)
]
→
[
p
→
¬
¬
p
]
{\displaystyle [p\to (\neg p\to \neg \neg p)]\to [p\to \neg \neg p]}
reguła odrywania: 3,4
6.
p
→
(
¬
p
→
¬
¬
p
)
{\displaystyle p\to (\neg p\to \neg \neg p)}
prawo przepełnienia
7.
p
→
¬
¬
p
{\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 (
H
=
{
0
,
1
}
×
{
0
,
1
,
2
}
{\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:
¬
¬
c
=
d
≠
c
.
{\displaystyle \neg \neg c=d\neq c.}
W algebrze tej nie zachodzi także prawo wyłączonego środka (tertium non datur) :
p
∨
¬
p
.
{\displaystyle p\vee \neg p.}
W rzeczy samej, w algebrze tej
c
∨
¬
c
=
c
∨
a
=
b
.
{\displaystyle c\vee \neg c=c\vee a=b.}
Jest to o tyle naturalne, że w intuicjonistycznym rachunku zdań
dowodliwa jest formuła
(
p
∨
¬
p
)
→
(
¬
¬
p
→
p
)
:
{\displaystyle (p\vee \neg p)\to (\neg \neg p\to p){:}}
1.
¬
p
→
(
¬
¬
p
→
p
)
{\displaystyle \neg p\to (\neg \neg p\to p)}
prawo redukcji do absurdu
2.
p
→
(
¬
¬
p
→
p
)
{\displaystyle p\to (\neg \neg p\to p)}
prawo poprzedzania
3.
(
p
→
(
¬
¬
p
→
p
)
)
→
[
(
¬
p
→
(
¬
¬
p
→
p
)
)
→
(
p
∨
¬
p
→
(
¬
¬
p
→
p
)
)
]
{\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.
(
¬
p
→
(
¬
¬
p
→
p
)
)
→
(
p
∨
¬
p
→
(
¬
¬
p
→
p
)
)
{\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.
p
∨
¬
p
→
(
¬
¬
p
→
p
)
{\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 :
¬
p
∨
¬
¬
p
.
{\displaystyle \neg p\vee \neg \neg p.}
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.
pojęcia podstawowe
funktory zdaniotwórcze prawa rachunku zdań – jegotautologie z jedną zmienną i bez przeczenia
z jedną zmienną i przeczeniem
z dwoma zmiennymi i bez przeczenia
z dwoma zmiennymi i przeczeniem
z trzema zmiennymi i bez przeczenia
powiązane pojęcia