Natürliches Schließen

Der deutsche Logiker und Mathematiker Gerhard Gentzen hat in seiner 1935 veröffentlichten Dissertation „Untersuchungen über das logische Schließen“ einen logischen Formalismus mit Namen „Kalkül des natürlichen Schließens“ eingeführt. Im Gegensatz zu den vorher verwendeten Systemen etwa von Frege, Russell oder Hilbert, die überwiegend aus vielen Axiomen bestehen auf welche dann nur einige wenige Ableitungsregeln angewendet werden ( z.B. nur modus ponens ), ist Gentzens Kalkül fast ausschließlich aus anwendbaren Ableitungs-regeln aufgebaut, wodurch es einen stärker prozeduralen Charakter erhält.

Gentzen selbst gibt explizit als sein Ziel an: „Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt.“ Obwohl Gentzens System in der mathematischen Logik weltweite Verbreitung gefunden hat und heute auch als Standardkalkül in Einführungs-vorlesungen verwendet wird, blieb dieser psychologische Anspruch lange Zeit unbeachtet.

Gerhard Gentzen selbst (24.11.1909 – 4.8.1945) hatte nach Studium der Mathematik an den Universitäten Greifswald, Göttingen, München und Berlin im Sommer 1933 in Göttingen das Staatsexamen abgelegt und promoviert und war ab 1934 Assistent bei David Hilbert in Göttingen. Er habilitierte sich im Jahr 1942 und wurde im Herbst 1943 Dozent an der deutschen Universität Prag. Gentzen selbst ist leider schon 1945 in amerikanischer Internierung vermutlich wegen allgemeiner Schwäche verstorben, und seine Dissertation wurde erst 1964 in englischer Übersetzung international zugänglich.

1978 hat dann der amerikanische Psychologe Martin S. Braine – angeregt durch seinen Bruder, einen Logiker – Gentzens Kalkül an Hand von mehreren experimentellen Studien weiterentwickelt zu einer „Natural Logic of Reasoning“, deren 1984er Version ich im Folgenden im Vergleich mit Gentzens ursprünglichem Kalkül darstellen werde.

In beiden Systemen erfolgt das Schließen durch sich verzweigende Figuren („Herleitungsbäume“), welche von „( freien ) Annahmen“ durch die wiederholte Anwendung von Schlußregeln des jeweiligen Systems zu genau einer „Endformel“ führen. Die Anwendung einer Schlußregel wird dabei durch einen waagrechten Strich gekennzeichnet, unter dem die Konklusion dieser Regel und über dem zwei, eine oder auch keine Prämissen stehen. Dabei kann bei der Anwendung gewisser Schlußregeln eine freie Annahme, die oberhalb dieser Regel ein- oder auch mehrmals auftritt, „gebunden“ werden, d.h. die Konklusion und alle nachfolgenden Formeln hängen nicht mehr von dieser Annahme ab. Dies wird angezeigt, indem man die gebundenen Annahmen in eckige Klammern setzt.

Beispiel ( experimentelles Problem xli. aus Braine 1984, Appendix ):

There is a B, and there is an I or an N
If there is both a B and an I, then there is an X
If there is both a B and an N, then there is a Z
? There is an X or a Z ?

dasselbe symbolisch notiert

B ∧ (I ∨ N)
( B ∧ I ) → X
( B ∧ N ) → Z
zeige: X ∨ Z

ein formaler Herleitungsbaum mit den Regeln von Gentzen:

eine äquivalente Herleitung mit den komplexeren Regeln von Braine:

Kurz zur Schreibweise:

Eine Herleitung ist von oben nach unten zu lesen: die Aussage unter einem horizontalen Strich wird hergeleitet aus den Aussagen über diesem Strich. Aussagen ohne Strich darüber sind gegebene Voraussetzungen oder, falls sie in eckigen Klammern stehen, („gebundene“) Annahmen, die zu einer weiter unten stehenden Schlußregel gehören. Die Buchstaben A,B,C,… stehen für beliebige Aussagen, s,t,… für beliebige Terme, A(v) heißt, dass der Term v an gewissen Stellen in der Aussage A vorkommen kann. Zusammengesetzte Aussagen werden gebildet mit den Junktoren ∧ (und), ∨ (oder), → (wenn, dann; materiale lmplikation) und ggf. den Quantoren ∀x („für alle x“) und ∃x („es gibt ein x“).

Die Herleitung nach Gentzen kann mit Worten und in der willkürlich gewählten Reihenfolge von 1 bis 10 etwa so wiedergegeben werden:

Aus der Voraussetzung B∧(I∨N) schließen wir (1) auf I∨N. Aus derselben Voraussetzung schließen wir (2) auch auf B, dazu nehmen wir an, dass I gelte und können damit (3) auf B∧I schliessen. Mit der weiteren Voraussetzung B∧I→X können wir (4) nun auf X schließen, und aus X folgt (5) insbesondere X∨Z. Analog (6) können wir mit der Annahme N auf B∧N schließen (7) , daraus erhalten wir (8) mittels der dritten Voraussetzung B∧N→Z das Z und aus Z folgt (9) ebenfalls insbesondere X∨Z . Nun haben wir eine Herleitung von X∨Z unter der Annahme I sowie eine Herleitung von X∨Z unter der Annahme N, und wir wissen, daß I∨N gilt, damit können wir abschließend folgern (10), daß das gesuchte Ergebnis X∨Z in allen Fällen gilt.

Die Herleitung nach Braine dagegen besagt etwa folgendes:

Aus der Voraussetzung B∧(I∨N) schliessen wir (1) distributiv auf (B∧I)∨(B∧N) und mit den beiden anderen Voraussetzungen (B∧I)→X und (B∧N)→Z können wir daraus (2) direkt das gesuchte Ergebnis X∨Z folgern.

Wie man schon an diesem Beispiel deutlich erkennt, erlaubt das ursprüngliche Gentzensche System eine deutlich feinere Analyse einer Herleitung.

Um eine bessere Vergleichbarkeit zu erhalten, habe ich beide Kalküle äußerlich gegenüber den Orginalarbeiten leicht verändert: So betrachte ich Konjunktion und Disjunktion als implizit kommutativ, d.h. anders als Gentzen in seiner Orginalarbeit werde ich zwischen (A∧B) und (B∧A) bzw. (A∨B) und (B∨A) nicht unterscheiden, wodurch spiegelsymmetrische Paare von Schlußregeln vermieden werden. Andererseits werde ich mich auf zweistellige Junktoren beschränken, anders als Braine, der Konjunktion und Disjunktion im theoretischen Teil seiner Arbeit grundsätzlich n-stellig verwendet. Bei der Negation werde ich einer von Gentzen angegebenen Alternativ-Darstellung folgen, wobei das „Incompatible“ bei Braine mit Gentzens Falsum ⊥ gleichgesetzt wird.

Worin steckt nun die Schwierigkeit ?

Eine große Wahrheit ist, dass das Wort „nicht“ überflüssig ist.

Bertrand Russell, 1954

Es ist meines Erachtens eine leider verbreitete Fehleinschätzung, die Negation als die theoretisch einfachste und daher problemloseste logische Operation zu betrachten, wie es auch manche psychologischen Textbücher tun, nur um sich hinterher über „the strange case of the awkward negative“ (Johnson 1972) zu wundern. Wenn man dagegen Arbeiten von Logikern betrachtet, sieht man, dass unter den Standardjunktoren nur die Negation als problematisch zu betrachten ist: Durch Weglassen nur der Negation erhält man bereits die sogenannte Minimallogik. Die Schwierigkeit mit der Negation kommt sehr vage gesagt daher, dass sie sich als einzige aussagenlogische Operation auf die Klasse aller Aussagen bezieht. Tatsächlich wurde bereits mit bemerkenswerten Erfolgen der Versuch unternommen, Mathematik zu betreiben unter völligem Verzicht auf die Negation (Heyting 1956).

Die Kriterien zur Gestaltung der hier verglichenen Systeme

Beim Vergleich der beiden folgenden Systeme ist es wichtig zu berücksichtigen, dass ihre Schlußregeln nach unterschiedlichen Kriterien ausgewählt wurden:
Gentzen dürfte neben den in der Logik üblichen Grundkriterien Gültigkeit (Korrektheit), Redundanzfreiheit und Vollständigkeit auch auf subjektive Natürlichkeit, Regelmäßigkeit und gewisse metatheoretisch nützliche Eigenschaften (etwa die sogenannte Teilformeleigenschaft) gezielt haben, er will dabei allerdings trotzdem ausdrücklich „einen Formalismus aufstellen, der möglichst genau das wirkliche logische Schließen bei mathematischen Beweisen widergibt.“

Braine gibt explizit die folgenden 3 Auswahlkriterien an:

1. psychologische Gültigkeit (d.h. die Regel wird im Experiment von im wesentlichen allen Versuchspersonen als richtig bezeichnet),
2. psychologische Unzerlegbarkeit (d.h. die Regel erscheint im Experiment leichter als die Summe der Schwierigkeiten möglicher Teilregeln ), und
3. psychologische Vollständigkeit (d.h. jede Regel, die 1. und 2. erfüllt, soll zum System gehören).

Das Kalkül des natürlichen Schließens von Gerhard Gentzen

Einer der großen Vorteile dieses Systems ist sein regulärer Aufbau: es enthält für jedes logische Grundzeichen jeweils eine +-Regel , die es erzeugt, und eine –-Regel, die es entfernt. Jede Regel enthält nur das jeweils erzeugte oder entfernte Grundzeichen explizit. Darüberhinaus gilt ein sogenanntes ‚Inversion Principle‘, welches besagt, dass jeweils die –-Regel cum grano salis die genaue Umkehrung der entsprechenden +-Regel darstellt, d.h. mit der –-Regel kann man aus einer zusammengesetzten Aussage jeweils genau das wiedergewinnen, was man beim Zusammensetzen dieser Aussagen als Prämissen der entsprechenden +-Regel hineingesteckt hat.

Die aussagenlogischen Regeln:

Konjunktion:

Disjunktion:

Implikation:

*(wie schon erwähnt sind ∧ und ∨ stets kommutierbar zu verstehen)

Diese sechs Regeln formalisieren die Minimallogik; die noch fehlende Negation wird über eine Aussagenkonstante ⊥ „Falsum“ ( Widerspruch, „Incompatible“, das Falsche ) eingeführt. Der einstellige Negationsoperator ¬ ist dann als Abkürzung zu lesen: ¬A ≡ A → ⊥ . Die einzige Regel für Falsum lautet

‚Wenn Falsum ableitbar ist, ist jeden beliebige Formel ableitbar‘, mit anderen Worten: ‚Falsum ist die allgemeinste aller Aussagen‘. Dies ist nicht ein ‚Beweis durch Widerspruch‘, denn hier darf keine Annahme gebunden werden !

Diese folgenden Regel für Quantoren und Gleichheit ermöglichen die ebenso systematische Erweiterung zur vollen Prädikatenlogik erster Stufe mit Gleichheit:

Allquantor:

Existenzquantor:

Gleichheitszeichen:

Bei den mit * markierten Quantorenregeln sind allerdings zusätzliche sogenannte Variablenbedingungen zu beachten : bei (∀+) darf die Variable t in keiner freien Annahme auftreten, von der A(t) abhängt; bei (∃-) darf t in F nicht auftreten und in keiner der Annahmen, von denen F abhängt, mit Ausnahme von A(t) natürlich.

Induktive Definition einer Herleitung

Mehr aus Gründen der Vollständigkeit will ich jetzt den Begriff „aussagen-logische Herleitung von A mit den freien Annahmen F“ noch einmal verbal definieren. F ist hier eine Menge von Aussagen. Dabei handelt es sich um eine induktive Definition:

Induktionsanfang:
Jede Aussage A ist auch eine Herleitung von A mit den freien Annahmen {A}.

Induktionsschritt:

(∧+) Wenn es eine Herleitung von A mit den freien Annahmen F1 und eine weitere Herleitung von B mit den freien Annahmen F2 gibt, so kann man eine Herleitung von A∧B mit den freien Annahmen F1 ∪ F2 bilden.

(∧-) Wenn es eine Herleitung von A∧B mit den freien Annahmen F gibt, so kann man eine Herleitung von A mit denselben freien Annahmen bilden.

(→+) Wenn es eine Herleitung von B mit den freien Annahmen F gibt, so kann man eine Herleitung von A→B mit den freien Annahmen F\{A} bilden. ( A muss nicht, aber wird in der Regel in F auftreten. )

(→-) „modus ponens“ Wenn es eine Herleitung von A mit den freien Annahmen F1 und eine Herleitung von A→B mit den freien Annahmen F2 gibt, so kann man eine Herleitung von B mit den freien Annahmen F1 ∪ F2 bilden.

(∨+) „Abschwächung“ Wenn es eine Herleitung von A mit den freien Annahmen F gibt, so kann man eine Herleitung von A∨B mit denselben Annahmen bilden.

(∨-) „Fallunterscheidung“ Wenn es eine Herleitung von A∨B mit den freien Annahmen F0 und zwei Herleitungen von F mit den freien Annahmen F1 respektive F2 gibt, so kann man eine Herleitung von F mit den freien Annahmen F0 ∪ (F1\{A}) ∪ (F2\{B}) bilden.

(⊥) „ex falso quodlibet“ Wenn es eine Herleitung von ⊥ mit den freien Annahmen F gäbe, so könnte man für eine beliebige Aussage A eine Herleitung von A mit den freien Annahmen F bilden.

Die oben eingeführten Schlußregeln bilden allerdings noch kein vollständiges System im Sinne der klassischen oder aristotelischen Logik, d.h. nicht alle nach klassischer Interpretation gültigen Aussagen lassen sich mit diesen Regeln auch herleiten. Diese Regeln gestatten vielmehr nur eine echte Untermenge aller klassisch gültigen Beweise, nämlich solche, welche auch den verschärften Gültigkeitskriterien des Intuitionismus genügen. Wenn wir sie ergänzen wollen zu einem klassisch vollständigem System, können wir beispielsweise für jede Aussage A das ‚Tertium non datur‘-Axiom A∨¬A zulassen; andere Optionen zur Vervollständigung wären die Hinzunahme der Regel

oder die Ersetzung der Regel (⊥) durch die ähnliche, aber viel stärkere Regel

„Beweis durch Widerspruch“:

Im Gegensatz zur (⊥)-Regel darf also beim Beweis durch Widerspruch (⊥*) die Negation der Behauptung als zusätzliche Voraussetzung verwendet werden!

Natural Propositional Logic nach Martin Braine et al.

Der amerikanische Psychologe Martin Braine hat zusammen mit Brian Reiser und Barbara Rumain 1984 eine Formalisierung der natürlichen Aussagenlogik veröffentlicht, die aus einer experimentell begründeten Modifikation und Erweiterung des Gentzenschen Systems besteht. Braine betrachtet formal nur Aussagenlogik, aber bei endlichem Objektbereich, was eine psychologisch plausible Annahme wäre, kann man All- bzw. Existenzaussagen als entsprechend vielstellige Kon- bzw. Disjunktionen auffassen, so daß für diesen Fall keine zusätzlichen Quantorenregeln notwendig werden.

( Die Regeln P6 und P6′ sind bei Braine eine Äquivalenz-Gleichung, ansonsten folgen die Bezeichnungen genau Braine 1984 )

Gemeinsamkeiten und Unterschiede der beiden Systeme:

• P15 ist genau der Induktionsanfang der Herleitungsdefinition von Gentzen, wird dort aber nicht als Regel klassifiziert.
• die Regeln für Konjunktion und Implikation sind in beiden Systemen gleich: P1 ≡ (∧+), P2 ≡ (∧-), P12 ≡ (→-), P13 ≡ (→+).
• bezüglich der Disjunktion ist cum grano salis, nämlich bis auf zwei P13- bzw. (→-)-Anwendungen die Regel P10 äquivalent zu (∨-).
• interpretiert man auch bei Braine die Negation ¬A ≡ A→⊥, so wird P3 ein Sonderfall von P12, P16 von P13 und (cum grano salis) P4 von P10.
• die Regeln P6/P6′, P7, P9 und P11 sind logisch zusammengesetzte Schlüsse der Minimallogik, welche Braine empirisch als psychologisch elementar gefunden hat.
• ebenfalls zusammengesetzte Schlüsse sind P5 und P8, wobel man hier auch die (⊥)-Regel verwenden muss, für P5 noch zusätzlich ein (A∨¬A)-Axiom.
• P14 entspricht bei Gentzen dem Axiomenschema A∨¬A, dem ‚Tertium non datur‘, welches, wie Brouwer immer betonte, keine logische Tautologie ist, sondern eine inhaltliche Behauptung über die jeweilige Aussage A, und aus diesem Grund nicht als Schlußregel eingeführt wurde.
• der (⊥)-Regel entspricht bei Braine wohl seine Definition von „incompatible“, jedenfalls kann man sie durch die stärkere Regel P5 ( und P13 ) dargestellen.
• es fehlt bei Braine aber explizit die (∨+)-Regel, da sie sich im Experiment als psychologisch nicht gültig erwiesen hat; allerdings kann sie mittels P11, P14, P13, P16 und P5 dargestellt werden, wenn auch nur ziemlich trickreich:

Das System von Braine ist somit ebenfalls im Sinn der klassischen Logik gültig und vollständig. Alle seine Regeln mit Ausnahme von P5 und P14 sind auch intuitionistisch gültig. Würde man diese beiden Regeln weglassen, hätte man ein intuitionistisches Teilsystem, welches allerdings unvollständig wäre, da man ohne P14 die (∨+)-Regel nicht nachbilden kann.

Braine schreibt über dieses Fehlen der (∨+)-Regel : „If the schema [(∨+)] were part of the essential meaning of or for subjects, then it should not be possible for them to reject the inference on simple problems.“, was aber fast 50% seiner Probanden eben taten; daher betrachtet er diese Regel als psychologisch nicht gültig.

Ich meine aber, daß man dieses Verhalten durchaus schlüssig erklären kann: Eine einzelne Anwendung von (∨+), wie sie in den ’simple problems‘ von Braine’s Studie verlangt wird, ist im realen Leben nämlich fast immer sinnlos, da sie nichts anderes bewirkt als die Ungewissheit (im Sinne von Entropie) einer Aussage zu erhöhen. Mit ‚fast immer‘ meine ich ‚immer außer in Fällen, wo die Person gute Gründe hat, die Ungewissheit erhöhen zu wollen‘, z.B. bei dem logisch gültigen Schluß von „Ich bin zu schnell gefahren“ auf „Ich bin zu schnell gefahren oder der Fahrbahnbelag war zu glatt“. Dagegen ist eine Abschwächung einer Aussage durch (∨+), beispielsweise der linken Seite einer Implikation, innerhalb einer komplexeren Herleitung oft sinnvoll und nützlich. Es erscheint mir daher völlig plausibel anzunehmen, dass viele Versuchs-personen einen einzelnen unmotivierten (∨+)-Schluß als unkorrekt, weil sinnlos, ablehnen werden, obwohl sie denselben Schluß in einem sinnvollen Zusammenhang automatisiert anwenden würden. Diese These bedürfte natürlich experimenteller Überprüfung.

Schwierigkeitsfaktoren

Braine hat in drei Experimenten logische Probleme in der Art des am Anfang gegebenen Beispiels von Studenten lösen und dabei nach ihrer Schwierigkeit bewerten lassen (121, 99 resp. 85 Aufgaben durch 31, 28 resp. 28 Teilnehmer, davon aber 3, 4 resp. 4 als Ausreißer nicht gewertet). Für ein lineares Modell zur Darstellung der Schwierigkeitsratings der einzelnen Aufgaben konnte er empirisch durch Parameteranpassung die folgenden Schwierigkeitsfaktoren der von ihm als ‚direkt‘ klassifizierten Regeln P1 bis P13 bestimmen:

Die Vorhersagen des mit diesen Parametern versehenen Modells korrellieren mit .92 mit den zur Parameterbestimmung verwendeten Schwierigkeitsdaten, aber auch mit .95 mit den unabhängigen Daten eines vorhergehenden Experiments.

Sehr überraschend ist hierbei zunächst die fast-Null-Schwierigkeit von P13 ≡ (→+), da diese Regel wegen der auftretenden Bindung einer freien Annahme eigentlich indirekt und daher theoretisch schwieriger sein sollte. Dagegen spricht es für die intuitionistische Interpretation, dass die von der Gestalt her sehr einfache, aber intuitionistisch nicht gültige Regel P5 einen relativ hohen Schwierigkeitskoeffizienten erhält. Die Höchstwerte bei P8 und P9 erscheinen allerdings kaum verständlich.

Der dynamische Aspekt des Schließens

Mindestens ebenso wichtig wie die Frage »Was ist eine logisch bzw. psychologisch gültige Herleitung ?« sind für eine psychologische Theorie des Schließens die Fragen »Wie wird eine Herleitung gefunden ?« und »Wann kann überhaupt eine Herleitung gefunden werden ?«. Braine gibt hierzu nur ein „heuristic reasoning program“ an, welches nicht immer eine Entscheidung finden kann und daher noch durch „quasilogische“ Hilfsprozeduren ergänzt werden muss.

Für das intuitionistische System vom Gentzen gibt es dagegen einen sehr natürlichen und trotzdem vollständigen Algorithmus zur Konstruktion von Herleitungen. Das System ist gerade so gewählt, dass ein solcher Algorithmus noch möglich ist: das algorithmisch nicht behandelbare „tertium non datur“ ist gerade darum nicht als Regel klassifiziert. Der Algorithmus beruht auf der Beobachtung, daß alle Schlußregeln die sogenannte Teilformeleigenschaft aufweisen, d.h. bei den +-Regeln treten alle Prämissen als Teile in der Konklusion auf, während bei den –-Regeln die Konklusion aus Prämissen oder Teilen von diesen besteht (auf die technischen Details kann hier nicht eingegangen werden). Man kann zeigen, dass immer, wenn überhaupt eine Herleitung existiert, auch eine solche in einer einfachen, umwegfreien Standardform möglich ist, die sich dadurch auszeichnet, dass niemals eine –-Regel unterhalb von einer +-Regel steht. Mit anderen Worten:

In einer Standardherleitung werden die Voraussetzungen durch die jeweils einzig passenden –-Regeln solange in Bestandteile zerlegt, bis aus diesen durch +-Regeln direkt die gesuchte Endformel zusammengebaut werden kann. Insbesondere treten dabei überhaupt keine Aussagen auf, die nicht selbst Teil der Voraussetzungen oder der Endformel sind.