Logika dla informatyków/Logika drugiego rzędu

Logika drugiego rzędu

Składnię logiki drugiego uzyskujemy przez rozszerzenie zbioru reguł składniowych dla logiki pierwszego rzędu o kwantyfikatory wiążące symbole relacyjne. Z przyczyn technicznych tym razem wygodnie nam będzie przyjąć, że podstawowymi spójnikami logicznymi są $\mathrm{\neg },\vee$ i $\mathrm{\exists }$.

Definicja 12.1

Definicja formuł drugiego rzędu jest indukcyjna, podobnie jak analogiczna Definicja 2.5 dla logiki pierwszego rzędu. Jednak tym razem nie ustalamy sygnatury z góry.

• Każda formuła atomowa nad sygnaturą $\mathrm{\Sigma }$ jest formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$.
• Jeśli $\phi ,\psi$ są formułami drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$, to $\phi \vee \psi$ jest też formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$.
• Jeśli $\phi$ jest formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$, to $\mathrm{\neg }\phi$ jest też formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$.
• Jeśli $\phi$ jest formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$ a Parser nie mógł rozpoznać (nieznana funkcja „\ZI”): {\displaystyle \displaystyle x\in\ZI} jest zmienną indywiduową, to $\mathrm{\exists }x\phi$ jest też formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$.
• Jeśli $\phi$ jest formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }$, a $R$ jest symbolem relacji $k$-argumentowej z $\mathrm{\Sigma },$ to $\mathrm{\exists }R\phi$ jest formułą drugiego rzędu nad sygnaturą $\mathrm{\Sigma }-\{R\}.$

Definicja semantyki jest też podobna jak dla logiki pierwszego rzędu.

• Znaczenie formuł atomowych jest identyczne jak w logice pierwszego rzędu.
• Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle (\mathfrak{A},\varrho)\vDash\varphi\vee\psi}} , gdy zachodzi $(\mathfrak{𝔄},\varrho )\models \phi$ lub zachodzi $(\mathfrak{𝔄},\varrho )\models \psi$.
• $(\mathfrak{𝔄},\varrho )\models \mathrm{\neg }\phi$, gdy nie zachodzi $(\mathfrak{𝔄},\varrho )\models \phi$.
• $(\mathfrak{𝔄},\varrho )\models \mathrm{\exists }x\phi$ wtedy i tylko wtedy, gdy istnieje takie $a\in A$, że zachodzi $(\mathfrak{𝔄},{\varrho }_x^a)\models \phi$.
• Jeśli $\mathfrak{𝔄}=⟨A,R_1,\dots ,f_1,\dots ⟩$ jest strukturą sygnatury $\mathrm{\Sigma }-\{R\}$ oraz $\varrho$ jest wartościowaniem w tej strukturze, to $(\mathfrak{𝔄},\varrho )\models \mathrm{\exists }R\phi$ wtedy i tylko wtedy gdy istnieje struktura ${\mathfrak{𝔄}}^{\prime }$ nad sygnaturą $\mathrm{\Sigma }$ o postaci $⟨A,R,R_1,\dots ,f_1\dots ⟩$ spełniająca $(\mathfrak{𝔄},\varrho )\models \phi .$

Dualny kwantyfikator drugiego rzędu $\mathrm{\forall }$ wprowadzamy jako skrót notacyjny:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \forall R\varphi \hspace{4cm} } oznacza $\mathrm{\neg }\mathrm{\exists }R\mathrm{\neg }\phi .$

Nieaksjomatyzowalność logiki drugiego rzędu

Spójrzmy na następujący przykład zdania $Ind$ nad sygnaturą arytmetyki:

$\mathrm{\forall }R(R(0)\wedge \mathrm{\forall }n(R(n)\to R(s(n)))\to \mathrm{\forall }nR(n)).$

Orzeka ono, że każda relacja jednoargumentowa (czy podzbiór uniwersum), która zawiera $0$ i jest zamknięta ze względu na operację następnika, zawiera wszystkie elementy uniwersum. Jest to wyrażona w języku drugiego rzędu zasada indukcji matematycznej. Twierdzenie Dedekinda orzeka, że po dołożeniu tego aksjomatu do zwykłych aksjomatów arytmetyki Peano PA (z których można wtedy usunąć dotychczasowy schemat aksjomatu indukcji), otrzymujemy aksjomatyzację kategoryczną, czyli taką, która ma z dokładnością do izomorfizmu tylko jeden model $\mathfrak{𝔑}---$ ten standardowy. Zauważmy przy okazji, że przykład ten wskazuje, iż dla logiki drugiego rzędu nie zachodzi górne twierdzenie Skolema-Lowenheima.

Wracając do poprzedniego przykładu, widzimy, że zbiór wszystkich zdań $\phi$ logiki pierwszego rzędu, dla których $PA\cup \{Ind\}\models \phi$, jest tożsamy z Parser nie mógł rozpoznać (nieznana funkcja „\strN”): {\displaystyle \displaystyle {\bf Th}(\strN)} . Możemy teraz udowodnić, że w odróżnieniu od logiki pierwszego rzędu,

Twierdzenie

Logika drugiego rzędu nie ma żadnego pełnego i poprawnego systemu dowodowego.

Dowód

Zbiór konsekwencji semantycznych Parser nie mógł rozpoznać (nieznana funkcja „\strN”): {\displaystyle \displaystyle \{\varphi~|~PA\cup\{Ind\}\models\varphi\}={\bf Th}(\strN)} nie jest nawet rekurencyjnie przeliczalny, na mocy Wniosku Uzupelnic przescieradlo|. Tymczasem dla każdego poprawnego systemu dowodzenia $X$ dla logiki drugiego rzędu, zbiór formuł wyprowadzalnych z rekurencyjnego zbioru $PA\cup \{Ind\}$ jest rekurencyjnie przeliczalny.

Widzimy teraz jasno, że logika drugiego rzędu jest niezwykle skomplikowana w badaniu, gdyż właściwie żadne z pożytecznych twierdzeń dotyczących logiki pierwszego rzędu nie zachodzi dla logiki drugiego rzędu. Jedynym, co zostaje, to odpowiednia modyfikacja gier Ehrenfeuchta i metoda Fra{}sse. Jednak ich praktyczna użyteczność jest również znikoma wobec ich złożoności. Np.w grze muszą występować rundy, w których gracze wybierają i zaznaczają całe relacje na uniwersum obu struktur. Jednak dla bardzo ograniczonych syntaktycznie fragmentów logiki drugiego rzędu możliwym staje się zapanowanie nad strategiami w odpowiadających im uproszczonych wersjach gry. Tymi właśnie metodami udowodniono kilka twierdzeń o niemożności zdefiniowania w różnych fragmentach logiki drugiego rzędu różnych konkretnych własności.

W dalszym ciągu tego rozdziału dowiemy się, jaki jest stopień trudności pytań o wyrażalność bądĽ niewyrażalność różnych własności w logice drugiego rzędu.

Równoważność logiki MSO i automatów skończonych

W zastosowaniach często spotyka się różne fragmenty logiki drugiego rzędu, która w całości dla wielu zastosowań jest zbyt silna. W tym rozdziale będziemy zajmowali się monadyczną logiką drugiego rzędu, która jest fragmentem logiki drugiego rzędu, powstałym przez ograniczenie kwantyfikacji drugiego rzędu tylko do relacji jednoargumentowych (czyli zbiorów). Na oznaczenie tej logiki powszechnie stosuje się skrót MSO (od Monadic Second Order).

MSO jest logiką bardzo często pojawiającą się w związku z informatyką. Tutaj zaprezentujemy klasyczny wynik, łączący tę logikę z teorią automatów skończonych.

Niech ${\mathrm{\Sigma }}_n$ będzie sygnaturą złożoną z symboli $\le ,X_1,\dots ,X_n$, w której wszystkie symbole relacyjne $X_i$ są jednoargumentowe.

Definicja

Model sygnatury ${\mathrm{\Sigma }}_n$ nazwiemy modelem-słowem gdy jego nośnikiem jest skończony odcinek początkowy zbioru liczb naturalnych a interpretacją symbolu $\le$ jest naturalny liniowy porządek liczb. Zbiór modeli-słów nad ${\mathrm{\Sigma }}_n$ będziemy oznaczać $W_n$.

Skorzystamy też tutaj z naturalnej wzajemnie jednoznacznej odpowiedniości pomiędzy modelami-słowami a niepustymi słowami nad alfabetem $A_n=\{0,1{\}}^n$: słowu $w\in A_n^{+}$ odpowiada model Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \strA(w)\in W_n} o mocy równej długości $w,$ a jego element $k$ należy do interpretacji relacji $X_i$ wtedy i tylko wtedy, gdy $k$-ta litera słowa $w$ jest ciągiem zerojedynkowym, który ma jedynkę na pozycji $i$.

Odtąd będziemy momentami umyślnie zacierali rozróżnienie pomiędzy słowami a odpowiadającymi im modelami-słowami. Zbiór Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \{\strA\in W_n~|~\strA\models\varphi\}} można więc naturalnie uważać za język słów nad $A_n$.

Sformułowane przez nas twierdzenie stosuje się wprost tylko do alfabetów o mocy postaci $2^n$. Ponieważ jednak każdy język regularny można traktować (po odpowiednim zakodowaniu) jako język nad takim właśnie alfabetem, z którego nie wszystkie litery są wykorzystywane, ograniczenie to nie narusza ogólności naszych rozważań.

Twierdzenie Buchi, Elgot

Dla każdego zdania $\phi$ monadycznej logiki drugiego rzędu zbiór Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \{w\in A_n^+~|~\strA(w)\models\varphi\}} jest regularny, oraz dla każdego języka regularnego $L$ nad $A_n$ istnieje takie zdanie $\phi$ logiki { MSO}, że

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \{w\in A_n^+~|~\strA(w)\models\varphi\}=L-\{\epsilon\}.}

Czasami treść tego twierdzenia wyraża się sloganem $\mathrm{M}\mathrm{S}\mathrm{O}=Reg.$

W myśl tego twierdzenia, MSO można traktować jako jeszcze jeden formalizm służący definiowaniu (niepustych) języków regularnych, oprócz powszechnie znanych wyrażeń regularnych, automatów skończonych i gramatyk regularnych.

Dowód

Zaczniemy od prostszej drugiej części twierdzenia. Niech $M=⟨Q,A_n,q_0,\mathrm{\Delta },F⟩$ będzie automatem skończonym rozpoznającym $L$, gdzie $Q$ to zbiór stanów, $q_0\in Q$ to stan początkowy, $F\subseteq Q$ to zbiór stanów akceptujących a $\mathrm{\Delta }\subseteq Q\times A_n\times Q$ to relacja przejścia. Niech $Q=\{q_1,\dots ,q_{\ell }\}.$ Chcemy wyrazić za pomocą zdania MSO, że istnieje akceptujące obliczenie $M$ na danym słowie.

Stanom $M$ będą odpowiadały dodatkowe symbole relacji jednoargumentowych $X_{n+1},\dots ,X_{n+\ell }.$ Początkowo będziemy więc mieli do czynienia z modelami-słowami nad większą sygnaturą ${\mathrm{\Sigma }}_{n+\ell }$. Modele te mają odpowiadać obliczeniom $M$ na właściwym słowie wejściowym.

Formuła ${\phi }_1$ postaci Parser nie mógł rozpoznać (nieznana funkcja „\Land”): {\displaystyle \displaystyle \forall x(\Land_{n<i\neq j\leq n+\ell}\lnot (X_i(x)\land X_j(x))\land\Lor_{i=n+1}^{n+\ell}X_i(x))} mówi o danym słowie, że w każdym kroku obliczenia automat był w jednym i tylko jednym stanie.

Formuła ${\phi }_2$ postaci $\mathrm{\exists }x\mathrm{\forall }y(x\le y\wedge X_{n+1}(x))$ mówi, że w momencie rozpoczęcia obliczenia automat był w stanie początkowym.

Formuła ${\phi }_3$ postaci Parser nie mógł rozpoznać (nieznana funkcja „\Lor”): {\displaystyle \displaystyle \exists x\forall y(y\leq x \land \Lor_{q_i\in F}X_{n+i}(x))} mówi, że w momencie zakończenia obliczenia automat był w jednym ze stanów akceptujących.

Formuła ${\phi }_4$ jest postaci Parser nie mógł rozpoznać (nieznana funkcja „\Lor”): {\displaystyle \displaystyle \forall x\forall y (\lnot\exists z( x<z\land z< y)\to \Lor_{\langle q_i,\vec{a},q_k\rangle\in \Delta}X_{n+i}(x)\land\psi_{\vec{a}}(x)\land X_{n+k}(y))} , gdzie $\overrightarrow{a}=a_1\dots a_n$ jest literą z $A_n$, zaś ${\psi }_{\overrightarrow{a}}(x)$ jest formułą Parser nie mógł rozpoznać (nieznana funkcja „\Land”): {\displaystyle \displaystyle \Land_{\{i~|~a_i=1\}}X_i(x)\land \Land_{\{i~|~a_i=0\}}\lnot X_i(x)} . Formuła ta mówi, że dla każdych dwóch bezpośrednio po sobie następujących pozycji w słowie, przejście pomiędy nimi odbyło się zgodnie z jedną z możliwości dostępnych w relacji przejścia automatu $M.$

Teraz zdanie

$\mathrm{\exists }{X}_{n+1}\dots X_{n+\ell }({\phi }_1\wedge {\phi }_2\wedge {\phi }_3\wedge {\phi }_4)$

orzeka, że istnieje akceptujące obliczenie automatu $M$ na danym słowie.

Przechodzimy teraz do dowodu pierwszej części. Tym razem dla danego zdania MSO musimy skonstruować automat skończony, który akceptuje dokładnie te słowa nad $A_n$, w których to zdanie jest prawdziwe.

W pierwszym kroku zastąpimy MSO przez trochę inną logikę, którą nazwiemy ${\mathrm{M}\mathrm{S}\mathrm{O}}_0$. Pokażemy, że jej formuły definiują wszystkie języki modeli-słów, które można zdefiniować w MSO.

Specyficzną cechą ${\mathrm{M}\mathrm{S}\mathrm{O}}_0$ jest to, że nie ma w niej zmiennych indywiduowych (czyli tych, których wartościami są elementy) ani wiążących je kwantyfikatorów, a tylko symbole relacji i kwantyfikatory drugiego rzędu. Natomiast jest znacznie więcej formuł atomowych.

Oto definicja składni i jednocześnie semantyki ${\mathrm{M}\mathrm{S}\mathrm{O}}_0$ -- oczywiście indukcyjna. Wobec braku zmiennych pierwszego rzędu w definicji semantyki nie występuje wartościowanie.

• Formuła atomowa $X_i\subseteq X_j$ jest prawdziwa w modelu Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \strA\in W_n} gdy relacja $X_i$ jest zawarta w relacji $X_j$.
• Formuła atomowa $Singl(X_i)$ jest prawdziwa w modelu Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \strA\in W_n} gdy relacja $X_i$ jest singletonem (to właśnie kwantyfikowaniem

 po relacjach, które są singletonami zastąpimy kwantyfikację po
 elementach obecną w MSO).

• Formuła atomowa $LessEq(X_i,X_j)$ jest prawdziwa w modelu Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \strA\in W_n} , gdy wszystkie elementy w relacji $X_i$ są mniejsze bądĽ równe

 od wszystkich elementów w relacji $X_j.$

• Jeśli $\phi ,\psi$ są formułami ${\mathrm{M}\mathrm{S}\mathrm{O}}_0$ a $X_i$ jest

 symbolem relacyjnym, to formułami są także Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \varphi\lor\psi,\   \lnot\varphi}
 i $\mathrm{\exists }{X}_i\phi ,$ których semantyka jest
 standardowa.

Tłumaczenie danego zdania $\phi$ z MSO nad ${\mathrm{\Sigma }}_n$ na równoważne mu w $W_n$ zdanie $\tilde{\phi }$ w ${\mathrm{M}\mathrm{S}\mathrm{O}}_0$ definiuje się następująco. Po pierwsze, zamieniamy nazwy związanych zmiennych pierwszego rzędu tak, że zmienna wiązana przez każdy kwantyfikator jest inna. Bez utraty ogólności możemy założyć, że są to zmienne $x_1,\dots ,x_{\ell }.$ Teraz wszystkim zmiennym występującym w $\phi$ przypisujemy dodatkowe, nowe symbole relacji, powiedzmy, że zmiennej $x_i$ przypisujemy $X_{n+i}$.

• $\widetilde{X_i(x_j)}$ to $X_{n+j}\subseteq X_i$.
• $\widetilde{(x_i=x_j)}$ to $X_{n+i}\subseteq X_{n+j}\wedge X_{n+j}\subseteq X_{n+i}.$
• $\widetilde{(x_i\le x_j)}$ to

$LessEq(X_{n+i},X_{n+j}).$

• $\widetilde{(\phi \vee \psi )}$ ma postać

$\tilde{\phi }\vee \tilde{\psi }$.

• $\widetilde{(\mathrm{\neg }\phi )}$ ma postać $\mathrm{\neg }\tilde{\phi }$.
• Formułę $\widetilde{(\mathrm{\exists }{x}_i\phi )}$ definiujemy jako $\mathrm{\exists }{X}_{n+i}(Singl(X_{n+i})\wedge \tilde{\phi }).$
• Formułę $\widetilde{(\mathrm{\exists }{X}_i\phi )}$ dla $i\le n$ definiujemy jako

 $\mathrm{\exists }{X}_i\tilde{\phi }.$

Przez indukcję  budowę $\phi$ udowodnimy teraz, że

Dla każdego modelu-słowa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<A,X_1,\dots,X_n\>}
 i każdych

$a_1,\dots ,a_{\ell }$ z jego nośnika, następujące warunki są równoważne:

• Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle (\<A,X_1,\dots,X_n\>,x_1:a_1,\dots,x_\ell:a_\ell)\models\varphi}
• Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \<A,X_1,\dots,X_n,\{a_1\},\dots,\{a_\ell\}\>\models\widetilde\varphi}

Wszystkie kroki indukcji sa całkowicie standardowe i pozostawiamy je Czytelnikowi.

Zatem istotnie, każdy zbiór słów-modeli, który można zdefiniować zdaniem MSO można też zdefiniować zdaniem ${\mathrm{M}\mathrm{S}\mathrm{O}}_0$. Teraz dla takiego zdania pozostaje skonstruować automat skończony, który akceptuje dokładnie te słowa nad $A$, w których to zdanie jest prawdziwe.

Sprawa jest teraz dużo łatwiejsza niż dla oryginalnego MSO, bo każda formuła ${\mathrm{M}\mathrm{S}\mathrm{O}}_0$ definiuje jakiś język nad $A_{n+k}$.

Sprawdzenie, że formuły atomowe definiują języki regularne, pozostawiamy Czytelnikowi jako ćwiczenie.

Język definiowany przez $\phi \vee \psi$ jest sumą języków definiowanych przez $\phi$ i $\psi$, czyli jako suma języków regularnych sam jest regularny.

Język definiowany przez $\mathrm{\neg }\phi$ jest dopełnieniem regularnego języka definiowanego przez $\phi$, czyli sam też jest regularny.

W wypadku formuły $\mathrm{\exists }{X}_i\phi$, o której zakłądamy, że $i$ jest najwyższym indeksem symbolu relacyjnego występującego w $\phi ,$ bierzemy automat rozpoznający język nad $A_i$ definiowany przez $\phi .$ Następnie modyfikujemy go tak, by działał nad alfabetem $A_{i-1}$, przy każdym przejściu niedeterministycznie zgadując, czy $i$-tą współrzędną litery z alfabetu $A_i$ znajdującej się w tej komórce taśmy jest 1 czy 0.

Twierdzenie Buchi ma daleko idące konsekwencje dla rozstrzygalności wielu interesujących problemów.

Wniosek

Następujące problemy są rozstrzygalne:

• Czy istnieje model-słowo, w którym dane zdanie $\phi$ z MSO

 jest prawdziwe?

• Czy dane zdanie $\phi$ z MSO jest prawdziwe w każdym

 modelu-słowie?

Dowód

Procedura rozstrzygająca oba problemy polega na przetworzeniu formuły $\phi$ w równoważny jej automat skończony (np.w sposób opisany w dowodzie poprzedniego twierdzenia), a następnie przeprowadzeniu testu na automacie.

Informacja o tw. Fagina i Stockmeyera

Naturalne jest pytanie, czy można równie elegancko, jak to zrobił Buchi, scharakteryzować zbiory modeli definiowalnych w pełnej logice drugiego rzędu. OdpowiedĽ na to pytanie pojawiła się w dwóch krokach.

W pierwszej charakteryzacji występuje egzystencjalna logika drugiego rzędu, czasami oznaczana symbolem ${\mathrm{\Sigma }}_1^1,$ czyli zbiór tych formuł pełnej logiki drugiego rzędu, w których wszystkie kwantyfikatory drugiego rzędu wystepują na początku formuły, a za nimi jest już tylko zwykłe zdanie pierwszego rzędu:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \exists X_1~\dots \exists X_n \hspace{-4mm}\underbrace{\varphi(X_1\dots X_n)}_{\text{zdanie pierwszego rzędu}}.}

Dla tej logiki sytuacja wygląda następująco:

Twierdzenie Fagin

Dla każdego zdania $\phi$ egzystencjalnej logiki drugiego rzędu zbiór Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \{w\in A_n^+~|~\strA(w)\models\varphi\}} należy do { NP}, oraz dla każdego języka $L\in \mathrm{N}\mathrm{P}$ istnieje zdanie $\phi$ egzystencjalnej logiki drugiego rzędu takie, że

Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \displaystyle \{w\in A_n^+~|~\strA(w)\models\varphi\}=L-\{\epsilon\}.}

Podobnie jak twierdzenie Buchi i Elgota, ono też bywa reprezentowane sloganem ${\mathrm{\Sigma }}_1^1=\mathrm{N}\mathrm{P}.$

Oczywiście { NP} to słynna klasa złożoności probelmów rozstrzyganych przez niedeterministyczne maszyny Turinga o wielomianowej złożoności czasowej.

Pełna logika drugiego rzędu, oznaczona tu przez SO, też ma analogiczną charakteryzację, która w postaci sloganu wyraża się przez $\mathrm{S}\mathrm{O}=\mathrm{P}\mathrm{H}$ i została udowodniona przez Stockmeyera. Precyzyjna postać tego twierdzenia jest analogiczna do poprzednich, a PH to hierarchia wielomianowa, również doskonale znana z teorii złożoności.

Przed przejściem do następnego tematu wypada zauważyć, że twierdzenia Fagina i Stockmeyera w istocie obowiązują w zakresie szerszym niż tylko dla modeli-słów. Dotyczą one także dowolnych struktur skończonych, o ile założy się odpowiednio rozsądny sposób opisywania ich we wzajemnie jednoznaczny sposób za pomocą słów.

Po poznaniu twierdzeń Fagina i Stockmeyera lepiej rozumiemy trudności badania logiki drugiego rzędu. Jest to zadanie co najmniej równie niełatwe, jak najtrudniejsze pytania teorii złożoności, z którymi uczeni borykają się od kilkudziesięciu lat, jak dotychczas bezskutecznie. Np.dowód, że każdy zbiór słów, który jest definiowalny formułą logiki drugiego rzędu, jest też definiowalny formułą ${\mathrm{\Sigma }}_1^1$, implikowałby natychmiast, że $\mathrm{N}\mathrm{P}=\mathrm{P}\mathrm{H},$ a zatem także $\mathrm{N}\mathrm{P}=\mathrm{c}\mathrm{o}\mathrm{N}\mathrm{P}$. Zauważmy przy tym, że każdy zbiór słów, który jest definiowalny w MSO, jest też definiowalny za pomocą formuły która należy jednocześnie do MSO i ${\mathrm{\Sigma }}_1^1$. Wynika to z postaci formuły definiującej zbiory regularne, która pojawia się w dowodzie twierdzenia Buchi. Zatem na poziomie kwantyfikacji wyłącznie po relacjach jednoargumentowych, pożądana równość zachodzi. Jednak przejście do relacji o dowolnej liczbie argumentów wydaje się niezmiernie trudne.

Informacja o tw. Rabina

Twierdzenie Rabina to inne, daleko idące uogólnienie twierdzenia Buchi.

Nieskończone pełne drzewo binarne to struktura Parser nie mógł rozpoznać (nieznana funkcja „\strT”): {\displaystyle \displaystyle \strT} nad sygnaturą $=,s_0,s_1,$ w której $s_0$ i $s_1$ to symbole jednoargumentowych funkcji. Nośnik Parser nie mógł rozpoznać (nieznana funkcja „\strT”): {\displaystyle \displaystyle \strT} to zbiór $\{0,1{\}}^{*}$ skończonych słów zerojedynkowych, a funkcje są określone przez równości $s_0(w)=w0$ oraz $s_1(w)=w1.$

Twierdzenie Rabin

Zbiór zdań logiki MSO, które są prawdziwe w Parser nie mógł rozpoznać (nieznana funkcja „\strT”): {\displaystyle \displaystyle \strT} jest rozstrzygalny.

Wszystkie znane dowody twierdzenia Rabina opierają się na tym samym pomyśle, który poznaliśmy w dowodzie twierdzenia Buchi: formuły logiki MSO są tłumaczone na równoważne im automaty w taki sposób, że formuła jest prawdziwa w drzewie Parser nie mógł rozpoznać (nieznana funkcja „\strT”): {\displaystyle \displaystyle \strT} (poetykietowanym dodatkowymi symbolami w wierzchołkach) wtedy i tylko wtedy, gdy automat akceptuje to drzewo. Szczegóły tych dowodów są zawsze bardzo skomplikowane. Nagrodą jest za to wynik, który jest jednym z najsilniejszych znanych twierdzeń o rozstrzygalności, nie tylko zresztą w logice. Rozstrzygalność wielu innych problemów decyzyjnych wykazano po raz pierwszy przez ich odpowiednie przetłumaczenie (czyli zredukowanie) na pytanie o prawdziwość zdań MSO w nieskończonym drzewie binarnym.