Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ja, herzlich willkommen. Wir haben uns in der letzten Sitzung angesehen, die Syntax und Semantik

von Aussagen, Logik und wie eingangs angekündigt gehört zu einer anständigen Logik auch noch ein

formales Deduktionssystem und für Aussagen Logik werden wir uns ein solches jetzt anschauen.

So, Moment, was hatten wir gesagt?

Hinten nach vorne hatten wir letztes Mal gesagt, ne?

Aber nicht ernst und Bacon, was ist das?

Also, formale Deduktion zunächst in der Aussagenlogik.

Ja, was heißt formale Deduktion? Formale Deduktion heißt, wir leiten eben Formeln,

hin her als, ja in irgendeinem Sinne gültig, das werden wir später präzisieren,

durch syntaktische Manipulation. Das heißt, wir entfernen uns von der Bedeutung der Formel, wir vergessen,

dass die Formel etwas bedeutet. Wir sehen die Formel schlicht und einfach als String.

Und wir haben Manipulationsregeln, die uns gestatten, diese Strings auseinanderzunehmen

und auf andere Weise wieder zusammenzusetzen und die uns erlauben, auf diese Weise von einer gültigen Formel zur nächsten zu gelangen.

Das hat dann am Ende hoffentlich was zu tun mit der Bedeutung der Formel, sonst wäre es eine sinnlose Tätigkeit.

Aber diese Verbindung, die kommt eben nachher. Also wir haben separat die Semantik definiert, wir definieren separat

die syntaktische Manipulation von Formeln zu ihrer formalen Herleitung und wir setzen die beiden dann hinterher in Beziehung.

Ein typisches Deduktionssystem setzt sich aus zweierlei Artenmaschinerie zusammen, aus Axiomen und aus Regeln.

Axiome sind Dinge, die wir einfach mal so eben ohne weitere Entschuldigung hinschreiben dürfen.

Regeln sind Vorgehensweisen, wie man einem sagen, wie man sich aus schon hingeschriebenem Zeugs die Erlaubnis herleitet,

oder das Zeug hinzuschreiben. Meistens haben Regeln die folgende Form.

Sie beinhalten einen Strich, der zwei Dinge trennt. Oberhalb des Strichs befindet sich eine oder mehrere Prämissen

und unterhalb des Strichs finde ich die sogenannte Konklusion.

Und die Regel sagt uns nicht, ich darf die Konklusion herleiten,

wenn bereits alle Prämissen hergeleitet sind.

Dann gibt es noch so einen Platz rechts neben der Regel.

Da finde ich eventuell sogenannte Seitenbedingungen.

Das sind also Bedingungen, die erfüllt sein müssen, damit ich die Regel anwenden kann, die nicht in der Syntax der Logik formuliert sind,

sondern die zum Beispiel weitere syntaktische Einschränkungen an die Formeln sind, die da vorkommen.

Das heißt, ich, die dürfen bestimmte Variablen erwähnen oder nicht erwähnen, solches Zeugs.

Das kann sehr weit gehen. Im schlimmsten Fall, einer der aktuellen Programmverifikationslogiken,

da finden sich sogar semantische Seitenbedingungen in der Formel.

Die Formel darf angewandt werden, wenn bestimmte Sachen semantisch gelten. Das ist natürlich abenteuerlich, aber das gibt es auch.

Bei uns sind die Seitenbedingungen immer harmlos.

Das ist die grundsätzliche Struktur eines Regelsystems oder eines Deluktionssystems.

Malen wir mal ein Beispiel einer Regel hin, die in unserem Kontext der Aussagenlogik sinnvoll wäre.

Da male ich mal hin zwei Prämissen. Meistens haben diese Regeln eine Form, wo keine konkrete Syntax oben steht,

sondern wo Formeln mit Platzhaltern gewissermaßen stehen. Das hier sind zwei Formeln mit Platzhaltern.

Die eine besteht nur aus dem Platzhalter, ich nenne ihn mal Phi. Die andere besteht aus zwei Platzhaltern, Phi und Phi,

verbunden durch eine Implikation. Das soll heißen, da darf ich für Phi und Phi beliebige Aussagenlogische Formel einsetzen.

Ich fahre hier rechts mal hin.

Phi und Phi sind Platzhalter für Formeln.

Als Konklusion habe ich dann Phi. Die Regel sagt mir, wenn ich Phi impliziert,

dann darf ich Psi herleiten.

Diese Formel illustriert sehr gut den Unterschied zwischen einer Regel und einer einfachen Implikation in der Logik.

Wie viele von Ihnen kennen noch das Douglas-Rufstatter-Buch Gödel-Escher-Bach? Einer.

Also früher, also vor zehn Jahren, werden ja alle am hochgegangen. Okay, so ändern sich also die Geschmäcker in Literatur.

Also ein sehr lesenswertes Buch, gerade für Informatiker. Da kommt vor ein Dialog zwischen Achilles und der Schildkröte.

Der ist nicht von Hofstatter, der ist da nur abgedruckt. Der stammt von einem bekannten Mathematiker, nämlich von Louis Caroll,

der zufällig auch Alice in Wonderland geschrieben hat.