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$ .

Informatyka MIMUW