Tekst źródłowy strony Rachunek predykatów pierwszego rzędu

'''Rachunek predykatów pierwszego rzędu''' ({{ang.|first order predicate calculus}}) – system [[Logika matematyczna|logiczny]], w którym zmienna, na której oparty jest [[kwantyfikator]], może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być [[Zbiór|zbiorem]] takich elementów. Tak więc nie mogą występować kwantyfikatory typu „dla każdej [[Funkcja|funkcji]] z X na Y…” (gdyż funkcja jest [[Podzbiór|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'''<ref name="epwn">{{Encyklopedia PWN | id = 3965156 | tytuł = rachunek kwantyfikatorów | data dostępu = 2023-11-21 }}</ref>, ale często używa się też nazwy '''logika pierwszego rzędu''' (szczególnie wśród matematyków zajmujących się [[logika matematyczna|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 [[Liczby rzeczywiste|zbiór liczb rzeczywistych]] ma [[Kresy dolny i górny|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 [[Rachunek zdań|rachunku zdań]]), lecz półrozstrzygalny (czyli ''rekurencyjnie przeliczalny''), ale jeszcze nadaje się do [[Automatyczne dowodzenie twierdzeń|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<ref>{{Cytuj |autor = Martin Goldstern |tytuł = The Incompleteness Phenomenon. A new course in mathematical logic |data = 1995 |isbn = 1-56881-029-6 |inni = Haim Judah |miejsce = Wellesley, Massachusetts |wydawca = A K Peters |oclc = 29254857}}</ref>. Wśród innych źródeł omawiających te zagadnienia należy wymienić podręcznik Witolda Pogorzelskiego<ref>{{Cytuj |autor = Witold Adam Pogorzelski |tytuł = Klasyczny rachunek kwantyfikatorów, zarys teorii |data = 1981 |isbn = 83-01-00567-X |miejsce = Warszawa |wydawca = Państwowe Wydawnictwo Naukowe |oclc = 69480408}}</ref>, czy też książkę Zofii Adamowicz i Pawła Zbierskiego<ref>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}}.</ref>. Bardzo popularnym jest też opracowanie Josepha Shoenfielda<ref>Joseph R. Shoenfield: ''Mathematical Logic'', Association for Symbolic Logic, 1967. {{ISBN|1-56881-135-7}}.</ref>.

== 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 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 [[Kurt Gödel|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),
* [[Symbol funkcyjny|symboli funkcyjnych]] (funktory nazwotwórcze od argumentów nazwowych),
* stałych logicznych (spójniki prawdziwościowe [[Rachunek zdań|rachunku zdań]] i [[kwantyfikator]]y),
* 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 ''[[Zdanie logiczne|zdania]]''. Przykładowy schemat kwantyfikatorowy zdania: ''Nie ma czegoś, czym ciekawią się wszyscy…''
:: <math>\neg(\exist x)(S(x)\and(\forall y)(I(y)\implies C(y,x)))</math>

(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 𝓛(𝜏) ==
<!-- Znaczniki <math>w nagłówkach powodują nieprawidłowe wyświetlanie się spisu treści: https://phabricator.wikimedia.org/T295091 więc zamiast tego używamy najbliższych symboli Unicode, skopiowanych z https://en.wikipedia.org/wiki/Mathematical_Alphanumeric_Symbols#Tables_of_styled_letters_and_digits -->

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

Niech <math>\tau</math> 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ą [[Argumentowość|arność]] (która jest dodatnią [[Liczby całkowite|liczbą całkowitą]]). Zbiór <math>\tau</math> będzie nazywany '''alfabetem''' naszego języka, a sam język wyznaczony przez ten alfabet będzie oznaczany przez <math>\mathcal L(\tau).</math> Ustalmy też nieskończoną listę '''zmiennych''' (zwykle <math>x_0,x_1,\dots</math>).

Najpierw definiujemy '''termy''' języka <math>\mathcal L(\tau)</math> jako elementy najmniejszego zbioru <math>\mathbf T</math> takiego, że:
* wszystkie stałe i zmienne należą do <math>\mathbf T,</math>
* jeśli <math>t_1,\dots,t_n\in \mathbf T</math> i <math>f\in\tau</math> jest <math>n</math>-arnym symbolem funkcyjnym, to <math>f(t_1,\dots,t_n)\in \mathbf T.</math>

Następnie określamy zbiór '''formuł''' języka <math>\mathcal L(\tau)</math> jako najmniejszy zbiór <math>\mathbf F</math> taki, że:
* jeśli <math>t_1, t_2\in \mathbf T,</math> to wyrażenie <math>t_1= t_2</math> należy do <math>\mathbf F,</math>
* jeśli <math>t_1,\dots,t_n\in \mathbf T</math> zaś <math>P\in\tau</math> jest <math>n</math>-arnym symbolem relacyjnym, to wyrażenie <math>P(t_1,\dots,t_n)</math> należy do <math>\mathbf F,</math>
* jeśli <math>\varphi,\psi\in \mathbf F</math> i <math>*</math> jest binarnym spójnikiem zdaniowym ([[alternatywa|alternatywą]] <math>\vee,</math> [[Koniunkcja (logika)|koniunkcją]] <math>\wedge,</math> [[Implikacja logiczna|implikacją]] <math>\Rightarrow</math> lub [[równoważność|równoważnością]] <math>\Leftrightarrow</math>), to <math>(\varphi*\psi)\in \mathbf F</math> oraz <math>\neg \varphi\in \mathbf F,</math>
* jeśli <math>x_i</math> jest zmienną oraz <math>\varphi\in \mathbf F,</math> to także <math>(\exists x_i)(\varphi)\in \mathbf F</math> i <math>(\forall x_i)(\varphi)\in \mathbf F.</math>

W formułach postaci <math>(\exists x_i)(\varphi)</math> i <math>(\forall x_i)(\varphi)</math> mówimy, że zmienna <math>x_i</math> znajduje się w zasięgu [[kwantyfikator]]a 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 <math>(\exists x_i)(\varphi),</math> czy też <math>(\forall x_i)(\varphi)</math> pojawia się jako jedna z części użytych w budowie, ale ograniczamy się do występowań zmiennej <math>x_i</math> w <math>\varphi</math> (i mówimy, że konkretne wystąpienie zmiennej jest wolne lub związane).

'''[[Zdanie logiczne|Zdanie]]''' w języku pierwszego rzędu <math>\mathcal L(\tau)</math> 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 [[teoria mnogości|teorii mnogości]] to <math>\mathcal L(\{\in\}),</math> gdzie <math>\in</math> jest binarnym symbolem relacyjnym.
* Język [[teoria grup|teorii grup]] to <math>\mathcal L(\{*\}),</math> gdzie <math>*</math> jest binarnym symbolem funkcyjnym.
* Język [[Ciało uporządkowane|ciał uporządkowanych]] to <math>\mathcal L(\{+,\cdot,0,1,\leqslant\}),</math> gdzie <math>+,\cdot</math> są binarnymi symbolami funkcyjnymi a <math>\leqslant</math> jest binarnym symbolem relacyjnym.

== Dowody w językach pierwszego rzędu ==
Ustalmy alfabet <math>\tau</math> (tak więc jest to zbiór złożony ze stałych, symboli funkcyjnych i [[Symbol relacyjny|symboli relacyjnych]]).

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

W przypadku zmiennej <math>\xi,</math> termu <math>t</math> i formuły <math>\varphi</math> podstawienie <math>\varphi(\xi/t)</math> definiuje się bardziej subtelnie, co najlepiej ująć indukcyjnie względem budowy formuły <math>\varphi</math> (por. [2]):
* jeśli <math>\varphi</math> jest formułą atomową <math>P(t_1,\dots,t_n),</math> to <math>\varphi(\xi/t)=P(t_1(\xi/t),\dots,t_n(\xi/t))</math>
* jeśli <math>\varphi=\psi_1\circ\psi_2,</math> to <math>\varphi(\xi/t)=\psi_1(\xi/t)\circ\psi_2(\xi/t),</math> gdzie <math>\circ\in\{\wedge,\vee,\to,\leftrightarrow\}</math>
* jeśli <math>\varphi=\neg\psi,</math> to <math>\varphi(\xi/t)=\neg\psi(\xi/t)</math>

oraz
* jeśli <math>\varphi=(\mathcal Q\zeta)\psi,</math> gdzie <math>\mathcal Q\in\{\forall,\exists\},</math> to <math>\varphi(\xi/t)=\varphi,</math> jeśli <math>\zeta\in\{\xi\}\cup\mathbf{Vf}(t)</math> oraz <math>\varphi(\xi/t)=(\mathcal Q\zeta)\psi(\xi/t),</math> 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 <math>t</math> w formule <math>\varphi</math> za zmienną <math>\xi</math> jest ''dopuszczalne'' lub, że ''zmienna <math>\xi</math> jest '''wolna''' dla termu <math>t</math> w formule <math>\varphi</math>'', ozn. <math>\xi\in\mathbf{Ff}(t,\varphi),</math> gdy (nieformalnie) literalne wstawienie tego termu w rozważanej formule w miejscu któregoś z wolnych wystąpień zmiennej <math>\xi</math> spowodowałoby związanie pewnej zmiennej termu <math>t</math> (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:
<!-- <math>\xi\in\mathbf{Ff}(t,\varphi)</math> indukcyjnie ze względu na budowę formuły:-->
* jeśli <math>\xi\notin\mathbf{Vf}(\varphi),</math> to <math>\xi\in\mathbf{Ff}(t,\varphi)</math>
* jeśli <math>\varphi</math> jest formułą atomową, to <math>\xi\in\mathbf{Ff}(t,\varphi)</math>
* jeśli <math>\varphi=\psi_1\circ\psi_2,</math> to <math>\xi\in\mathbf{Ff}(t,\varphi)\Leftrightarrow\xi\in\mathbf{Ff}(t,\psi_1) \cap \mathbf{Ff}(t,\psi_2),</math> gdzie <math>\circ\in\{\wedge,\vee,\to,\leftrightarrow\}</math>
* jeśli <math>\varphi=\neg\psi,</math> to <math>\xi\in\mathbf{Ff}(t,\varphi)\Leftrightarrow\xi\in\mathbf{Ff}(t,\psi)</math>

oraz
* jeśli <math>\varphi=(\mathcal Q\zeta)\psi,</math> to <math>\xi\in\mathbf{Ff}(t,\varphi)\Leftrightarrow\xi\in\mathbf{Ff}(t,\psi)\&\zeta\notin\mathbf{Vf}(t),</math> gdzie <math>\mathcal Q\in\{\forall,\exists\}.</math>

==== Przykłady ====
Rozważmy język ciał uporządkowanych <math>\mathcal L(\{+,\cdot,0,1,\leqslant\}).</math> Niech termami <math>t,s,u</math> będą, odpowiednio <math>0+x_1+x_2,</math> <math>(1+1)\cdot x_1</math> oraz <math>x_3\cdot x_4.</math> Rozważmy formułę <math>\varphi=(\forall x_3)(\exists x_4)((x_1+x_3)\cdot x_7=x_4+1+0).</math> Wówczas
* <math>s(x_1/t)</math> to term <math>(1+1)\cdot (0+x_1+x_2),</math>
* <math>s(x_1/u)</math> to term <math>(1+1)\cdot (x_3\cdot x_4),</math>
* <math>\varphi(x_1/t)</math> to formuła <math>(\forall x_3)(\exists x_4)((0+x_1+x_2+x_3)\cdot x_7=x_4+1+0)</math> i podstawienie termu <math>t</math> za zmienną <math>x_1</math> w <math>\varphi</math> jest dopuszczalne,
* <math>\varphi(x_3/u)</math> oraz <math>\varphi(x_7/u)</math> są równokszałtne z <math>\varphi,</math> przy czym podstawienie termu <math>u</math> za zmienną <math>x_7</math> jest '''niedopuszczalne''', zaś podstawienie tego samego termu za zmienną <math>x_3</math> 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 [[Tautologia (logika)|tautologii]] [[rachunek zdań|rachunku zdań]],
* formuły postaci <math>(\forall x)(\varphi\Rightarrow\psi)\ \Rightarrow\ ((\forall x)(\varphi)\Rightarrow(\forall x)(\psi))</math> (gdzie <math>\varphi,\psi</math> to formuły),
* formuły postaci <math>(\forall x_i)(\varphi)\ \Rightarrow\ \varphi(x_i/t),</math> gdzie term <math>t</math> może być podstawiony za zmienną <math>x_i</math> w <math>\varphi,</math>
* formuły postaci <math>\varphi\Rightarrow (\forall x_i)(\varphi),</math> gdzie zmienna <math>x_i</math> nie jest wolna w formule <math>\varphi,</math>
* formuły postaci
:: <math>x=x,</math>
:: <math>x=y\ \Rightarrow y=x</math> i
:: <math>x=y\ \wedge\ y=z\ \Rightarrow\ x=z,</math>
: gdzie <math>x,y,z</math> są (niekoniecznie różnymi) zmiennymi,
* formuły postaci
:: <math>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)),</math>
: gdzie <math>z_1,\dots,z_k,y_1,\dots,y_k</math> są zmiennymi a <math>P\in \tau</math> jest <math>k</math>-arnym symbolem relacyjnym,
* formuły postaci
:: <math>y_1=z_1\ \wedge\ \ldots\ \wedge y_k=z_k\ \Rightarrow\ (f(y_1,\dots,y_k)=f(z_1,\dots,z_k)),</math>
: gdzie <math>z_1,\dots,z_k,y_1,\dots,y_k</math> są zmiennymi a <math>f\in \tau</math> jest <math>k</math>-arnym symbolem funkcyjnym.

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

=== Reguła wnioskowania ===
Jeśli <math>\varphi_1,\varphi_2,\psi</math> są formułami języka <math>\mathcal L(\tau),</math> oraz <math>\varphi_1</math> jest postaci <math>\varphi_2\ \Rightarrow\ \psi</math> to powiemy, że ''formuła <math>\psi</math> może być wywnioskowana z <math>\varphi_1,\varphi_2</math> w oparciu o regułę [[Modus ponendo ponens|modus ponens]]''.

=== Dowód ===
Niech <math>A\subseteq \mathbf F</math> będzie jakimś zbiorem formuł języka <math>\mathcal L(\tau)</math> (możliwie pustym). '''Dowodem ze zbioru aksjomatów ''A''''' nazywamy skończony [[Ciąg (matematyka)|ciąg]] formuł <math>\langle\varphi_1,\dots,\varphi_k\rangle</math> taki, że dla każdego <math>1\leqslant j\leqslant k,</math>
: <math>\varphi_j</math> jest jedną z formuł z <math>A</math> lub
: <math>\varphi_j</math> jest aksjomatem logicznym, lub
: <math>\varphi_j</math> może być wywnioskowana z <math>\varphi_k,\varphi_l</math> w oparciu o regułę modus ponens. dla pewnych <math>k,l.</math>

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

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

=== Podstawowe własności ===
Niech <math>A\subseteq \mathbf F</math> będzie jakimś zbiorem formuł języka <math>\mathcal L(\tau)</math> oraz niech <math>\varphi,\psi</math> będą formułami tegoż języka.
* '''[[Twierdzenie o dedukcji]]:''' <math>A\vdash \varphi\Rightarrow\psi</math> wtedy i tylko wtedy, gdy <math>A\cup\{\varphi\}\vdash\psi.</math>
* '''Twierdzenie o uogólnianiu:''' Jeśli zmienna <math>x</math> nie pojawia się jako zmienna wolna żadnej z formuł w <math>A</math> oraz <math>A\vdash\varphi,</math> to <math>A\vdash (\forall x)(\varphi).</math>
* '''Twierdzenie o wprowadzeniu kwantyfikatora <math>\forall{:}</math>'''
: (1) Przypuśćmy że term <math>t</math> może być podstawiony za zmienną <math>x</math> w <math>\psi.</math> Jeśli <math>A\vdash \psi(x/t)\Rightarrow\varphi,</math> to <math>A\vdash (\forall x)(\psi)\Rightarrow\varphi.</math>
: (2) Przypuśćmy że zmienna <math>x</math> nie jest wolna w <math>\psi</math> ani w żadnej z formuł w zbiorze <math>A.</math> Jeśli <math>A\vdash \psi\Rightarrow\varphi,</math> to <math>A\vdash \psi\Rightarrow (\forall x)(\varphi).</math>
* '''Twierdzenie o wprowadzeniu kwantyfikatora <math>\exists{:}</math>'''
: (1) Przypuśćmy że term <math>t</math> może być podstawiony za zmienną <math>x</math> w <math>\varphi.</math> Jeśli <math>A\vdash \varphi\Rightarrow\psi(x/t),</math> to <math>A\vdash \varphi\Rightarrow(\exists x)(\psi).</math>
: (2) Przypuśćmy że zmienna <math>x</math> nie jest wolna w <math>\psi</math> ani w żadnej z formuł w zbiorze <math>A.</math> Jeśli <math>A\vdash \varphi\Rightarrow\psi,</math> to <math>A\vdash (\exists x)(\varphi)\Rightarrow\psi.</math>
* '''[[Twierdzenie o zwartości]] I:''' zbiór zdań <math>A</math> 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 <math>\tau,</math> ponadto ustalmy, że <math>S_\tau</math> jest zbiorem stałych tego alfabetu, <math>F_\tau</math> jest zbiorem symboli funkcyjnych a <math>R_\tau</math> to zbiór symboli relacyjnych.

=== Modele ===
'''Interpretacją''' lub '''[[Struktura matematyczna|modelem]] języka''' <math>\mathcal L(\tau)</math> nazywamy układ
:: <math>\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},</math>

gdzie:
* <math>M</math> jest niepustym zbiorem zwanym dziedziną lub uniwersum modelu <math>\mathcal M</math> (często uniwersum modelu <math>\mathcal M</math> oznacza się przez <math>|\mathcal M|</math>),
* dla <math>n</math>-arnego symbolu relacyjnego <math>R\in R_\tau,</math> <math>R^\mathcal M</math> jest <math>n</math>-argumentową [[Relacja (matematyka)|relacją]] na zbiorze <math>M,</math> tzn. <math>R^\mathcal M\subseteq M^n,</math>
* dla <math>n</math>-arnego symbolu funkcyjnego <math>f\in F_\tau,</math> <math>f^\mathcal M</math> jest <math>n</math>-argumentowym [[Działanie algebraiczne|działaniem]] na zbiorze <math>M,</math> tzn. <math>f^\mathcal M: M^n\longrightarrow M,</math>
* dla stałej <math>c\in S_\tau,</math> <math>c^\mathcal M</math> jest elementem zbioru <math>M.</math>

=== Interpretacja termów w modelu ===
Przez indukcję po złożoności termów języka <math>\mathcal L(\tau)</math> definiujemy '''interpretację termu w modelu <math>\mathcal M</math>'''. Dla termu <math>t\in \mathbf T</math> o zmiennych wolnych zawartych wśród <math>x_1,\dots,x_n</math> i dla elementów <math>m_1,\dots,m_n\in M</math> uniwersum modelu <math>\mathcal M</math> wprowadzamy <math>t^\mathcal M[m_1,\dots,m_n]\in M</math> następująco.
* Jeśli <math>t</math> jest stałą <math>c</math> alfabetu τ, to <math>t^\mathcal M[m_1,\dots,m_n]=c^\mathcal M.</math>
* Jeśli <math>t</math> jest zmienną <math>x_i,</math> to <math>t^\mathcal M[m_1,\dots,m_n]=m_i.</math>
* Jeśli <math>t_1,\dots,t_k\in \mathbf T</math> i <math>f\in\tau</math> jest <math>k</math>-arnym symbolem funkcyjnym, to <math>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]).</math>

=== Relacja spełniania w modelu ===
Przez indukcję po złożoności formuł języka <math>\mathcal L(\tau)</math> definiujemy, kiedy '''formuła jest spełniona w modelu <math>\mathcal M</math>'''. Dla formuły <math>\varphi\in \mathbf F</math> o zmiennych wolnych zawartych wśród <math>x_1,\dots,x_n</math> i elementów <math>m_1,\dots,m_n\in M</math> uniwersum modelu <math>\mathcal M</math> wprowadzamy relację <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> (czyt. „formuła <math>\varphi</math> jest spełniona w modelu <math>\mathcal M</math> na elementach <math>m_1,\dots,m_n</math>”) następująco.
* Jeśli <math>\varphi</math> jest formułą <math>t_1=t_2</math> dla pewnych termów <math>t_1,t_2\in \mathbf T,</math> których zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy elementy <math>t_1^\mathcal M[m_1,\dots,m_n]</math> i <math>t_2^\mathcal M[m_1,\dots,m_n]</math> zbioru <math>M</math> są identyczne.
* Jeśli <math>\varphi</math> jest formułą <math>P(t_1,\dots,t_k)</math> dla pewnych termów <math>t_1,\dots,t_k\in \mathbf T,</math> których zmienne wolne są zawarte wśród <math>x_1,\dots,x_n</math> i k-arnego symbolu relacyjnego <math>P\in\tau,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy elementy <math>(t_1^\mathcal M[m_1,\dots,m_n],\dots, t_k^\mathcal M[m_1,\dots,m_n])\in P^\mathcal M.</math>
* Jeśli <math>\varphi</math> jest formułą <math>(\psi_1\wedge\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in \mathbf F,</math> których zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy <math>\mathcal M\models \psi_1[m_1,\dots,m_n]</math> oraz <math>\mathcal M\models \psi_2[m_1,\dots,m_n].</math>
* Jeśli <math>\varphi</math> jest formułą <math>(\psi_1\vee\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in \mathbf F,</math> których zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy <math>\mathcal M\models \psi_1[m_1,\dots,m_n]</math> lub <math>\mathcal M\models \psi_2[m_1,\dots,m_n].</math>
* Jeśli <math>\varphi</math> jest formułą <math>(\psi_1\Rightarrow\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in \mathbf F,</math> których zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy <math>\mathcal M\models \psi_2[m_1,\dots,m_n]</math> lub nie zachodzi, że <math>\mathcal M\models \psi_1[m_1,\dots,m_n].</math>
* Jeśli <math>\varphi</math> jest formułą <math>(\psi_1\Leftrightarrow\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in \mathbf F,</math> których zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy albo oba zdania <math>\mathcal M\models \psi_1[m_1,\dots,m_n]</math> i <math>\mathcal M\models \psi_2[m_1,\dots,m_n]</math> są prawdziwe, albo oba są fałszywe.
* Jeśli <math>\varphi</math> jest formułą <math>\neg\psi</math> dla pewnej formuły <math>\psi\in \mathbf F,</math> której zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy zdanie <math>\mathcal M\models \psi[m_1,\dots,m_n]</math> jest fałszywe.
* Jeśli <math>\varphi</math> jest formułą <math>(\forall x_j)(\psi)</math> dla pewnej formuły <math>\psi\in \mathbf F,</math> której zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy zdanie <math>\mathcal M\models \psi[m_1^*,\dots,m_n^*,\dots,m^*_k]</math> jest prawdziwe dla każdego ciągu <math>m_1^*,\dots,m_n^*,\dots,m^*_k</math> elementów uniwersum <math>M</math> takich, że <math>j\leqslant k</math> oraz <math>m^*_i=m_i</math> ilekroć <math>x_i</math> jest zmienną wolną w <math>\varphi.</math>
* Jeśli <math>\varphi</math> jest formułą <math>(\exists x_j)(\psi)</math> dla pewnej formuły <math>\psi\in \mathbf F,</math> której zmienne wolne są zawarte wśród <math>x_1,\dots,x_n,</math> to stwierdzimy, że <math>\mathcal M\models \varphi[m_1,\dots,m_n]</math> jest prawdziwe wtedy i tylko wtedy, gdy dla pewnego ciągu <math>m_1^*,\dots,m_n^*,\dots,m^*_k</math> elementów uniwersum <math>M</math> takich, że <math>j\leqslant k</math> oraz <math>m^*_i=m_i</math> ilekroć <math>x_i</math> jest zmienną wolną w <math>\varphi</math> mamy, że <math>\mathcal M\models \psi[m_1^*,\dots,m_n^*,\dots,m^*_k].</math>

=== Podstawowe własności ===
* '''[[Twierdzenie o pełności]]:''' zbiór zdań <math>A</math> jest niesprzeczny wtedy i tylko wtedy, gdy ma on model (tzn. jest spełniony w pewnym modelu języka <math>\mathcal L(\tau)</math>).
* '''[[Twierdzenie o zwartości]] II:''' zbiór zdań <math>A</math> 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 [[Liczby naturalne|liczb naturalnych]] posiada modele niestandardowe. W szczególności posiada je aksjomatyka Peana. Przykładem niestandardowego modelu aksjomatyki Peana są liczby hipernaturalne, czyli nieujemne [[Aksjomaty i konstrukcje liczb|liczby hiperrzeczywiste]], które są równe swojej części całkowitej. Istnieją nawet ''przeliczalne'' modele niestandardowe [[Arytmetyka|arytmetyki]]. Dokładne opisanie takich modeli jest trudne, gdyż zarówno dodawanie, jak i [[mnożenie]] jest w nich [[rozstrzygalność|nierozstrzygalne]].

== Przypisy ==
{{Przypisy}}

== Linki zewnętrzne ==
* {{MathWorld | adres = First-OrderLogic | tytuł = First-Order Logic }} [dostęp 2024-03-07].

{{Teorie formalne logiki}}

{{Kontrola autorytatywna}}

[[Kategoria:Logika matematyczna]]