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.

• Anders als bei den allermeisten anderen Kalkültypen wie Tableaukalkül, Axiomatischem 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.

Geschichte

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. 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 nahekommt. So ergab sich ein „Kalkül des natürlichen Schließens“.

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.

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. Jaśkowskis 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.

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.)

Ein wenig später reichte Gentzen im August 1935 eine Arbeit mit dem Titel Die Widerspruchsfreiheit der reinen Zahlentheorie ein, in der er den aus seinem Sequenzenkalkül entstammenden Begriff der Sequenz auf das natürliche Schließen übertrug. Hiermit kann die Abhängigkeit von Annahmen und deren Tilgung ohne weitere Hilfsbegriffe in expliziter Weise innerhalb der Schlussregeln beschrieben werden. Mithin stellt jede ableitbare Sequenz für sich allein bereits ein Theorem dar, da sie sämtliche Abhängigkeiten ihrer Hinterformel enthält.

Zum ersten Mal in einem Lehrbuch verwendet werden KdnS in Quines „Methods of Logic“ von 1950. 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). 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.

Die Regeln

Annahmeregel und Abhängigkeit

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_{0}$ … $C_{n}$ abhängig, so bestünden diese Abhängigkeiten weiter fort. „Wenn A, dann B“ wäre dann also immer noch von $C_{0}$ … $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_{0}$ … $B_{n}$, so hat man gezeigt, dass $B_{0}$ … $B_{n}$ die Aussage A logisch implizieren.

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 Skolem war 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 Skolem war 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\quad A\vdash \lnot B}{\lnot A}}$

Wenn sich aus einer Aussage A sowohl B als auch „nicht B“ und damit ein Widerspruch herleiten lässt, dann darf auf die Negation „nicht A“ geschlossen werden.

Beispiel: Aus der Aussage „Der Norweger Skolem ist Schwede“ (A) folgt zum einen „Skolem war Norweger“ (B). Es folgt aber auch „Skolem war kein Norweger“ (¬B), weil er nach (A) ja Schwede ist. Wir können also schließen: „Es trifft nicht zu, dass der Norweger Skolem Schwede ist“ (¬A).

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 xA$ oder $\exists xA$) 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 xA}}$, 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 xA}{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 xA}}$

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 gab Norweger“.

$\exists B:\ {\frac {\exists xA\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

Diese Ableitung beweist die Kontraposition $(A\rightarrow B)\rightarrow (\lnot B\rightarrow \lnot A)$.

Abhängigkeit(en)	Zeile	Aussage	Regel	angewendet auf
1	1	$A\rightarrow B$	fixe Annahme
2	2	$\lnot B$	fixe 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 sogenannten 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 zulässig (eliminierbar) ist. ($\Gamma$ und $\Delta$ sind Listen von Formeln.)

Literatur

• Ludwik Borkowski: Formale Logik. Logische Systeme. Einführung in die Metalogik. Akademie-Verlag, Berlin 1976, S. 41–83.
• Irving Copi: Einführung in die Logik (= Uni-Taschenbücher. Philosophie 2031). München, Fink 1998, ISBN 3-8252-2031-1.
• Wilhelm K. Essler, Elke Brendel, Rosa F. Martínez Cruzado: Grundzüge der Logik. Band 1: Wilhelm K. Essler, Rosa F. Martínez Cruzado: Das logische Schließen. 4. Auflage. Klostermann, Frankfurt am Main 1991, ISBN 3-465-02501-6.
• Frederic Brenton Fitch: Symbolic Logic. An Introduction. Ronald Press Company, New York NY 1952.
• Gerhard Gentzen: Untersuchungen über das logische Schließen. In: Mathematische Zeitschrift. Band 39, 1935, S. 176–210, 405–431, Nachdruck in: Karel Berka, Lothar Kreiser: Logik-Texte. Kommentierte Auswahl zur Geschichte der modernen Logik. 4., gegenüber der 3., erweiterte, durchgesehene Auflage. Akademie-Verlag, Berlin 1986; Online-Version der Universität Göttingen: Teil 1 und Teil 2.
• Gerhard Gentzen: Die Widerspruchsfreiheit der reinen Zahlentheorie. In: Mathematische Annalen. Band 112. Springer, Berlin 1936, S. 493–565.  Band 112 online via GDZ.

• Gerhard Gentzen: The Collected Papers. Edited by Manfred E. Szabo. North-Holland Publishing Co., Amsterdam u. a. 1969.
• Michael Huth, Mark Ryan: Logic in Computer Science: Modelling and Reasoning about Systems. 2nd edition, Cambridge University Press, 2004.
• Stanisław Jaśkowski: On the Rules of Suppositions in Formal Logic (= Uniwersytet Darszawski. Seminarjum Filozoficzne. Studia logica. Nr. 1). Nakładem Seminarjum Filozoficznego Wydziału Matematyczno-Przyrodniczego Uniwersytetu Warszawskiego, Warschau 1934.
• Ingebrigt Johansson: Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. In: Compositio Mathematica. Band 4, 1937, S. 119–136, numdam.org (PDF; 1,4 MB)
• Willard Van Orman Quine: Methods of Logic. Holt, Rinehart and Winston, New York NY u. a. 1950.
• Eike von Savigny: Grundkurs im logischen Schließen. Übungen zum Selbststudium (= Kleine Vandenhoeck-Reihe. Band 1504). 2., verbesserte Auflage. Vandenhoeck & Ruprecht, Göttingen 1984, ISBN 3-525-33502-4.
• Patrick Suppes: Introduction to Logic. Van Nostrand, New York NY u. a. 1957.

Weblinks

• Andrzej Indrzejczak: Natural Deduction. In: J. Fieser, B. Dowden (Hrsg.): Internet Encyclopedia of Philosophy.
• Francis Jeffry Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. (PDF; 182 kB) In: John Woods, Bryson Brown (Hrsg.): Logical consequence. Rival approaches. Proceedings of the 1999 Conference of the Society of Exact Philosophy. Hermes Science, Oxford 2001, ISBN 1-903398-17-7, S. 105–138.
• Richard Bornat und Bernard Sufrin: Jape (Just Another Proof Editor) Programm für interaktives natürliches Schließen
• Burkhardt Renz et al.: Logic Workbench in Clojure mit einem Programm für interaktives natürliches Schließen in der Aussagen-, Prädikaten- und linearen temporalen Logik.
• Cezary Kaliszyk et al.: ProofWeb, ein webbasiertes Programm für interaktives natürliches Schließen, basierend auf Coq.
• Michel Lévy: Propositional natural deduction prover