7738996302

Klasycznym przykładem zastosowania powyższej metody, jest dowód, że teoria MSO jest rozstrzygalna w liczbach całkowitych z następnikiem. Możemy mianowicie interpretować liczby całkowite w liczbach naturalnych, z włożeniem

{0    dla k = 0

2 k    dla k > 0

-2k - 1 dla k < 0

Odpowiednie formuły dla relacji następnika i zera można podać jako proste ćwiczenie.

Zdefiniowane powyżej interpretacje nazywane są też interpretacjami typu element-element. Znajdują one zastosowanie dla wszystkich logik nad sygnaturami relacyjnymi. Możemy jednak ograniczyć stosowalność do szczególnych logik i rozszerzyć pojęcie interpretacji.

Definicja 5. Powiemy, że model M\ interpretuje się w Mi typu element-zbiór, jeśli istnieje włożenie i : |Mi| —* 2^^Ma< oraz formuły monadyczne p(X) i ipn analogicznie jak w zwykłych interpretacjach.

Dzięki powyższej definicji możemy przenosić rozstrzygalność teorii MSO w M% na rozstrzygalność FO w Mi- Ciekawy przykład wykorzystania tej metody, to interpretacja liczb naturalnych z dodawaniem w liczbach naturalnych z następnikiem, metodą element-zbiór. Główną ideą jest kodowanie binar ne, zaczynając od końca. Implikuje to rozstrzygalność logiki pierwszego rzędu dla arytmetyki Presburgera.

20