Beweis & Schluss Logik Einführung Kapitel 7
Beweis & Schluss Logik Einführung Kapitel 7
Aber kommen wir zu unserem eigentlichen Ziel: dem automatisierten Generieren neuer Sätze und damit neuen Wissens.
Wir werden zunächst das semantische Konzept des logischen Schlusses (auch „Schlussfolgerung“ genannt) erläutern,
und dann beschreiben, wie wir dieses durch das syntaktische Konzept des logischen Beweises (auch „Ableitung“ genannt) abbilden, und so durch mechanische Systeme handhabbar machen können.
Der logische Schluss
(Logik Einführung Kapitel 7.1)
Beispiel – Die Nadel im Heuhaufen: logischer Schluss
Suchen wir die Nadel im Heuhaufen, besteht der logische Schluss darin, dass:
- Wenn jemand die Nadel im Heuhaufen fallen gelassen hat, muss sie dort sein
also:
- Die Nadel ist im Heuhaufen ist eine logische Konsequenz davon, dass jemand diese darin fallen gelassen hat.
bzw.
- Aus der Tatsache, dass jemand die Nadel im Heuhaufen fallen gelassen hat folgt, dass sie dort sein muss
D.h.:
- Eine Formel ist genau dann eine logische Konsequenz einer Formelmenge,
- wenn alle Interpretationen, welche die Menge erfüllen,
- auch die Formel erfüllen.
Dies können wir formal wie folgt ausdrücken:
Wir sagen auch γ ist eine logische Konsequenz von Γ.
Γ bezeichnen wir als Annahmen oder Prämissen,
γ als Konklusion.
Führen wir den Folgerungsoperator |= ein,
schreiben wir Γ|=γ
wenn γ eine logische Konsequenz aus Γ ist
und sagen dann auch Γ|=γ ist (semantisch) gültig.
Die Behauptung, dass die Konklusion aus den Prämissen folgt, also Γ|=γ, bezeichnen wir als Argument.
D.h.:
- Haben wir eine Formelmenge Γ
- eine Formel γ
- und ist γ immer (in allen Welten) erfüllbar, wenn (in denen) alle Formeln in Γ erfüllbar sind
- sagen wir γ folgt aus Γ
- und schreiben Γ|=γ
Beispiel – Logischer Schluss: Wumpus-Welt
Betrachten wir wieder die Wumpus-Welt.
Angenommen wir wissen, dass
Prämisse 1 NICHT Gestank(A,1) Prämisse 2 WENN (NICHT Gestank(A,1))
DANN (NICHT Wumpus(A,1)
UND NICHT Wumpus(A,2)
UND NICHT Wumpus(B,1))Daraus folgern wir vernünftigerweise z.B.
Konklusion NICHT Wumpus(A,2) und schreiben
Argument {
NICHT Gestank(A,1),
WENN (NICHT Gestank(A,1)) DANN (NICHT Wumpus(A,1) UND NICHT Wumpus(A,2) UND NICHT Wumpus(B,1))
} |= NICHT Wumpus(A,2)Dies ist vernünftig, weil es den Spezifikationen des Spieles und der Bedeutung der Aussagen entspricht:
wir wissen, dass es auf
- Feld [A,1] nicht stinkt
und laut Spieldefinition
- kann sich der Wumpus also weder auf dem Feld, noch auf einem direkt benachbarten Feld befinden.
In jeder Spielumgebung in der es auf Feld [A,1] nicht stinkt, kann sich der Wumpus also z.B. auch nicht auf Feld [A,2] befinden.
Jede Interpretation unter der
- NICHT Gestank(A,1) wahr ist,
muss also auch
- NICHT Wumpus(A,2) wahr sein.
D.h. jedes
- Modell von NICHT Gestank(A,1)
ist auch ein
- Modell von NICHT Wumpus(A,2)
Die Konklusion folgt also aus den Prämissen.
Das Argument ist (semantisch) gültig.
Eine Tautologie ist ein Satz, der sich ohne Verwendung von Prämissen folgern lässt, also für den |=γ gültig ist, da ihn alle Interpretationen erfüllen.
Der logische Beweis
(Logik Einführung Kapitel 7.2)
Innerhalb einer Ableitung werden Formeln
- mechanisch
- nach festgelegten Regeln (die so genannten „Schlussregeln“)
- unter eventueller Miteinbeziehung vorgegebener Formeln (die so genannten „Axiome“)
umgeformt, sodass neue Formeln entstehen.
In diesem Kapitel wollen wir definieren, was ein logische Schluss ist. Auf die Definition der Schlussregeln und Axiome wird in den nächsten Kapiteln näher eingegangen.
Beispiel – Die Nadel im Heuhaufen: logischer Beweis
Suchen wir die Nadel im Heuhaufen, besteht der logische Beweis darin, dass wir nach irgendeiner Methode so lange Halme abtragen, bis wir die Nadel finden.
Γ bezeichnen wir als Annahmen oder Prämissen,
γ als Konklusion,
die Umformungsregeln als Schlussregeln,
und die Grundvoraussetzungen als Axiome.
Die Abfolge der Regeln bezeichnen wir als Beweis (oder auch Ableitung).
Führen wir den Ableitungsoperator |– ein,
schreiben wir Γ|–γ
wenn γ aus Γ ableitbar ist.
D.h.:
- Haben wir eine Formelmenge Γ
- wenden wir die Umformungsregeln auf diesen endlich oft an, wobei wir bei jedem Schritt Grundvoraussetzungen hinzunehmen können
- und kommen so zum Ergebnis γ
- sagen wir γ lässt sich aus Γ ableiten
- und schreiben Γ|–γ
Beispiel – Logischer Beweis: Wumpus-Welt
Lösen wir das das Beispiel aus dem Kapitel „Der logische Schluss“ syntaktisch.
Angenommen, wir wissen, dass
Prämisse NICHT Gestank(A,1) Axiom WENN (NICHT Gestank(A,1))
DANN (NICHT Wumpus(A,1)
UND NICHT Wumpus(A,2)
UND NICHT Wumpus(B,1))Nehmen wir weiters an, wir haben eine Schlussregel 1, die besagt, dass
- haben wir eine Formel der Gestalt
- WENN γ DANN δ
wobei γ und δ beliebige Formeln sind
und ist
- γ gegeben
können wir
- δ ableiten
Dann können wir in Schritt 1 unserer Inferenz aus der Prämisse unter Miteinbeziehung des Axiomes
Wissen 1 NICHT Wumpus(A,1) UND NICHT Wumpus(A,2) UND NICHT Wumpus(B,1) ableiten.
Angenommen, wir haben eine weitere Regel, Schlussregel 2, die besagt, dass
- haben wir eine Formel der Gestalt
- γ UND δ
können wir
- γ ableiten
und
- δ ableiten
Dann können wir in Schritt 2 unserer Inferenz aus dem Wissen 1
Wissen 2 NICHT Wumpus(A,1) Wissen 3 NICHT Wumpus(A,2) Wissen 4 NICHT Wumpus(B,1) ableiten.
D.h.
- NICHT Gestank(A,1) |– NICHT Wumpus(A,2)
So können wir aus der Wahrnehmung und den Grundvoraussetzungen (Spielregeln) automatisiert (ohne jegliches Wissen darüber, was Wumpus oder Gestank bedeuten) darauf schließen, dass sich der Wumpus nicht auf Feld [A,2] befinden kann.
Die Schritte 1 und 2 bezeichnen wir als Beweis, und sagen ‚NICHT Wumpus(A,2)‘ lässt sich aus ‚NICHT Gestank(A,1)‘ ableiten.
Haben wir die Spielregeln nicht als Axiome innerhalb unserer Logik definiert, müssen wir das Axiom als weitere Prämisse hinzufügen, und erhalten
- {
NICHT Gestank(A,1),
WENN (NICHT Gestank(A,1)) DANN (NICHT Wumpus(A,1) UND NICHT Wumpus(A,2) UND NICHT Wumpus(B,1))
} |– NICHT Wumpus(A,2)
Axiome
(Logik Einführung Kapitel 7.2.1)
Unsere Problemstellung baut eventuell auf gewissen Grundannahmen auf, die wir als Voraussetzungen für unsere Ableitungen brauchen.
Beispiel –
Betrachten wir wieder die Wumpus-Welt.
Definieren wir einen spezifischen Kalkül für unsere Wumpus-Welt, so können wir die Spielregeln, also:
- WENN (NICHT Gestank(A,1))
DANN (NICHT Wumpus(A,1)
UND NICHT Wumpus(A,2)
UND NICHT Wumpus(B,1))- WENN (NICHT Gestank(B,1))
DANN (NICHT Wumpus(A,1)
UND NICHT Wumpus(B,2)
UND NICHT Wumpus(B,1)
UND NICHT Wumpus(C,1))- …
- WENN (Gestank(A2)
DANN (Wumpus(A,1)
ODER Wumpus(A,2)
ODER Wumpus(A,3)
ODER Wumpus(B,2))- etc.
als Axiome betrachten.
Da sich der Wumpus nicht auf Feld [A,1] befinden kann, fügen wir unserem Kalkül die Formel
- NICHT Wumpus(A,1)
Schlussregeln
(Logik Einführung Kapitel 7.2.2)
Nun brauchen wir noch Regeln, die es uns erlauben, innerhalb unseres Systems Formeln mechanisch zu manipulieren um neue Formeln zu erhalten.
Beispiel –
Betrachten wir wieder die Wumpus-Welt.
Haben wir z.B. die Formeln
- WENN (NICHT Gestank(A,1))
DANN (NICHT Wumpus(A,1)
UND NICHT Wumpus(A,2)
UND NICHT Wumpus(B,1))- NICHT GestankA1
wollen wir daraus automatisiert schließen können, dass
- NICHT Wumpus(A,1) UND NICHT Wumpus(A,2) UND NICHT Wumpus(B,1)
Dies soll allgemein für jede Formel der Gestalt WENN..DANN gelten.
Da wir die Bedeutung der Aussagen verstehen, erscheint uns der Schluss klar. Ein Automat jedoch, der nur Symbole manipulieren kann benötigt hierfür jedoch eine Regel.
Also fügen wir unserem Kalkül folgende Schlussregel hinzu:
- Haben wir eine Formel der Gestalt
- WENN γ DANN δ
wobei γ und δ beliebige Formeln sind
und ist
- γ gegeben
können wir
- δ ableiten
D.h.
- „Haben wir eine WENN..DANN-Formel, und ist die Voraussetzung gegeben, so können wir den Schluss zu unserem Wissen hinzufügen“
Diese Regel ist in vielen Logiken enthalten und wird als „Modus Ponens“ oder auch „Implikations-Elimination“ bezeichnet.
Haben wir z.B. die Formel
- NICHT Wumpus(A,2) UND NICHT Wumpus(B,1)
wollen wir auf jede einzelne Teilaussage schließen können, also z.B.
- NICHT Wumpus(A,2)
Dies soll allgemein für alle UND-Verknüpften Formeln gelten.
Wieder erscheint es uns klar, dass, wenn die Gesamtaussage gilt, auch all ihre Teilaussagen gelten müssen – doch wieder müssen wir dies mit einer Schlussregel definieren:
- Haben wir eine Formel der Gestalt
- γ UND δ
wobei γ und δ beliebige Formeln sind
können wir
- γ ableiten
und
- δ ableiten
D.h.
- „Sind 2 Teilaussagen durch UND verbunden, so können wir jede dieser Teilaussagen zu unserem Wissen hinzufügen“
Auch diese Regel ist in vielen Logiken enthalten und wird als ‚Und-Elimination‚ bezeichnet.
Haben wir z.B. die Formel
- Wumpus(A,2) ODER Wumpus(B,1)
wissen aber bereits, dass eine dieser Teilaussage nicht gilt, also z.B.
- NICHT Wumpus(A,2)
wollen wir auf die andere Teilaussage schließen können, also z.B.
- Wumpus(B,1)
Dies soll allgemein für alle ODER-Verknüpften Formeln gelten.
Das Konzept erscheint uns klar, da wir die Bedeutung kennen: gilt eine Teilaussage nicht, muss die andere Teilaussage gelten – doch wieder müssen wir dies mit einer Schlussregel definieren:
- Haben wir eine Formel der Gestalt
- γ ODER δ
wobei γ und δ beliebige Formeln sind
und
- NICHT γ
können wir
- δ ableiten
D.h.
- „Sind 2 Teilaussagen durch ODER verbunden, und gilt eine dieser Teilaussagen nicht, so können wir die andere Teilaussage zu unserem Wissen hinzufügen“
Auch diese Regel ist in vielen Logiken enthalten und wird als ‚Einfacher Widerspruch‚ bezeichnet.
So müssen wir nacheinander alle benötigten Regeln definieren, die es uns erlauben aus unserem Grundwissen und den zur Laufzeit generierten Informationen, weitere Schlüsse zu ziehen, und diese unserem Kalkül als Schlussregeln hinzufügen.
Den Transformationsregeln kommt natürlich keinerlei inhaltliche Bedeutung zu – sie sind ja rein formale Regeln, wie Zeichenketten umgeformt werden können.
Wir werden diese Regeln jedoch sinnvoller Weise so definieren, dass umgeformte Sätze auch semantisch aus den Ausgangssätzen folgen.
als Axiom hinzu.
Korrektheit & Vollständigkeit
(Logik Einführung Kapitel 7.3)
- ein Kalkül ist korrekt, wenn sich nur semantisch gültige Sätze der zugrunde liegenden Logik ableiten lassen.
D.h. wenn Γ|–γ gilt, gilt auch Γ|=γ. - ein Kalkül ist vollständig, wenn sich alle semantisch gültige Sätze der zugrunde liegenden Logik ableiten lassen.
D.h. wenn Γ|=γ gilt, gilt auch Γ|–γ.
Ein Kalkül ist adäquat, wenn er vollständig und korrekt ist
Ist ein Kalkül adäquat, können in ihm genau alle gültigen Aussagen der zugrunde liegenden Logik abgeleitet werden.
Selbstverständlich sind wir bestrebt, einen adäquaten Kalkül für unsere Problemstellung zu finden.
Wie Kurt Gödel jedoch in seinem Unvollständigkeitssatz bewiesen hat, ist es für alle Systeme, die so mächtig sind wie die Arithmetik, nicht mehr möglich solch einen Kalkül zu definieren.
Außerdem ist zu bemerken, dass ein korrekter Kalkül immer widerspruchsfrei ist – denn wäre ein Widerspruch vorhanden bzw. ableitbar, wäre in weiterer Folge alles ableitbar und damit auch alle nichtgültigen Formeln.
Semantische Gültigkeit & logischer Beweis
(Logik Einführung Kapitel 7.4)
Wollen wir neben der Gültigkeit auch die
- Erfüllbarkeit
- Widerlegbarkeit
- Unerfüllbarkeit
von Sätzen automatisiert zeigen, müssen wir uns an die Zusammenhänge erinnern:
- Die Erfüllbarkeit eines Satzes können wir zeigen, indem wir zeigen, dass seine Negation keine Tautologie (also nicht ableitbar) ist.
- Die Unerfüllbarkeit eines Satzes können wir zeigen, indem wir zeigen, dass seine Negation eine Tautologie (also ableitbar) ist.
- Die Widerlegbarkeit eines Satzes können wir zeigen, indem wir zeigen, dass weder der Satz, noch sein Negat eine Tautologie (also beide nicht ableitbar) sind.