Systeme natürlichen Schließens

Systeme (oder Kalküle) natürlichen Schließens bezeichnen in der mathematischen und philosophischen Logik einen 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 A eine Aussage B abzuleiten, so kann auf die Aussage „Wenn A, dann B“ übergegangen werden. (Dies ist die Implikations-Einführung $\rightarrow E$, siehe auch unten.) Indem die Annahme A nun sozusagen explizit in die Aussage mit aufgenommen wurde („Wenn A, …“), kann die Abhängigkeit von ihr getilgt werden. D.h. "Wenn A, dann B" ist nicht länger von A abhängig. Wäre B noch von weiteren Aussagen C₀ … C_n abhängig, so bestünden diese Abhängigkeiten weiter fort. „Wenn A, dann B“ wäre dann also immer noch von C₀ … C_n abhängig.

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

Die Regeln

Klassische Logik

Aussagenlogik

Für die klassische Aussagenlogik werden meist folgende Einführungs- (E) und Beseitigungsregeln (B) verwendet. Dabei stehen die Prämissen oberhalb des Folgerungsstrichs, die Konklusion unterhalb, eckige Klammern markieren zu beseitigende Abhängigkeiten:

$\wedge E:\ \frac{A\quad B}{A \wedge B}\qquad\frac{A\quad B}{B \wedge A}$

Aus zwei Aussagen A und B kann die Konjunktion „A und B“ geschlossen werden (Regel der Einführung der Konjunktion).

Beispiel: Aus den Aussagen „Skolem war Norweger“ (A) und „Skolem war Logiker“ (B) kann geschlossen werden: „Skolem war Norweger und Logiker“ (A ∧ B).

$\wedge B:\ \frac{A \wedge B}{A}\qquad \frac{A \wedge B}{B}$

Aus einer Konjunktion „A und B“ kann jedes einzelne Konjunkt, also sowohl A als auch B erschlossen werden (Regel der Beseitigung der Konjunktion).

Beispiel: Aus „Skolem war Norweger und Logiker“ (A ∧ B) kann geschlossen werden: „Skolem war Norweger“ (A) [und auch „Skolem war Logiker“ (B)].

$\vee E:\ \frac{A}{A \vee B}\qquad \frac{A}{B \vee A}$

Aus einer Aussage A kann die Disjunktion „A oder B“ geschlossen werden.

Beispiel: Aus „Skolem war Norweger“ (A) kann geschlossen werden: „Skolem war Schwede oder Norweger“ (A ∨ B).

$\vee B:\ \frac{A \vee B\quad A\vdash C\quad B\vdash C}{C}$

Wenn es gelingt, aus jedem Disjunkt einer Disjunktion „A oder B“ einen Satz C herzuleiten, dann folgt dieser Satz aus der Disjunktion.

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

Diese Regel entspricht der Beweistechnik der „Fallunterscheidung“ (vgl. Beweis (Mathematik)).

$\rightarrow E:\ \frac{A\vdash B}{A \rightarrow B}$

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

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

Diese Regel entspricht der Beweistechnik „Konditionaler Beweis“.

$\rightarrow B:\ \frac{A \rightarrow B \quad A}{B}$

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

Beispiel: Aus „Wenn Skolem Norweger war, dann war er Skandinavier“ (A → B) folgt zusammen mit „Skolem war Norweger“ (A) die Aussage „Skolem war Skandinavier“ (B).

$\lnot E:\ \frac{A \vdash B \wedge \lnot B}{\lnot A}$

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

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

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

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

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

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

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 A$ oder $\exists x A$, durch den Term t, A(t) ist das Resultat der Ersetzung aller in A freien Vorkommnisse von x durch t. Eine Parametrisierung einer dieser Aussagen durch den Parameter u, A(u), ist eine Instantiierung durch u, wobei u nicht schon in A vorkommen darf.

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

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

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

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

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

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

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

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

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

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

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

Beispiel: Ich weiß, dass es einen norwegischen Logiker gibt. Aus der Aussage „Skolem war Norweger und Skolem war Logiker“ kann ich schließen „Es gibt einen skandinavischen Logiker“, wobei in diesen Schluss keine weiteren Informationen über Skolem 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 A}{A(t1//t2)}$

Aus „t1=t2“ und einer Aussage A kann eine Aussage A(t1//t2) geschlossen werden, wobei A(t1//t2) aus A hervorgeht, indem alle oder einige Vorkommnisse von t1 in A 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

Abhängigkeit(en)	Zeile	Aussage	Regel	angewendet auf
1	1	$A \rightarrow B$	Annahme
2	2	$\lnot B$	Annahme
3	3	$A\$	Annahme
1, 3	4	$B\$	$\rightarrow B$	1, 3
1, 2, 3	5	$B \wedge \lnot B$	$\wedge E$	2, 4
1, 2	6	$\lnot A$	$\lnot E$	(3,) 5
1	7	$\lnot B \rightarrow \lnot A$	$\rightarrow E$	(2,) 6
	8	$(A \rightarrow B) \rightarrow (\lnot B \rightarrow \lnot A)$	$\rightarrow E$	(1,) 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{\Gamma\vdash A \qquad \Delta,A\vdash B}{\Gamma,\Delta\vdash B}$

in den Systemen natürlichen Schließens gültig ist. (Γ und Δ sind Listen von 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“ (PDF-Datei; 182 kB)
• Visualisierung des Kalküls

Literatur

• Ludwik Borkowski: Formale Logik. Akademie Verlag, Berlin 1976, S. 41-83.
• Irving M. Copi: Einführung in die Logik. - München, Fink 1998 (UTB; 2031).
• Essler/Martínez, Grundzüge der Logik I, 4. Aufl. (1991).
• 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.