Second order logic (SO) and monadic second order logic (MSO)

SO

Zad. 1

Pokazać, że dla każdego zdania \(\varphi\) logiki drugiego rzędu SO istnieje inne zdanie \(\varphi'\) tejże samej logiki takie, że
\(Spec(\varphi')=\mathbb{N}_+\setminus Spec(\varphi).\)

Dodatkowe informacje

\(\mathbb{N}_+\) oznacza zbiór liczb naturalnych dodatnich.

Odpowiedź na analogiczne pytanie dla FO jest dotąd nierozstrzygnięta. Wiadomo, że jest to równoważne znanemu otwartemu problemowi z teorii złożoności obliczeniowej.

Zad. 2

Pokazać, że odpowiednik twierdzenia o zwartości nie zachodzi dla logiki drugiego rzędu.

Zad. 3

Napisać zdanie \(\Pi^1_1\), czyli uniwersalnego fragmentu logiki drugiego rzędu, którego wszystkimi modelami są dokładnie struktury skończone.

Zad. 4

Spróbować naszkicowac dowód tw. Fagina, że \(\Sigma^1_1=NP\) nad słowami (było sformułowane na wykładzie).

Zad. 5

Rozważamy skończone grafy \(\mathfrak{G}\) (ta litera to gotyckie G, w rozwiązaniu można pisać zwykłe G) nad sygnaturą składającą się z jednego dwuargumentowego symbolu relacyjnego \(E\).

Napisać zdanie \(\varphi\) logiki drugiego rzędu postaci \(\exists R_{1}\ldots\exists R_{k}\psi(R_{1},\ldots,R_{k}),\) w którym \(\psi\) jest zdaniem pierwszego rzędu takie, że dla każdego skończonego grafu \(\mathfrak{G}\) zachodzi równoważność: \(\mathfrak{G}\models\varphi\) wtw \(\mathfrak{G}\) ma cykl Eulera.

MSO

Zad. 1

Na wykładzie podany został dowód, że dla każdego zdania \(\varphi\) logiki MSO istnieje automat, który akceptuje dokładnie te słowa, w których \(\varphi\) jest prawdziwe.

Oszacować, jaki jest stosunek rozmiaru minimalnego deterministycznego automatu do długości formuły.

Wskazówka 1

Nie bądźmy drobiazgowi w liczeniu stanów automatu. Wiadomo, że automat skończony, który akceptuje w ogóle jakieś słowo, akceptuje też słowo o długości nie większej niż swoja liczba stanów. Piszmy więc zdania, które mają modele-słowa, ale wyłącznie bardzo długie w porównaniu z długością zdania. Wtedy wiadomo będzie, że automat nie może mieć mniej stanów, niż długość najkótszego modelu-słowa.

Wskazówka 2

Rozmiar automatu rośnie szybciej niż każda funkcja postaci \(2^{2^{2^{\cdots^{2^n}}}}\).

Zad. 2

Udowodnić, że każde zdanie MSO nad słowami jest równoważne zdaniu z tylko jednym kwantyfikatorem egzystencjalnym po relacji unarnej, w dodatku umieszczonym na początku.

Przypomnienie

Konstrukcja z wykładu gwarantowała ciąg kwantyfikatorów egzystencjalnych po relacjach unarnych na początku.

Zad. 3

Skonstruować zdanie logiki MSO, które ma wyłącznie modele mocy co najmniej \(\mathfrak{c}\).

Wskazówka

Zakodować porządek ciągły.

Zad. 4

Skonstruować zdanie logiki MSO, które ma wyłącznie modele mocy co najmniej \(2^{\mathfrak{c}}\).

Wskazówka

Rozważyć, co wyraża (lekko niepoprawnie) zdanie \(\forall X\exists x\forall y X(y)\leftrightarrow E(x,y).\)

Zad. 5

Skonstruować zdanie logiki MSO, którego spektrum to zbiór wszystkich liczb pierwszych.

Zad. 6

Rozważamy skończone grafy nieskierowane \(\mathfrak{G}\) (ta litera to gotyckie G, w rozwiązaniu można pisać zwykłe G) nad sygnaturą składającą się z jednego dwuargumentowego symbolu relacyjnego \(E\).

Napisać zdanie \(\varphi\) logiki MSO postaci \(\forall R_1\ldots\forall R_k\psi(R_1,\ldots,R_k),\) w którym \(\psi\) jest zdaniem pierwszego rzędu takie, że dla każdego skończonego grafu \(\mathfrak{G}\) zachodzi równoważność: \(\mathfrak{G}\models\varphi\) wtw \(\mathfrak{G}\) jest grafem acyklicznym.

Zad. 7

Napisać zdanie MSO, którego wszystkie skończone modele to dokładnie te grafy, które są 3-kolorowalne.

Zad. 8

Rozważamy modele dla PDL postaci skończonego łańcucha złożonego z dwóch programów atomowych: \(u\) i \(v\). Między każdymi dwoma kolejnymi stanami przechodzi jeden i tylko jeden z tych programów. Zmienne zdaniowe są dwie: \(p\) prawdziwa tylko w pierwszym stanie łańcucha i \(k\) prawdziwa tylko w ostatnim stanie. Innych zmiennych zdaniowych nie ma.

Każdą taką strukturę można naturalnie uważać również za strukturę pierwszego rzędu, wówczas \(u\) i \(v\) są relacjami dwuargumentowymi a \(p\) i \(k\) relacjami jednoargumentowymi.

Udowodnić, że dla każdego zdania \(\varphi\) logiki MSO istnieje zdanie \(\phi\) logiki PDL takie, że dla każdej struktury \(\mathfrak{A}\) jak powyżej, \(\phi\) jest prawdziwe w stanie początkowym struktury \(\mathfrak{A}\) wtedy i tylko wtedy, gdy \(\mathfrak{A}\models\varphi\).