Rachunek predykatów pierwszego rzędu
Z Wikipedii, wolnej encyclopedia
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].