Kalküle natürlichen Schließens

Systeme (oder Kalküle) natürlichen Schließens sind ein Kalkültyp, der 1934 von Gerhard Gentzen und etwa zeitgleich von Stanisław Jaśkowski, einem Vertreter der Lemberg-Warschau-Schule, entwickelt wurde.

Der Begriff des Kalküls des natürlichen Schließens (KdnS) ist nicht streng definiert, stattdessen gibt es eine Reihe von Merkmalen, die auf KdnS in unterschiedlichem Maße zutreffen und dabei bestimmen, wie typisch das Exemplar für die Gattung ist.^[1]

• Anders als bei den allermeisten anderen Kalkültypen wie Tableauxkalkül, Axiomatischer Kalkül, Dialogkalkül etc. gibt es im KdnS die Möglichkeit, Aussagen anzunehmen, die für eine Weile innerhalb der Ableitung ihre Gültigkeit haben. Diese Annahmen können später wieder getilgt werden (siehe dazu auch unten). Dieses Merkmal macht einen großen Anteil an der „Natürlichkeit“ des Schließens im KdnS aus, denn es entspricht der gängigen Praxis in mathematischen Beweisen.

• Im Gegensatz zu axiomatischen Kalkülen enthält ein System natürlichen Schließens keine bzw. kaum Axiome, sondern hauptsächlich eine größere Zahl von Schlussregeln. Zusammen mit den gleichfalls von Gentzen entwickelten Sequenzenkalkülen gehören Systeme des natürlichen Schließens deshalb zur Familie der Regellogiken oder Regelkalküle.

• Die Schlussregeln in einem KdnS sollten intuitiv zu rechtfertigen sein, am besten prätheoretisch akzeptierten Beweistechniken entsprechen. Auch dieses Merkmal trägt zur „Natürlichkeit“ des Schließens bei.

• Üblicherweise werden die Schlussregeln so systematisiert, dass für jeden logischen Operator (Junktor bzw. Quantor) eine Einführungs- und eine Beseitigungsregel angegeben ist. Die Einführungsregel für einen Operator O erlaubt es, zu einer Aussage mit O als Hauptoperator überzugehen; die Beseitigungsregel führt von einer Aussage mit O als Hauptoperator zu einer anderen Aussage.

Aufgrund der Natürlichkeit des Schließens und der Systematisierung in Einführungs- und Beseitigungsregeln lässt sich mit einem KdnS der Anspruch einer „beweistheoretischen Semantik“ verbinden, welche die Bedeutung der logischen Operatoren durch die Angabe von Schlussregeln festlegen will.

Abhängigkeit von Annahmen

In einem KdnS gibt es eine Annahmeregel, die es erlaubt, beliebige Aussagen anzunehmen. Schlussregeln werden meistens auf bereits gewonnene Aussagen angewendet. Sind diese Aussagen Annahmen, so sagt man, dass das Resultat der Regel „in Abhängigkeit von“ diesen Annahmen gewonnen wurde. Dasselbe gilt, wenn die Aussagen, auf welche die Regel angewendet wurde, zwar keine Annahmen sind, aber selbst wiederum in Abhängigkeit von irgendwelchen Annahmen gewonnen wurden. Im Resultat der Regeln summieren sich dann alle beteiligten Abhängigkeiten. Manche Regeln erlauben es jedoch, ganz bestimmte Annahmen zu „tilgen“. Dies bedeutet, dass das Resultat der Regel von einer bestimmten Annahme nicht mehr abhängig ist, von der noch eine der Aussagen, auf die sie angewendet wurde, abhängig war.

Hierzu ein Beispiel: Wenn es gelingt, in Abhängigkeit von einer Aussage P1 eine Aussage P2 abzuleiten, so kann auf die Aussage „Wenn P1, dann P2“ übergegangen werden. (Dies ist die Implikations-Einführung $\rightarrow E$, siehe auch unten.) Indem die Annahme P1 nun sozusagen explizit in die Aussage mit aufgenommen wurde („Wenn P1, …“), kann die Abhängigkeit von ihr getilgt werden. D.h. "Wenn P1, dann P2" ist nicht länger von P1 abhängig. Wäre P2 noch von weiteren Aussagen P3 … Pn abhängig, so bestünden diese Abhängigkeiten weiter fort. „Wenn P1, dann P2“ wäre dann also immer noch von P3 … Pn abhängig.

Will man ein logisches Theorem beweisen, so muss die bewiesene Aussage ganz frei von Abhängigkeiten sein. Ist die bewiesene Aussage P1 noch abhängig von Aussagen P2 … Pn, so hat man gezeigt, dass P2 … Pn die Aussage P1 logisch implizieren.

Die Regeln

Klassische Logik

Aussagenlogik

Für die klassische Aussagenlogik werden meist folgende Regeln verwendet (die Prämissen stehen oberhalb des Folgerungsstrichs, die Konklusion unterhalb, eckige Klammern markieren zu beseitigende Abhängigkeiten):

$\wedge E:\ \frac{P1\quad P2}{P1 \wedge P2}\qquad\frac{P1\quad P2}{P2 \wedge P1}$

Aus zwei Aussagen P1 und P2 kann die Konjunktion „P1 und P2“ geschlossen werden.

Beispiel: Aus den Aussagen „Skolem war Norweger“ und „Skolem war Logiker“ kann geschlossen werden: „Skolem war Norweger und Logiker“.

$\wedge B:\ \frac{P1 \wedge P2}{P1}\qquad \frac{P1 \wedge P2}{P2}$

Aus einer Konjunktion „P1 und P2“ kann jedes einzelne Konjunkt, also sowohl P1 als auch P2 erschlossen werden.

Beispiel: Aus „Skolem war Norweger und Logiker“ kann geschlossen werden: „Skolem war Norweger“ (und auch „Skolem war Logiker“).

$\vee E:\ \frac{P1}{P1 \vee P2}\qquad \frac{P1}{P2 \vee P1}$

Aus einer Aussage P1 kann die Disjunktion „P1 oder P2“ geschlossen werden.

Beispiel: Aus „Skolem war Norweger“ kann geschlossen werden: „Skolem war Schwede oder Norweger“.

$\vee B:\ \frac{P1 \vee P2\quad[P1]\ P3\quad[P2]\ P3}{P3}$

Wenn es gelingt, aus jedem Disjunkt einer Disjunktion „P1 oder P2“ einen Satz P3 herzuleiten, dann folgt dieser Satz aus der Disjunktion.

Beispiel: Nehmen wir an, ich weiß, dass Skolem Norweger oder Schwede war. Aus „Skolem war Norweger“ folgt „Skolem war Skandinavier“. Dasselbe folgt aus „Skolem war Schwede“. Ich kann also aus „Skolem war Norweger oder Schwede“ folgern „Skolem war Skandinavier“.

Diese Regel entspricht der Beweistechnik der „Fallunterscheidung“.

$\rightarrow E:\ \frac{[P1] \ P2}{P1 \rightarrow P2}$

Wenn es gelingt, aus einer Aussage P1 eine Aussage P2 herzuleiten, dann ist – begründet durch das Deduktionstheorem – auch die Implikation „Wenn P1, dann P2“ herleitbar.

Beispiel: Wenn ich aus der Annahme „Skolem war Norweger“ folgern darf „Skolem war Skandinavier“, so darf ich (frei von dieser Annahme) folgern: „Wenn Skolem Norweger war, so war er Skandinavier“.

Diese Regel entspricht der Beweistechnik „Konditionaler Beweis“.

$\rightarrow B:\ \frac{P1 \rightarrow P2 \quad P1}{P2}$

Modus ponens: Aus der Implikation „Wenn P1, dann P2“ folgt zusammen mit P1 die Aussage P2.

Beispiel: Aus „Wenn Skolem Norweger war, dann war er Skandinavier“ folgt zusammen mit „Skolem war Norweger“ die Aussage „Skolem war Skandinavier“.

$\lnot E:\ \frac{[P1] \ P2 \wedge \lnot P2}{\lnot P1}$

Wenn sich aus einer Aussage P1 ein beliebiger Widerspruch herleiten lässt, dann darf auf die Negation „nicht P1“ geschlossen werden.

Beispiel: Nehmen wir an, wir wüssten, dass Skolem Norweger war. Aus der Aussage „Skolem war Schwede“ folgt aber „Skolem war kein Norweger“. Dies steht aber im Widerspruch zu der bereits bekannten Aussage „Skolem war Norweger“. Wir können also auf die Negation von „Skolem war Schwede“, also auf „Skolem war kein Schwede“, schließen.

Diese Regel entspricht der Beweistechnik „Indirekter Beweis“ bzw. Reductio ad absurdum.

$\lnot\lnot B:\ \frac{\lnot \lnot P1}{P1}$

Duplex negatio affirmat: Aus der Aussage „nicht nicht P1“ kann auf P1 geschlossen werden.

Beispiel: Aus „Es stimmt nicht, dass Skolem kein Norweger war“ folgt „Skolem war Norweger“.

Prädikatenlogik

Für einen Kalkül des natürlichen Schließens für die Prädikatenlogik sind zusätzliche Einführungs- und Beseitigungsregeln für die Quantoren erforderlich.

Bei der Formulierung der Regeln wird auf sogenannte „Parameter“ zurückgegriffen. Parameter sind Terme, die nicht in Axiomen vorkommen dürfen. Es wird unterstellt, dass ein unendlicher Vorrat an Parametern zur Verfügung steht. Ein Parameter spielt im Kalkül des Natürlichen Schließens in etwa dieselbe Rolle, die freie Variablen in anderen Kalkülen spielen, allerdings können Parameter nicht durch Quantoren gebunden werden.

Für eine exakte Formulierung der Quantorenregeln werden zwei Hilfsbegriffe benötigt: Eine Instantiierung einer All- oder Existenzaussage, $\forall x P1$ oder $\exists x P1$, durch den Term t, P1(t) ist das Resultat der Ersetzung aller in P1 freien Vorkommnisse von x durch t. Eine Parametrisierung einer dieser Aussagen durch den Parameter u, P1(u), ist eine Instantiierung durch u, wobei u nicht schon in P1 vorkommen darf.

$\forall E:\ \frac{P1(u)}{\forall x P1}$, wobei P1(u) nicht abhängig von einer Aussage ist, in der u vorkommt.

Aus der Parametrisierung P1(u) darf die Aussage „Für jedes x gilt P1“ geschlossen werden. Zusatzbedingung ist hier, dass P1(u) nicht abhängig von irgendwelchen Aussagen ist, die den Parameter u enthalten.

Beispiel: Wenn ich geschlossen habe, dass John Doe vergänglich ist, und wenn in diesen Schluss keinerlei Information über John Doe eingegangen ist, dann kann ich schließen, dass alles vergänglich ist. Der Klausel, dass in diesen Schluss keinerlei Information über John Doe eingegangen ist, entspricht dabei die Klausel, dass P1(u) nicht abhängig von einer Aussage sein darf, in der u vorkommt.

$\forall B:\ \frac{\forall x P1}{P1(t)}$

Aus der Aussage „Für jedes x gilt P1“ darf die Instantiierung P1(t) geschlossen werden.

Beispiel: Aus „Alles ist vergänglich“ kann geschlossen werden „Skolem ist vergänglich“

$\exists E:\ \frac{P1(t)}{\exists x P1}$

Aus der Instantiierung P1(t) darf „Es gibt ein x, für das P1 gilt“ geschlossen werden.

Beispiel: Aus „Skolem war Norweger“ kann geschlossen werden „Es gibt einen Norweger“

$\exists B:\ \frac{\exists x P1\quad[P1(u)]\ P2}{P2}$, wobei u weder in P2 vorkommt noch in irgendeiner Aussage, von der P2 abhängig ist, ausgenommen die Parametrisierung P1(u).

Aus der Aussage „Es gibt ein x, für das P1 gilt“ kann eine Aussage P2 geschlossen werden, wenn es gelingt, aus der Parametrisierung P1(u) P2 abzuleiten. Zusatzbedingung ist, dass P2 nicht u enthält und auch nicht abhängig von irgendwelchen Aussagen ist, die u enthalten, außer eben P1(u).

Beispiel: Ich weiß, dass es einen norwegischen Logiker gibt. Aus der Aussage „John Doe war Norweger und John Doe war Logiker“ kann ich schließen „Es gibt einen skandinavischen Logiker“, wobei in diesen Schluss keine weiteren Informationen über John Doe eingehen (außer dass er Norweger und Logiker ist). Dann kann ich aus „Es gibt einen norwegischen Logiker“ schließen: „Es gibt einen skandinavischen Logiker“.

Identität

Auch dem Identitätszeichen kann vermittels Einführungs- und Beseitigungsregeln eine Bedeutung verliehen werden.

$= E:\ \frac{}{t=t}$

Die Aussage „t=t“ kann erschlossen werden.

Beispiel: Es gilt die Aussage „Skolem ist gleich Skolem“. Man beachte, dass diese Regel nicht auf irgendwelche Aussagen angewendet werden muss.

$= B:\ \frac{t1=t2\quad P1}{P1(t1//t2)}$

Aus „t1=t2“ und einer Aussage P1 kann eine Aussage P1(t1//t2) geschlossen werden, wobei P1(t1//t2) aus P1 hervorgeht, indem alle oder einige Vorkommnisse von t1 in P1 durch t2 ersetzt wurden.

Beispiel: Aus „Skolem ist identisch mit dem Erfinder der skolemschen Normalform“ und „Skolem war Norweger“ kann geschlossen werden: „Der Erfinder der skolemschen Normalform war Norweger“.

Eine Beispielableitung

Zeile	Aussage	Regel	angewendet auf	Abhängigkeit(en)
1	$P1 \rightarrow P2$	Annahme
2	$\lnot P2$	Annahme
3	$P1\$	Annahme
4	$P2\$	$\rightarrow B$	1, 3	1, 3
5	$P2 \wedge \lnot P2$	$\wedge E$	2, 4	1, 2, 3
6	$\lnot P1$	$\lnot E$	5	1, 2
7	$\lnot P2 \rightarrow \lnot P1$	$\rightarrow E$	6	1
8	$(P1 \rightarrow P2) \rightarrow (\lnot P2 \rightarrow \lnot P1)$	$\rightarrow E$	7

Nichtklassische Logik

Ebenso, wie man aus einem axiomatischen Kalkül für die klassische Logik nichtklassische logische Systeme erzeugt, indem man einzelne Axiome weglässt oder durch neue Axiome ersetzt, kann man nichtklassische Systeme natürlichen Schließens erzeugen, indem man einzelne Regeln aus dem obigen Regelsatz streicht beziehungsweise durch bestimmte andere Regeln ersetzt:

• Ersetzt man die Beseitigungsregel für die doppelte Negation, $\lnot\lnot B$, durch die Regel ex contradictione sequitur quodlibet, $\frac{P \quad \lnot P}{Q}$, erhält man einen dem Intuitionismus entsprechenden Kalkül. Er entspricht der Verwendung der effektiven Rahmenregel in der Dialogischen Logik.
• Streicht man die Beseitigungsregel für die doppelte Negation, $\lnot\lnot B$ ersatzlos, erhält man den sogenannten Minimalkalkül (Kolmogorow 1924, Johansson 1937).
• Streicht man dagegen die Regeln zur Einführung der Konjunktion, $\wedge E$, so erhält man einen so genannten nicht adjunktiven parakonsistenten Logikkalkül.

Schnittregel

Der Gentzensche Hauptsatz besagt, dass die Schnittregel

$\mathrm{cut}\quad\frac{[\Sigma]P1 \qquad [\Sigma,P1]\ P2}{[\Sigma]P2}$

in den Systemen natürlichen Schließens gültig ist. (Σ ist eine Liste ableitbarer Formeln)

Geschichte der Kalküle des natürlichen Schließens

Den Anstoß für die Entwicklung der KdnS durch Jaśkowski gab Łukasiewicz. Im Jahre 1926 charakterisierte er die gängige Beweispraxis der Mathematiker so, dass diese Annahmen aufstellen und zusehen, wohin diese führen. Er formulierte als Seminarthema das Projekt, eine logische Theorie aufzustellen, die solche Schlussweisen erlaube.^[2] Sehr ähnlich, aber unabhängig davon charakterisiert Gentzen seine Motivation:

Mein erster Gesichtspunkt war folgender: Die Formalisierung des logischen Schließens, wie sie insbesondere durch Frege, Russell und Hilbert entwickelt worden ist, entfernt sich ziemlich weit von der Art des Schließens, wie sie in Wirklichkeit bei mathematischen Beweisen geübt wird. […] Ich wollte nun zunächst einmal einen Formalismus aufstellen, der dem wirklichen Schließen möglichst nahe kommt. So ergab sich ein „Kalkül des natürlichen Schließens“.^[3]

Der wesentlichste äußerliche Unterschied zwischen NJ-Herleitungen und Herleitungen in den Systemen von Russell, Hilbert, Heyting ist folgender: Bei letzteren werden die richtigen Formeln aus einer Reihe von „logischen Grundformeln“ durch wenige Schlussweisen hergeleitet; das natürliche Schließen geht jedoch im allgemeinen nicht von logischen Grundsätzen aus, sondern von Annahmen […], an welche sich logische Schlüsse anschließen. Durch einen späteren Schluss wird dann das Ergebnis wieder von der Annahme unabhängig gemacht.^[4]

Um die Reichweite der Abhängigkeit von einer Annahme anzuzeigen, entwickelte Jaśkowski zwei unterschiedliche Verfahren: Zum einen werden diejenigen Formeln, die von einer bestimmten Formel abhängig sind, in ein Rechteck eingeschlossen. Solche Rechtecke können ineinander geschachtelt sein, sie dürfen sich aber nicht überschneiden, in dem Sinne, dass sich die Oberseite eines Rechtecks innerhalb und die Unterseite außerhalb eines anderen Rechtecks befindet.^[5] Jaśkowski andere Methode ist im Wesentlichen äquivalent: Hier wird die Gültigkeit von Annahmen durch eine an den Rand des Beweises geschriebene Kette von Zahlen repräsentiert. ^[6]

Gentzen verwendete zur Repräsentation der Abhängigkeiten dagegen eine baumartige Anordnung der Formeln im Beweis: Blätter des Baumes entsprechen Annahmen und die Wurzel der bewiesenen Formel. Manche Kanten sind mit Informationen über getilgte Annahmen annotiert. Neu bei Gentzen ist die Systematik der Regeln; anders als bei Jaśkowski gibt es hier zum ersten Mal Einführungs- und Beseitigungsregeln für jeden Operator. (Bei Gentzen ergibt sich hierdurch jedoch der intuitionistische Kalkül, die klassischen Folgerungen stellen sich bei ihm erst durch zusätzliche Axiome ein.)

Zum ersten Mal in einem Lehrbuch verwendet werden KdnS in Quines „Methods of Logic“ von 1950.^[7] Im Jahre 1952 kombiniert Fitch Gentzens Systematik von Einführungs- und Beseitigungsregel mit Jaśkowskis Rechteck-Repräsentation („Fitch-Kalkül“, allerdings wird bei Fitch das Rechteck nicht geschlossen, sondern nur an der linken Seite als „Hypothesenstrich“ angedeutet) .^[8] Im Jahre 1957 entwickelt Suppes eine neue Repräsentationsform für Abhängigkeiten: Ähnlich wie bei Jaśkowskis zweiter Darstellungsform erscheinen die Abhängigkeiten als Annotation an der Seite des Beweises. Im Unterschied zu Jaśkowski und zu jedem anderen bis dahin existierenden KdnS brauchen bei Suppes die Formeln, die von einer bestimmten Annahme abhängig sind, nicht mehr hintereinander zu stehen. Es ist dadurch nicht länger notwendig, Annahmen zu „schachteln“, und Beweise können in einer eher linearen Form geschrieben werden. Eine weitere Neuerung bei Suppes ist die Einführung von Parametern.^[9]

Fußnoten/Quellen

1. ↑ vgl. F.J. Pelletier: „A History of Natural Deduction and Elementary Logic Textbooks“ S. 106ff (zum Text siehe Weblinks).
2. ↑ Pelletier: "A History ..." S.107 f
3. ↑ Gentzen: „Untersuchungen …“ S. 176
4. ↑ Gentzen: „Untersuchungen …“ S. 184
5. ↑ Pelletier: „A History …“ S. 109
6. ↑ Pelletier: „A History ...“ S. 110
7. ↑ Pelletier: „A History …“ S. 121
8. ↑ Pelletier: „A History …“ S. 124 f
9. ↑ Pelletier: „A History …“ S. 129

Weblinks

• F.J. Pelletier: „A History of Natural Deduction and Elementary Logic Textbooks“
• Visualisierung des Kalküls

Literatur

• F.B. Fitch: Symbolic Logic, New York 1952.
• Gerhard Gentzen: „Untersuchungen über das logische Schließen“, Mathematische Zeitschrift 39, 1934–1935

Nachdruck in: Karel Berka, Lothar Kreiser: Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik, Akademie-Verlag Berlin 4. Aufl. 1986.

Online-Version der Universität Göttingen: Teil 1 und Teil 2

• Gerhard Gentzen (hrsg. M. E. Szabo): The Collected Papers of Gerhard Gentzen, Amsterdam 1969.
• STANISŁAW JAŚKOWSKI, On The Rules Of Suppositions In Formal Logic, POŚWIĘCONE LOGICE I JEJ HISTORJI, 1, WARSZAWA 1934
• Ingebrigt Johansson: „Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus“, Compositio Mathematica, 4(1937), Seite 119–136
• W.V.O. Quine: Methods of Logic, New York, 1950.
• Eike von Savigny: Grundkurs im logischen Schließen: Übungen zum Selbststudium. – 2. verb. Aufl. – Göttingen: Vandenhoeck und Rupprecht, 1984. ISBN 3-525-33502-4.
• Patrick Suppes: Introduction to Logic, Princeton 1957.