Rachunek predykatów pierwszego rzędu

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

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ą).

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

Wstęp do formalizacji[edytuj | edytuj kod]

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

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

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

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

Niech \tau 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 \tau 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.

Przykłady[edytuj | edytuj kod]

  • 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,\leqslant\}), gdzie +,\cdot są binarnymi symbolami funkcyjnymi a \leqslant jest binarnym symbolem relacyjnym.

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

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

Podstawienia termów za zmienne[edytuj | edytuj kod]

Przypuśćmy, że t i s są termami języka {\mathcal L}(\tau) oraz \xi jest jedną ze zmiennych. Definiujemy podstawienie s(\xi/t) jako term, który powstaje z s poprzez literalne zastąpienie w nim wszystkich egzemplarzy zmiennej \xi termem t.

W przypadku zmiennej \varphi, termu t i formuły \varphi podstawienie \varphi(\xi/t) definiuje się bardziej subtelnie, co najlepiej ująć indukcyjnie względem budowy formuły \varphi (por. [2]:

  • Jeśli \varphi\, jest formułą atomową P(t_1,...,t_n)\,, to \varphi(\xi/t)=P(t_1(\xi/t),...,t_n(\xi/t))\,
  • Jeśli \varphi=\psi_1\circ\psi_2, to \varphi(\xi/t)=\psi_1(\xi/t)\circ\psi_2(\xi/t), gdzie \circ\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}
  • Jeśli \varphi=\neg\psi, to \varphi(\xi/t)=\neg\psi(\xi/t)

oraz

  • jeśli \varphi=({\mathcal Q}\zeta)\psi, gdzie {\mathcal Q}\in\{\forall,\exists\}, to \varphi(\xi/t)=\varphi, jeśli \zeta\in\{\xi\}\cup\bold{Vf}(t) oraz \varphi(\xi/t)=({\mathcal Q}\zeta)\psi(\xi/t), 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 t w formule \varphi za zmienną \xi jest dopuszczalne lub, że zmienna \xi jest wolna dla termu t w formule \varphi, ozn. \xi\in\bold{Ff}(t,\varphi), gdy (nieformalnie) literalne wstawienie tego termu w rozważanej formule w miejscu któregoś z wolnych wystąpień zmiennej \xi spowodowałoby związanie pewnej zmiennej termu t (w szczególności zmienne nie bę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 \xi\not\in\bold{Vf}(\varphi), to \xi\in\bold{Ff}(t,\varphi)
  • Jeśli \varphi jest formułą atomową, to \xi\in\bold{Ff}(t,\varphi)
  • Jeśli \varphi=\psi_1\circ\psi_2, to \xi\in\bold{Ff}(t,\varphi)\Leftrightarrow\xi\in\bold{Ff}(t,\psi_1) \cap \bold{Ff}(t,\psi_2), gdzie \circ\in\{\wedge,\vee,\rightarrow,\leftrightarrow\}
  • Jeśli \varphi=\neg\psi, to \xi\in\bold{Ff}(t,\varphi)\Leftrightarrow\xi\in\bold{Ff}(t,\psi)

oraz

  • jeśli \varphi=({\mathcal Q}\zeta)\psi, to \xi\in\bold{Ff}(t,\varphi)\Leftrightarrow\xi\in\bold{Ff}(t,\psi)\&\zeta\not\in\bold{Vf}(t), gdzie {\mathcal Q}\in\{\forall,\exists\}.

Przykłady[edytuj | edytuj kod]

Rozważmy język ciał uporządkowanych {\mathcal L}(\{+,\cdot,0,1,\leqslant\}). Niech termami 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 podstawienie termu t za zmienną x_1 w \varphi jest dopuszczalne,
  • \varphi(x_3/u) oraz \varphi(x_7/u) są równokszałtne z \varphi, przy czym podstawienie termu u za zmienną x_7 jest niedopuszczalne, zaś podstawienie tego samego termu za zmienną x_3 jest dopuszczalne (choć nieskuteczne), bowiem zmienna ta nie jest wolna w rozważanej formule.

Aksjomaty logiczne[edytuj | edytuj kod]

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.

Reguła wnioskowania[edytuj | edytuj kod]

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

Dowód[edytuj | edytuj kod]

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\leqslant j\leqslant 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.

Podstawowe własności[edytuj | edytuj kod]

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 \psi. 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 \psi 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 \psi 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.

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

Ustalmy alfabet \tau, ponadto ustalmy że S_\tau jest zbiorem stałych tego alfabetu, F_\tau jest zbiorem symboli funkcyjnych a R_\tau to zbiór symboli relacyjnych.

Modele[edytuj | edytuj kod]

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.

Interpretacja termów w modelu[edytuj | edytuj kod]

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]).

Relacja spełniania w modelu[edytuj | edytuj kod]

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\leqslant 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\leqslant 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].

Podstawowe własności[edytuj | edytuj kod]

  • Twierdzenie o peł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 ma model.

Modele niestandardowe[edytuj | edytuj kod]

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 Peano. Przykładem niestandardowego modelu aksjomatyki Peano 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.

Zobacz też[edytuj | edytuj kod]

Przypisy

  1. Martin Goldstern; Haim Judah: The Incompleteness Phenomenon. A new course in mathematical logic. A K Peters, Wellesley, Massachusetts, 1995. ISBN 1-56881-029-6
  2. Witold A. Pogorzelski: Klasyczny rachunek kwantyfikatorów, zarys teorii, Państwowe Wydawnictwo Naukowe, Warszawa 1981. ISBN 83-01-00567-X
  3. 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.
  4. Joseph R. Shoenfield: Mathematical Logic, Association for Symbolic Logic, 1967. ISBN 1-56881-135-7.