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ł $\Delta$ i dowolnej formuły Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi} , jeśli Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \Delta\models\var\varphi} , to istnieje skończony podzbiór $\Delta _{0}\subseteq \Delta$ taki, że Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \Delta_0\models\var\varphi} .
2. Dla dowolnego zbioru formuł $\Delta$, jeśli każdy skończony podzbiór$\Delta _{0}\subseteq \Delta$ jest spełnialny, to $\Delta$ też jest spełnialny.

Dowód

W części pierwszej, jeśli Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \Delta\models\var\varphi} , to z twierdzenia o pełności wynika, że Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \Delta\vdash_H\var\varphi} . W dowodzie występuje tylko skończenie wiele formuł z $\Delta$. Jeśli $\Delta _{0}$ jest zbiorem wszystkich tych formuł, to oczywiścieParser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \Delta_0\vdash_H\var\varphi} . Z twierdzenia o poprawności wynika, że Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \Delta_0\models\var\varphi} .

Część druga wynika z części pierwszej, gdy przyjmiemy Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \var\varphi=\bot} . Niespełnialność zbioru $\Delta$ to bowiem to samo, co $\Delta \models \bot$.

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

Dowód

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

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

Wynika stąd, że ${\bar {\Delta }}$ jest zbiorem niesprzecznym. Stosując do niego twierdzenie o istnieniu modelu, otrzymujemy model ${\bar {\mathfrak {B}}}$ o mocy nie przekraczającej mocy zbioru wszystkich formuł logiki pierwszego rzędu nad $\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 ${\bar {\mathfrak {B}}}$ zignorujemy interpretację stałych z $C$ to otrzymamy $\Sigma$-strukturę ${\mathfrak {B}}$ mocy $m$, która jest modelem zbioru $\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 $\Delta$ zdań logiki pierwszego rzędu, który ma model nieskończony ${\mathfrak {A}}$ i zarazem dla każdej struktury ${\mathfrak {B}}$ spełniającej $\Delta$ zachodzi ${\mathfrak {B}}\cong {\mathfrak {A}}$

.

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

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

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

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

Twierdzenie 8.6 (Skolema-Löwenheima

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

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ć (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\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 {N} }$), żadna funkcja z interpretacji $\mathbb {N}$ zbioru liczb naturalnych na interpretację P(${\mathbb {N} }$) sama nie jest elementem tego modelu. To już wystarcza, aby spełniał on zdanie mówiące, że P(${\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 {R} ,\leq >\equiv <\mathbb {Q} ,\leq >$, 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ń $\Delta$ ma modele skończone dowolnie dużej mocy, to ma też model nieskończony.

Dowód

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

Niech Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\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ć (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\displaystyle \bigwedge_{i<j}x_i\neqx_j} oznacza koniunkcję wszystkich $n(n-1)$ formuł postaci $x_{i}\neq x_{j}$, w których $i<j$.

Zbiór ${\bar {\Delta }}$ jest spełnialny, bo każdy jego skończony podzbiór ${\bar {\Delta }}_{0}\subseteq {\bar {\Delta }}$ jest spełnialny. Istotnie, modelem ${\bar {\Delta }}_{0}$ jest każdy model $\Delta$ mocy co najmniej Parser nie mógł rozpoznać (SVG (MathML może zostać włączone przez wtyczkę w przeglądarce): Nieprawidłowa odpowiedź („Math extension cannot connect to Restbase.”) z serwera „https://wazniak.mimuw.edu.pl/api/rest_v1/”:): {\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 ${\bar {\Delta }}$jest też spełnialny. Ma on wyłącznie modele nieskończone, a każdy jego model jest też modelem dla $\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 $\Delta$ formuł pierwszego rzędu nad sygnaturą $=,\leq$ takiego, że każdy dobry porządek jest modelem $\Delta$, istnieje też taka struktura ${\mathfrak {A}}$ nie będąca dobrym porządkiem, że ${\mathfrak {A}}\models \Delta$.

Dowód

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

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

Zatem na mocy twierdzenia o zwartości ${\bar {\Delta }}$ jest również spełnialny. Niech ${\mathfrak {A}}$ będzie modelem ${\bar {\Delta }}$. Relacja$\leq ^{\mathfrak {A}}$ jest porządkiem liniowym, spełnia $\Delta$, ale nie jest porządkiem dobrym, bo zawiera nieskończony ciąg zstępujący $c_{0}^{\mathfrak {A}}>c_{1}^{\mathfrak {A}}>c_{2}^{\mathfrak {A}}>\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.