Jedną z najstarszych logik, innych od HOL, jest tzw. logika pierwszego rzędu. Nie różni się ona niczym od logiki wyższych rzędów, oprócz ograniczenia, że wszelkie kwantyfikatory mogą wiązać tylko pojedyncze elementy rozpatrywanej struktury. Na przykład, gdy rozpatrywana struktura to liczby naturalne z porządkiem \(<\mathbb N,\leq>\), to formuła \(\lnot\exists_x\forall_y y\leq x\) jest (zresztą prawdziwą) formułą pierwszego rzędu. Mówi ona, że nie istnieje największa liczba naturalna. Natomiast formuła \(\forall_{X\subseteq \mathbb N}\exists_y\forall_x x\in X\Rightarrow x\leq y\) nie jest formułą logiki pierwszego rzędu, gdyż zawiera kwantyfikator obejmujący wszystkie podzbiory struktury.
Logikę pierwszego rzędu oznaczamy FOL, od angielskiego First Order Logic.
Są własności, które można wyrazić w HOL, nie można natomiast tego zrobić w FOL. Rozważmy na przykład strukturę \(<\mathbb N,0,s>\), czyli liczby naturalne z zerem i funkcją s(x) = x + 1. Struktura ta nazywa się liczby naturalne z następnikiem. Można w niej napisać formułę HOL \(\varphi(x)\), mówiącą że dana liczba x jest parzysta. Co prawda nie można do tego użyć mnożenia (bo nie jest dostępne w strukturze), ale możemy napisać tak:
- \(\varphi(x)\equiv\exists_{X\subseteq\mathbb N}0\in X\wedge x\in X\wedge \forall_a\forall_b\forall_c \left(a\in X\wedge s(a)=b\wedge s(b)=c\right)\Rightarrow (b\notin X\wedge c\in X)\).
Formuła ta mówi, że istnieje zbiór X, który zawiera zero i daną liczbę x i jeśli zawiera a, to nie zawiera a + 1 i zawiera a + 2. Czyli równoważnie, że istnieje zbiór będący zbiorem liczb parzystych, do którego należy x.
Okazuje się, że używając specjalnej techniki, nazywanej grą Echrenfeuhta-Fraissego, można pokazać, że nie istnieje formuła \(\varphi(x)\) logiki pierwszego rzędu, wyrażająca że liczba x jest parzysta. Czyli logika ta jest istotnie słabsza (pod względem siły wyrazu) niż HOL.
Z drugiej strony, już w logice pierwszego rzędu można wyrażać bardzo skomplikowane własności rozpatrywanych modeli. Wiadomo na przykład, że nie może istnieć program komputerowy, który wczytywałby zdanie logiki pierwszego rzędu wypowiadające coś o arytmetyce liczb naturalnych i odpowiadałby na pytanie, czy to zdanie można udowodnić.
Monadyczna logika drugiego rzędu
Jest to szczególny przykład logiki, w której dopuszczalne są kwantyfikacje po elementach modelu (jak w FOL) i po podzbiorach modelu. Czyli dopuszczalna jest podana wyżej formuła mówiąca, że dana liczba jest parzysta, ale nie można na przykład kwantyfikować po funkcjach \(\mathbb R\to\mathbb R\). Logika ta jest oznaczana MSO od angielskiego Monadic Second Order Logic. Ma ona duże znaczenie we współczesnej logice teoretycznej, m.in. dlatego że niektóre własności tej logiki mogą być sprawdzane z użyciem programu komputerowego.
Poniższe ćwiczenie dotyczy zdania logiki monadycznej, które nie jest zdaniem FOL.
|
Ćwiczenie Co mówi formuła \(\forall_{X\subseteq \mathbb N}\exists_{y\in\mathbb N}\forall_{x\in\mathbb N} x\in X\Rightarrow x < y\)? Czy jest prawdziwa w strukturze liczb naturalnych z porządkiem? |
MSO+P
Można rozważyć rozszerzenie logiki MSO o dodatkowy kwantyfikator \(\mathbf P\). Aby była to dobrze określona logika, trzeba powiedzieć kiedy dana formuła tej logiki jest spełniona. W tym celu trzeba określić znaczenie kwantyfikatora \(\mathbf P\). Robimy to następująco:
- Kwantyfikator \(\mathbf P\) będzie wiązać zbiory elementów. Formuła \(\mathbf{P}_X \varphi(X)\) jest prawdą w strukturze S, jeśli każdy skończony podzbiór struktury \(X\subseteq S\), dla którego zachodzi \(\varphi(X)\), ma liczbę elementów będącą liczbą pierwszą.
Dzięki powyższej definicji, określiliśmy kiedy \(S\models\psi\), dla dowolnego zdania ψ tej logiki.
Okazuje się, że logika ta jest silniejsza od MSO, a jednocześnie słabsza od HOL. Podana jest tutaj, jako przykład logiki powstałej z rozszerzenia czegoś znanego, o nową konstrukcję.
Dla logik powstałych na tej drodze często nie definiuje się systemów dowodzenia. Chodzi o to, że nie są one tworzone by dowodzić jakiś własności, tylko by wyrażać, że rozpatrywana struktura ma jakąś własność. A do tego wystarcza relacja \(\models\).