Wikipedia

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

Przeglądaj historię interaktywnie
[wersja przejrzana][wersja przejrzana]
← poprzednia edycjanastępna edycja →
Usunięta treść Dodana treść
WizualnieWikikod
Findepi (dyskusja | edycje)
45 edycji
MastiBot (dyskusja | edycje)
Boty
3 415 359 edycji
m Wspomagane przez robota ujednoznacznienie: Przegląd zagadnień z zakresu logiki - Zmieniono link(i) Wikipedia:Skarbnica Wikipedii/Przegląd zagadnień z zakresu logiki; zmiany kosmetyczne
Linia 1:
'''Rachunek predykatów pierwszego rzędu''' – ([[język angielski|ang.]] ''first order predicate calculus'') to 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 (matematyka)|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ę [[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 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.
Linia 7:
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<ref>Martin Goldstern; Haim Judah: ''The Incompleteness Phenomenon. A new course in mathematical logic''. A K Peters, Wellesley, Massachusetts, 1995. ISBN 1-56881-029-6</ref>. Wśród innych źródeł omawiających te zagadnienia należy wymienić podręcznik Witolda Pogorzelskiego<ref>Witold A. Pogorzelski: ''Klasyczny rachunek kwantyfikatorów, zarys teorii'', Państwowe Wydawnictwo Naukowe, Warszawa 1981. ISBN 83-01-00567-X</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 ==
Linia 22:
* 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>
Linia 42:
* jeśli <math>t_1, t_2\in {\bold T}</math>, to wyrażenie <math>t_1= t_2</math> należy do <math>{\bold F}</math>,
* jeśli <math>t_1,\ldots,t_n\in {\bold T}</math> zaś <math>P\in\tau</math> jest <math>n</math>-arnym symbolem relacyjnym, to wyrażenie <math>P(t_1,\ldots,t_n)</math> należy do <math>{\bold F}</math>,
* jeśli <math>\varphi,\psi\in {\bold F}</math> i <math>*</math> jest binarnym spójnikiem zdaniowym ([[alternatywa|alternatywą]] <math>\vee</math>, [[Koniunkcja (matematyka)|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 {\bold F}</math> oraz <math>\neg \varphi\in {\bold F}</math>,
* jeśli <math>x_i</math> jest zmienną oraz <math>\varphi\in {\bold F}</math>, to także <math>(\exists x_i)(\varphi)\in {\bold F}</math> i <math>(\forall x_i)(\varphi)\in {\bold 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.
 
Linia 73:
* 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
Linia 96:
: <math>\varphi_j</math> jest jedną z formuł z ''A'', 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,\ldots,\varphi_k\rangle</math> jest dowodem ze zbioru aksjomatów ''A'', 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 ''A'' jest zbiorem pustym to możemy pominąć je w naszych oznaczeniach i napisać <math>\vdash \varphi</math>.
Linia 107:
* '''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>.
* '''Twierdzenie o wprowadzeniu kwantyfikatora <math>\forall</math>''':
: (1) Przypuśćmy że term ''t'' może być podstawiony za zmienną ''x'' 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 ''x'' nie jest wolna w <math>\psi</math> ani w żadnej z formuł w zbiorze ''A''. 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 ''t'' może być podstawiony za zmienną ''x'' 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 ''x'' nie jest wolna w <math>\psi</math> ani w żadnej z formuł w zbiorze ''A''. 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ń ''A'' 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 ===
Linia 122:
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 {\bold T}</math> o zmiennych wolnych zawartych wśród <math>x_1,\ldots,x_n</math> i dla elementów <math>m_1,\ldots,m_n\in M</math> uniwersum modelu <math>{\mathcal M}</math> wprowadzamy <math>t^{\mathcal M}[m_1,\ldots,m_n]\in M</math> następująco.
* Jeśli ''t'' jest stałą ''c'' alfabetu τ, to <math>t^{\mathcal M}[m_1,\ldots,m_n]=c^{\mathcal M}</math>.
Linia 134:
 
=== 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 {\bold F}</math> o zmiennych wolnych zawartych wśród <math>x_1,\ldots,x_n</math> i elementów <math>m_1,\ldots,m_n\in M</math> uniwersum modelu <math>{\mathcal M}</math> wprowadzamy relację <math>{\mathcal M}\models \varphi[m_1,\ldots,m_n]</math> (czyt. "formuła <math>\varphi</math> jest spełniona w modelu <math>{\mathcal M}</math> na elementach <math>m_1,\ldots,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 {\bold T}</math> których zmienne wolne są zawarte wśród <math>x_1,\ldots,x_n</math>, to stwierdzimy że <math>{\mathcal M}\models \varphi[m_1,\ldots,m_n]</math> jest prawdziwe wtedy i tylko wtedy gdy elementy <math>t_1^{\mathcal M}[m_1,\ldots,m_n]</math> i <math>t_2^{\mathcal M}[m_1,\ldots,m_n]</math> zbioru ''M'' są identyczne.
* Jeśli φ jest formułą <math>P(t_1,\ldots,t_k)</math> dla pewnych termów <math>t_1,\ldots,t_k\in {\bold T}</math> których zmienne wolne są zawarte wśród <math>x_1,\ldots,x_n</math> i k-arnego symbolu relacyjnego <math>P\in\tau</math>, to stwierdzimy że <math>{\mathcal M}\models \varphi[m_1,\ldots,m_n]</math> jest prawdziwe wtedy i tylko wtedy gdy elementy <math>(t_1^{\mathcal M}[m_1,\ldots,m_n],\ldots, t_k^{\mathcal M}[m_1,\ldots,m_n])\in P^{\mathcal M}</math>.
Linia 150:
 
== Zobacz też ==
* [[Wikipedia:Skarbnica Wikipedii/Przegląd zagadnień z zakresu logiki|przegląd zagadnień z zakresu logiki]]
* [[przegląd zagadnień z zakresu matematyki]]
* [[forma preneksowa]]
Linia 158:
* [[twierdzenie Herbranda]]
* [[twierdzenie Craiga]]
* [[Prolog_Prolog (język_programowaniajęzyk programowania)|język programowania Prolog]].
 
{{Przypisy}}
Źródło: „https://pl.wikipedia.org/wiki/Rachunek_predykatów_pierwszego_rzędu”