\begin{slide}{Mehrsortiger Signaturen/Algebren}

\emph{Sorte}:(Name für einen ) Typ

\emph{mehrsortige Signatur} zu Sorten $S_1,\ldots, S_n$:

eine Menge von Funktionssymbolen, 
zu jedem ein Tupel von Sorten $(A_1,\ldots, A_k, R)$

\emph{mehrsortige Algebra}

für jede Sorte $S$ eine Menge $[S]$,

für jedes Funktionssymbol $f$ eine Funktion $[f]$
vom entsprechenden Typ.

\end{slide}

\begin{slide}{Mehrsortig \dots Beispiel}

Sorten: $P, G, B$, wobei $[B]=$ Boolean

Signatur: $I:P\times G \to B$ 

Axiome:
\begin{eqnarray*}
&& \forall x\in P, y\in P: x\neq y 
\implies \exists_{=1} z\in G: I(x,z)\wedge I(y,z) \\
&\wedge& \forall x\in G, y\in G: x\neq y 
\implies \exists_{=1} z\in P: I(z,x)\wedge I(z,y) \\
&\wedge& \exists n\in \NN: 
\begin{array}{ll}
  & (\forall x\in G: \exists_{=n} y\in P:I(y,x)) \\
  \wedge & (\forall x\in P: \exists_{=n} y\in G:I(x,y))
\end{array} \\
& \wedge & |P|=|G| \wedge |P|\neq\emptyset
\end{eqnarray*}

Finde je ein Modell mit $n=2, 3, \ldots$
\end{slide}
