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.
Nie jesteś zalogowany |
