Istnieje odrębny dział logiki, w którym wszystkie rozpatrywane struktury są skończone. Na przykład strukturą skończoną jest \(<\{0,1,2\},0,\leq>\), czyli zbiór {0,1,2} ze stałą 0 i porządkiem. Natomiast liczby naturalne z dodawaniem nie są strukturą skończoną.
Struktury takie mają dwie zasadnicze zalety z punktu widzenia informatyki:
- Strukturę skończoną można bezpośrednio reprezentować w pamięci komputera.
- Można napisać program, który sprawdza, czy w danej strukturze skończonej prawdziwa jest dana formuła. Gdy program taki ma sprawdzić, czy prawdziwa jest formuła postaci \(\exists_x\varphi(x)\), sprawdza on po prostu wszystkie możliwe wartości x i jeśli dla jakiejkolwiek z nich zajdzie \(\varphi(x)\), uznaje że formuła jest prawdziwa, w przeciwnym przypadku uznaje że jest nieprawdziwa. Analogicznie z kwantyfikatorem \(\forall\).
Oprócz informatycznych zalet, okazuje się, że ograniczenie do skończonych struktur ma duże znaczenie z punktu widzenia teoretycznego. Na przykład wiele twierdzeń i własności które zachodzą w ogólności, przestaje być prawdziwych gdy ograniczamy się do struktur skończonych.
Słowa
Szczególnym przykładem struktur skończonych są słowa. Można mianowicie z każdym słowem w o literach \(a_1,a_2,\ldots,a_n\), związać strukturę której elementy to liczby \(\{1,2,\ldots,n\}\). Dodatkowo, w strukturze tej dostępne są predykaty \(A,B,C,\ldots,Z\) oznaczające że na odpowiedniej pozycji stoi odpowiednia litera. Na przykład D(7) jest prawdą wtedy i tylko wtedy gdy siódma litera w słowie w to 'D'. Załóżmy jeszcze, że w strukturze tej dostępny jest porządek \(\leq\) na jej elementach. Strukturę taką oznaczać będziemy Sw.
Można teraz rozpatrywać różne zdania logiki. Na przykład zdanie
- \(\varphi_Z\equiv\exists_a Z(a)\wedge \forall_b a\leq b\)
mówi, że istnieje taka pozycja w słowie, na której stoi literka 'Z' i jest to najmniejsza pozycja w słowie. Czyli zachodzi \(S_w\models \varphi_Z\) wtedy i tylko wtedy, gdy pierwszą literką w jest 'Z'. Na przykład \(M_{ZABA}\models\varphi_Z\), ale nie jest prawdą, że \(M_{BOCIAN}\models \varphi_Z\).
Można widzieć to tak, że dowolna formuła korzystająca z porządku \(\leq\) i predykatów \(A,B,C,\ldots,Z\), definiuje zbiór takich słów w, że \(S_w\models\varphi\). Zbiór ten oznaczmy \(L(\varphi)\) i nazywamy językiem słów definiowanych przez \(\varphi\). Istnieje duża i ważna gałąź nauki, z pogranicza matematyki i informatyki, badająca jakie zbiory słów daje się definiować używając formuł różnorodnych logik.
Wyrażanie własności
Oprócz badania obiektów skończonych, reprezentowanych bezpośrednio w pamięci komputera, czasami chcielibyśmy badać też inne pojęcia. Wyobraźmy sobie serwer, którego zadaniem jest nieustannie reagować na wiadomości wysyłane przez użytkowników i w zależności od typu wiadomości, przesyłać ją dalej, lub niszczyć. Teoretyczny zapis działania takiego serwera, od dnia uruchomienia w przód, to w naturalny sposób nieskończony ciąg operacji jakie ten serwer mógłby wykonać w czasie swego nieograniczonego w czasie działania. Oczywiście to tylko teoria, bo w praktyce każdy serwer działa tylko skończenie długo. Ale jeśli chcielibyśmy modelować taki hipotetyczny serwer, działający już zawsze, potrzebne nam będą nowe pojęcia.
Z pomocą przychodzi tutaj logika. Możemy mianowicie nie trzymać w pamięci całego (nieskończonego) zapisu działania serwera, zamiast tego możemy trzymać formułę jakiejś logiki, która opisuje własności tego działania. Następnie, korzystając ze sprytnie napisanych programów komputerowych, możemy wywnioskować z tych własności serwera, że na przykład nigdy się on nie zawiesi. Takie zagadnienia są badane, jedną z logik wygodnych do takich operacji jest właśnie logika MSO, opisana w jednym z poprzednich rozdziałów.
Opisana powyżej, w dużym skrócie, metoda pozwala przenieść problemy dotyczące konkretnych, niekoniecznie skończonych struktur (np. działającego nieskończenie długo serwera) na badanie formuł logiki. A formuły takie zawsze są skończonymi napisami, z którymi dobrze może sobie radzić komputer.