2010-12-07.tex

\section{VL vom 07. Dezember 2010}

\subsection{FO Theorien}

\begin{enumerate}
  \item $\Taut(\tau)$ ist Theorie:
  \begin{enumerate}
    \item erfüllbar, denn $\Afrak\models\Taut(\tau)$ für jede Struktur
    $\Afrak$
    
    \item Wenn $\Taut(\tau)\models\psi$ erfüllbar, dann ist $\varphi$
    Tautologie, also $\varphi\in\Taut(\tau)$
  \end{enumerate}
  
  Nicht vollständig, denn es gibt Sätze $\varphi$, die weder Tautologie
  sind noch unerfüllbar (also $\NOT\varphi$ keine Tautologie).
  
  \item $\cl(\emptyset)$ ist genau $\Taut(\tau)$, also nicht vollständig.
  
  \item Vollständig: Für jede Struktur $\Afrak$ und FO-Satz $\varphi$
  gilt: $\Afrak\models\varphi$ oder $\Afrak\models\NOT\varphi$.
  
  \item Nicht vollständig: Wenn $\mathcal{K}$ die Klasse aller
  Strukturen, dann $\Th(\mathcal{K}) = \Taut(\tau)$
\end{enumerate}

\subsection{?? (vor Axiomatisierung)}

\begin{description}[style=nextline]
  \item[(1)$\IMPL$(2)]
  Sei $\Gamma$ vollständig. Da $\Gamma$ erfüllbar gibt es Struktur
  $\Afrak$ mit $\Afrak\models\Gamma$, also $\Gamma\subseteq\Th(\Afrak)$.
  Es gilt auch $\Th(\Afrak)\subseteq\Gamma$: Wenn $\varphi\in\Th(\Afrak)$,
  dann $\varphi\in\Gamma$ oder $\NOT\varphi\in\Gamma$. Letzteres ist
  unmöglich wegen $\Afrak\models\Gamma$.
  
  \item[(2)$\IMPL$(3)]
  Sei $\Gamma=\Th(\Afrak)$, $\Afrak', \Afrak''$ Meodell von $\Gamma$ und
  $\Afrak'\models\varphi$. Zu zeigen: $\Afrak''\models\varphi$. Wegen
  $\Afrak\models\varphi$ oder $\Afrak\models\NOT\varphi$, also
  $\varphi\in\Gamma$ oder $\NOT\varphi\in\Gamma$. Da $\Afrak'\models\Gamma$
  und $\Afrak'\models\varphi$ ist letzteres unmöglich. Also $\varphi\in\Gamma$
  und wegen $\Afrak''\models\Gamma$ also auch $\Afrak''\models\varphi$.
  
  \item[(3)$\IMPL$(1)]
  Seien alle Modelle von $\Gamma$ elementar äquivalent, und $\varphi\in
  FO(\tau)$. Angenommen, $\varphi\not\in\Gamma$ und $\NOT\varphi\not\in\Gamma$.
  Dann $\Gamma\not\models\varphi$ und $\Gamma\not\models\NOT\varphi$, also
  gibt es Modelle $\Afrak, \Afrak'$ von $\Gamma$ mit $\Afrak\models\varphi$
  und $\Afrak'\models\NOT\varphi$. Dan sind $\Afrak$ und $\Afrak'$ nicht
  elementar äquivalent.
\end{description}

\subsection{Axiomatisierbarkeit}

\begin{description}
  \item[\enquote{$\Leftarrow$}]
  Sei $\Gamma$ eine Theorie und $\varphi_1, \varphi_2, \ldots$ rekursive
  Aufzählung von $\Gamma$.
  Für $n\geq1$ definiere
  \[
    \psi_n = \varphi_n \AND true \AND \dots \AND true \qquad \text{$n$ mal}
  \]
  wobei \enquote{$true$} eine feste FO-Tautologie ist, z.B. \enquote{$c=c$}.
  
  Sei $\Pi=\set{\psi_1,\psi_2,\psi_3,\dots}$. Offensichtlich gilt
  $\Gamma\EQUIV\Pi$, also auch $\Gamma=\cl(\Pi)$. Es bleibt zu zeigen, dass $\Pi$
  entscheidbar ist. Der Algorithmus ist wie folgt: Bei Eingabe $\psi$
  berechnet er zunächst $m=|\psi|$, die Anzahl der Zeichen in $\psi$. Da
  $|\psi_n| \geq n$ für alle $n$, kann $\psi\in\Pi$, wenn
  $\psi\in\set{\psi_1,\dots,\psi_m}$. Der Algorithmus kann dies leicht prüfen,
  indem er $\psi_1,\dots,\psi_m$ aufzählt (via $\varphi_1,\dots,\varphi_n$).
    
  \item[\enquote{$\Rightarrow$}]
  Sei $\Gamma$ eine FO-Theorie mit Axiomatisierung $\Pi$. Wir werden später
  zeigen, dass FO kompakt ist und alle FO-Tautologien rekursiv aufzählbar
  sind. Wegen $\varphi\in\Gamma=\cl(\Pi)$ gibt es also endliche Teilmenge
  $\Pi_f\subseteq\Pi$ mit $\Pi_f\models\varphi$. Der Algorithmus kann also
  alle Paare $(\Pi_f,\psi)$ aufzählen mit $\Pi_f\in\Pi$ endlich und $\psi$
  FO-Tautologie. Er eliminiert alle Paare, für die $\psi$ nicht die Form
  $\ANDop\Pi_f\IMPL\vartheta$ hat. Die $\vartheta$-Komponenten der verbleibenden Paare
  sind eine Aufzählung von $\Gamma$.
\end{description}

\begin{enumerate}[start=2]% wo ist 1??
  \item Mit 1. reicht es zu zeigen: jede vollständige Theorie $\Gamma$
  ist entscheidbar, gdw. sie rekursiv aufzählbar ist.
  
  \begin{description}
    \item[\enquote{$\Leftarrow$}] trivial.
    \item[\enquote{$\Rightarrow$}]
    Wenn $\Gamma$ rekursiv aufzählbar, so kann man $\varphi\stackrel{?}{\in}\Gamma$
    entscheiden, indem man $\Gamma$ aufzählt: \enquote{ja} antwortet,
    wenn $\varphi$ generiert wird und \enquote{nein}, wenn $\NOT\varphi$
    generiert wird.
  \end{description}
\end{enumerate}
\qed