Logika dla informatyków/Teoria modeli

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ł $\mathrm{\Delta }$ 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 ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$ taki, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta_0\models\var\varphi} .
2. Dla dowolnego zbioru formuł $\mathrm{\Delta }$, jeśli każdy skończony podzbiór${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$ jest spełnialny, to $\mathrm{\Delta }$ 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 $\mathrm{\Delta }$. Jeśli ${\mathrm{\Delta }}_0$ 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 $\mathrm{\Delta }$ to bowiem to samo, co $\mathrm{\Delta }\models \mathrm{\perp }$.

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ł $\mathrm{\Delta }$ nad $\mathrm{\Sigma }$ ma model nieskończony, to ma także model każdej mocy $m\ge max\{{\mathrm{\aleph }}_0,|\mathrm{\Sigma }|\}$ gdzie $|\mathrm{\Sigma }|$ to moc sygnatury $\mathrm{\Sigma }$.

Dowód

Niech $C$ będzie zbiorem nowych symboli stałych, dotychczas niewystępujących w $\mathrm{\Sigma }$, którego moc wynosi $m$. Niech $\overline{\mathrm{\Delta }}=\mathrm{\Delta }\cup \{c\ne d|c,d\in \mathrm{\Sigma }$ oraz $c$ różne od $d$ }.

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

Wynika stąd, że $\overline{\mathrm{\Delta }}$ jest zbiorem niesprzecznym. Stosując do niego twierdzenie o istnieniu modelu, otrzymujemy model $\overline{\mathfrak{𝔅}}$ o mocy nie przekraczającej mocy zbioru wszystkich formuł logiki pierwszego rzędu nad $\mathrm{\Sigma }(C)$, która wynosi $m$, ale jednocześnienie mniejszej niż $|C|=m$, bo wszystkie stałe z $C$ muszą być w nim zinterpretowane jako różne elementy.

Jeśli teraz w modelu $\overline{\mathfrak{𝔅}}$ zignorujemy interpretację stałych z $C$ to otrzymamy $\mathrm{\Sigma }$-strukturę $\mathfrak{𝔅}$ mocy $m$, która jest modelem zbioru $\mathrm{\Delta }$

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 $\mathrm{\Delta }$ zdań logiki pierwszego rzędu, który ma model nieskończony $\mathfrak{𝔄}$ i zarazem dla każdej struktury $\mathfrak{𝔅}$ spełniającej $\mathrm{\Delta }$ zachodzi $\mathfrak{𝔅}\cong \mathfrak{𝔄}$

.

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 $\mathrm{\Sigma }$ ma model o mocy nie większej niż moc zbioru formuł logiki pierwszego rzędu nad $\mathrm{\Sigma }$.

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

Jeśli zbiór zdań nad $\mathrm{\Sigma }$ ma model nieskończony, to dla każdego$\mathfrak{𝔪}$ ma model o mocy nie mniejszej niż $\mathfrak{𝔪}$.

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

Twierdzenie 8.6 (Skolema-Löwenheima

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

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($\mathbb{\mathbb{N}}$), żadna funkcja z interpretacji $\mathbb{\mathbb{N}}$ zbioru liczb naturalnych na interpretację P($\mathbb{\mathbb{N}}$) sama nie jest elementem tego modelu. To już wystarcza, aby spełniał on zdanie mówiące, że P($\mathbb{\mathbb{N}}$) jest nieprzeliczalny.

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

Twierdzenia 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ść $<\mathbb{ℝ},\le >\equiv <\mathbb{\mathbb{Q}},\le >$, 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ń $\mathrm{\Delta }$ ma modele skończone dowolnie dużej mocy, to ma też model nieskończony.

Dowód

Przypuśćmy, że $\mathrm{\Delta }$ 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 $n(n-1)$ formuł postaci $x_i\ne x_j$, w których $i<j$.

Zbiór $\overline{\mathrm{\Delta }}$ jest spełnialny, bo każdy jego skończony podzbiór ${\overline{\mathrm{\Delta }}}_0\subseteq \overline{\mathrm{\Delta }}$ jest spełnialny. Istotnie, modelem ${\overline{\mathrm{\Delta }}}_0$ jest każdy model $\mathrm{\Delta }$ 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 $\overline{\mathrm{\Delta }}$jest też spełnialny. Ma on wyłącznie modele nieskończone, a każdy jego model jest też modelem dla $\mathrm{\Delta }$.

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 $\mathrm{\Delta }$ formuł pierwszego rzędu nad sygnaturą $=,\le$ takiego, że każdy dobry porządek jest modelem $\mathrm{\Delta }$, istnieje też taka struktura $\mathfrak{𝔄}$ nie będąca dobrym porządkiem, że $\mathfrak{𝔄}\models \mathrm{\Delta }$.

Dowód

Niech zbiór zdań $\mathrm{\Delta }$ 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 $\mathrm{\Delta }$zawiera już zwykłe aksjomaty liniowych porządków. Niech$C=\{c_0,c_1,\dots \}$ będzie zbiorem nowych stałych.

Niech $\overline{\mathrm{\Delta }}=\mathrm{\Delta }\cup \{c_i<c_j|j<i\}$. Każdy skończony podzbiór ${\overline{\mathrm{\Delta }}}_0\subseteq \overline{\mathrm{\Delta }}$ jest spełnialny, np. w zbiorze $\mathbb{\mathbb{N}}$, w którym każda stała $c_i$ występująca w ${\overline{\mathrm{\Delta }}}_0$ jest interpretowana jako $2|{\overline{\mathrm{\Delta }}}_0|-i$, zaś pozostałe stałe jako $0$.

Zatem na mocy twierdzenia o zwartości $\overline{\mathrm{\Delta }}$ jest również spełnialny. Niech $\mathfrak{𝔄}$ będzie modelem $\overline{\mathrm{\Delta }}$. Relacja${\le }^{\mathfrak{𝔄}}$ jest porządkiem liniowym, spełnia $\mathrm{\Delta }$, ale nie jest porządkiem dobrym, bo zawiera nieskończony ciąg zstępujący $c_0^{\mathfrak{𝔄}}>c_1^{\mathfrak{𝔄}}>c_2^{\mathfrak{𝔄}}>\dots$

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