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 Parser nie mógł rozpoznać (nieznana funkcja „\m”): {\displaystyle \m} , która jest modelem zbioru $\mathrm{\Delta }$

Wniosek

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 Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i zarazem dla każdej strukturyParser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} spełniającej $\mathrm{\Delta }$ zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB\cong\strA.}

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 Dolne twierdzenie Skolema-L\"owenheima

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 Górne twierdzenie Skolema-L\"owenheima

Jeśli zbiór zdań nad $\mathrm{\Sigma }$ ma model nieskończony, to dla każdegoParser nie mógł rozpoznać (błąd składni): {\displaystyle \frak m} ma model o mocy nie mniejszej niż Parser nie mógł rozpoznać (błąd składni): {\displaystyle \frak m} .

Najstarszym pr\leftrightarrowplastą tej grupy twierdzeń było po prostu

Twierdzenie Skolema-L\"owenheima

Każda nieskończona struktura Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} nad co najwyżej przeliczalnąsygnaturą zawiera co najwyżej przeliczalną podstrukturę,\Delta\vdashlementarnierównoważną z Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA.}

W tym sformułowaniu twierdzenie to daje się\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić bez odwołania dotwierdzeń o pełności ani o istnieniu modelu i było znane wcześniej odnich.

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 onzawierać zbiory nieprzeliczalne, jak np. Parser nie mógł rozpoznać (nieznana funkcja „\pot”): {\displaystyle \pot{\NN}} ? Oczywiście niktwolał głośno nie wypowiadać drugiej\Delta\vdashwentualności: że teoria mnogościnie 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 teoriimnogości, to wszystkie zbiory do niego należące oglądane \textit{zzewnątrz} są przeliczalne. Jednak dla niektórych z nich, np.\ dlainterpretacji Parser nie mógł rozpoznać (nieznana funkcja „\pot”): {\displaystyle \pot{\NN}} , żadna funkcja z interpretacji Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle \NN} zbioruliczb naturalnych na interpretację Parser nie mógł rozpoznać (nieznana funkcja „\pot”): {\displaystyle \pot{\NN}} sama nie jest\Delta\vdashlementem\textit{tego modelu}. \Rightarrow już wystarcza, aby spełniał on zdaniemówiące, że Parser nie mógł rozpoznać (nieznana funkcja „\pot”): {\displaystyle \pot{\NN}} jest nieprzeliczalny.

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

Twierdzenie o zwartości i twierdzeń Skolema-L\"owenheima często\boldsymbol{s}}\def\blank{\hbox{\sf Bżywasię do tego, by wykazać istnienie różnych nietypowych modeli. Jeśliprzypomnimy sobie\Delta\vdashlementarną równoważność </math>\langle\mathbb{R},\leq\rangle\equiv\langle \mathbb{Q},\leq\rangle</math>,wyprowadzoną jako wniosek z Twierdzenia #Cantoro, to rozpoznamy wniej również potencjalny\Delta\vdashfekt zastosowania \begin{eqnarray*}dolnego\end{eqnarray*} twierdzeniaSkolema-L\"owenheima.

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

Twierdzenie

Jeśli zbiór zdań $\mathrm{\Delta }$ ma modele skończone dowolnie dużej mocy, toma też model nieskończony.

<span id=" n\in\NN\}Parser nie mógł rozpoznać (błąd składni): {\displaystyle . Oczywiście } \\bigwedge_{i<j}x_i\neqx_j</math> oznacza koniunkcję wszystkich Parser nie mógł rozpoznać (błąd składni): {\displaystyle n\begin{eqnarray*}n-1\end{eqnarray*}} formuł postaci

$x_i<x_j,$

wktó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\mbox{</math>\max\{n " style="font-variant:small-caps">Dowód

  \begin{eqnarray*}\exists x_1\dots\exists x_n\\bigwedge_{i<j}x_i\neqx_j\end{eqnarray*}\in\bar\Delta_0\}</math>}. 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

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 Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} nie będąca dobrym porządkiemtaka, że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\Delta.}

Dowód

{{{3}}}

\def\blank{\hbox{\sf Btraty 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \bar\Delta=\Delta\cup\{c_i<c_j&nbsp;|&nbsp;j<i\}.} Każdy skończonypodzbiór ${\overline{\mathrm{\Delta }}}_0\subseteq \overline{\mathrm{\Delta }}$ jest spełnialny, np. w zbiorze Parser nie mógł rozpoznać (nieznana funkcja „\NN”): {\displaystyle \NN,} 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 Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} będzie modelem $\overline{\mathrm{\Delta }}$. RelacjaParser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \leq^\strA} jest porządkiem liniowym, spełnia $\mathrm{\Delta }$, ale nie jestporządkiem dobrym, bo zawiera nieskończony ciąg zstępującyParser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle c_0^\strA>c_1^\strA>c_2^\strA>\dots} .}}

Interesujące jest porównanie powyższego dowodu z alternatywnym dowodemza pomocą metody Fra\"{\i}ss\'e, sugerowanym w Ćwiczeniu #c doRozdziału #EF.

\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}