Logika dla informatyków. Ćwiczenia z gwiazdką

• Wykaż, że każda funkcja boolowska o n zmiennych może być wyrażona formułą zdaniową, a każda funkcja monotoniczna może być wyrażona formułą używającej tylko koniunkcji i alternatywy.
• Lemat Craige'a o interpolacji (dla logiki zdaniowej). Niech alpha -> beta będzie tautologią rachunku zdań. Znaleźć formułę gamma, taką że alpha -> gamma oraz gamma -> beta są tautologiami, oraz gamma używa wyłącznie zmiennych używanych jednocześnie przez alpha i beta.
• Udowodnij, że przeliczalny zbiór formuł zdaniowych nad ustalonym skończonym zbiorem zmiennych jest spełnialny wttw, gdy każdy jego podzbiór jest spełnialny.
• Twierdzenie o zwartości (dla logiki zdaniowej). Przeliczalny zbiór formuł zdaniowych (nad przeliczalnym zbiorem zmiennych) jest spełnialny wttw, gdy każdy jego podzbiór jest spełnialny. Dowód z Lematu Koeniga.
• Udowodnij Lemat Koeniga za pomocą tw.o zwartości
• Wykaż, że graf nieskończony jest k-kolorowalny wttw gdy każdy jego skoczony podgraf jest k-kolorowalny.
• Wykaż, że każdy przeliczalny porządek częściowy można uzupełnić do porządku liniowego.
• Więcej zastosowań

• Napisac formule, ktora mowi, ze uniwersum ma moc n.
• Napisac formule, ktora dla kazdego n ma n nieizomorficznych modeli mocy n; 2^n nieizomorficznych modeli mocy n; n!; itp. (sygnatura do wyboru)
• Dla danej struktury A napisac formule, ktora mowi "Struktura jest izomorficzna z A".
• Pokaz, ze spektrami sa nastepujace zbiory: zbior liczb parzystych, zbior kwadratow, zbior liczb zlozonych, zbior poteg dwojki.

• Rozgrzewka: pokaz, ze klasa spektrow jest zamknieta na przeciecie i sume. Uwaga: zamkniecie na negacje jest slynnym problemem otwartym.
• Na poprzednich zajeciach pokazywalismy, ze spektrami sa nastepujace zbiory: liczby parzyste, kwadraty liczb naturalnych, liczby zlozone, potegi dwojki. A czy dopelnienia tych zbiorow sa spektrami? (Rozwiazanie: oczywiscie tak. Trzeba zaksjomatyzowac skonczone odcinki liczb naturalnych z pelna arytmetyka.)
• Na wykladzie bylo udowodnione, ze problem spelnialnosci dla logiki pierwszego rzedu jest nierozstrzygalny. Wykaz, ze problem staje sie rozstrzygalny (w NEXPTIME) jesli ograniczymy sie do formul postaci istnieje x_1, istnieje x_2, ... istnieje x_n, ze dla kazdego y_1, dla kazdego y_2, ... dla kazdego y_m psi(x_1,...,x_n, y_1, ..., y_m) , gdzie psi jest formula bez kwantyfikatorow i nie uzywa symboli funkcyjnych.

• Pokaz, ze klasa relacji rownowaznosci, ktorych skonczone klasy abstrakcji sa parzyste, nie jest definiowalna.
• Pokaz, ze klasa grafow, w ktorych par niepolaczonych jest tyle samo co polaczonych, nie jest aksjomatyzowalna.
• Pokazac, ze formula o randze kwantyfikatorowej m mozna zdefiniowac porzadek liniowy o dlugosci 2^m (z grubsza).
• Pokazac, ze formuly o randze m nie odrozniaja porzadkow o dlugosci wiekszej niz 2^m.
• Porzadki liniowe czy geste sa definiowalne. A porzadki dobre?

• Pokazac, ze 3-wymiarowa hiperkostke binarna mozna odroznic o 4-wymiarowej za pomoca formuly o randze 3, ale nie 2.
• Acyklicznosc i spojnosc nie jest definiowalna w obrebie grafow skonczonych.
• Rozstrzygalnosc FO z relacjami unarnymi (bez funkcji) i rownoscia.
• Nierozstrzygalnosc FO z choc jedna binarna relacja.
• To samo dla MSO.
• Rozstrzygalnosc spelnialnosci dla klasy Ackermanna bez rownosci (?).