Zadanie 1.1. Zbiór słów W C A* nazywamy kodem jeśli każde słowo w € A* ma conajwyżej jeden rozkład w = wi ■ ■ • wn dla w\,... ,wn. Dla skończonego zbioru słów W napsiać w logica MSO(s) zdanie <fiw> które ma model wtedy i tylko wtedy gdy W jest kodem.
Zadanie 1.2. Pokazać, że dla każdej formuły MSO(s) istnieje równoważna (na słowach skończonych) formuła postaci 3Xip(X), gdzie ą>(X) jest formułą logiki pierwszego rzędu. Innymi słowy, wystarczy jeden kwan-tyfikator drugiego rzędu.
Zadanie 1.3. Formułę <p(x,y) nazwiemy linijką długości d, jeśli jest prawdziwa dokładnie wtedy, gdy odległość między x a y to d. Pokazać, że dla dowolnego n istnieje linijka długości większej niż 2n, która opisuje się formułą MSO(s) rozmiaru wielomianowego ze względu na n.
Zadanie 1.4. Uogólnić powyższe zadanie na funkcje podwójnie, potrójnie i więcej razy wykładnicze. Dokładniejszy opis poniżej. Niech expfc(n) będzie k-krotnie wykładniczą funkcją od n, czyli
exp0(n) = n expfc+1(n) = 2exp*(n).
Ustalmy k. Pokazać, że dla dowolnego n istnieje linijka długości większej niż expfc(n), która opisuje się formułą MSO(s) rozmiaru wielomianowego ze względu na n. Stałe i wykładnik wielomianu mogą zależeć od k.
Zadanie 1.5. Korzystając z linijki w poprzednim zadaniu udowodnić, że nie istnieje algorytm rozstrzygający spełnialność dla MSO(s) na słowach skończonych, który by działał w czasie wykładniczym, czy też podwójnie wykładniczym, potrójnie wykładniczym, itd.
Zadanie 1.6. Dodajmy do sygnatury relację x = y + z. Pokazać, że spełnialność MSO(s,+) na słowach skończonych jest nierozstrzygalna.
Zadanie 1.7. Napisać formuły FOL (logiki pierwszego rzędu) definiujące następujące własności: a istnieje dokładnie k elementów w uniwersum, b pomiędzy wierzchołkami u, v istnieje ścieżka długości < k, c w uniwersum nie ma cyklu długości k,
Czy można napisać także formuły definiujące następujące własności (na pierwszy rzut oka prostsze wersje podpunktów wyżej)?
a’ uniwersum ma parzyście wiele elementów, b’ istnieje ścieżka między wierzchołkami u i v, c’ w uniwersum nie istnieje cykl.