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,≤>, 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 ∃xφ(x), sprawdza on po prostu wszystkie możliwe wartości x i jeśli dla jakiejkolwiek z nich zajdzie φ(x), uznaje że formuła jest prawdziwa, w przeciwnym przypadku uznaje że jest nieprawdziwa. Analogicznie z kwantyfikatorem ∀.
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 a1,a2,…,an, związać strukturę której elementy to liczby {1,2,…,n}. Dodatkowo, w strukturze tej dostępne są predykaty A,B,C,…,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 ≤ na jej elementach. Strukturę taką oznaczać będziemy Sw.
Można teraz rozpatrywać różne zdania logiki. Na przykład zdanie
- φZ≡∃aZ(a)∧∀ba≤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 Sw⊨φZ wtedy i tylko wtedy, gdy pierwszą literką w jest 'Z'. Na przykład MZABA⊨φZ, ale nie jest prawdą, że MBOCIAN⊨φZ.
Można widzieć to tak, że dowolna formuła korzystająca z porządku ≤ i predykatów A,B,C,…,Z, definiuje zbiór takich słów w, że Sw⊨φ. Zbiór ten oznaczmy L(φ) i nazywamy językiem słów definiowanych przez φ. 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.