Ist D eine Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$ und ist E eine Deduktion von $\psi$ mit Hypothesen aus $\Gamma$, so ergibt sich die folgende Deduktion von $\varphi\wedge\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\varphi\wedge\psi$ mit Hypothesen aus $\Gamma$, so ergeben sich die folgenden Deduktionen von $\varphi$ bzw. von $\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\psi$ mit Hypothesen aus $\Gamma\cup\{\varphi\}$, so ergibt sich die folgende Deduktion von $\varphi\rightarrow\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$ und ist E eine Deduktion von $\varphi\rightarrow\psi$ mit Hypothesen aus $\Gamma$, so ergibt sich die folgende Deduktion von $\psi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\varphi\vee\psi$ mit Hypothesen aus $\Gamma$, ist E eine Deduktion von $\sigma$ mit Hypothesen aus $\Gamma\cup\{\varphi\}$und ist F eine Deduktion von $\sigma$ mit Hypothesen aus $\Gamma\cup\{\psi\}$, so ergibt sich die folgende Deduktion von $\sigma$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\bot$ mit Hypothesen aus $\Gamma\cup\{\varphi\}$, so ergibt sich die folgende Deduktion von $\lnot\varphi$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\lnot\varphi$ mit Hypothesen aus $\Gamma$ und ist E eine Deduktion von $\varphi$ mit Hypothesen aus $\gamma$, so ergibt sich die folgende Deduktion von $\bot$ mit Hypothesen aus $\Gamma$:
Ist D eine Deduktion von $\bot$ mit Hypothesen aus $\Gamma\cup\{\lnot\varphi\}$, so ergibt sich die folgende Deduktion von $\varphi$ mit Hypothesen aus $\Gamma$:
\note{Definition}{Für eine Formelmenge $\Gamma$ und eine Formel $\varphi$ schreiben wir $\Gamma\Vdash\varphi$ wenn es eine Deduktion gibt mit Hypothesen aus $\Gamma$ und Konklusion $\varphi$. Wir sagen ''$\varphi$ ist eine syntaktische Folgerung von $\Gamma$''. Eine Formel $\varphi$ ist ein Theorem, wenn $\varnothing\Vdash\varphi$ gilt.}
$\Gamma\Vdash\varphi$ sagt nichts über den Inhalt der Formeln in $\Gamma\cup\{\varphi\}$ aus, sondern nur über die Tatsache, dass $\varphi$ mithilfe des natürlichen Schließens aus den Formeln aus $\Gamma$ hergeleitet werden kann.
\note{Definition}{Sei W eine Menge und $R\subseteq W\times W$ eine binäre Relation.
\begin{itemize*}
\item R ist reflexiv, wenn $(a,a)\in R$ für alle $a\in W$ gilt.
\item R ist antisymmetrisch, wenn $(a,b),(b,a)\in R$ impliziert, dass $a=b$ gilt (für alle $a,b\in W$).
\item R ist transitive, wenn $(a,b),(b,c)\in R$ impliziert, dass $(a,c)\in R$ gilt (für alle $a,b,c\in W$).
\item R ist eine Ordnungsrelation, wenn R reflexiv, antisymmetrisch und transitiv ist. In diesem Fall heißt das Paar $(W,R)$ eine partiell geordnete Menge.
\note{Definition}{Sei $(W,\leq)$ partiell geordnete Menge, $M\subseteq W$ und $a\in W$.
\begin{itemize*}
\item a ist obere Schranke von $M$, wenn $m\leq a$ für alle $m\in M$ gilt.
\item a ist kleinste obere Schranke oder Supremum von $M$, wenn $a$ obere Schranke von $M$ ist und wenn $a\leq b$ für alle oberen Schranken $b$ von $M$ gilt. Wir schreiben in diesem Fall $a=sup \ M$.
\item a ist untere Schranke von $M$, wenn $a\leq m$ für alle $m\in M$ gilt.
\item a ist größte untere Schranke oder Infimum von $M$, wenn a untere Schranke von $M$ ist und wenn $b\leq a$ für alle unteren Schranken $b$ von $M$ gilt. Wir schreiben in diesem Fall $a=inf\ M$.
\note{Definition}{ Ein (vollständiger) Verband ist eine partiell geordnete Menge $(W,\leq)$, in der jede Menge $M\subseteq W$ ein Supremum $sup\ M$ und ein Infimum $inf\ M$ hat.}
In einem Verband $(W,\leq)$ definieren wir:
\begin{itemize*}
\item$0_W = inf\ W$ und $1_W= sup\ W$
\item$a\wedge_W b= inf\{a,b\}$ und $a\vee_W b= sup\{a,b\}$ für $a,b\in W$
In jedem Verband $(W,\leq)$ gelten $0_W= sup\ \varnothing$ und $1_W= inf\ \varnothing$ (jedes Element von $W$ ist obere und untere Schranke von $\varnothing$).
\note{Definition}{Ein Wahrheitswertebereich ist ein Tupel $(W,\leq,\rightarrow W,\lnot W)$, wobei $(W,\leq)$ ein Verband und $W\rightarrow W:W^2\rightarrow W$ und $\lnot W:W\rightarrow W$ Funktionen sind.}
Sei W ein Wahrheitswertebereich und B eine W-Belegung. Induktiv über den Formelaufbau definieren wir den Wahrheitswert $\hat{B}(\phi)\in W$ jeder zu $B$ passenden Formel $\phi$:
\begin{itemize*}
\item$\hat{B}(\bot)=0_W$
\item$\hat{B}(p)= B(p)$ falls $p$ eine atomare Formel ist
Eine Formel $\phi$ heißt eine W-Folgerung der Formelmenge $\Gamma$, falls für jede W-Belegung B, die zu allen Formeln aus $\Gamma\cup\{\phi\}$ paßt, gilt: $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\phi)$
\note{Korrektheitslemma für nat. Schließen \& Wahrheitswertebereich B}{Sei $D$ eine Deduktion mit Hypothesen in der Menge $\Gamma$ und Konklusion $\varphi$. Dann gilt $\Gamma\vdash_B \varphi$, d.h. $inf\{B(\gamma)|\gamma\in\Gamma\}\leq B(\varphi)$ für alle passenden B-Belegungen $B$.}
Ist die letzte Schlußregel in der Deduktion $D$ von der Form $(\wedge I), (\vee E), (\rightarrow I)$ oder $(raa)$, so ist die Behauptung des Lemmas gezeigt.
\note{Korrektheitssatz für natürliches Schließen \& Wahrheitswertebereich $B$}{Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_B\varphi$.}
Beweis: Wegen $\Gamma\vdash\varphi$ existiert eine Deduktion $D$ mit Hypothesen in $\Gamma$ und Konklusion $\varphi$. Nach dem Korrektheitslemma folgt $\Gamma\vdash_B \varphi$.
\note{Korollar}{Jedes Theorem ist eine B-Tautologie.}
\note{Korrektheitssatz für natürliches Schließen \& Wahrheitswertebereich $B$}{Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt $\Gamma\vdash\varphi\Rightarrow\Gamma\vdash_{B_\mathbb{R}}\varphi$.}
Beweis: verallgemeinere den Beweis von Korrektheitslemma und Korrektheitssatz für $B$ auf $B_\mathbb{R}$ (Problem: wir haben mehrfach ausgenutzt, dass $B=\{0,1\}$ mit $0<1$)
\note{Korrektheitslemma für nat. Schließen \& Wahrheitswertebereich $H_{\mathbb{R}}$}{Sei $D$ eine Deduktion mit Hypothesen in der Menge $\Gamma$ und Konklusion $\varphi$, die die Regel $(raa)$ nicht verwendet. Dann gilt $\Gamma\vdash_{H_\mathbb{R}}\varphi$.}
\note{Korrektheitssatz für nat. Schließen \& Wahrheitswertebereich $H_{\mathbb{R}}$}{Für jede Menge von Formeln $\Gamma$ und jede Formel $\varphi$ gilt $\Gamma\vdash\varphi$ ohne $(raa)$$\Rightarrow\Gamma\vdash_{H_{\mathbb{R}}}\varphi$.}
\note{Lemma}{Sei $\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $\Gamma\not\vdash\varphi\Leftrightarrow\Gamma\cup\{\lnot\varphi\}$ konsistent.}
\note{Definition}{Eine Formelmenge $\Delta$ ist maximal konsistent, wenn sie konsistent ist und wenn gilt ''$\sum\supseteq\Delta$ konsistent $\Rightarrow\sum=\Delta$''.}
\note{Lemma 2}{Sei $\Delta$ maximal konsistent und $\varphi$ Formel. Dann gilt $\varphi\not\in\Delta\Leftrightarrow\lnot\varphi\in\Delta$.}
\subsection{Erfüllbare Mengen}
\note{Definition}{Sei $\Gamma$ eine Menge von Formeln. $\Gamma$ heißt erfüllbar, wenn es eine passende B-Belegung $B$ gibt mit $B(\gamma)=1_B$ für alle $\gamma\in\Gamma$.}
\begin{itemize*}
\item Die Erfüllbarkeit einer endlichen Menge $\Gamma$ ist entscheidbar:
\note{Lemma}{Sei $\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $\Gamma\not\Vdash_B\varphi\Leftarrow\Rightarrow\Gamma\cup\{\lnot\varphi\}$ erfüllbar.}
\note{Beobachtung}{Sei $W$ einer der Wahrheitswertebereiche $B, K_3, F, H_R$ und $B_R,\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $\Gamma\Vdash W\varphi\Rightarrow\Gamma\Vdash B\varphi$.}
\note{Satz (Vollständigkeitssatz)}{Sei $\Gamma$ eine Menge von Formeln, $\varphi$ eine Formel und $W$ einer der Wahrheitswertebereiche $B,K_3 , F, B_R$ und $H_R$. Dann gilt $\Gamma\Vdash_W\varphi\Rightarrow\Gamma\vdash\varphi$. Insbesondere ist jede W-Tautologie ein Theorem.}
\note{Satz}{Seien $\Gamma$ eine Menge von Formeln und $\varphi$ eine Formel. Dann gilt $\Gamma\vdash\varphi\Leftarrow\Rightarrow\Gamma\Vdash_B \varphi$. Insbesondere ist eine Formel genau dann eine B-Tautologie, wenn sie ein Theorem ist.}
Da es nur endlich viele solche Abbildungen gibt und $B(\varphi)$ berechnet werden kann, ist dies eine entscheidbare Aussage.
\subsubsection{Folgerung 2: Äquivalenzen und Theoreme}
\note{Definition}{Zwei Formeln $\alpha$ und $\beta$ heißen äquivalent $(\alpha\equiv\beta)$, wenn für alle passenden B-Belegungen $B$ gilt: $B(\alpha)=B(\beta)$.}
\note{Satz}{Sei $\Gamma$ eine u.U. unendliche Menge von Formeln und $\varphi$ eine Formel mit $\Gamma\Vdash_B\varphi$. Dann existiert $\Gamma'\subseteq\Gamma$ endlich mit $\Gamma'\Vdash_B \varphi$.}
\note{Folgerung (Kompaktheits- oder Endlichkeitssatz)}{Sei $\Gamma$ eine u.U. unendliche Menge von Formeln. Dann gilt $\Gamma$ unerfüllbar $\Leftarrow\Rightarrow\exists\Gamma'\subseteq\Gamma$ endlich: $\Gamma'$ unerfüllbar}
\note{Definition}{Ein Graph ist ein Paar $G=(V,E)$ mit einer Menge $V$ und $E\subseteq\binom{V}{2}=\{X\subseteq V:|V\Vdash2\}$. Für $W\subseteq V$ sei $G\upharpoonright_W=(W,E\cap\binom{W}{2})$ der von $W$ induzierte Teilgraph. Der Graph G ist 3-färbbar, wenn es eine Abbildung $f:V\rightarrow\{1,2,3\}$ mit $f(v)\not=f(w)$ für alle $\{v,w\}\in E$.}
Sei $B$ erfüllende Belegung. Für $n\in N$ existiert genau ein $c\in\{1,2,3\}$ mit $B(p_{n,c})=1$. Setze $f(n)=c$. Dann ist $f$ eine gültige Färbung des Graphen $G$.
\note{Definition}{Ein Kachelsystem besteht aus einer endlichen Menge C von ''Farben'' und einer Menge K von Abbildungen $\{N,O,S,W\}\rightarrow C$ von ''Kacheln''.
\note{Satz}{Sei $K$ ein Kachelsystem. Es existiert genau dann eine Kachelung von $Z\times Z$, wenn für jedes $n\in N$ eine Kachelung von $\{(i,j) :|i|,|j| \leq n\}$ existiert.}
\note{Definition}{Eine Hornklausel hat die Form $(\lnot\bot\wedge p_1\wedge p_2\wedge ... \wedge p_n)\rightarrow q$ für $n\geq0$, atomare Formeln $p_1 ,p_2 ,... ,p_n$ und $q$ atomare Formel oder $q=\bot$.
Eine Hornformel ist eine Konjunktion von Hornklauseln.}
\item Der Algorithmus terminiert: in jedem Durchlauf der while-Schleife wird wenigstens eine atomare Formel markiert. Nach endlich vielen Schritten terminiert die Schleife also.
\item Wenn der Algorithmus eine atomare Formel q markiert und wenn $B$ eine B-Belegung ist, die $\Gamma$ erfüllt, dann gilt $B(q)=1_B$.
\note{Definition}{Sei $\Gamma$ eine Menge von Hornklauseln. Eine SLD-Resolution aus $\Gamma$ ist eine Folge $(M_0\rightarrow\bot,M_1\rightarrow\bot,... ,M_m\rightarrow\bot)$ von Hornklauseln mit
\begin{itemize*}
\item$(M_0\rightarrow\bot)\in\Gamma$
\item für alle $0\leq n<m$ existiert $(N\rightarrow q)\in\Gamma$ mit $q\in M_n$ und $M_{n+1}= M_n\backslash\{q\}\cup N$
\note{Lemma A}{Sei $\Gamma$ eine (u.U. unendliche) Menge von Hornklauseln und $(M_0\rightarrow\bot, M_1\rightarrow\bot,... , M_m\rightarrow\bot)$ eine SLD-Resolution aus $\Gamma$ mit $M_m=\varnothing$. Dann ist $\Gamma$ nicht erfüllbar.}
\note{Lemma B}{Sei $\Gamma$ eine (u.U. unendliche) unerfüllbare Menge von Hornklauseln. Dann existiert eine SLD-Resolution $(M_0\rightarrow\bot,...,M_m\rightarrow\bot)$ aus $\Gamma$ mit $M_m=\varnothing$.}
Beweis: Endlichkeitssatz: es gibt $\Delta\subseteq\Gamma$ endlich und unerfüllbar. Bei Eingabe von$\Delta$ terminiert Markierungsalgorithmus mit ''unerfüllbar''
\item$q_i...$ Atomformel, die in $i$ Runde markiert wird $(1\leq i\leq r)$
\end{itemize*}
Behauptung: Es gibt $m\leq r$ und SLD-Resolution $(M_0\rightarrow\bot,...,M_m\rightarrow\bot)$ aus $\Delta$ mit $M_m=\varnothing$ und $M_n\subseteq\{q_1,q_2,... ,q_{r-n}\}$ f.a. $0\leq n\leq m$. (5)
\note{Satz}{Sei $\Gamma$ eine (u.U. unendliche) Menge von Hornklauseln. Dann sind äquivalent:
\begin{enumerate*}
\item$\Gamma$ ist nicht erfüllbar.
\item Es gibt eine SLD-Resolution $(M_0\rightarrow\bot,M_1\rightarrow\bot,... ,M_m\rightarrow\bot)$ aus $\Gamma$ mit $M_m=\varnothing$.
\end{enumerate*}
}
Die Suche nach einer SLD-Resolution mit $M_m=\varnothing$ kann grundsätzlich auf zwei Arten erfolgen:
Um über Graphen Aussagen in der Aussagenlogik zu machen, verwenden wir Formeln $\varphi_{i,j}$ für $1\leq i,j\leq9$ mit $\varphi_{i,j}=\begin{cases}\lnot\bot\quad\text{ falls}(v_i,v_j) Kante\\\bot\quad\text{ sonst}\end{cases}$
\item Die aussagenlogische Formel $\bigvee_{1\leq i,j\leq9}\varphi_{i,j}$ sagt aus, dass der Graph eine Kante enthält.
\item Die aussagenlogische Formel $\bigwedge_{1\leq i\leq9}\bigvee_{1\leq j\leq9}\varphi_{i,j}$ sagt aus, dass jeder Knoten einen Nachbarn hat
\item Die aussagenlogische Formel $\bigvee_{1\leq i,j,k\leq9 verschieden}\varphi_{i,j}\wedge\varphi_{j,k}\wedge\varphi_{k,i}$ sagt aus, dass der Graph ein Dreieck enthält.
\note{Definition}{Eine Signatur ist ein Tripel $\sum=(\Omega, Rel,ar)$, wobei $\Omega$ und $Rel$ disjunkte Mengen von Funktions- und Relationsnamen sind und $ar:\Omega\cup Rel\rightarrow\mathbb{N}$ eine Abbildung ist.}
Eine $\sum$-Formel $\varphi$ ist geschlossen oder ein $\sum$-Satz, wenn $FV(\varphi)=\varnothing$ gilt.}
\note{Definition}{Sei $\sum$ eine Signatur. Eine $\sum$-Struktur ist ein Tupel $A=(U_A,(f^A)_{f\in\Omega},(R^A)_{R\in Rel})$, wobei
\begin{itemize*}
\item$U_A$ eine nichtleere Menge, das Universum,
\item$R^A\supseteq U_A^{ar(R)}$ eine Relation der Stelligkeit $ar(R)$ für $R\in Rel$ und
\item$f^A:U_A^{ar(f)}\rightarrow U_A$ eine Funktion der Stelligkeit $ar(f)$ für $f\in\Omega$ ist.
\end{itemize*}
}
Bemerkung: $U_A^0=\{()\}$.
\begin{itemize*}
\item Also ist $a^A:U_A^0\rightarrow U_A$ für $a\in\Omega$ mit $ar(a)=0$ vollständig gegeben durch $a^A(())\in U_A$. Wir behandeln 0-stellige Funktionen daher als Konstanten.
\item Weiterhin gilt $R^A=\varnothing$ oder $R^A=\{()\}$ für $R\in Rel$ mit $ar(R)=0$.
\end{itemize*}
\note{Definition}{Sei $\sum$ eine Signatur, $\varphi$ eine $\sum$-Formel, $\Delta$ eine Menge von $\sum$-Formeln und $A$ eine $\sum$-Struktur.
\begin{itemize*}
\item$A\Vdash\varphi$ ($A$ ist Modell von $\varphi$) falls $A\Vdash_p\varphi$ für alle Variableninterpretationen $\rho$ gilt.
\item$A\Vdash\Delta$ falls $A\Vdash\Psi$ für alle $\Psi\in\Delta$.
\end{itemize*}
}
\note{Definition}{Sei $\sum$ eine Signatur, $\varphi$ eine $\sum$-Formel, $\Delta$ eine Menge von $\sum$-Formeln und $A$ eine $\sum$-Struktur.
\begin{itemize*}
\item$\Delta$ ist erfüllbar, wenn es $\sum$-Struktur $B$ und Variableninterpretation $\rho:Var\rightarrow U_B$ gibt mit $B\Vdash_\rho\Psi$ für alle $\Psi\in\Delta$.
\item$\varphi$ ist semantische Folgerung von $\Delta(\Delta\Vdash\varphi)$ falls für alle $\sum$-Strukturen $B$ und alle Variableninterpretationen $\rho:Var\rightarrow U_B$ gilt: Gilt $B\Vdash_\rho\Psi$ für alle $\Psi\in\Delta$, so gilt auch $B\Vdash_\rho\varphi$.
\item$\varphi$ ist allgemeingültig, falls $B\Vdash\rho\varphi$ für alle $\sum$-Strukturen $B$ und alle Variableninterpretationen $\rho$ gilt.
\end{itemize*}
}
Bemerkung: $\varphi$ allgemeingültig gdw. $\varnothing\Vdash\varphi$ gdw. $\{\lnot\varphi\}$ nicht erfüllbar. Hierfür schreiben wir auch $\Vdash\varphi$.
\subsection{Substitutionen}
\note{Definition}{Eine Substitution besteht aus einer Variable $x\in Var$ und einem Term $t\in T_{\sum}$, geschrieben $[x:=t]$.}
Die Formel $\varphi[x:=t]$ ist die Anwendung der Substitution $[x:=t]$ auf die Formel $\varphi$. Sie entsteht aus $\varphi$, indem alle freien Vorkommen von $x$ durch $t$ ersetzt werden. Sie soll das über $t$ aussagen, was $\varphi$ über $x$ ausgesagt hat.
\note{Lemma}{Seien $\sum$ Signatur, $A$$\sum$-Struktur, $\rho:Var\rightarrow U_A$ Variableninterpretation, $x\in Var$ und $s,t\in T_{\sum}$. Dann gilt $\rho(s[x:=t])=\rho[x\rightarrow\rho(t)](s)$.}
\note{Definition}{Sei $[x:=t]$ Substitution und $\varphi$$\sum$-Formel. Die Substitution $[x:=t]$ heißt für $\varphi$ zulässig, wenn für alle $y\in Var$ gilt: $y$ Variable in $t\Rightarrow\varphi$ enthält weder $\exists y$ noch $\forall y$}
\note{Lemma}{Sei $\sum$ Signatur, A $\sum$-Struktur, $\rho:Var\rightarrow U_A$ Variableninterpretation, $x\in Var$ und $t\in T_{\sum}$. Ist die Substitution $[x:=t]$ für die $\sum$-Formel $\varphi$ zulässig, so gilt $A\Vdash_p\varphi[x:=t]\Leftrightarrow A\Vdash_{p[x\rightarrow\rho(t)]}\varphi$.}
\note{Lemma V0}{Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des natürlichen Schließens der Aussagenlogik verwendet. Dann gilt $\Gamma\Vdash\varphi$.}
Umgekehrt ist nicht zu erwarten, dass aus $\Gamma\Vdash\varphi$ folgt, dass es eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$ gibt, denn die bisher untersuchten Regeln erlauben keine Behandlung von $=,\forall$ bzw. $\exists$. Solche Regeln werden wir jetzt einführen.
Zunächst kümmern wir uns um Atomformeln der Form $t_1=t_2$. Hierfür gibt es die zwei Regeln $(R)$ und $(GfG)$:
\note{Reflexivität}{Für jeden Term $t$ ist $\frac{}{t=t}$ eine hypothesenlose Deduktion mit Konklusion $t=t$. %\includegraphics[width=\linewidth]{Assets/Logik-reflexivität-kurz.png}
\note{Gleiches-für-Gleiches}{Seien $s$ und $t$ Terme und $\varphi$ Formel, so dass die Substitutionen $[x:=s]$ und $[x:=t]$ für $\varphi$ zulässig sind. Sind $D$ und $E$ Deduktionen mit Hypothesen in $\Gamma$ und Konklusionen $\varphi[x:=s]$ bzw. $s=t$, so ist das folgende eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi[x:=t]$
Bedingung: über keine Variable aus $s$ oder $t$ wird in $\varphi$ quantifiziert
\note{Lemma V1}{Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des natürlichen Schließens der Aussagenlogik, $(R)$ und $(GfG)$ verwendet. Dann gilt $\Gamma\Vdash\varphi$.}
\note{$\forall$-Einführung}{ Sei $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$ und sei $x$ eine Variable, die in keiner Formel aus $\Gamma$ frei vorkommt. Dann ist das folgende eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\forall x\varphi: \frac{\phi}{\forall x\varphi}$
Bedingung: $x$ kommt in keiner Hypothese frei vor}
\note{Lemma V2}{Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des natürlichen Schließens der Aussagenlogik, (R), (GfG) und ($\forall$ -I) verwendet. Dann gilt $\Gamma\Vdash\varphi$.}
\note{$\forall$ -Elimination}{Sei $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\forall x\varphi$ und seit Term, so dass Substitution [x:=t] für $\varphi$ zulässig ist. Dann ist das folgende eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi[x:=t]:\frac{\forall x\varphi}{\varphi[x:=t]}$
Bedingung: über keine Variable aus $t$ wird in $\varphi$ quantifiziert}
\note{Lemma V3}{ Sei $\sum$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Sei weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des natürlichen Schließens der Aussagenlogik, (R), (GfG), ($\forall$-I) und ($\forall$-E) verwendet. > Dann gilt $\Gamma\Vdash\varphi$.}
\note{$\exists$ -Elimination}{Sei $\Gamma$ eine Menge von Formeln, die die Variable $x$ nicht frei enthalten und enthalte die Formel $\sigma$ die Variabel $x$ nicht frei. Wenn $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\exists x\varphi$ und $E$ eine Deduktion mit Hypothesen in $\Gamma\cup\{\varphi\}$ und Konklusion $\sigma$ ist, dann ist das folgende eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\sigma:\frac{\exists x\varphi\quad\quad\sigma}{\sigma}$
Bedingung: $x$ kommt in den Hypothesen und in $\sigma$ nicht frei vor.}
\note{Lemma V4}{Sei $\sigma$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sigma$ -Formel. Sei weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des natürlichen Schließens der Aussagenlogik, (R), (GfG), ($\forall$-I), ($\forall$-E) und ($\exists$-E) verwendet. Dann gilt $\Gamma\Vdash\varphi$.}
\note{$\exists$ -Einführung}{Sei die Substitution $[x:=t]$ für die Formel $\varphi$ zulässig. Sei weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi[x:=t]$. Dann ist das folgende eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\exists x\varphi:\frac{\varphi[x:=t]}{\exists x\varphi}$
Bedingung: über keine Variable in $t$ wird in $\varphi$ quantifiziert}
\note{Korrektheitslemma für das natürliche Schließen in der Prädikatenlogik}{
Sei $\sigma$ eine Signatur, $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sigma$ -Formel.
Sei weiter $D$ eine Deduktion mit Hypothesen in $\Gamma$ und Konklusion $\varphi$, die die Regeln des natürlichen Schließens der Aussagenlogik, (R), (GfG), ($\forall$-I), ($\forall$-E), ($\exists$ -E) und ($\exists$ -I) verwendet. Dann gilt $\Gamma\Vdash\varphi$.}
\note{Definition}{Für eine Menge $\Gamma$ von $\sum$-Formeln und eine $\sum$-Formel $\varphi$ schreiben wir $\Gamma\vdash\varphi$ wenn es eine Deduktion gibt mit Hypothesen in $\Gamma$ und Konklusion $\varphi$. Wir sagen ''$\varphi$ ist eine syntaktische Folgerung von $\Gamma$''.
Eine Formel $\varphi$ ist ein Theorem, wenn $\varnothing\vdash\varphi$ gilt.}
\note{Korrektheitssatz}{Für eine Menge von $\sum$-Formeln $\Gamma$ und eine $\sum$-Formel $\varphi$ gilt $\Gamma\vdash\varphi\Rightarrow\Gamma\Vdash\varphi$.}
\subsection{Vollständigkeit}
\note{Definition}{Eine Menge $\Delta$ von Formeln hat Konkretisierungen, wenn für alle $\exists x\varphi\in\Delta$ ein variablenloser Term $t$ existiert mit $\varphi[x:=t]\in\Delta$.}
\note{Satz}{Sei $\Delta$ eine maximal konsistente Menge von $\sum$-Formeln. Dann existiert eine Signatur $\sum^+\supseteq\sum$ und eine maximal konsistente Menge von $\sum^+$-Formeln mit Konkretisierungen, so dass $\Delta\subseteq\Delta^+$.}
\note{Satz}{Sei $\Delta^+$ maximal konsistente Menge von $\sum^+$-Formeln mit Konkretisierungen. Dann ist $\Delta^+$ erfüllbar.}
\note{Satz: Vollständigkeitssatz der Prädikatenlogik }{Sei $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Dann gilt $\Gamma\Vdash\varphi\Rightarrow\Gamma\vdash\varphi$.
Insbesondere ist jede allgemeingültige Formel ein Theorem.}
\note{Satz}{Sei $\Gamma$ höchstens abzählbar unendliche und konsistente Menge von Formeln. Dann hat $\Gamma$ ein höchstens abzählbar unendliches Modell.}
\note{Satz}{Seien $\Gamma$ eine Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel. Dann gilt $\Gamma\vdash\varphi\Leftrightarrow\Gamma\Vdash\varphi$.
Insbesondere ist eine $\sum$-Formel genau dann allgemeingültig, wenn sie ein Theorem ist.}
Beweis: Folgt unmittelbar aus Korrektheitssatz und Vollständigkeitssatz.
\subsubsection{Folgerung 1: Kompaktheit}
\note{Satz}{Seien $\Gamma$ eine u.U. unendliche Menge von $\sum$-Formeln und $\varphi$ eine $\sum$-Formel mit $\Gamma\Vdash\varphi$. Dann existiert $\Gamma'\subseteq\Gamma$ endlich mit $\Gamma'\Vdash\varphi$.}
\note{Folgerung (Kompaktheits- oder Endlichkeitssatz)}{Sei $\Gamma$ eine u.U. unendliche Menge von $\sum$-Formeln. Dann gilt $\Gamma$ erfüllbar $\Leftrightarrow\forall\Gamma'\subseteq\Gamma$ endlich: $\Gamma'$ erfüllbar}
\note{Satz}{Sei $\Delta$ eine u.U. unendliche Menge von $\sum$-Formeln, so dass für jedes $n\in\mathbb{N}$ eine endliche Struktur $A_n$ mit $A_\Vdash\Delta$ existiert, die wenigstens $n$ Elemente hat. Dann existiert eine unendliche Struktur $A$ mit $A\Vdash\Delta$.}
Frage: Gibt es eine Menge $\Gamma$ von $\sum$-Formeln, so dass für alle Strukturen $A$ gilt: $A\Vdash\Gamma\Leftrightarrow A\cong(\mathbb{R},+,*, 0 , 1)$?
\note{Satz von Löwenheim-Skolem}{Sei $\Gamma$ erfüllbare und höchstens abzählbar unendliche Menge von $\sum$-Formeln. Dann existiert ein höchstens abzählbar unendliches Modell von $\Gamma$.}
Teste für jede Zeichenkette $w$ nacheinander, ob sie hypothesenlose Deduktion mit Konklusion $\varphi$ ist. Wenn ja, so gib aus ''$\varphi$ ist allgemeingültig''. Ansonsten gehe zur nächsten Zeichenkette über.
Wegen $\varphi$ allgemeingültig $\Leftrightarrow\lnot\varphi$ unerfüllbar reicht es zu zeigen, dass die Menge der erfüllbaren Sätze nicht entscheidbar ist.
\note{Definition}{Eine Horn-Formel ist eine Konjunktion von $\sum$-Formeln der Form $\forall x_1\forall x_2 ...\forall x_n((\lnot\bot\wedge\alpha_1\wedge\alpha_2\wedge...\wedge\alpha_m)\rightarrow\beta)$, wobei $\alpha_1,...,\alpha_m$ und $\beta$ atomare $\sum$-Formeln sind.}
\note{Lemma}{Angenommen, das Korrespondenzsystem $I$ hat keine Lösung. Dann ist die Horn-Formel $\varphi_I=\psi_I \wedge\forall x(R(x,x)\rightarrow x=e)$ erfüllbar.}
\note{Lemma}{Sei $B$ Struktur mit $B\Vdash\psi_I$. Dann gilt $(f_{u_{i_1} u_{i_2} ...u_{i_n}}^B (e^B),f_{v_{i_1} v_{i_2}...v_{i_n}}^B(e^B))\in R^B$ für alle $n\geq0, 1\leq i_1,i_2,...,i_n \leq k$.}
\note{Lemma}{Angenommen, $(i_1,...,i_n)$ ist eine Lösung von $I$. Dann ist die $\sum$-Formel $\varphi_I$ unerfüllbar.}
\note{Satz}{Die Menge der unerfüllbaren Horn-Formeln ist nicht entscheidbar.}
\note{Folgerung (Church 1936)}{Die Menge der allgemeingültigen $\sum$-Formeln ist nicht entscheidbar.}
Beweis: Eine $\sum$-Formel $\varphi$ ist genau dann unerfüllbar, wenn $\lnot\varphi$ allgemeingültig ist. Also ist $\varphi\rightarrow\lnot\varphi$ eine Reduktion der unentscheidbaren Menge der unerfüllbaren $\sum$-Formeln auf die Menge der allgemeingültigen $\sum$-Formeln, die damit auch unentscheidbar ist.
\subsection{Theorie der natürlichen Zahlen}
\note{Definition}{Sei $A$ eine Struktur. Dann ist $Th(A)$ die Menge der prädikatenlogischen $\sum$-Formeln $\varphi$ mit $A\Vdash\varphi$. Diese Menge heißt die(elementare) Theorie von $A$.}
Beispiel: Sei $N=(N,\leq,+,*, 0 , 1)$. Dann gelten
\begin{itemize*}
\item$(\forall x\forall y:x+y=y+x)\in Th(N)$
\item$(\forall x\exists y:x+y=0)\not\in Th(N)$
\item aber $(\forall x\exists y:x+y=0)\in Th((Z,+, 0))$.
\end{itemize*}
\note{Lemma}{Die Menge $Th(N)$ aller Sätze $\varphi$ mit $N\Vdash\varphi$ ist nicht entscheidbar.}
\note{Zahlentheoretisches Lemma}{Für alle $n\in N,x_0,x_1,...,x_n\in N$ existieren $c,d\in N$, so dass für alle $0\leq i\leq n$ gilt: $x_i=c\ mod (1+d*(i+1))$.}
\note{Satz}{Sei $A$ eine Struktur, so dass $Th(A)$ semi-entscheidbar ist. Dann ist $Th(A)$ entscheidbar.}
\note{Korollar}{Die Menge $TH(N)$ der Aussagen $\varphi$ mit $N\Vdash\varphi$ ist nicht semi-entscheidbar.}
\note{Korollar (1. Gödelscher Unvollständigkeitssatz)}{Sei $Gamma$ eine semi-entscheidbare Menge von Sätzen mit $N\Vdash\gamma$ für alle $\gamma\in\Gamma$. Dann existiert ein Satz $\varphi$ mit $\Gamma\not\vdash\varphi$ und $\Gamma\not\vdash\lnot\varphi$ (d.h. ''$\Gamma$ ist nicht vollständig'').}
\note{Definition}{Zwei $\sum$-Formeln $\varphi$ und $\psi$ heißen erfüllbarkeitsäquivalent, wenn gilt: $\varphi$ ist erfüllbar $\Leftrightarrow\psi$ ist erfüllbar}
\subsubsection{Elimination von Gleichungen}
\note{Definition}{Eine $\sum$-Formel ist gleichungsfrei, wenn sie keine Teilformel der Form $s=t$ enthält. }
Idee: Die Formel $\varphi'$ entsteht aus $\varphi$, indem alle Teilformeln der Form $x=y$ durch $GI(x,y)$ ersetzt werden, wobei $GI$ ein neues Relationssymbol ist.
Notationen
\begin{itemize*}
\item Sei $\sum=(\Omega,Rel,ar)$ endliche Signatur und $\varphi$$\sum$-Formel
\item$\sum_{GI}=(\Omega, Rel\bigcup^+\{GI\},ar_{GI})$ mit $ar_{GI}(f)$ für alle $f\in\Omega\cup Rel$ und $ar_{GI}(GI)=2$
\item Für eine $\sum$-Formel $\varphi$ bezeichnet $\varphi_{GI}$ die $\sum_{GI}$-Formel, die aus $\varphi$ entsthet, indem alle Vorkommen und Teilformen $s=t$ durch $GI(s,t)$ ersetzt werden.
\end{itemize*}
\note{Definition}{Sei A eine $\sum$-Struktur und $\sim$ eine binäre Relation auf $U_A$. Die Relation $\sim$ heißt Kongruenz auf A, wenn gilt:
\begin{itemize*}
\item$\sim$ ist eine Äquivalentrelation (d.h. reflexiv, transitiv und symmetrisch)
\item für alle $f\in\Omega$ mit $k=ar(f)$ und alle $a_1,b_1,...,a_k,b_k\in U_A$ gilt $a_1\sim b_1,a_2\sim b_2,...,a_k\sim b_k\Rightarrow f^A(a_1,...,a_k)\sim f^A(b_1,...,b_k)$
\item für alle $R\in Rel$ mit $k=ar(R)$ und alle $a_1,b_1,...,a_k,b_k\in U_A$ gilt $a_1\sim b_1,...,a_k\sim b_k,(a_1,...,a_k)\in R^A\Rightarrow(b_1,...,b_k)\in R^A$.
\end{itemize*}
}
\note{Definition}{Sei $A$ eine $\sum$-Struktur und $\sim$ eine Kongruenz auf A.
\begin{enumerate*}
\item Für $a\in U_A$ sei $[a]=\{b\in U_A|a\sim b\}$ die Äquivalenzklasse von a bzgl $\sim$.
\item Dann definieren wir den Quotienten $B=A\backslash\sim$ von $A$ bzgl $\sim$ wie folgt:
\begin{itemize*}
\item$U_B=U_A\backslash\sim=\{[a]|a\in U_A\}$
\item Für jedes $f\in\Omega$ mit $ar(f)=k$ und alle $a_1,...,a_k\in U_A$ setzten wir $f^B([a_1],...,[a_k])=[f^A(a_1,...,a_k)]$
\item für jede $R\in Rel$ mit $ar(R)=k$ setzten wir $R^B=\{([a_1],[a_2],...,[a_k])|(a_1,...,a_k)\in R^A\}$
\end{itemize*}
\item Sei $p:Var\rightarrow U_A$ Variableninterpretation. Dann definieren die Variableninterpretation $p\backslash\sim: Var\rightarrow U_B:x\rightarrow[p(x)]$.
\end{enumerate*}
}
\note{Lemma 1}{Sei A Struktur, $p:Var\rightarrow U_A$ Variableninterpretation und $\sim$ Kongruenz. Seien weiter $B=A\backslash\sim$ und $p_B=p\backslash\sim$. Dann gilt für jeden Term $:[p(t)]=p_B(t)$}
\note{Lemma 2}{Sei $A$$\sum$-Struktur, $\sim$ Kongruenz und $B=A\backslash\sim$. Dann gilt für alle $R\in Rel$ mit $k=ar(R)$ und alle $c_1,...,c_k\in U_A$: $([c_1],[c_2],...,[c_k])\in R^B\Leftrightarrow(c_1,c_2,...,c_k)\in R^A$}
\note{Satz}{Seien $A$$\sum_{GI}$-Struktur und $p:Var\rightarrow U_A$ Variableninterpretation, so dass $\sim=GI^A$ Kongruenz auf A ist.
Seien $B=A\backslash\sim$ und $p_B=p\backslash\sim$.
Dann gilt für alle $\sum$-Formeln $\varphi: A\Vdash_p \varphi_{GI}\Leftrightarrow B\Vdash_{p_B}\varphi$
}
\note{Lemma}{Aus einer endlichen Signatur $\sum$ kann ein gleichungsfreuer Horn-Satz $Kong_{\sum}$ über $\sum_{GI}$ berechnet werden, so dass für alle $\sum_{GI}$-Strukturen $A$ gilt: $A\Vdash Kong_{\sum}\Leftrightarrow GI^A$ ist eine Kongruenz}
\note{Satz}{Aus einer endlichen Signatur $\sum$ und einer $\sum$-Formel $\varphi$ kann eine gleichungsfreie und erfüllbarkeitsäquivalente $\sum_{GI}$-Formel $\varphi'$ berechnet werden. Ist $\varphi$ Horn Formel, so ist auch $\varphi'$ Horn Formel.}
\subsection{Skolemform}
Ziel: Jede $\sum$-Formel $\varphi$ ist erfüllbarkeitsäquivalent zu einer $\sum$'-Formel $\varphi'=\forall x_1\forall x_2 ...\forall x_k \psi$, wobei $\psi$ kein Quantoren enthält, $\varphi'$ heißt in Skolemform.
2 Schritte:
\begin{enumerate*}
\item Quantoren nach vorne (d.h. Pränexform)
\item Existenzquantoren eliminieren
\end{enumerate*}
\note{Definition}{Zwei $\sum$-Formeln $\varphi$ und $\psi$ sind äquivalent (kurz:$\varphi\equiv\psi$), wenn für alle $\sum$-Strukturen $A$ und alle Variableninterpretationen $\rho$ gilt: $A\Vdash_{\rho}\psi\Leftrightarrow A\Vdash_{\rho}\psi$.}
\note{Lemma}{Seien $Q\in\{\exists ,\forall\}$ und $\oplus\in\{\wedge,\vee,\rightarrow,\leftarrow\}$. Sei $\varphi=(Qx \alpha)\oplus\beta$ und sei $y$ eine Variable, die weder in $\alpha$ noch in $\beta$ vorkommt. Dann gilt $\varphi\equiv\begin{cases} Qy(\alpha[x:=y]\oplus\beta)\text{ falls }\oplus\in\{\wedge,\vee,\leftarrow\}\\\forall y(\alpha[x:=y]\rightarrow\beta)\text{ falls }\oplus=\rightarrow,Q=\exists\\\exists y(\alpha[x:=y]\rightarrow\beta)\text{ falls }\oplus=\rightarrow,Q=\forall\end{cases}$}
\note{Lemma}{Seien $Q\in\{\exists,\forall\}$ und $\oplus\in\{\wedge,\vee,\rightarrow,\leftarrow\}$. Sei $\varphi=(Qx\alpha)\oplus\beta$ und sei $y$ eine Variable, die weder in $\alpha$ noch in $\beta$ vorkommt. Dann gilt $\varphi\equiv\begin{cases} Qy(\alpha[x:=y]\oplus\beta)\text{ falls }\oplus\in\{\wedge,\vee,\leftarrow\}\\\forall y(\alpha[x:=y]\rightarrow\beta)\text{ falls }\oplus=\rightarrow,Q=\exists\\\exists y(\alpha[x:=y]\rightarrow\beta)\text{ falls }\oplus=\rightarrow,Q=\forall\end{cases}$}
\note{Satz}{Aus einer endlichen Signatur $\sum$ und einer $\sum$-Formel $\varphi$ kann eine äquivalente $\sum$-Formel $\varphi'=Q_1 x_1 Q_2 x_2 ...Q_k x_k \psi$ (mit $Q_i\in\{\exists,\forall\},\psi$ quantorenfrei und $x_i$ paarweise verschieden) berechnet werden. Eine Formel $\varphi'$ dieser Form heißt Pränexform. Ist $\varphi$ gleichungsfrei, so ist auch $\varphi'$ gleichungsfrei.}
\item eliminiere $\exists$-Quantoren durch Einführen neuer Funktionssymbole
\end{enumerate*}
\note{Lemma}{Die Formeln $\varphi$ und $\varphi'$ sind erfüllbarkeitsäquivalent.}
\note{Satz}{Aus einer Formel $\varphi$ kann man eine erfüllbarkeitsäquivalente Formel $\varphi$ in Skolemform berechnen. Ist $\varphi$ gleichungsfrei, so auch $\varphi$.}
\subsection{Herbrand-Strukturen und Herbrand-Modelle}
Sei $\sum=(\Omega,Rel,ar)$ eine Signatur. Wir nehmen im folgenden an, dass $\Omega$ wenigstens ein Konstantensymbol enthält.
Das Herbrand-Universum $D(\sum)$ ist die Menge aller variablenfreien $\sum$-Terme.
Beispiel: $\Omega=\{b,f\}$ mit $ar(b)=0$ und $ar(f)=1$. Dann gilt $D(\sum)=\{b,f(b),f(f(b)),f(f(f(b))),...\}$
\note{Satz}{Sei $\varphi$ eine gleichungsfreie Aussage in Skolemform. $\varphi$ ist genau dann erfüllbar, wenn $\varphi$ ein Herbrand-Modell besitzt.}
Ist $\psi$ eine quantoren- und gleichungsfreie Aussage, so gilt $A\vdash_{\rho}\psi\Leftrightarrow B\vdash_{\rho B}\psi$. Diese Behauptung wird induktiv über den Aufbau von $\psi$ gezeigt.
Ist $\psi$ eine gleichungsfreie Aussage in Skolemform, so gilt $A\vdash_\rho\psi\Rightarrow B\vdash_{\rho B}\psi$ (hieraus folgt dann $B\vdash_{\rho B}\varphi$ wegen $A\vdash_\rho\varphi$). Diese Behauptung wird induktiv über die Anzahl $n$ der Quantoren in $\psi$ bewiesen.
\item hat als Universum das Herbrand-Universum $D(\sum)=\{a,f(a),f^2(a),...\}=\{f^n(a)|n\geq0\}$
\item erfüllt $f^A(f^n(a))= f^{n+1}(a)$ für alle $n\geq0$
\end{itemize*}
\note{Konstruktion}{Sei $B:\{P(t_1,...,t_k)|P\in Rel,k=ar(P),t_1,...,t_k\in D(\sum)\}\rightarrow B$ eine
B-Belegung. Die hiervon induzierte Herbrand-Struktur $A_B$ ist gegeben durch $P^{A_B}=\{(t_1,...,t_k)|t_1,...,t_k\in D(\sum),B(P(t_1,...,t_k))=1\}$ für alle $P\in Rel$ mit $ar(P)=k$. }
\note{Lemma}{Für jede quantoren- und gleichungsfreie Aussage $\alpha$ und jede Variableninterpretation $\rho$ in $A_B$ gilt $A_B\Vdash_\rho\alpha\Leftrightarrow B(\alpha)=1$.}
\note{Lemma}{Sei $\varphi=\forall y_1\forall y_2 ...\forall y_n\psi$ gleichungsfreie Aussage in Skolemform. Sie hat genau dann ein Herbrand-Modell, wenn die Formelmenge $E(\varphi)$ (im aussagenlogischen Sinn) erfüllbar ist.}
\note{Satz von Gödel-Herbrand-Skolem}{Sei $\varphi$ gleichungsfreie Aussage in Skolemform. Sie ist genau dann erfüllbar, wenn die Formelmenge $E(\varphi)$ (im aussagenlogischen Sinn) erfüllbar ist.}
\note{Satz von Herbrand}{Eine gleichungsfreie Aussage $\varphi$ in Skolemform ist genau dann unerfüllbar, wenn es eine endliche Teilmenge von $E(\varphi)$ gibt, die (im aussagenlogischen Sinn) unerfüllbar ist. (Jacques Herbrand (1908-1931))}
\item Wir müssen die Unerfüllbarkeit einer gleichungsfreien Horn-Formel der Prädikatenlogik testen.
\item Ist $\varphi$ gleichungsfreie Horn-Klausel der Prädikatenlogik, so ist $E(\varphi)$ eine Menge von Horn-Klauseln der Aussagenlogik.
\end{itemize*}
Schreib- und Sprechweise
\begin{itemize*}
\item$\{\alpha_1,\alpha_2,...,\alpha_n\}\rightarrow\beta$ für Horn-Klausel der Prädikatenlogik $(\lnot\bot\wedge\alpha_1\wedge\alpha_2\wedge...\wedge\alpha_n)\rightarrow\beta$ insbes. $\varnothing\rightarrow\beta$ für $\lnot\bot\rightarrow\beta$
\item$\{(N_i\rightarrow\beta_i) | 1\leq i\leq m\}$ für Horn-Formel $\bigwedge_{1\leq i\leq m}(N_i\rightarrow\beta_i)$
\end{itemize*}
Folgerung: Sei $\varphi=\bigwedge_{1\leq i\leq n}\varphi_i$ gleichungsfreie Horn-Formel der Prädikatenlogik. Dann ist $\varphi$ genau dann unerfüllbar, wenn $\bigcup_{1\leq i\leq n} E(\varphi_i)$ im aussagenlogischen Sinne unerfüllbar ist.
Folgerung: Eine gleichungsfreie Horn-Formel der Prädikatenlogik $\varphi=\bigwedge_{1\leq i\leq n}\varphi_i$ ist genau dann unerfüllbar, wenn es eine SLD-Resolution $(M_0\rightarrow\bot,M_1\rightarrow\bot,...,M_m\rightarrow\bot)$ aus $\bigcup_{1\leq i\leq n} E(\varphi_i)$ mit $M_m =\varnothing$ gibt.
\subsection{Substitutionen}
Eine verallgemeinerte Substitution $\sigma$ ist eine Abbildung der Menge der Variablen in die Menge aller Terme, so daß nur endlich viele Variable $x$ existieren mit $\sigma(x)\not=x$.
Sei $Def(\sigma)=\{x\ Variable|x\not=\sigma(x)\}$ der Definitionsbereich der verallgemeinerten Substitution $\sigma$. Für einen Term $t$ definieren wir den Term $t\sigma$ wie folgt induktiv:
\note{Lemma}{Seien $\sigma$ Substitution, $x$ Variable und $t$ Term, so dass
\begin{itemize*}
\item (i) $x\not\in Def(\sigma)$ und
\item (ii) $x$ in keinem der Terme $y\sigma$ mit $y\in Def(\sigma)$ vorkommt.
Dann gilt $[x:=t]\sigma=\sigma[x:=t\sigma]$.
\end{itemize*}
}
\subsection{Unifikator/Allgemeinster Unifikator}
Gegeben seien zwei gleichungsfreie Atomformeln $\alpha$ und $\beta$. Eine Substitution $\sigma$ heißt Unifikator von $\alpha$ und $\beta$, falls $\alpha\sigma=\beta\sigma$.
Ein Unifikator $\sigma$ von $\alpha$ und $\beta$ heißt allgemeinster Unifikator von $\alpha$ und $\beta$, falls für jeden Unifikator $\sigma'$ von $\alpha$ und $\beta$ eine Substitution $\tau$ mit $\sigma'=\sigma\tau$ existiert.
\note{Lemma}{Sind $\sigma_1$ und $\sigma_2$ allgemeinste Unifikatoren von $\alpha$ und $\beta$, so existiert eine Variablenumbenennung $\rho$ mit $\sigma_2=\sigma_1\rho$.}
\item (C) Wenn die Eingabe $(\alpha,\beta)$ unifizierbar ist, dann findet der Unifikationsalgorithmus einen allgemeinsten Unifikator von $\alpha$ und $\beta$.
\end{itemize*}
}
\note{Lemma (A)}{Der Unifikationsalgorithmus terminiert für jede Eingabe($\alpha$, $\beta$).}
\note{Lemma (C1)}{Sei $\sigma'$ ein Unifikator der Eingabe $(\alpha,\beta)$, so dass keine Variable aus $\alpha$ oder $\beta$ auch in einem Term aus $\{y\sigma'|y\in Def(\sigma')\}$ vorkommt. Dann terminiert der Unifikationsalgorithmus erfolgreich und gibt einen Unifikator $\sigma$ von $\alpha$ und $\beta$ aus. Außerdem gibt es eine Substitution $\tau$ mit $\sigma'=\sigma\tau$.}
\item Nach (2) terminiert der Algorithmus erfolgreich mit der Substitution $\sigma_N$. Daher gilt aber $\alpha\sigma_N=\beta\sigma_N$, d.h. $\sigma_N$ ist ein Unifikator.
\item Nach (1) gibt es auch eine Substitution $\tau_n$ mit $\sigma'=\sigma_N\tau_n$.
\note{Lemma (C)}{Sei die Eingabe $(\alpha,\beta)$ unifizierbar. Dann terminiert der Unifikationsalgorithmus erfolgreich und gibt einen allgemeinsten Unifikator $\sigma$ von $\alpha$ und $\beta$ aus.}
\item (C) Wenn die Eingabe $(\alpha,\beta)$ unifizierbar ist, dann findet der Unifikationsalgorithmus immer einen allgemeinsten Unifikator von $\alpha$ und $\beta$.
\note{Definition}{Sei $\Gamma$ eine Menge von gleichungsfreien Horn-Klauseln der Prädikatenlogik. Eine SLD-Resolution aus $\Gamma$ ist eine Folge $((M_0\rightarrow\bot,\sigma_0),(M_1\rightarrow\bot,\sigma_1),...,(M_m\rightarrow\bot,\sigma_m))$ von Horn-Klauseln und Substitutionen mit
\begin{itemize*}
\item$(M_0\rightarrow\bot)\in\Gamma$ und $Def(\sigma_0)=\varnothing$
\item für alle $0\leq n<m$ existieren $\varnothing\not=Q\subseteq M_n,(N\rightarrow\alpha)\in\Gamma$ und Variablenumbenennung $\rho$, so dass
\begin{itemize*}
\item$(N\cup\{\alpha\})\rho$ und $M_n$ variablendisjunkt sind,
\item$\sigma_{n+1}$ ein allgemeinster Unifikator von $\alpha\rho$ und $Q$ ist und
\item Es gibt eine SLD-Resolution $((M_n\rightarrow\bot,\sigma_n))_{0\leq n\leq m}$ aus $\Gamma\cup\{M_0\rightarrow\bot\}$ mit $M_0=\{\Psi(x_1,...,x_{\iota})\}$ und $M_m=\varnothing$ und eine Substitution $\tau$, so dass $s_i=x_i\sigma_0\sigma_1 ...\sigma_m\tau$ für alle $1\leq i\leq\iota$ gilt.
\note{Lemma}{Sei $\Gamma$ Menge von gleichungsfreien Horn-Klauseln der Prädikatenlogik und $(M_n \rightarrow\bot,\sigma_n))_{0\leq n\leq m}$ eine SLD-Resolution aus $\Gamma\cup\{M_0\rightarrow\bot\}$ mit $M_m=\varnothing$.
Dann gilt $\Gamma\Vdash\Psi\sigma_0\sigma_1\sigma_2...\sigma_m$ für alle $\Psi\in M_0$.}
\note{Lemma}{Sei $\Gamma$ eine Menge von definiten gleichungsfreien Horn-Klauseln der Prädikatenlogik, sei $M\rightarrow\bot$ eine gleichungsfreie Horn-Klausel und sei $\nu$ Substitution, so dass $M\nu$ variablenlos ist und $\Gamma\Vdash M\nu$ gilt. Dann existieren eine prädikatenlogische SLD-Resolution $((M_n \rightarrow\bot,\sigma_n))_{0\leq n\leq m}$ und eine Substitution $\tau$ mit $M_0=M,M_m=\varnothing$ und $M_0\sigma_0\sigma_1... \sigma_m \tau=M_{\nu}$.}
\note{Satz}{Sei $\Gamma$ eine Menge von definiten gleichungsfreien Horn-Klauseln der Prädikatenlogik, sei $M\rightarrow\bot$ eine gleichungsfreie Horn-Klausel und sei $\nu$ Substitution, so dass $M\nu$ variablenlos ist. Dann sind äquivalent:
\begin{itemize*}
\item$\Gamma\Vdash M\nu$
\item Es existieren eine SLD-Resolution $((M_n\rightarrow\bot,\sigma_n))_{0\leq n\leq m}$ aus $\Gamma\cup\{M\nu\rightarrow\bot\}$ und eine Substitution $\tau$ mit $M_0=M,M_m=\varnothing$ und $M_0\sigma_0\sigma_1...\sigma_m\tau=M\nu$.
\item Die SLD-Resolution ist ein praktikables Verfahren, um die Menge der ''Lösungen'' $(s_1,...,s_{\iota})$ von $\Gamma\Vdash\psi(s_1,...,s_{\iota})$ zu bestimmen (wobei $\Gamma$ Menge von gleichungsfreien Horn-Klauseln und $\psi$ Konjunktion von gleichungsfreien Atomformeln sind.
\item Über HORN-Klauseln gibt es ein korrektes und vollständiges Ableitungsverfahren. $\{K_1, ...,K_n\}\Vdash H$ , gdw. $\{K_1,...,K_n\}\vdash_{ROB} H$
\item Eine Menge von HORN-Klauseln mit nichtleeren Klauselköpfen ist stets erfüllbar; es lassen sich keine Widersprüche formulieren. $K_1\wedge K_2...\wedge K_n \not= false$
\item Erzeugung der Konjunktiven Normalform (KNF): Durch systematische Anwendung des Distributivgesetzes $A\vee(B\wedge C)\equiv(A\vee B)\wedge(A\vee C)$
\item Erzeugung der Klauselform (KF): Jede der Elementardisjunktionen $(L_1^j \vee...\vee L_1^{j_k})$ der KNF kann man als äquivalente Implikation (Klausel) $(L_i^j \vee...\vee L_i^{j_m})\leftarrow(L_1^{j_{m+1}}\wedge ...\wedge L_1^{j_k})$ notieren, indem man alle positiven Literale $L_i^j,...,L_i^{j_m}$ disjunktiv verknüpft in den DANN-Teil (Klauselkopf) und alle negativen Literale $L_i^{j_{m+1}},...,L_i^{j_k}$ konjunktiv verknüpft in den WENN-Teil (Klauselkörper) notiert.
\item In dem Spezialfall, dass alle Klauselköpfe dabei aus genau einem Literal bestehen, war die systematische Erzeugung von HORN-Klauseln erfolgreich; anderenfalls gelingt sie auch nicht durch andere Verfahren.
\subsubsection{Inferenz in PROLOG: Resolution nach ROBINSON}
\note{Satz von ROBINSON}{$M'\equiv\bigwedge_{i=1}^n K_i\wedge\lnot H$ ist kontradiktorisch ($kt\ M‘$), gdw. durch wiederholte Resolutionen in endlich vielen Schritten die negierte Hypothese $\lnot H\equiv false \leftarrow H$ durch die leere Klausel $false\leftarrow true$ ersetzt werden kann.}
\item Substitutionen, die zwei Terme syntaktisch identisch machen, heißen Unifikator: $\nu$unifiziert zwei Atomformeln $s$ und $t$, falls dessen Einsetzung $s$ und $t$ syntaktisch identisch macht.
Die Unifizierbarkeit zweier Terme richtet sich nach deren Sorte:
\begin{enumerate*}
\item Zwei Konstanten $t_1$ und $t_2$ sind unifizierbar, gdw. $t_1= t_2$
\item Zwei strukturierte Terme $f(t_{11},...,t_{1n})$ und $f(t_{21},...,t_{2n})$ sind unifizierbar, gdw.
\begin{itemize*}
\item sie die gleichen Funktionssymbole aufweisen ($f_1= f_2$),
\item sie die gleichen Stelligkeiten aufweisen ($n=m$) und
\item die Terme $t_{1i}$ und $t_{2i}$ jeweils miteinander unifizierbar sind.
\end{itemize*}
\item Eine Variable $t_1$ ist mit einer Konstanten oder einem strukturierten Term $t_2$ unifizierbar. $t_1$ wird durch $t_2$ ersetzt (instanziert): $t_1:= t_2$
\item Zwei Variablen $t_1$ und $_2$ sind unifizierbar und werden gleichgesetzt: $t_1:=t_2$ bzw. $t_2:= t_1$
\item die Substitution $\nu$ ein Unifikator von $s$ und $t$ ist und
\item für jeden anderen Unifikator $\sigma$ von $s$ und $t$ eine nichtleere und nicht identische Substitution $\tau$ existiert, so dass $\sigma=\tau\circ\nu$ ist.
Was darf der Programmierer erwarten? Dass das ''Deduktionstool'' PROLOG $M \Vdash H$ zu zeigen versucht, indem systematisch die Resolutionsmethode auf $\lnot H$ und eine der Klauseln aus $M$ angewandt wird, solange bis $\lnot H\equiv false\leftarrow true$ entsteht
Es werden anwendbare Klauseln für das erste Teilziel gesucht. Gibt es ...
\begin{itemize*}
\item ... genau eine, so wird das 1. Teilziel durch deren Körper ersetzt.
\item ... mehrere, so wird das aktuelle Ziel inklusive alternativ anwendbarer Klauseln im Backtrack-Keller abgelegt und die am weitesten oben stehende Klausel angewandt.
\item ... keine (mehr), so wird mit dem auf dem Backtrack-Keller liegendem Ziel die Bearbeitung fortgesetzt.
\end{itemize*}
Dies geschieht solange, bis
\begin{itemize*}
\item das aktuelle Ziel leer ist oder
\item keine Klausel (mehr) anwendbar ist und der Backtrack-Keller leer ist.
Zusätzliche Markierung der Kanten mit der Variablenersetzung (dem Unifikator).
\subsubsection{PROLOG aus prozeduraler Sicht}
\note{Deklarative Interpretation}{In einem Objektbereich $I=\{mueller, mayer, schulze, ...\}$ bildet das Prädikat $weisungsrecht(X,Y)$$[X,Y]$ auf wahr ab, gdw.
\begin{itemize*}
\item das Prädikat $chef_von(X,Y)$ das Paar $[X,Y]$ auf wahr abbildet oder
\item es ein $Z\in I$ gibt, so dass
\begin{itemize*}
\item das Prädikat $chef_von(X,Z)$ das Paar $[X,Z]$ auf wahr abbildet und
\item das Prädikat $weisungsrecht(Z,Y)$ das Paar $[Z,Y]$ auf wahr abbildet.
\end{itemize*}
\end{itemize*}
}
\note{Prozedurale Interpretation}{Die Prozedur $weisungsrecht(X,Y)$ wird abgearbeitet, indem
\begin{enumerate*}
\item die Unterprozedur $chef_von(X,Y)$ abgearbeitet wird. Im Erfolgsfall ist die Abarbeitung beendet; anderenfalls werden
\item die Unterprozeduren $chef_von(X,Z)$ und $weisungsrecht(Z,Y)$ abgearbeitet; indem systematisch Prozedurvarianten beider Unterprozeduren aufgerufen werden. Dies geschieht bis zum Erfolgsfall oder erfolgloser erschöpfender Suche.
Prädikate zur Steuerung der Suche nach einer Folge von Resolutionsschritten!
Das Prädikat $!/0$ ist stets wahr. In Klauselkörpern eingefügt verhindert es ein Backtrack der hinter $!/0$ stehenden Teilziele zu den vor $!/0$ stehenden Teilzielen sowie zu alternativen Klauseln des gleichen Kopfprädikats. Die Verarbeitung von $!/0$ schneidet demnach alle vor der Verarbeitung verbliebenen Lösungswege betreffenden Prozedur ab.
Eine Prozedur heißt rekursiv, wenn in mindestens einem der Klauselkörper ihrer Klauseln ein erneuter Aufruf des Kopfprädikates erfolgt.
Ist der Selbstaufruf die letzte Atomformel des Klauselkörpers der letzten Klausel dieser Prozedur - bzw. wird er es durch vorheriges ''Abschneiden'' nachfolgender
\item Zwei nichtleere Listen $[K_1|R_1]$ und $[K_2|R_2]$ sind miteinander unifizierbar, wenn ihre Köpfe ($K_1$ und $K_2$) und ihre Restlisten ($R_1$ und $R_2$) jeweils miteinander unifizierbar sind.
\item Eine Liste $L$ und eine Variable $X$ sind miteinander unifizierbar, wenn die Variable selbst nicht in der Liste enthalten ist. Die Variable $X$ wird bei erfolgreicher Unifikation mit der Liste $L$ instanziert: $X:=L$.
\item Die Differenz aus einer leeren Liste und einer (beliebigen) Liste ist die leere Liste: $[]- L =[]$
\item Die Differenz aus einer Liste $[E|R]$ und der Liste $L$, welche $E$ enthält, ist die Liste $D$,
wenn die Differenz aus $R$ und $L$ (abzügl. $E$) die Liste $D$ ist: $[E|R]-L = D$, wenn $E\in L$ und $R-(L-[E])= D$
\item Die Differenz aus einer Liste $[E|R]$ und einer Liste $L$, welche $E$ nicht enthält, ist die Liste $[E|D]$, wenn die Differenz aus $R$ und $L$ die Liste $D$ ist: $[E|R]- L =[E|D]$, wenn $E\in L$ und $R-L=D$
\item Alternierende Zielklauseln: Ein aktuelles Ziel wiederholt sich und die Suche nach einer Folge von Resolutionsschritten endet nie oder die Suche nach Resolutionsschritten endet mit einem Überlauf des Backtrack-Kellers
\item Expandierende Zielklauseln: Das erste Teilziel wird in jeden Resolutionsschritt durch mehrere neue Teilziele ersetzt; die Suche endet mit einem Speicherüberlauf
\item Metalogische Prädikate und konstruktive Lösungen: Das Prädikat $not/1$ hat eine Aussage als Argument und ist somit eine Aussage über eine Aussage, also metalogisch.
\item Für die systematische Suche eines Pfades kann der Suchprozess einer Folge von Resolutionsschritten genutzt werden. Man muss den Suchprozess nicht selbst programmieren.
\item Für eine heuristische Suche eines Pfades gilt Botschaft 4: Sie ist das klassische Einsatzgebiet zahlreicher KI-Tools - auch der Logischen Programmierung.
\item ''Logeleien'' sind oft Aussagen über Belegungen von Variablen mit endlichem Wertebereich, ergänzt um eine Frage zu einem nicht explizit gegebenen Wert.
\item Dabei handelt es sich um Grunde um eine Deduktionsaufgabe mit einer Hypothese zu einem mutmaßlichen Wert der gesuchten Variablen. Deshalb ist es oft auch mit dem ''Deduktionstool'' Prolog lösbar, denn Prolog tut im Grunde nichts anderes als ein ziel-gerichtetes ''Durchprobieren'' legitimer Deduktionsschritte im ''Generate - and - Test'' - Verfahren.
\item Auch hier geht es oft um gesuchte Werte für Variablen. Deshalb ist es oft auch mit dem ''Deduktionstool'' Prolog lösbar, denn Prolog tut im Grunde nichts anderes als ein ziel-gerichtetes ''Durchprobieren'' legitimer Deduktionsschritte im ''Generate - and - Test'' - Verfahren.
