Nierozstrzygalność logiki MSO+U; wspólne wyniki z M. Bojańczykiem, T. Gogaczem i M. Skrzypczakiem

Speaker(s)

Henryk Michalewski

Affiliation

Uniwersytet Warszawski

Date

Nov. 27, 2013, 4:15 p.m.

Room

room 5050

Seminar

Topology and Set Theory Seminar

---

Mówimy, że logika L nad modelem M jest rozstrzygalna, jeśli istnieje
algorytm, który dla każdego otrzymanego na wejściu zdania phi logiki L odpowiada TAK, jeśli phi zachodzi w modelu M i odpowiada NIE w przeciwnym przypadku.

Na najbliższym seminarium planuję przedstawić pewne znane z literatury
wyniki odnośnie rozstrzygalności logik. Mianowicie, planuję przekonywać, że logika jest rozstrzygalna, jeśli istnieje sensowny/prosty model obliczeń odpowiadający tej logice.  Jako przykład tego sposobu rozumowania dowiodę, że logika nad liczbami naturalnymi, w której można kwantyfikować po podzbiorach liczb naturalnych i w której dany jest predykat następnika, jest rozstrzygalna dzięki temu, że jest w odpowiedniości z pewnym modelem automatu.  Z drugiej strony wykażę, że podobna logika nad kwadratem liczb naturalnych z operacjami następnika po pierwszej i po drugiej współrzędnej, nie jest rozstrzygalna, gdyż można w niej wyrazić problem stopu. 

Wyżej wymieniony pozytywny wynik dla liczb naturalnych został
wzmocniony przez M.O. Rabina do wyniku o drzewach: rozstrzygalna jest
logika, w której można kwantyfikować po podzbiorach wraz z "drzewowym
następnikiem" (dla wierzchołka v w drzewie możemy mówić L(v),P(v) -
lewym i prawym następniku w drzewie binarnym).

Kwantyfikator U(X) przed formułą phi ze zmienną wolną X oznacza, że

\forall_{n\in\nat} \exists_{X,|X|>n} \phi(X)

M. Bojańczyk postawił pytanie, czy jeśli wzmocnimy logikę drzewową z tw.
Rabina o kwantyfikator U, to pozostaje ona rozstrzygalna. Przy
założeniu V=L wykażę, że pytanie to ma negatywną odpowiedź. Jest
to nieco zaskakujący, ale łatwy technicznie wniosek z wyniku S. Shelaha o nierozstrzygalności logiki monadycznej na liczbach rzeczywistych oraz przedstawionej niedawno przez Sz. Hummela i M. Skrzypczaka konstrukcji skomplikowanych zbiorów rzutowych uzyskanych za pomocą kwantyfikatora U.

---