\begin{slide}{Wdhlg. Prädikatenlogik (Syntax)}

\begin{tabular}{ll}
Signatur $\Sigma$ &
\begin{minipage}{0.5\textwidth}
\begin{itemize}
\item Relationssymbole $R_1,\ldots,$
\item Funktionssymbole $f_1,\ldots,$
\end{itemize}
\end{minipage} \\ \hline
Term $t$ &
\begin{minipage}{0.5\textwidth}
\begin{itemize}
\item Variable $x$
\item $f(t_1,\ldots,t_k)$
\end{itemize}
\end{minipage} \\ \hline
Formel $F$ &
\begin{minipage}{0.8\textwidth}
\begin{itemize}
\item $R(t_1,\ldots,t_k)$
\item $F_1\wedge F_2; F_1\vee F_2;F_1\to F_2;F_1\leftrightarrow F_2;\neg F_1$
\item $\forall x: F_1; \exists x: F_1$
\end{itemize}
\end{minipage}
\end{tabular}

Menge der freien, gebundenen Variablen einer Formel

\emph{geschlossene} (closed) Formel: keine freien Variablen

\end{slide}


\begin{slide}{Prädikatenlogik (Semantik)}

zu Signatur $\Sigma=(\Sigma_F,\Sigma_R)$ passende \emph{Struktur}:
\begin{itemize}
\item ein Grundbereich $M$
\item zu jedem $f\in\Sigma_{F,k}$ ein $[f]:M^k\to M$
\item zu jedem $r\in\Sigma_{R,k}$ ein $[r]:M^k\to \Bool$
\end{itemize}

\emph{Belegung}: $b : \Var\to M$

\bigskip

Definiere
\begin{itemize}
\item Wert eines Terms $t$ in Struktur $M$ unter Belegung $b$
\item Wert einer Formel $F$ in Struktur $M$ unter Belegung $b$
\item Wert einer geschlossenen Formel $F$ in Struktur $M$
\end{itemize}

\end{slide}

\newcommand{\NN}{\mathbb{N}}

\begin{slide}{Theorien}
  Theorie einer Struktur $=$ alle Formeln,  die in dieser Struktur wahr sind.

\bigskip

  Beispiel: Signatur $\Sigma_F=\{0_0,S_1,+_2\}, \Sigma_R=\{=_2\}$,

  Struktur: $\NN$ mit Null, Nachfolger, Plus, Gleichheit.

  Theorie $T$ der natürlichen Zahlen mit Addition.

  Formel $(\forall x:\forall y:\forall z:x+(y+z)=(x+y)+z) \in T$.

\bigskip

typische (algorithmische) Fragen:
  \begin{itemize}
  \item Erfüllbarkeit (gehört $\exists$-Abschluß von Formel $F$ zu $T$?)
  \item Wahrheit (gehört geschlossene Formel $F$ zu $T$?)
  \end{itemize}

\end{slide}


