Logika dla informatyków/Teoria modeli

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

W tym rozdziale poznamy podstawowe fakty z teorii modeli. Większość znich to wnioski z twierdzenia o pełności.

Zaczniemy od twierdzenia o zwartości.

Twierdzenie 8.1 (o zwartości)

  1. Dla dowolnego zbioru formuł i dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} , to istnieje skończony podzbiór taki, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\models\var\varphi} .
  2. Dla dowolnego zbioru formuł , jeśli każdy skończony podzbiór jest spełnialny, to też jest spełnialny.


Dowód

W części pierwszej, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} , to z twierdzenia o pełności wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} . W dowodzie występuje tylko skończenie wiele formuł z . Jeśli jest zbiorem wszystkich tych formuł, to oczywiścieParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\vdash_H\var\varphi} . Z twierdzenia o poprawności wynika, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\models\var\varphi} .

Część druga wynika z części pierwszej, gdy przyjmiemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi=\bot} . Niespełnialność zbioru to bowiem to samo, co .

End of proof.gif


Pierwszym ważnym przykładem zastosowania twierdzenia o zwartości jest dowód innego ważnego twierdzenia teorii modeli.

Twierdzenie 8.2 (Skolem, Löwenheim, Tarski)


Jeśli zbiór formuł nad ma model nieskończony, to ma także model każdej mocy gdzie to moc sygnatury .

Dowód

Niech będzie zbiorem nowych symboli stałych, dotychczas niewystępujących w , którego moc wynosi . Niech oraz różne od }.

Ten nowy zbiór formuł nad nową sygnaturą jest spełnialny. Aby się o tym przekonać, weźmy dowolny skończony podzbiór oraz nieskończony model zbioru (o którego istnieniu wiemy z założeń). Zinterpretujmy w skończenie wiele symboli z , które występują w , jako dowolnie wybrane, różne elementy. Jest oczywiste, że określony w ten sposób model  spełnia . Zatem na mocy twierdzenia o zwartości, istotnie też ma model.

Wynika stąd, że jest zbiorem niesprzecznym. Stosując do niego twierdzenie o istnieniu modelu, otrzymujemy model o mocy nie przekraczającej mocy zbioru wszystkich formuł logiki pierwszego rzędu nad , która wynosi , ale jednocześnienie mniejszej niż , bo wszystkie stałe z muszą być w nim zinterpretowane jako różne elementy.

Jeśli teraz w modelu zignorujemy interpretację stałych z to otrzymamy -strukturę mocy , która jest modelem zbioru 

End of proof.gif


Wniosek 8.3

Żadna struktura nieskończona nie daje się opisać zbiorem zdań logiki pierwszego rzędu z dokładnością do izomorfizmu. Dokładniej, nie istnieje zbiór zdań logiki pierwszego rzędu, który ma model nieskończony i zarazem dla każdej struktury spełniającej zachodzi

.


Historycznie rzecz biorąc, twierdzenie Skolema-Löwenheima-Tarskiego jest następcą dwóch słabszych i starszych twierdzeń, które zresztą nadal są przywoływane. Zatem dla pełności informacji formułujemy je poniżej.

Twierdzenie 8.4 (Dolne twierdzenie Skolema-Löwenheima)

Każdy spełnialny zbiór zdań nad ma model o mocy nie większej niż moc zbioru formuł logiki pierwszego rzędu nad 

Twierdzenie 8.5 (Górne twierdzenie Skolema-Löwenheima)

Jeśli zbiór zdań nad ma model nieskończony, to dla każdego ma model o mocy nie mniejszej niż .

Najstarszym protoplastą tej grupy twierdzeń było po prostu

Twierdzenie 8.6 (Skolema-Löwenheima

Każda nieskończona struktura nad co najwyżej przeliczalną sygnaturą zawiera co najwyżej przeliczalną podstrukturę, elementarnie równoważną z .

W tym sformułowaniu twierdzenie to daje się udowodnić bez odwołania do twierdzeń o pełności i o istnieniu modelu i było znane wcześniej od nich.

Wywołało ono kiedyś potężny ferment w dziedzinie logiki: jak to jest możliwe, że teoria mnogości ma przeliczalny model, gdy skądinąd musi on zawierać zbiory nieprzeliczalne, jak np. Parser nie mógł rozpoznać (nieznana funkcja „\pot”): {\displaystyle \pot{\mathbb N}} ? Oczywiście nikt wolał głośno nie wypowiadać drugiej ewentualności: że teoria mnogości nie ma żadnego modelu i jest po prostu sprzeczna. Nic więc dziwnego,że to twierdzenie było znane początkowo jako Paradoks Skolema. Na szczęście staranna analiza wskazuje, że nie mamy tu jednak do czynienia z antynomią. Otóż jeśli mamy przeliczalny model teorii mnogości, to wszystkie zbiory do niego należące oglądane z zewnątrz są przeliczalne. Jednak dla niektórych z nich, np. dla interpretacji P(), żadna funkcja z interpretacji zbioru liczb naturalnych na interpretację P() sama nie jest elementem tego modelu. To już wystarcza, aby spełniał on zdanie mówiące, że P() jest nieprzeliczalny.

Tradycyjnie o wszystkich twierdzeniach z powyższej grupy mówi się "twierdzenie Skolema-Löwenheima".


Twierdzenie o zwartości i twierdzeń Skolema-Löwenheima często używa się do tego, by wykazać istnienie różnych nietypowych modeli. Jeśli przypomnimy sobie elementarną równoważność , wyprowadzoną jako wniosek z Twierdzenia 4.13, to rozpoznamy w niej również potencjalny efekt zastosowania (dolnego) twierdzenia Skolema-Löwenheima.

Klasycznym przykładem zastosowania twierdzenia o zwartości jest poniższy fakt:

Twierdzenie 8.7

Jeśli zbiór zdań ma modele skończone dowolnie dużej mocy, to ma też model nieskończony.

Dowód

Przypuśćmy, że ma modele skończone dowolnie dużej mocy.

Niech Parser nie mógł rozpoznać (błąd składni): {\displaystyle \bar\Delta=\Delta\cup\{ (\exists x_1\dots\exists x_n\bigwedge_{i<j}x_i\neq x_j)&nbsp;|&nbsp;n\in\mathbb N\}} . Oczywiście Parser nie mógł rozpoznać (nieznana funkcja „\neqx”): {\displaystyle \bigwedge_{i<j}x_i\neqx_j} oznacza koniunkcję wszystkich formuł postaci , w których

Zbiór jest spełnialny, bo każdy jego skończony podzbiór jest spełnialny. Istotnie, modelem jest każdy model mocy co najmniej Parser nie mógł rozpoznać (nieznana funkcja „\neqx”): {\displaystyle max\{n | (\exists x_1\dots\exists x_n \bigwedge_{i<j}x_i\neqx_j) \in\bar\Delta_0\}} . Na mocy twierdzenia o zwartości jest też spełnialny. Ma on wyłącznie modele nieskończone, a każdy jego model jest też modelem dla

End of proof.gif

Twierdzenie o zwartości może też służyć do dowodzenia niewyrażalności pewnych pojęć w logice pierwszego rzędu. Posłużymy się tu następującym przykładem.

Twierdzenie 8.8

Pojęcie dobrego porządku nie jest wyrażalne w logice pierwszego rzędu.Dokładniej, dla każdego zbioru formuł pierwszego rzędu nadsygnaturą takiego, że każdy dobry porządek jest modelem , istnieje też struktura nie będąca dobrym porządkiem taka, że

Dowód

Niech zbiór zdań ma tę właściwość, że każdy dobry porządek jest jego modelem. Bez utraty ogólności możemy założyć, że zawiera już zwykłe aksjomaty liniowych porządków. Niech będzie zbiorem nowych stałych.

Niech . Każdy skończony podzbiór jest spełnialny, np. w zbiorze , w którym każda stała występująca w jest interpretowana jako , zaś pozostałe stałe jako .

Zatem na mocy twierdzenia o zwartości jest również spełnialny. Niech będzie modelem . Relacja jest porządkiem liniowym, spełnia , ale nie jest porządkiem dobrym, bo zawiera nieskończony ciąg zstępujący . End of proof.gif

Interesujące jest porównanie powyższego dowodu z alternatywnym dowodem za pomocą metody Fraïssé, sugerowanym w Ćwiczeniu 4 do Rozdziału 4.