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 jestdowó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 matakże model każdej mocy $m\ge max\{{\mathrm{\aleph }}_0,|\mathrm{\Sigma }|\},$ gdzie $|\mathrm{\Sigma }|$ to moc zbioru symboli występujących w $\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 doniego twierdzenie o istnieniu modelu, otrzymujemy model $\overline{\mathfrak{𝔅}}$ omocy 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ęduktó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\"owenheima-Tarskiegojest następcą dwóch słabszych i starszych twierdzeń, które zresztąnadal są przywoływane. Zatem dla pełności informacji formułujemy jeponiż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ększejniż 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 dotwierdzeń o pełności ani o istnieniu modelu i było znane wcześniej od nich.

Wywołało ono kiedyś potężny ferment w dziedzinie logiki: jak to jestmożliwe, że teria 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. Naszczęście staranna analiza wskazuje, że nie mamy tu jednak doczynienia 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}}$ zbioruliczb 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".

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ść $<\mathbb{ℝ},\le >\equiv <\mathbb{\mathbb{Q}},\le >$,wyprowadzoną jako wniosek z Twierdzenia 4.13, to rozpoznamy wniej 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, toma 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<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 jegomodel jest też modelem dla $\mathrm{\Delta }.$

Twierdzenie o zwartości może też służyć do dowodzenia niewyrażalnościpewnych pojęć w logice pierwszego rzędu. Posłużymy się tu następującymprzykł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 nadsygnaturą $=,\le$ takiego, że każdy dobry porządek jest modelem$\mathrm{\Delta },$ istnieje też struktura $\mathfrak{𝔄}$ nie będąca dobrym porządkiem taka, ż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 }}$. RelacjaParser nie mógł rozpoznać (nieznana funkcja „\math”): {\displaystyle \leq^\math A} 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.

\subsection*{Ćwiczenia}\begin{small}

1. Wskazać przykład takiego zbioru $\mathrm{\Delta }$ zdań logiki pierwszego rzędu,że każde dwa jego \textit{przeliczalne} modele są izomorficzne, aleistnieją dwa \textit{nieprzeliczalne}, nieizomorficzne ze soba modelezbioru $\mathrm{\Delta }.$
2. Udowodnić, że dla każdej struktury skończonej Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} nad skończonąsygnaturą istnieje taki zbiór $\mathrm{\Delta }$ zdań pierwszego rzędu,że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\Delta} i dla każdej struktury Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\models\Delta} zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\cong\strA.}

1. Niech $\mathrm{\Sigma }$ będzie skończoną sygnaturą. Udowodnić, że dlakażdego zbioru zdań $\mathrm{\Delta }$ nad $\mathrm{\Sigma },$ następujące dwa warunkisą równoważne
   • $\mathrm{\Delta }$ ma wyłącznie skończone modele.
   • $\mathrm{\Delta }$ ma z dokładnością do izomorfizmu skończenie wiele modeli.

\item Udowodnić, że klasa wszystkich struktur izomorficznych zestrukturą postaci \mbox{</math>\strA=\langle\mathcal{P}\begin{eqnarray*}A\end{eqnarray*},\cup,\cap,\subseteq\rangle</math>}, gdzie $\cup ,\cap$ oraz$\subseteq$ są odpowiednio sumą, przecięciem i zawieraniem zbiorów,nie jest aksjomatyzowalna żadnym zbiorem zdań pierwszego rzędu.

\item Pokazać, że jeśli klasa ${𝒜}$ struktur nad sygnaturą$\mathrm{\Sigma }$ jest aksjomatyzowalna pewnym zbiorem zdań logiki pierwszegorzędu, oraz jej dopełnienie składające sięze struktur sygnatury $\mathrm{\Sigma },$ ktore nie należą do ${𝒜}$ teżjest aksjomatyzowalne, to każda z tych klas jest w istocie aksjomatyzowalna\textit{jednym} zdaniem pierwszego rzędu.

{\em Wskazówka:\/} Założyć, że pierwsza klasa jest aksjomatyzowalnaprzez $\mathrm{\Delta }$, a druga przez ${\mathrm{\Delta }}^{\prime },$ ale żaden skończony podzbiór$\mathrm{\Delta }$ nie jest aksjomatyzacją ${𝒜}.$ Pokazać, że$\mathrm{\Delta }\cup {\mathrm{\Delta }}^{\prime }$ spełnia założenia twierdzenia o zwartości.

\item Pokazać następujące twierdzenie Robinsona: Jeśli$\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }$ są spełnialnymi zbiorami zdań nad pewną sygnaturą$\mathrm{\Sigma },$ zaś $\mathrm{\Delta }\cup {\mathrm{\Delta }}^{\prime }$ nie jest spełnialny, to istniejetakie zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} orazParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta'\models\lnot\var\varphi.}

{\em Wskazówka:\/} Pokazać, że jeśli teza nie zachodzi, to$\mathrm{\Delta }\cup {\mathrm{\Delta }}^{\prime }$ spełnia założenia twierdzenia o zwartości.

\item Niech Parser nie mógł rozpoznać (błąd składni): {\displaystyle Spec\begin{eqnarray*}\var\varphi\end{eqnarray*}} oznacza zbiór mocy wszystkich skończonych modeli formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi.} Pokazać, że jeśli $\mathrm{\Delta }$ jest takim zbiorem zdań, iż dlakażdego Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\in\Delta} zbiór Parser nie mógł rozpoznać (błąd składni): {\displaystyle Spec\begin{eqnarray*}\lnot\var\varphi\end{eqnarray*}} jest skończony,oraz jeśli $\mathrm{\Delta }\models \psi ,$ to także Parser nie mógł rozpoznać (błąd składni): {\displaystyle Spec\begin{eqnarray*}\lnot\psi\end{eqnarray*}} jestskończony.

\end{small}