Rachunek predykatów pierwszego rzędu

Z Wikipedii

Rachunek predykatów pierwszego rzędu – (ang. first order predicate calculus) to system logiczny, w którym kwantyfikatory mogą mówić tylko o obiektach, nie zaś o ich zbiorach. Tak więc nie mogą występować kwantyfikatory typu "dla każdej funkcji z X na 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ą).

Rachunek predykatów pierwszego rzędu jest nierozstrzygalny (w przeciwieństwie do rachunku zdań), ale jeszcze nadaje się do komputerowej analizy (co już niekoniecznie można powiedzieć o rachunku predykatów wyższych rzędów, które dopuszczają kwantyfikatory dla zbiorów).

Znaczna część rozważań matematycznych może być sformalizowana na gruncie logiki pierwszego rzędu. Ponadto logika ta ma wiele własności czyniących ją bardziej użyteczną od innych logik, co ma wpływ na pewne preferowanie teorii formalizowalnych na jej gruncie.

W literaturze istnieje szereg równoważnych rozwinięć tego tematu. Prezentacja przedstawiona poniżej jest do pewnego stopnia oparta o książkę Martina Goldsterna i Haima Judaha^[1]. Wśród innych źródeł omawiających te zagadnienia należy wymienić podręcznik Witolda Pogorzelskiego^[2] czy też książkę Zofii Adamowicz i Pawła Zbierskiego^[3]. Bardzo popularnym jest też opracowanie Josepha Shoenfielda^[4].

Spis treści

1 Wstęp do formalizacji
2 Formalizacja języka
- 2.1 Przykłady
3 Dowody w językach pierwszego rzędu
4 Interpretacje (modele) języka pierwszego rzędu
5 Zobacz też
6 Bibliografia

[edytuj] Wstęp do formalizacji

Logika pierwszego rzędu jest podstawą na której formalizujemy większość matematyki. We wstępie do wspomnianej powyżej książki Goldsterna i Judaha traktującej właśnie o tej tematyce, Saharon Shelah napisał:

[Na gruncie matematyki] możemy zdefiniować czym jest dowód i wykazać że w pewnym sensie "być prawdziwym" i "mieć dowód" znaczą to samo (twierdzenie Gödla o zupełności). (...) Nie możemy wyciągnąć sami siebie z bagna za włosy: nie możemy udowodnić w naszym systemie, że nie ma w nim sprzeczności (twierdzenie Gödla o niezupełności) (...) Możemy zbudować ogólną teorię teorii matematycznych (teoria modeli).

Czym jest system rachunku predykatów pierwszego rzędu? Składa się on z:

zmiennych nazwowych (litery, za które wolno podstawić nazwy dowolnych przedmiotów)
stałych nazwowych (nazwy własne przedmiotów)
liter predykatowych (predykaty)
symboli funkcyjnych (funktory nazwotwórcze od argumentów nazwowych)
stałych logicznych (spójniki prawdziwościowe rachunku zdań i kwantyfikatory)
znaków pomocniczych (nawiasy)
symbolu równości.

Używając symboli wymienionych powyżej i przestrzegając naturalnych reguł możemy budować poprawnie zbudowane napisy. Niektóre z tych napisów mogą być interpretowane jako nazwy na pewne obiekty, a inne będą mówić o własnościach tych obiektów. Pierwsza grupa napisów poprawnie zbudowanych to termy, a druga to zdania. Przykładowy schemat kwantyfikatorowy zdania: Nie ma czegoś, czym ciekawią się wszyscy...

$\neg(\exist x)(S(x)\and(\forall y)(I(y)\implies C(y,x)))$

(czyt.: Nie istnieje taki x, że x jest substratem wiedzy, i dla każdego y, że jeżeli y jest istotą rozumną, to y ciekawi się x.)

Następnie ustalimy reguły wnioskowania a także metody interpretacji naszych napisów.

[edytuj] Formalizacja języka ${\mathcal L}(\tau)$

Każdy język pierwszego rzędu jest zdeterminowany przez ustalenie alfabetu.

Niech $τ$ będzie pewnym zbiorem stałych, symboli funkcyjnych i symboli relacyjnych (predykatów). Każdy z tych symboli ma jednoznacznie określony charakter (tzn wiadomo czy jest to stała, czy symbol funkcyjny czy też predykat) i każdy z symboli funkcyjnych i predykatów ma określoną arność (która jest dodatnią liczbą całkowitą). Zbiór $τ$ będzie nazywany alfabetem naszego języka, a sam język wyznaczony przez ten alfabet będzie oznaczany przez ${\mathcal L}(\tau)$ . Ustalmy też nieskończoną listę zmiennych (zwykle $x_0,x_1,\ldots$ ).

Najpierw definiujemy termy języka ${\mathcal L}(\tau)$ jako elementy najmniejszego zbioru ${\bold T}$ takiego, że:

wszystkie stałe i zmienne należą do ${\bold T}$ ,
jeśli $t_1,\ldots,t_n\in {\bold T}$ i $f\in\tau$ jest $n$ -arnym symbolem funkcyjnym, to $f(t_1,\ldots,t_n)\in {\bold T}$ .

Następnie określamy zbiór formuł języka ${\mathcal L}(\tau)$ jako najmniejszy zbiór ${\bold F}$ taki, że:

jeśli $t_1, t_2\in {\bold T}$ , to wyrażenie $t 1 = t 2$ należy do ${\bold F}$ ,
jeśli $t_1,\ldots,t_n\in {\bold T}$ zaś $P\in\tau$ jest $n$ -arnym symbolem relacyjnym, to wyrażenie $P(t_1,\ldots,t_n)$ należy do ${\bold F}$ ,
jeśli $\varphi,\psi\in {\bold F}$ i $*$ jest binarnym spójnikiem zdaniowym (alternatywą $\vee$ , koniunkcją $\wedge$ , implikacją $\Rightarrow$ lub równoważnością $\Leftrightarrow$ ), to $(\varphi*\psi)\in {\bold F}$ oraz $\neg \varphi\in {\bold F}$ ,
jeśli $x i$ jest zmienną oraz $\varphi\in {\bold F}$ , to także $(\exists x_i)(\varphi)\in {\bold F}$ i $(\forall x_i)(\varphi)\in {\bold F}$ .

W formułach postaci $(\exists x_i)(\varphi)$ i $(\forall x_i)(\varphi)$ mówimy że zmienna $x i$ znajduje się w zasięgu kwantyfikatora i jako taka jest związana. Przez indukcję po złożoności formuł, rozszerzamy to pojęcie na wszystkie formuły w których $(\exists x_i)(\varphi)$ czy też $(\forall x_i)(\varphi)$ pojawia się jako jedna z części użytych w budowie, ale ograniczamy się do występowań zmiennej $x i$ w $\varphi$ (i mówimy że konkretne wystąpienie zmiennej jest wolne lub związane).

Zdanie w języku pierwszego rzędu ${\mathcal L}(\tau)$ to taka formuła, w której każda zmienna jest związana, czyli znajduje się w zasięgu działania jakiegoś kwantyfikatora.

[edytuj] Przykłady

Język teorii mnogości to ${\mathcal L}(\{\in\})$ gdzie $\in$ jest binarnym symbolem relacyjnym.
Język teorii grup to ${\mathcal L}(\{*\})$ gdzie $*$ jest binarnym symbolem funkcyjnym.
Język ciał uporządkowanych to ${\mathcal L}(\{+,\cdot,0,1,\leq\})$ gdzie $+,\cdot$ są binarnymi symbolami funkcyjnymi a $\leq$ jest binarnym symbolem relacyjnym.

[edytuj] Dowody w językach pierwszego rzędu

Ustalmy alfabet $τ$ (tak więc jest to zbiór złożony ze stałych, symboli funkcyjnych i symboli relacyjnych).

[edytuj] Podstawienia termów za zmienne

Przypuśćmy, że t i s są termami języka ${\mathcal L}(\tau)$ oraz $x 1$ jest jedną ze zmiennych. Definiujemy podstawienie $s (x 1 / t)$ jako term który jest otrzymany z s przez zastąpienie wszystkich wystąpień zmiennej $x 1$ w s przez t.

Podobnie, dla termu t i formuły $\varphi$ języka ${\mathcal L}(\tau)$ oraz zmiennej $x 1$ określamy podstawienie $\varphi(x_1/t)$ jako taką formulę, która jest otrzymana z $\varphi$ przez zastąpienie wszystkich wystąpień zmiennej $x 1$ w $\varphi$ przez term t. Powiemy, że term $t$ może być podstawiony za zmienną $x 1$ w $\varphi$ jeśli po podstawieniu, żadna ze zmiennych wolnych w t nie znalazła się w zasięgu kwantyfikatora wiążącego ją.

[edytuj] Przykłady

Rozważmy język ciał uporządkowanych ${\mathcal L}(\{+,\cdot,0,1,\leq\})$ . Niech termy $t, s, u$ bedą, odpowiednio $0 + x 1 + x 2$ , $(1+1)\cdot x_1$ oraz $x_3\cdot x_4$ . Rozważmy formułę $\varphi=(\forall x_3)(\exists x_4)((x_1+x_3)\cdot x_7=x_4+1+0)$ . Wówczas

$s (x 1 / t)$ to term $(1+1)\cdot (0+x_1+x_2)$ ,
$s (x 1 / u)$ to term $(1+1)\cdot (x_3\cdot x_4)$ ,
$\varphi(x_1/t)$ to formuła $(\forall x_3)(\exists x_4)(([0+x_1+x_2]+x_3)\cdot x_7=x_4+1+0)$ i term $t$ może być podstawiony za zmienną $x 1$ w $\varphi$ ,
$\varphi(x_3/u)$ to formuła $(\forall x_3)(\exists x_4)((x_1+[x_3\cdot x_4])\cdot x_7=x_4+1+0)$ i term $u$ nie może być podstawiony za zmienną $x 3$ w $\varphi$ .

[edytuj] Aksjomaty logiczne

Formuły następujących typów będą nazywane aksjomatami czystymi:

podstawienia formuł do tautologii rachunku zdań,
formuły postaci $(\forall x)(\varphi\Rightarrow\psi)\ \Rightarrow\ ((\forall x)(\varphi)\Rightarrow(\forall x)(\psi))$ (gdzie $\varphi,\psi$ to formuły),
formuły postaci $(\forall x_i)(\varphi)\ \Rightarrow\ \varphi(x_i/t)$ , gdzie term $t$ może być podstawiony za zmienną $x i$ w $\varphi$ ,
formuły postaci $\varphi\Rightarrow (\forall x_i)(\varphi)$ gdzie zmienna $x i$ nie jest wolna w formule $\varphi$ ,
formuły postaci

x = x

$x=y\ \Rightarrow y=x$ i

$x=y\ \wedge\ y=z\ \Rightarrow\ x=z$ ,

gdzie

x, y, z

są (niekoniecznie różnymi) zmiennymi,

formuły postaci

$y_1=z_1\ \wedge\ \ldots\ \wedge y_k=z_k\ \Rightarrow\ (P(y_1,\ldots,y_k)\Leftrightarrow P(z_1,\ldots,z_k))$ ,

gdzie $z_1,\ldots,z_k,y_1,\ldots,y_k$ są zmiennymi a $P\in \tau$ jest k-arnym symbolem relacyjnym,

formuły postaci

$y_1=z_1\ \wedge\ \ldots\ \wedge y_k=z_k\ \Rightarrow\ (f(y_1,\ldots,y_k)=f(z_1,\ldots,z_k))$ ,

gdzie $z_1,\ldots,z_k,y_1,\ldots,y_k$ są zmiennymi a $f\in \tau$ jest k-arnym symbolem funkcyjnym.

Aksjomaty czyste i formuły postaci $(\forall y_1)\ldots(\forall y_n)(\varphi)$ , gdzie $\varphi$ jest aksjomatem czystym, są nazywane aksjomatami logicznymi.

[edytuj] Reguła wnioskowania

Jeśli $\varphi_1,\varphi_2,\psi$ są formułami języka ${\mathcal L}(\tau)$ , oraz $φ 1$ jest postaci $\varphi_2\ \Rightarrow\ \psi$ to powiemy, że formuła $ψ$ może być wywnioskowana z $\varphi_1,\varphi_2$ w oparciu o regułę modus ponens.

[edytuj] Dowód

Niech $A\subseteq {\bold F}$ będzie jakimś zbiorem formuł języka ${\mathcal L}(\tau)$ (możliwie pustym). Dowodem ze zbioru aksjomatów A nazywamy skończony ciąg formuł $\langle\varphi_1,\ldots,\varphi_k\rangle$ taki, że dla każdego $1\leq j\leq k$ ,

$\varphi_j$ jest jedną z formuł z A, lub

$\varphi_j$ jest aksjomatem logicznym, lub

$\varphi_j$ może być wywnioskowana z $\varphi_k,\varphi_l$ w oparciu o regułę modus ponens. dla pewnych

k, l

Jeśli $\langle\varphi_1,\ldots,\varphi_k\rangle$ jest dowodem ze zbioru aksjomatów A, to powiemy że formuła $\varphi=\varphi_j$ jest dowodliwa z A albo też że $\varphi=\varphi_j$ jest twierdzeniem z A i napiszemy wtedy $A\vdash \varphi$ . Jeśli A jest zbiorem pustym to możemy pominąć je w naszych oznaczeniach i napisać $\vdash \varphi$ .

Powiemy, że A jest sprzecznym zbiorem aksjomatów, jeśli dla pewnej formuły $\varphi$ mamy zarówno że $A\vdash\varphi$ jak i $A\vdash\neg\varphi$ . W przeciwnym razie mówimy, że A jest niesprzeczny.

[edytuj] Podstawowe własności

Niech $A\subseteq {\bold F}$ będzie jakimś zbiorem formuł języka ${\mathcal L}(\tau)$ oraz niech $\varphi,\psi$ będą formułami tegoż języka.

Twierdzenie o dedukcji: $A\vdash \varphi\Rightarrow\psi$ wtedy i tylko wtedy gdy $A\cup\{\varphi\}\vdash\psi$ .
Twierdzenie o uogólnianiu: Jeśli zmienna x nie pojawia się jako zmienna wolna żadnej z formuł w A oraz $A\vdash\varphi$ , to $A\vdash (\forall x)(\varphi)$ .
Twierdzenie o wprowadzeniu kwantyfikatora $\forall$ :

(1) Przypuśćmy że term t może być podstawiony za zmienną x w

ψ

. Jeśli $A\vdash \psi(x/t)\Rightarrow\varphi$ , to $A\vdash (\forall x)(\psi)\Rightarrow\varphi$ .

(2) Przypuśćmy że zmienna x nie jest wolna w

ψ

ani w żadnej z formuł w zbiorze A. Jeśli $A\vdash \psi\Rightarrow\varphi$ , to $A\vdash \psi\Rightarrow (\forall x)(\varphi)$ .

Twierdzenie o wprowadzeniu kwantyfikatora $\exists$ :

(1) Przypuśćmy że term t może być podstawiony za zmienną x w $\varphi$ . Jeśli $A\vdash \varphi\Rightarrow\psi(x/t)$ , to $A\vdash \varphi\Rightarrow(\exists x)(\psi)$ .

(2) Przypuśćmy że zmienna x nie jest wolna w

ψ

ani w żadnej z formuł w zbiorze A. Jeśli $A\vdash \varphi\Rightarrow\psi$ , to $A\vdash (\exists x)(\varphi)\Rightarrow\psi$ .

Twierdzenie o zwartości I: zbiór zdań A jest niesprzeczny wtedy i tylko wtedy gdy każdy jego podzbiór skończony jest niesprzeczny.

[edytuj] Interpretacje (modele) języka pierwszego rzędu

Ustalmy alfabet $τ$ , ponadto ustalmy że $S τ$ jest zbiorem stałych tego alfabetu, $F τ$ jest zbiorem symboli funkcyjnych a $R τ$ to zbiór symboli relacyjnych.

[edytuj] Modele

Interpretacją lub modelem języka ${\mathcal L}(\tau)$ nazywamy układ

${\mathcal M} = (M; R^{\mathcal M},\ldots, f^{\mathcal M},\ldots, c^{\mathcal M},\ldots)_{R\in R_\tau, f\in F_\tau, c\in S_\tau}$

gdzie

M jest niepustym zbiorem zwanym dziedziną lub uniwersum modelu ${\mathcal M}$ (często uniwersum modelu ${\mathcal M}$ oznacza się przez $|{\mathcal M}|$ ),
dla n-arnego symbolu relacyjnego $R\in R_\tau$ , $R^{\mathcal M}$ jest n-argumentową relacją na zbiorze M, tzn. $R^{\mathcal M}\subseteq M^n$ ,
dla n-arnego symbolu funkcyjnego $f\in F_\tau$ , $f^{\mathcal M}$ jest n-argumentowym działaniem na zbiorze M, tzn. $f^{\mathcal M}: M^n\longrightarrow M$ ,
dla stałej $c\in S_\tau$ , $c^{\mathcal M}$ jest elementem zbioru M.

[edytuj] Interpretacja termów w modelu

Przez indukcję po złożoności termów języka ${\mathcal L}(\tau)$ definiujemy interpretację termu w modelu ${\mathcal M}$ . Dla termu $t\in {\bold T}$ o zmiennych wolnych zawartych wśród $x_1,\ldots,x_n$ i dla elementów $m_1,\ldots,m_n\in M$ uniwersum modelu ${\mathcal M}$ wprowadzamy $t^{\mathcal M}[m_1,\ldots,m_n]\in M$ następująco.

Jeśli t jest stałą c alfabetu τ, to $t^{\mathcal M}[m_1,\ldots,m_n]=c^{\mathcal M}$ .
Jeśli t jest zmienną $x i$ , to $t^{\mathcal M}[m_1,\ldots,m_n]=m_i$ .
Jeśli $t_1,\ldots,t_k\in {\bold T}$ i $f\in\tau$ jest $k$ -arnym symbolem funkcyjnym, to $t^{\mathcal M}[m_1,\ldots,m_n]=f^{\mathcal M}(t_1^{\mathcal M}[m_1,\ldots,m_n],\ldots,t_k^{\mathcal M}[m_1,\ldots,m_n])$ .

[edytuj] Relacja spełniania w modelu

Przez indukcję po złożoności formuł języka ${\mathcal L}(\tau)$ definiujemy kiedy formuła jest spełniona w modelu ${\mathcal M}$ . Dla formuły $\varphi\in {\bold F}$ o zmiennych wolnych zawartych wśród $x_1,\ldots,x_n$ i elementów $m_1,\ldots,m_n\in M$ uniwersum modelu ${\mathcal M}$ wprowadzamy relację ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ (czyt. "formuła $\varphi$ jest spełniona w modelu ${\mathcal M}$ na elementach $m_1,\ldots,m_n$ ") następująco.

Jeśli φ jest formułą $t 1 = t 2$ dla pewnych termów $t_1,t_2\in {\bold T}$ których zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy elementy $t_1^{\mathcal M}[m_1,\ldots,m_n]$ i $t_2^{\mathcal M}[m_1,\ldots,m_n]$ zbioru M są identyczne.
Jeśli φ jest formułą $P(t_1,\ldots,t_k)$ dla pewnych termów $t_1,\ldots,t_k\in {\bold T}$ których zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ i k-arnego symbolu relacyjnego $P\in\tau$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy elementy $(t_1^{\mathcal M}[m_1,\ldots,m_n],\ldots, t_k^{\mathcal M}[m_1,\ldots,m_n])\in P^{\mathcal M}$ .
Jeśli φ jest formułą $(\psi_1\wedge\psi_2)$ dla pewnych formuł $\psi_1,\psi_2\in {\bold F}$ których zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy ${\mathcal M}\models \psi_1[m_1,\ldots,m_n]$ oraz ${\mathcal M}\models \psi_2[m_1,\ldots,m_n]$ .
Jeśli φ jest formułą $(\psi_1\vee\psi_2)$ dla pewnych formuł $\psi_1,\psi_2\in {\bold F}$ których zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy ${\mathcal M}\models \psi_1[m_1,\ldots,m_n]$ lub ${\mathcal M}\models \psi_2[m_1,\ldots,m_n]$ .
Jeśli φ jest formułą $(\psi_1\Rightarrow\psi_2)$ dla pewnych formuł $\psi_1,\psi_2\in {\bold F}$ których zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy ${\mathcal M}\models \psi_2[m_1,\ldots,m_n]$ lub nie zachodzi że ${\mathcal M}\models \psi_1[m_1,\ldots,m_n]$ .
Jeśli φ jest formułą $(\psi_1\Leftrightarrow\psi_2)$ dla pewnych formuł $\psi_1,\psi_2\in {\bold F}$ których zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy albo oba zdania ${\mathcal M}\models \psi_1[m_1,\ldots,m_n]$ i ${\mathcal M}\models \psi_2[m_1,\ldots,m_n]$ są prawdziwe, albo oba są fałszywe.
Jeśli φ jest formułą $\neg\psi$ dla pewnej formuły $\psi\in {\bold F}$ której zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy zdanie ${\mathcal M}\models \psi[m_1,\ldots,m_n]$ jest fałszywe.
Jeśli φ jest formułą $(\forall x_j)(\psi)$ dla pewnej formuły $\psi\in {\bold F}$ której zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy zdanie ${\mathcal M}\models \psi[m_1^*,\ldots,m_n^*,\ldots,m^*_k]$ jest prawdziwe dla każdego ciągu $m_1^*,\ldots,m_n^*,\ldots,m^*_k$ elementów uniwersum M takich, że $j\leq k$ oraz $m^*_i=m_i$ ilekroć $x i$ jest zmienną wolną w φ.
Jeśli φ jest formułą $(\exists x_j)(\psi)$ dla pewnej formuły $\psi\in {\bold F}$ której zmienne wolne są zawarte wśród $x_1,\ldots,x_n$ , to stwierdzimy że ${\mathcal M}\models \varphi[m_1,\ldots,m_n]$ jest prawdziwe wtedy i tylko wtedy gdy dla pewnego ciągu $m_1^*,\ldots,m_n^*,\ldots,m^*_k$ elementów uniwersum M takich, że $j\leq k$ oraz $m^*_i=m_i$ ilekroć $x i$ jest zmienną wolną w φ mamy, że ${\mathcal M}\models \psi[m_1^*,\ldots,m_n^*,\ldots,m^*_k]$ .

[edytuj] Podstawowe własności

Twierdzenie o zupełności: zbiór zdań A jest niesprzeczny wtedy i tylko wtedy gdy ma on model (tzn jest spełniony w pewnym modelu języka ${\mathcal L}(\tau)$ .
Twierdzenie o zwartości II: zbiór zdań A ma model wtedy i tylko wtedy gdy każdy jego podzbiór skończony jest ma model.

[edytuj] Zobacz też

[edytuj] Bibliografia

↑ Martin Goldstern; Haim Judah: The Incompleteness Phenomenon. A new course in mathematical logic. A K Peters, Wellesley, Massachusetts, 1995. ISBN 1-56881-029-6
↑ Witold A. Pogorzelski: Klasyczny rachunek kwantyfikatorów, zarys teorii, Państwowe Wydawnictwo Naukowe, Warszawa 1981. ISBN 83-01-00567-X
↑ Zofia Adamowicz; Paweł Zbierski: Logic of mathematics. A modern course of classical logic. "Pure and Applied Mathematics" (New York). A Wiley-Interscience Publication. John Wiley & Sons, Inc., New York, 1997. ISBN 0-471-06026-7.
↑ Joseph R. Shoenfield: Mathematical Logic, Association for Symbolic Logic, 1967. ISBN 1-56881-135-7.

Kategoria: Logika matematyczna

Rachunek predykatów pierwszego rzędu

Z Wikipedii

Spis treści

[edytuj] Wstęp do formalizacji

[edytuj] Formalizacja języka ${\mathcal L}(\tau)$

[edytuj] Przykłady

[edytuj] Dowody w językach pierwszego rzędu

[edytuj] Podstawienia termów za zmienne

[edytuj] Przykłady

[edytuj] Aksjomaty logiczne

[edytuj] Reguła wnioskowania

[edytuj] Dowód

[edytuj] Podstawowe własności

[edytuj] Interpretacje (modele) języka pierwszego rzędu

[edytuj] Modele

[edytuj] Interpretacja termów w modelu

[edytuj] Relacja spełniania w modelu

[edytuj] Podstawowe własności

[edytuj] Zobacz też

[edytuj] Bibliografia

Views

nawigacja

zmiany

dla edytorów

Szukaj

W innych językach