Twierdzenie o dedukcji - Polski Serwis Naukowy

Poglądowo

Twierdzenie o dedukcji - klasyczne – Jeżeli $A$ jest zdaniem oraz $B\in \operatorname{Cn}_L (X\cup \{A\})$ , to formuła zdaniowa $A\rightarrow B$ należy do zbioru $\operatorname{Cn}_L(X)$ , gdzie $\operatorname{Cn}_L(X)$ to zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych $X$ .

Formalnie

Niech $\mathcal{L}$ będzie jakimkolwiek językiem rozszerzającym język klasycznego rachunku zdań i niech $\mathcal{S}$ będzie rachunkiem zdaniowym w tym języku.

Klasycznym twierdzeniem o dedukcji dla rachunku $\mathcal{S}$ nazywamy następujące stwierdzenie:

Rachunek predykatów pierwszego rzędu – (ang. first order predicate calculus) to system logiczny, w którym zmienna, na której oparty jest kwantyfikator, może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być zbiorem takich elementów. Tak więc nie mogą występować kwantyfikatory typu "dla każdej funkcji z X na Y ..." (gdyż funkcja jest podzbiorem X × Y), "istnieje własność p, taka że ..." czy "dla każdego podzbioru X zbioru Z ...". Rachunek ten nazywa się też krótko rachunkiem kwantyfikatorów, ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną).

Intuicjonistyczny rachunek zdań, INT, w wersji inwariantnej — rachunek zdaniowy w języku klasycznego rachunku zdań z regułą odrywania jako jedyną pierwotną regułą wnioskowania oraz aksjomatami następującej postaci:

Dla dowolnego zbioru formuł $X\,$ języka $\mathcal{L}$ oraz dwu formuł $\alpha,\beta\,$ zachodzi równoważność:

$\mathbf{C}\alpha\beta\in\mathbf{Cn}_\mathfrak{S}(X)\quad\Leftrightarrow\quad\beta\in\mathbf{Cn}_\mathfrak{S}(X\cup\{\alpha\})$

Prawdziwość twierdzenia o dedukcji wymaga wyprowadzalności reguły odrywania dla spójnika implikacji $\mathbf{C}$ .

Wyprowadzalność tej reguły nie jest niestety warunkiem wystarczającym do jego prawdziwości.

Niech bowiem $\mathfrak{S}=\langle\mathbf{Frm}(\mathcal{L}_\mathbf{KRZ}),\{\mathbf{r_o},\mathbf{r}_\star\},\mathbf{Ax}_\mathbf{KRZ}\rangle$ , gdzie $\mathbf{Frm}(\mathcal{L}_\mathbf{KRZ})$ jest zbiorem formuł języka klasycznego rachunku zdań, $\mathbf{r_o}$ jest regułą odrywania dla spójnika implikacji, $\mathbf{r}_\star$ jest regułą podstawiania dla języka klasycznego rachunku zdań oraz $\mathbf{Ax}_\mathbf{KRZ}$ jest zbiorem aksjomatów klasycznego rachunku zdań.

Wówczas $\mathbf{NCpp}\in\mathbf{Cn}_\mathfrak{S}(\{\mathbf{q}\})$ , chociaż w żadnym wypadku nie jest prawdą, że $\mathbf{CqNCpp}\in\mathbf{Cn}_\mathfrak{S}(\emptyset)$ , bo $\mathbf{Cn}_\mathfrak{S}(\emptyset)=\mathbf{Cn}_{c}(\emptyset)$ , a $\mathbf{CqNCpp}$ nie jest tautologią.

Klasyczne twierdzenie o dedukcji jest prawdziwe m.in. w klasycznym i intuicjonistycznym rachunku zdań oraz w rachunku predykatów w ujęciu Endertona.

Zobacz też

Rachunek zdaniowy

System formalny