7738996300

Rozdział 3

Interpretacje

Spisali: Michał Skrzypczak

W tym rozdziale rozpatrywać będziemy logiki FO i MSO, w strukturach relacyjnych. Kluczowym pojęciem będzie rozstrzygalność teorii

Definicja 3. Powiemy, że teoria ustalonej logiki, przy ustalonej signaturze E, w modelu M jest rozstrzy-galna, jeśli istnieje algorytm wczytujący dowolną formulę p i odpowiadający, czy M |= <p.

W zależności od logiki, sygnatury i modelu, problem spełnialności może być rozstrzygalny lub nie. Na przykład dla logiki składającej się z jednej formuły _L, nie spełnionej w żadnym modelu, problem ten jest zawsze rozstrzygalny. Z drugiej strony problem spełnialności formuł logiki pierwszego rzędu w liczbach naturalnych z dodawaniem i mnożeniem jest nierozstrzygalny (Godeł).

Celem będzie umiejętność przenoszenia rozstrzygalności problemu spełnialności z jednego modelu, na inny. Na przykład wiemy, że liczby naturalne z następnikiem mają rozstrzygalną teorię MSO. Chcielibyśmy z tego wywnioskować, że również liczby całkowite mają rozstrzygalną teorię MSO. Metodą dowodzenia takich twierdzeń będą interpretacje.

Definicja 4. Powiemy, że struktura relacyjna M\ nad sygnaturą Ei interpretuje się w strukturze M2 nad sygnaturą E2, jeśli istnieją:

•    różnowartościowe zanurzenie i: |Mj| —* IM2I, gdzie \Mj\ oznacza nośnik odpowiedniej struktury,

•    formuła logiczna p(x) nad sygnaturą E2, spełniona dla x € \M%\ wtedy i tylko wtedy, gdy x leży w obrazie i,

•    dla każdego symbolu relacyjnego R € Ei formuła Pr(x 1,... ,x_n) nad sygnaturą E2, taka że dla każdych

,x_n G |Mi|, mamy R(x 1,... ,x_n) wtedy i tylko wtedy, gdy M2 |= Pfł(i(xi), ■ ■ ■ ,i(x„)).

Nie wymagamy żadnych własności od włożenia i, może to być dowolna, teoriomnogościowa funkcja. Kluczem powyższej definicji jest możliwość mapowania dowolnej formuły p nad sygnaturą M\, na formułę p' nad sygnaturą E2, w ten sposób, by M\ |= p wtw. M% \= p' ■ Mapowanie to odbywa się w ten sposób, że w miejsce wystąpienia dowolnego symbolu relacyjnego R wstawiamy odpowiednią formułę Pr, a kwantyfikatory wzbogacamy o wymaganie, by kwantyfikowana zmienna x spełniała warunek p(x). Dzięki temu, otrzymujemy następujące twierdzenie.

Twierdzenie 11. Jeśli struktura M\ interpretuje się w strukturze WI2 i teoria M2 jest rozstrzygalną, wtedy rozstrzygalną jest również teoria M\.

Dowód

Można tu bezpośrednio skonstruować algorytm. Zakładamy, że dana jest formuła p. Obliczamy formułę p', zgodnie z podaną konstrukcją. Sprawdzamy, czy p' jest spełnione w M2. Odpowiedź jest jednocześnie odpowiedzią na pytanie, czy p było spełnione w M\. □

19