Rachunek predykatów pierwszego rzędu: Różnice pomiędzy wersjami

[wersja przejrzana][wersja przejrzana]
Usunięta treść Dodana treść
Linia 29:
Następnie ustalimy reguły wnioskowania, a także metody interpretacji naszych napisów.
 
== Formalizacja języka <math>{\mathcal L}(\tau)</math> ==
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ą 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>\boldmathbf T</math> takiego, że:
* wszystkie stałe i zmienne należą do <math>{\boldmathbf T},</math>
* jeśli <math>t_1,\dots,t_n\in {\boldmathbf T}</math> i <math>f\in\tau</math> jest <math>n</math>-arnym symbolem funkcyjnym, to <math>f(t_1,\dots,t_n)\in {\boldmathbf T}.</math>
 
Następnie określamy zbiór '''formuł''' języka <math>{\mathcal L}(\tau)</math> jako najmniejszy zbiór <math>\boldmathbf F</math> taki, że:
* jeśli <math>t_1, t_2\in {\boldmathbf T},</math> to wyrażenie <math>t_1= t_2</math> należy do <math>{\boldmathbf F},</math>
* jeśli <math>t_1,\dots,t_n\in {\boldmathbf 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>{\boldmathbf F},</math>
* jeśli <math>\varphi,\psi\in {\boldmathbf F}</math> i <math>*</math> jest binarnym spójnikiem zdaniowym ([[alternatywa|alternatywą]] <math>\vee,</math> [[Koniunkcja (logika)|koniunkcją]] <math>\wedge,</math> [[implikacja|implikacją]] <math>\Rightarrow</math> lub [[równoważność|równoważnością]] <math>\Leftrightarrow</math>), to <math>(\varphi*\psi)\in {\boldmathbf F}</math> oraz <math>\neg \varphi\in {\boldmathbf F},</math>
* jeśli <math>x_i</math> jest zmienną oraz <math>\varphi\in {\boldmathbf F},</math> to także <math>(\exists x_i)(\varphi)\in {\boldmathbf F}</math> i <math>(\forall x_i)(\varphi)\in {\boldmathbf 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 ==
Linia 57:
 
=== Podstawienia termów za zmienne ===
Przypuśćmy, że ''t'' i ''s'' 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 ''s'' poprzez literalne zastąpienie w nim wszystkich egzemplarzy zmiennej <math>\xi</math> termem ''t''.
 
W przypadku zmiennej <math>\xi,</math> termu ''t'' 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,\rightarrowto,\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\boldmathbf{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 ''t'' w formule <math>\varphi</math> za zmienną <math>\xi</math> jest ''dopuszczalne'' lub, że ''zmienna <math>\xi</math> jest '''wolna''' dla termu ''t'' w formule <math>\varphi</math>'', ozn. <math>\xi\in\boldmathbf{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 ''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:
<!-- <math>\xi\in\boldmathbf{Ff}(t,\varphi)</math> indukcyjnie ze względu na budowę formuły:-->
* jeśli <math>\xi\not\in\boldmathbf{Vf}(\varphi),</math> to <math>\xi\in\boldmathbf{Ff}(t,\varphi)</math>
* jeśli <math>\varphi</math> jest formułą atomową, to <math>\xi\in\boldmathbf{Ff}(t,\varphi)</math>
* jeśli <math>\varphi=\psi_1\circ\psi_2,</math> to <math>\xi\in\boldmathbf{Ff}(t,\varphi)\Leftrightarrow\xi\in\boldmathbf{Ff}(t,\psi_1) \cap \boldmathbf{Ff}(t,\psi_2),</math> gdzie <math>\circ\in\{\wedge,\vee,\rightarrowto,\leftrightarrow\}</math>
* jeśli <math>\varphi=\neg\psi,</math> to <math>\xi\in\boldmathbf{Ff}(t,\varphi)\Leftrightarrow\xi\in\boldmathbf{Ff}(t,\psi)</math>
 
oraz
* jeśli <math>\varphi=({\mathcal Q}\zeta)\psi,</math> to <math>\xi\in\boldmathbf{Ff}(t,\varphi)\Leftrightarrow\xi\in\boldmathbf{Ff}(t,\psi)\&\zeta\not\in\boldmathbf{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>
Linia 108:
 
=== 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 ponens]]''.
 
=== Dowód ===
Niech <math>A\subseteq {\boldmathbf 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 ''A'' lub
: <math>\varphi_j</math> jest aksjomatem logicznym, lub
Linia 121:
 
=== Podstawowe własności ===
Niech <math>A\subseteq {\boldmathbf 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 ''x'' nie pojawia się jako zmienna wolna żadnej z formuł w ''A'' oraz <math>A\vdash\varphi,</math> to <math>A\vdash (\forall x)(\varphi).</math>
Linia 136:
 
=== 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:
* ''M'' 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 ''n''-arnego symbolu relacyjnego <math>R\in R_\tau,</math> <math>R^{\mathcal M}</math> jest ''n''-argumentową [[Relacja (matematyka)|relacją]] na zbiorze ''M'', tzn. <math>R^{\mathcal M}\subseteq M^n,</math>
* dla ''n''-arnego symbolu funkcyjnego <math>f\in F_\tau,</math> <math>f^{\mathcal M}</math> jest ''n''-argumentowym [[Działanie algebraiczne|działaniem]] na zbiorze ''M'', 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 ''M''.
 
=== 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 {\boldmathbf 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 ''t'' jest stałą ''c'' alfabetu τ, to <math>t^{\mathcal M}[m_1,\dots,m_n]=c^{\mathcal M}.</math>
* Jeśli ''t'' 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 {\boldmathbf 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 {\boldmathbf 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 φ jest formułą <math>t_1=t_2</math> dla pewnych termów <math>t_1,t_2\in {\boldmathbf 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 ''M'' są identyczne.
* Jeśli φ jest formułą <math>P(t_1,\dots,t_k)</math> dla pewnych termów <math>t_1,\dots,t_k\in {\boldmathbf 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 φ jest formułą <math>(\psi_1\wedge\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in {\boldmathbf 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 φ jest formułą <math>(\psi_1\vee\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in {\boldmathbf 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 φ jest formułą <math>(\psi_1\Rightarrow\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in {\boldmathbf 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 φ jest formułą <math>(\psi_1\Leftrightarrow\psi_2)</math> dla pewnych formuł <math>\psi_1,\psi_2\in {\boldmathbf 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 φ jest formułą <math>\neg\psi</math> dla pewnej formuły <math>\psi\in {\boldmathbf 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 φ jest formułą <math>(\forall x_j)(\psi)</math> dla pewnej formuły <math>\psi\in {\boldmathbf 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 ''M'' takich, że <math>j\leqslant k</math> oraz <math>m^*_i=m_i</math> ilekroć <math>x_i</math> jest zmienną wolną w φ.
* Jeśli φ jest formułą <math>(\exists x_j)(\psi)</math> dla pewnej formuły <math>\psi\in {\boldmathbf 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 ''M'' takich, że <math>j\leqslant k</math> oraz <math>m^*_i=m_i</math> ilekroć <math>x_i</math> jest zmienną wolną w φ 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ń ''A'' 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ń ''A'' ma model wtedy i tylko wtedy, gdy każdy jego podzbiór skończony ma model.