Rachunek predykatów pierwszego rzędu (ang. first order predicate calculus) – 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[1], ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną).
Na przykład w rachunku predykatów pierwszego rzędu można zapisać zdanie „dla dowolnej liczby rzeczywistej istnieje liczba większa”, jednak nie można zapisać „każdy zbiór liczb rzeczywistych ma kres górny”, gdyż wówczas kwantyfikator ogólny musiałby przebiegać wszystkie możliwe podzbiory zbioru liczb rzeczywistych i potrzebny byłby rachunek predykatów co najmniej drugiego rzędu.
Rachunek predykatów pierwszego rzędu w ogólnym przypadku nie jest rozstrzygalny (w przeciwieństwie do rachunku zdań), lecz półrozstrzygalny (czyli rekurencyjnie przeliczalny), 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 na książce Martina Goldsterna i Haima Judaha[2]. Wśród innych źródeł omawiających te zagadnienia należy wymienić podręcznik Witolda Pogorzelskiego[3], czy też książkę Zofii Adamowicz i Pawła Zbierskiego[4]. Bardzo popularnym jest też opracowanie Josepha Shoenfielda[5].
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 Szelach 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 peł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).
System rachunku predykatów pierwszego rzędu składa się 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…
![{\displaystyle \neg (\exists x)(S(x)\land (\forall y)(I(y)\implies C(y,x)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d1a2ab0dcf4a6e8ecf98791fa58c31cad6ee7138)
(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.
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
Ustalmy też nieskończoną listę zmiennych (zwykle
).
Najpierw definiujemy termy języka
jako elementy najmniejszego zbioru
takiego, że:
- wszystkie stałe i zmienne należą do
![{\displaystyle \mathbf {T} ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/54d82d074d2fb67c09a19856005276cb16c4fbe5)
- jeśli
i
jest
-arnym symbolem funkcyjnym, to ![{\displaystyle f(t_{1},\dots ,t_{n})\in \mathbf {T} .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/262d4f36f40cf4e41451864cb8fee64860c9047a)
Następnie określamy zbiór formuł języka
jako najmniejszy zbiór
taki, że:
- jeśli
to wyrażenie
należy do ![{\displaystyle \mathbf {F} ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/624a25081e2040326a232d961e48b6bf2d95c328)
- jeśli
zaś
jest
-arnym symbolem relacyjnym, to wyrażenie
należy do ![{\displaystyle \mathbf {F} ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/624a25081e2040326a232d961e48b6bf2d95c328)
- jeśli
i
jest binarnym spójnikiem zdaniowym (alternatywą
koniunkcją
implikacją
lub równoważnością
), to
oraz ![{\displaystyle \neg \varphi \in \mathbf {F} ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b17562138c77011943bc0762d265aa20710c9938)
- jeśli
jest zmienną oraz
to także
i ![{\displaystyle (\forall x_{i})(\varphi )\in \mathbf {F} .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f9f927532ed6f6700db100df837fa9eb03b0896c)
W formułach postaci
i
mówimy, że zmienna
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
czy też
pojawia się jako jedna z części użytych w budowie, ale ograniczamy się do występowań zmiennej
w
(i mówimy, że konkretne wystąpienie zmiennej jest wolne lub związane).
Zdanie w języku pierwszego rzędu
to taka formuła, w której każda zmienna jest związana, czyli znajduje się w zasięgu działania jakiegoś kwantyfikatora.
Przykłady
- Język teorii mnogości to
gdzie
jest binarnym symbolem relacyjnym. - Język teorii grup to
gdzie
jest binarnym symbolem funkcyjnym. - Język ciał uporządkowanych to
gdzie
są binarnymi symbolami funkcyjnymi a
jest binarnym symbolem relacyjnym.
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).
Podstawienia termów za zmienne
Przypuśćmy, że
i
są termami języka
oraz
jest jedną ze zmiennych. Definiujemy podstawienie
jako term, który powstaje z
poprzez literalne zastąpienie w nim wszystkich egzemplarzy zmiennej
termem
W przypadku zmiennej
termu
i formuły
podstawienie
definiuje się bardziej subtelnie, co najlepiej ująć indukcyjnie względem budowy formuły
(por. [2]):
- jeśli
jest formułą atomową
to ![{\displaystyle \varphi (\xi /t)=P(t_{1}(\xi /t),\dots ,t_{n}(\xi /t))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fdb8ae9c09f3df379203c91ce07cd93632aea5e9)
- jeśli
to
gdzie ![{\displaystyle \circ \in \{\wedge ,\vee ,\to ,\leftrightarrow \}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/339628c9edbf2b7d48874f3fba88cdc7caa77b6e)
- jeśli
to ![{\displaystyle \varphi (\xi /t)=\neg \psi (\xi /t)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f603b59c818a26f900ffbf36d920957559baefcf)
oraz
- jeśli
gdzie
to
jeśli
oraz
w przeciwnym wypadku.
Aby móc wysłowić niektóre z aksjomatów Rachunku Predykatów konieczne jest pewne ograniczenie operacji podstawiania w formule. Mianowicie, powiadamy, że podstawienie termu
w formule
za zmienną
jest dopuszczalne lub, że zmienna
jest wolna dla termu
w formule
, ozn.
gdy (nieformalnie) literalne wstawienie tego termu w rozważanej formule w miejscu któregoś z wolnych wystąpień zmiennej
spowodowałoby związanie pewnej zmiennej termu
(w szczególności zmienne niebędące wolnymi w danej formule są wolne w niej dla wszystkich termów).
Formalnie natomiast definiujemy to pojęcie indukcyjnie ze względu na budowę formuły następująco:
- jeśli
to ![{\displaystyle \xi \in \mathbf {Ff} (t,\varphi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a2721d5174a3466240c2deeb6e5b3127f4dc9c46)
- jeśli
jest formułą atomową, to ![{\displaystyle \xi \in \mathbf {Ff} (t,\varphi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a2721d5174a3466240c2deeb6e5b3127f4dc9c46)
- jeśli
to
gdzie ![{\displaystyle \circ \in \{\wedge ,\vee ,\to ,\leftrightarrow \}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/339628c9edbf2b7d48874f3fba88cdc7caa77b6e)
- jeśli
to ![{\displaystyle \xi \in \mathbf {Ff} (t,\varphi )\Leftrightarrow \xi \in \mathbf {Ff} (t,\psi )}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3acf547d4f5474274abe8cd9c930da51ce69e664)
oraz
- jeśli
to
gdzie ![{\displaystyle {\mathcal {Q}}\in \{\forall ,\exists \}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/78624ee360cd92efcd6dc70cfcc8cb897e2af0e2)
Przykłady
Rozważmy język ciał uporządkowanych
Niech termami
będą, odpowiednio
oraz
Rozważmy formułę
Wówczas
to term ![{\displaystyle (1+1)\cdot (0+x_{1}+x_{2}),}](https://wikimedia.org/api/rest_v1/media/math/render/svg/083761e1e98b1b3de3ea588f1866452129b3193c)
to term ![{\displaystyle (1+1)\cdot (x_{3}\cdot x_{4}),}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3b2a79ac1130a4d994c1c12c99f7d65721ce9744)
to formuła
i podstawienie termu
za zmienną
w
jest dopuszczalne,
oraz
są równokszałtne z
przy czym podstawienie termu
za zmienną
jest niedopuszczalne, zaś podstawienie tego samego termu za zmienną
jest dopuszczalne (choć nieskuteczne), bowiem zmienna ta nie jest wolna w rozważanej formule.
Aksjomaty logiczne
Formuły następujących typów będą nazywane aksjomatami czystymi:
- podstawienia formuł do tautologii rachunku zdań,
- formuły postaci
(gdzie
to formuły), - formuły postaci
gdzie term
może być podstawiony za zmienną
w ![{\displaystyle \varphi ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aeb4baf1e617abd3f5384bab1851bf109ea0b614)
- formuły postaci
gdzie zmienna
nie jest wolna w formule ![{\displaystyle \varphi ,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/aeb4baf1e617abd3f5384bab1851bf109ea0b614)
- formuły postaci
![{\displaystyle x=x,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/081d1df39dd1532cf167eb55880007546e9e5da7)
i ![{\displaystyle x=y\ \wedge \ y=z\ \Rightarrow \ x=z,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1826bed120980c4805c3b8b91b5a606e3c853d62)
- gdzie
są (niekoniecznie różnymi) zmiennymi,
![{\displaystyle y_{1}=z_{1}\ \wedge \ \ldots \ \wedge y_{k}=z_{k}\ \Rightarrow \ (P(y_{1},\dots ,y_{k})\Leftrightarrow P(z_{1},\dots ,z_{k})),}](https://wikimedia.org/api/rest_v1/media/math/render/svg/df2a4412fb11384b2e9b24e060a863ce67cdc345)
- gdzie
są zmiennymi a
jest
-arnym symbolem relacyjnym,
![{\displaystyle y_{1}=z_{1}\ \wedge \ \ldots \ \wedge y_{k}=z_{k}\ \Rightarrow \ (f(y_{1},\dots ,y_{k})=f(z_{1},\dots ,z_{k})),}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1dd71e5846fcc11c144e388de4c844b9b4de45e2)
- gdzie
są zmiennymi a
jest
-arnym symbolem funkcyjnym.
Aksjomaty czyste i formuły postaci
gdzie
jest aksjomatem czystym, są nazywane aksjomatami logicznymi.
Reguła wnioskowania
Jeśli
są formułami języka
oraz
jest postaci
to powiemy, że formuła
może być wywnioskowana z
w oparciu o regułę modus ponens.
Dowód
Niech
będzie jakimś zbiorem formuł języka
(możliwie pustym). Dowodem ze zbioru aksjomatów A nazywamy skończony ciąg formuł
taki, że dla każdego
jest jedną z formuł z
lub
jest aksjomatem logicznym, lub
może być wywnioskowana z
w oparciu o regułę modus ponens. dla pewnych ![{\displaystyle k,l.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2b2ceaade030ed2d0f321b82562c689c87bef7e8)
Jeśli
jest dowodem ze zbioru aksjomatów
to powiemy, że formuła
jest dowodliwa z A albo też że
jest twierdzeniem z A i napiszemy wtedy
Jeśli
jest zbiorem pustym to możemy pominąć je w naszych oznaczeniach i napisać
Powiemy, że
jest sprzecznym zbiorem aksjomatów, jeśli dla pewnej formuły
mamy zarówno że
jak i
W przeciwnym razie mówimy, że
jest niesprzeczny.
Podstawowe własności
Niech
będzie jakimś zbiorem formuł języka
oraz niech
będą formułami tegoż języka.
- Twierdzenie o dedukcji:
wtedy i tylko wtedy, gdy ![{\displaystyle A\cup \{\varphi \}\vdash \psi .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/eece552a92eb58fa22cdab62d76d5af1ac056757)
- Twierdzenie o uogólnianiu: Jeśli zmienna
nie pojawia się jako zmienna wolna żadnej z formuł w
oraz
to ![{\displaystyle A\vdash (\forall x)(\varphi ).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a5e90a8ef820625d62f99d468e4d454d9191cec6)
- Twierdzenie o wprowadzeniu kwantyfikatora
![{\displaystyle \forall {:}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6adf27b909fcdfbf5195797d7a37939a87ffc489)
- (1) Przypuśćmy że term
może być podstawiony za zmienną
w
Jeśli
to ![{\displaystyle A\vdash (\forall x)(\psi )\Rightarrow \varphi .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/3a2a30abee247a27617190e44490fba5eb98e920)
- (2) Przypuśćmy że zmienna
nie jest wolna w
ani w żadnej z formuł w zbiorze
Jeśli
to ![{\displaystyle A\vdash \psi \Rightarrow (\forall x)(\varphi ).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/756ec60ae4831e1b1d62768756fb37573be84605)
- Twierdzenie o wprowadzeniu kwantyfikatora
![{\displaystyle \exists {:}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4ba93f4f835f8f7c15ac911e4ebecec41acf15c9)
- (1) Przypuśćmy że term
może być podstawiony za zmienną
w
Jeśli
to ![{\displaystyle A\vdash \varphi \Rightarrow (\exists x)(\psi ).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/1e3ea03392bd7d0a2288e233a570feb5cf05b0d3)
- (2) Przypuśćmy że zmienna
nie jest wolna w
ani w żadnej z formuł w zbiorze
Jeśli
to ![{\displaystyle A\vdash (\exists x)(\varphi )\Rightarrow \psi .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/46f324da83c21cb45740dc19499bfdaa4e9e1cae)
- Twierdzenie o zwartości I: zbiór zdań
jest niesprzeczny wtedy i tylko wtedy, gdy każdy jego podzbiór skończony jest niesprzeczny.
Interpretacje (modele) języka pierwszego rzędu
Ustalmy alfabet
ponadto ustalmy, że
jest zbiorem stałych tego alfabetu,
jest zbiorem symboli funkcyjnych a
to zbiór symboli relacyjnych.
Modele
Interpretacją lub modelem języka
nazywamy układ
![{\displaystyle {\mathcal {M}}=(M;R^{\mathcal {M}},\dots ,f^{\mathcal {M}},\dots ,c^{\mathcal {M}},\dots )_{R\in R_{\tau },f\in F_{\tau },c\in S_{\tau }},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fbd82144c34b7376fc9b2e8d90f92aa4b2f0d0c6)
gdzie:
jest niepustym zbiorem zwanym dziedziną lub uniwersum modelu
(często uniwersum modelu
oznacza się przez
), - dla
-arnego symbolu relacyjnego
jest
-argumentową relacją na zbiorze
tzn. ![{\displaystyle R^{\mathcal {M}}\subseteq M^{n},}](https://wikimedia.org/api/rest_v1/media/math/render/svg/18ddbb4f4a11b293fc6a594aac78595ad2e7d142)
- dla
-arnego symbolu funkcyjnego
jest
-argumentowym działaniem na zbiorze
tzn. ![{\displaystyle f^{\mathcal {M}}:M^{n}\longrightarrow M,}](https://wikimedia.org/api/rest_v1/media/math/render/svg/73204f4fde1e094b10fd5faa600b5750cf4cda8a)
- dla stałej
jest elementem zbioru ![{\displaystyle M.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b865c33e30eb83000cd6387517c66dbbf3c3df9e)
Interpretacja termów w modelu
Przez indukcję po złożoności termów języka
definiujemy interpretację termu w modelu
. Dla termu
o zmiennych wolnych zawartych wśród
i dla elementów
uniwersum modelu
wprowadzamy
następująco.
- Jeśli
jest stałą
alfabetu τ, to ![{\displaystyle t^{\mathcal {M}}[m_{1},\dots ,m_{n}]=c^{\mathcal {M}}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6c62f83d4a0a347a81501a6f54d41e2a07b75ecf)
- Jeśli
jest zmienną
to ![{\displaystyle t^{\mathcal {M}}[m_{1},\dots ,m_{n}]=m_{i}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/784202c7e3c84a3704eaf54ab54564cc17009b09)
- Jeśli
i
jest
-arnym symbolem funkcyjnym, to ![{\displaystyle t^{\mathcal {M}}[m_{1},\dots ,m_{n}]=f^{\mathcal {M}}(t_{1}^{\mathcal {M}}[m_{1},\dots ,m_{n}],\dots ,t_{k}^{\mathcal {M}}[m_{1},\dots ,m_{n}]).}](https://wikimedia.org/api/rest_v1/media/math/render/svg/527444295f2bd7c3fb62294b6c91970eb3909b9a)
Relacja spełniania w modelu
Przez indukcję po złożoności formuł języka
definiujemy, kiedy formuła jest spełniona w modelu
. Dla formuły
o zmiennych wolnych zawartych wśród
i elementów
uniwersum modelu
wprowadzamy relację
(czyt. „formuła
jest spełniona w modelu
na elementach
”) następująco.
- Jeśli
jest formułą
dla pewnych termów
których zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy elementy
i
zbioru
są identyczne. - Jeśli
jest formułą
dla pewnych termów
których zmienne wolne są zawarte wśród
i k-arnego symbolu relacyjnego
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy elementy ![{\displaystyle (t_{1}^{\mathcal {M}}[m_{1},\dots ,m_{n}],\dots ,t_{k}^{\mathcal {M}}[m_{1},\dots ,m_{n}])\in P^{\mathcal {M}}.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/60b4eddba2b40dec09ecf237ccb525b1de24ceda)
- Jeśli
jest formułą
dla pewnych formuł
których zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy
oraz ![{\displaystyle {\mathcal {M}}\models \psi _{2}[m_{1},\dots ,m_{n}].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea70d44be506f84444c9c36591e16e0fa76844a4)
- Jeśli
jest formułą
dla pewnych formuł
których zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy
lub ![{\displaystyle {\mathcal {M}}\models \psi _{2}[m_{1},\dots ,m_{n}].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea70d44be506f84444c9c36591e16e0fa76844a4)
- Jeśli
jest formułą
dla pewnych formuł
których zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy
lub nie zachodzi, że ![{\displaystyle {\mathcal {M}}\models \psi _{1}[m_{1},\dots ,m_{n}].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7db53436629e6ebdd6b75ab279901e66e59568d5)
- Jeśli
jest formułą
dla pewnych formuł
których zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy albo oba zdania
i
są prawdziwe, albo oba są fałszywe. - Jeśli
jest formułą
dla pewnej formuły
której zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy zdanie
jest fałszywe. - Jeśli
jest formułą
dla pewnej formuły
której zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy zdanie
jest prawdziwe dla każdego ciągu
elementów uniwersum
takich, że
oraz
ilekroć
jest zmienną wolną w ![{\displaystyle \varphi .}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b0b6c90c1e9984232aed2d530ac2fb2660ea000a)
- Jeśli
jest formułą
dla pewnej formuły
której zmienne wolne są zawarte wśród
to stwierdzimy, że
jest prawdziwe wtedy i tylko wtedy, gdy dla pewnego ciągu
elementów uniwersum
takich, że
oraz
ilekroć
jest zmienną wolną w
mamy, że ![{\displaystyle {\mathcal {M}}\models \psi [m_{1}^{*},\dots ,m_{n}^{*},\dots ,m_{k}^{*}].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/68e890fe91d9535ace9e8bf6b2376c807e0578e7)
Podstawowe własności
- Twierdzenie o pełności: zbiór zdań
jest niesprzeczny wtedy i tylko wtedy, gdy ma on model (tzn. jest spełniony w pewnym modelu języka
). - Twierdzenie o zwartości II: zbiór zdań
ma model wtedy i tylko wtedy, gdy każdy jego podzbiór skończony ma model.
Modele niestandardowe
Zazwyczaj podczas budowania zbioru aksjomatów matematycy mają na myśli jakiś konkretny model, który ma on opisywać. Niestety, najczęściej jeden zbiór aksjomatów posiada wiele nieizomorficznych modeli. „Właściwą” strukturę nazywa się wtedy modelem standardowym a każdą inną – modelem niestandardowym. Jedynie bardzo proste teorie posiadają dokładnie jeden model.
Fakt ten jest wadą logiki pierwszego rzędu. Dla większości teorii każdy skończony zbiór aksjomatów będzie zawsze nieprecyzyjny, tzn. nie będzie określał niektórych własności badanych obiektów i będzie można stworzyć zarówno model, gdzie taka własność zachodzi, jak i drugi model, gdzie ona nie zachodzi. Oba modele będą różne, ale jednak będą spełniać ten sam zestaw wyjściowych aksjomatów.
Modele niestandardowe można wyeliminować, ale potrzebne są do tego aksjomaty w logikach wyższego rzędu.
Każda aksjomatyzacja pierwszego rzędu liczb naturalnych posiada modele niestandardowe. W szczególności posiada je aksjomatyka Peana. Przykładem niestandardowego modelu aksjomatyki Peana są liczby hipernaturalne, czyli nieujemne liczby hiperrzeczywiste, które są równe swojej części całkowitej. Istnieją nawet przeliczalne modele niestandardowe arytmetyki. Dokładne opisanie takich modeli jest trudne, gdyż zarówno dodawanie, jak i mnożenie jest w nich nierozstrzygalne.
Przypisy
- ↑ rachunek kwantyfikatorów, [w:] Encyklopedia PWN [online], Wydawnictwo Naukowe PWN [dostęp 2023-11-21] .
- ↑ MartinM. Goldstern MartinM., The Incompleteness Phenomenon. A new course in mathematical logic, HaimH. Judah, Wellesley, Massachusetts: A K Peters, 1995, ISBN 1-56881-029-6, OCLC 29254857 . Brak numerów stron w książce
- ↑ Witold AdamW.A. Pogorzelski Witold AdamW.A., Klasyczny rachunek kwantyfikatorów, zarys teorii, Warszawa: Państwowe Wydawnictwo Naukowe, 1981, ISBN 83-01-00567-X, OCLC 69480408 . Brak numerów stron w książce
- ↑ 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.
Linki zewnętrzne
- Eric W.E.W. Weisstein Eric W.E.W., First-Order Logic, [w:] MathWorld, Wolfram Research (ang.). [dostęp 2024-03-07].
- Britannica: topic/lower-predicate-calculus
- Universalis: calcul-des-predicats
- БРЭ: 2179111