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

Ja, herzlich willkommen zu diesem leicht verspäteten Anfang. Thema heute formale

Deduktion. Wir haben letztes Mal kennengelernt den Begriff der logischen

Folgerung. Wann ist eine Formel in einem formal festnagelbaren Sinn eine

logische Folgerung aus einer Menge von Annahmen? Das hatten wir rein semantisch

definiert. Wir haben gesagt, okay, also eine Formel ist eine logische Folgerung aus

einer Menge von Annahmen, wenn sobald alle Annahmen von einer Wahrheitsbelegung

erfüllt werden, auch diese angebliche logische Folgerung erfüllt wird.

Das ist jetzt zunächst mal nur eine Definition. Wir haben letztes Mal einen

Algorithmus kennengelernt, mit dem man solche logischen Folgerungen auch

überprüfen kann, der nur allerdings sehr ineffizient war. Wir lernen heute eine

anders gelagerte Methode kennen, logische Folgerungen syntaktisch zu

überprüfen, und zwar indem wir uns ansehen einen Beweiskalkül, indem wir

also mittels geeigneter syntaktischer Maschinerie aus den Annahmen

schrittweise Folgerungen herleiten. Für die Aussagenlogik, für die wir das

zunächst mal einführen, ist das so ein bisschen Overkill. Es bildet dann aber

die Basis dafür, dass wir dieses System später erweitern auf Prädikatenlogik

erster Stufe. Und da haben wir dann nicht mehr solche Alternativen, wozu denn jetzt

formale Beweise führen, wir können ja auch einen Sat-Checker anwerfen. Ich habe

eingangs gesagt, dass das Sat-Problem ja eines der klassischen schweren Probleme

ist, das hindert aber die Industrie nicht daran, effiziente Sat-Checker zu bauen,

die also ihnen sämtliche Gläuenaufgaben, also in Sekundenbruchteilen lösen.

Das klappt aber dann für Prädikatenlogik nicht mehr, denn Prädikatenlogik ist,

das machen wir nur in den höheren Veranstaltungen, unentscheidbar. Es gibt

keinen Algorithmus, der mir zu einer gegebenen Menge prädikatenlogischer

Annahmen und einer angeblichen Folgerung nun sagt, ob das jetzt eine korrekte

Folgerung ist oder nicht. Da haben wir also nichts anderes in der Hand als

unser formales Schlusssystem, im Prinzip zumindest.

So, also wir steigen jetzt also ein in

unser System der formalen Deduktion. Ich fange erst mal an mit so ein bisschen

grundsätzlicher Einführung. In so formale Deduktion an sich, egal welche Logik

oder zur Not auch völlig andere Formalismen das betrifft, und zwar

bestehen solche formalen Systeme sehr breit angelegter Art. Das müssen gar

nicht logische Systeme sein, das können Typsysteme sein, das können

operationale Semantiken sein für Programmiersprachen, alles mögliche ist

so aufgebaut. Solche formalen Systeme bestehen sehr häufig aus zwei

verschiedenen Arten von Zutaten und zwar zum einen aus Axiomen und zum anderen

aus Regeln. So, Axiome sind Dinge, die darf ich einfach hinschreiben.

Ja, das ist also zum Beispiel eine Formel, die einfach angenommen wird. Und zum

anderen Regeln. Regeln haben eine kompliziertere Struktur, nämlich diese

hier. Also Regeln werden fast durchgängig notiert durch einen waagerechten Strich,

der zwei Dinge trennt. Oben stehen die sogenannten Prämissen, unten die

sogenannte Konklusion und das Prinzip so einer Regel ist, wann immer ich es

geschafft habe alle Prämissen hinzuschreiben, also formal herzuleiten in

meinem System, dann darf ich auch die Konklusion der Regel hinschreiben.

So, da gibt es noch manchmal was zusätzliches.

Dann gibt es manchmal noch eine Seitenbedingung und in der Tat wird das

manchmal bei unseren Regeln auftreten. Das ist also eine Bedingung für die

Anwendbarkeit der Regel, die jetzt nicht im Formalismus selber ausdrückbar ist,

die also keine Formel ist, sondern typischerweise irgendeine syntaktische