Rachunek predykatów pierwszego rzędu

Rachunek predykatów pierwszego rzędu () – 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 na książce Martina Goldsterna i Haima Judaha. Wśród innych źródeł omawiających te zagadnienia należy wymienić podręcznik Witolda Pogorzelskiego, czy też książkę Zofii Adamowicz i Pawła Zbierskiego. Bardzo popularnym jest też opracowanie Josepha Shoenfielda.

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

(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 𝓛(𝜏) 

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

Niech  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  będzie nazywany alfabetem naszego języka, a sam język wyznaczony przez ten alfabet będzie oznaczany przez  Ustalmy też nieskończoną listę zmiennych (zwykle ).

Najpierw definiujemy termy języka  jako elementy najmniejszego zbioru  takiego, że:
 wszystkie stałe i zmienne należą do 
 jeśli  i  jest -arnym symbolem funkcyjnym, to 

Następnie określamy zbiór formuł języka  jako najmniejszy zbiór  taki, że:
 jeśli  to wyrażenie  należy do 
 jeśli  zaś  jest -arnym symbolem relacyjnym, to wyrażenie  należy do 
 jeśli  i  jest binarnym spójnikiem zdaniowym (alternatywą  koniunkcją  implikacją  lub równoważnością ), to  oraz 
 jeśli  jest zmienną oraz  to także  i 

W formułach postaci  i  mówimy, że zmienna  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  czy też  pojawia się jako jedna z części użytych w budowie, ale ograniczamy się do występowań zmiennej  w  (i mówimy, że konkretne wystąpienie zmiennej jest wolne lub związane).

Zdanie w języku pierwszego rzędu  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 teorii mnogości to  gdzie  jest binarnym symbolem relacyjnym.
 Język teorii grup to  gdzie  jest binarnym symbolem funkcyjnym.
 Język ciał uporządkowanych to  gdzie  są binarnymi symbolami funkcyjnymi a  jest binarnym symbolem relacyjnym.

Dowody w językach pierwszego rzędu 
Ustalmy alfabet  (tak więc jest to zbiór złożony ze stałych, symboli funkcyjnych i symboli relacyjnych).

Podstawienia termów za zmienne 
Przypuśćmy, że  i  są termami języka  oraz  jest jedną ze zmiennych. Definiujemy podstawienie  jako term, który powstaje z  poprzez literalne zastąpienie w nim wszystkich egzemplarzy zmiennej  termem 

W przypadku zmiennej  termu  i formuły  podstawienie  definiuje się bardziej subtelnie, co najlepiej ująć indukcyjnie względem budowy formuły  (por. [2]):
 jeśli  jest formułą atomową  to 
 jeśli  to  gdzie 
 jeśli  to 

oraz
 jeśli  gdzie  to  jeśli  oraz  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  w formule  za zmienną  jest dopuszczalne lub, że zmienna  jest wolna dla termu  w formule , ozn.  gdy (nieformalnie) literalne wstawienie tego termu w rozważanej formule w miejscu któregoś z wolnych wystąpień zmiennej  spowodowałoby związanie pewnej zmiennej termu  (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:

 jeśli  to 
 jeśli  jest formułą atomową, to 
 jeśli  to  gdzie 
 jeśli  to 

oraz
 jeśli  to  gdzie

Przykłady 
Rozważmy język ciał uporządkowanych  Niech termami  będą, odpowiednio   oraz  Rozważmy formułę  Wówczas
  to term 
  to term 
  to formuła  i podstawienie termu  za zmienną  w  jest dopuszczalne,
  oraz  są równokszałtne z  przy czym podstawienie termu  za zmienną  jest niedopuszczalne, zaś podstawienie tego samego termu za zmienną  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 tautologii rachunku zdań,
 formuły postaci  (gdzie  to formuły),
 formuły postaci  gdzie term  może być podstawiony za zmienną  w 
 formuły postaci  gdzie zmienna  nie jest wolna w formule 
 formuły postaci
 
  i
 
 gdzie  są (niekoniecznie różnymi) zmiennymi,
 formuły postaci
 
 gdzie  są zmiennymi a  jest -arnym symbolem relacyjnym,
 formuły postaci
 
 gdzie  są zmiennymi a  jest -arnym symbolem funkcyjnym.

Aksjomaty czyste i formuły postaci  gdzie  jest aksjomatem czystym, są nazywane aksjomatami logicznymi.

Reguła wnioskowania 
Jeśli  są formułami języka  oraz  jest postaci  to powiemy, że formuła  może być wywnioskowana z  w oparciu o regułę modus ponens.

Dowód 
Niech  będzie jakimś zbiorem formuł języka  (możliwie pustym). Dowodem ze zbioru aksjomatów A nazywamy skończony ciąg formuł  taki, że dla każdego 
  jest jedną z formuł z  lub
  jest aksjomatem logicznym, lub
  może być wywnioskowana z  w oparciu o regułę modus ponens. dla pewnych 

Jeśli  jest dowodem ze zbioru aksjomatów  to powiemy, że formuła  jest dowodliwa z A albo też że  jest twierdzeniem z A i napiszemy wtedy  Jeśli  jest zbiorem pustym to możemy pominąć je w naszych oznaczeniach i napisać 

Powiemy, że  jest sprzecznym zbiorem aksjomatów, jeśli dla pewnej formuły  mamy zarówno że  jak i  W przeciwnym razie mówimy, że  jest niesprzeczny.

Podstawowe własności 
Niech  będzie jakimś zbiorem formuł języka  oraz niech  będą formułami tegoż języka.
 Twierdzenie o dedukcji:  wtedy i tylko wtedy, gdy 
 Twierdzenie o uogólnianiu: Jeśli zmienna  nie pojawia się jako zmienna wolna żadnej z formuł w  oraz  to 
 Twierdzenie o wprowadzeniu kwantyfikatora 
 (1) Przypuśćmy że term  może być podstawiony za zmienną  w  Jeśli  to 
 (2) Przypuśćmy że zmienna  nie jest wolna w  ani w żadnej z formuł w zbiorze  Jeśli  to 
 Twierdzenie o wprowadzeniu kwantyfikatora 
 (1) Przypuśćmy że term  może być podstawiony za zmienną  w  Jeśli  to 
 (2) Przypuśćmy że zmienna  nie jest wolna w  ani w żadnej z formuł w zbiorze  Jeśli  to 
 Twierdzenie o zwartości I: zbiór zdań  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  ponadto ustalmy, że  jest zbiorem stałych tego alfabetu,  jest zbiorem symboli funkcyjnych a  to zbiór symboli relacyjnych.

Modele 
Interpretacją lub modelem języka  nazywamy układ
 

gdzie:
  jest niepustym zbiorem zwanym dziedziną lub uniwersum modelu  (często uniwersum modelu  oznacza się przez ),
 dla -arnego symbolu relacyjnego   jest -argumentową relacją na zbiorze  tzn. 
 dla -arnego symbolu funkcyjnego   jest -argumentowym działaniem na zbiorze  tzn. 
 dla stałej   jest elementem zbioru

Interpretacja termów w modelu 
Przez indukcję po złożoności termów języka  definiujemy interpretację termu w modelu . Dla termu  o zmiennych wolnych zawartych wśród  i dla elementów  uniwersum modelu  wprowadzamy  następująco.
 Jeśli  jest stałą  alfabetu τ, to 
 Jeśli  jest zmienną  to 
 Jeśli  i  jest -arnym symbolem funkcyjnym, to

Relacja spełniania w modelu 
Przez indukcję po złożoności formuł języka  definiujemy, kiedy formuła jest spełniona w modelu . Dla formuły  o zmiennych wolnych zawartych wśród  i elementów  uniwersum modelu  wprowadzamy relację  (czyt. „formuła  jest spełniona w modelu  na elementach ”) następująco.
 Jeśli  jest formułą  dla pewnych termów  których zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy elementy  i  zbioru  są identyczne.
 Jeśli  jest formułą  dla pewnych termów  których zmienne wolne są zawarte wśród  i k-arnego symbolu relacyjnego  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy elementy 
 Jeśli  jest formułą  dla pewnych formuł  których zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy  oraz 
 Jeśli  jest formułą  dla pewnych formuł  których zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy  lub 
 Jeśli  jest formułą  dla pewnych formuł  których zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy  lub nie zachodzi, że 
 Jeśli  jest formułą  dla pewnych formuł  których zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy albo oba zdania  i  są prawdziwe, albo oba są fałszywe.
 Jeśli  jest formułą  dla pewnej formuły  której zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy zdanie  jest fałszywe.
 Jeśli  jest formułą  dla pewnej formuły  której zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy zdanie  jest prawdziwe dla każdego ciągu  elementów uniwersum  takich, że  oraz  ilekroć  jest zmienną wolną w 
 Jeśli  jest formułą  dla pewnej formuły  której zmienne wolne są zawarte wśród  to stwierdzimy, że  jest prawdziwe wtedy i tylko wtedy, gdy dla pewnego ciągu  elementów uniwersum  takich, że  oraz  ilekroć  jest zmienną wolną w  mamy, że

Podstawowe własności 
 Twierdzenie o pełności: zbiór zdań  jest niesprzeczny wtedy i tylko wtedy, gdy ma on model (tzn. jest spełniony w pewnym modelu języka ).
 Twierdzenie o zwartości II: zbiór zdań  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 liczb naturalnych posiada modele niestandardowe. W szczególności posiada je aksjomatyka Peana. Przykładem niestandardowego modelu aksjomatyki Peana 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ż 
 forma preneksowa
 język programowania Prolog
 prawa rachunku kwantyfikatorów
 rachunek predykatów drugiego rzędu
 skolemizacja
 term
 twierdzenie Craiga
 twierdzenie Gödla
 twierdzenie Herbranda

Przypisy 

Logika matematyczna