\newcommand{\Lang}{\operatorname{Lang}}

\begin{slide}{Entscheidungsverfahren (Ansatz)}

Def.: Menge $M\subset \NN^k$ heißt
\emph{P-definierbar} 

$\iff$ es gibt eine
P-Formel $F$ so daß $M = \Mod(F)$ 

wobei $\Mod(F) := \{ m \in \NN^k \mid  \{ x_1\mapsto m_1,\ldots,
x_k\mapsto m_k\}\models F \}$

für $F$ mit freien Var. $x_1,\ldots,x_k$,

\bigskip

Satz: jede solche Modellmenge $\Mod(F)$ 
ist \emph{effektiv regulär}:
\begin{itemize}\itemsep 0pt
\item es gibt einen Algorithmus, der zu jeder
  P-Formel $F$ \dots
\item \dots einen endl. Automaten $A$ konstruiert
  mit $\Lang(A) = \text{Kodierung von} \Mod(F)$
\end{itemize}

\bigskip

Folgerung: Allgemeingültigkeit ist entscheidbar:

$\Lang(A)=\emptyset$ gdw. $\Mod(F)=\emptyset$
gdw. $F$ ist widersprüchlich gdw. $\neg F$ ist
allgemeingültig.

\end{slide}

