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:

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 , 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  …  abhängig, so bestünden diese Abhängigkeiten weiter fort. „Wenn A, dann B“ wäre dann also immer noch von  …  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  … , so hat man gezeigt, dass  …  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:

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

, wobei A(u) nicht abhängig von einer Aussage ist, in der u vorkommt.

, wobei u weder in B vorkommt noch in irgendeiner Aussage, von der B abhängig ist, ausgenommen die Parametrisierung A(u).

Identität

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

Eine Beispielableitung

Diese Ableitung beweist die Kontraposition .

Abhängigkeit(en)	Zeile	Aussage	Regel	angewendet auf
1	1		fixe Annahme
2	2		fixe Annahme
3	3		Annahme
1, 3	4			1, 3
1, 2, 3	5			2, 4
1, 2	6			(3,) 5
1	7			(2,) 6
8			(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, , durch die Regel ex contradictione sequitur quodlibet, , 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, ersatzlos, erhält man den sogenannten Minimalkalkül (Kolmogorow 1924, Johansson 1937).
• Streicht man dagegen die Regeln zur Einführung der Konjunktion, , so erhält man einen so genannten nicht adjunktiven parakonsistenten Logikkalkül.

Schnittregel

Der Gentzensche Hauptsatz besagt, dass die Schnittregel

in den Systemen natürlichen Schließens zulässig (eliminierbar) ist. ( und 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

Einzelnachweise

1. Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. 2001, S. 106 ff. (zum Text siehe Weblinks).
2. Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. 2001, S. 107 f.
3. Gentzen: Untersuchungen über das logische Schließen. 1935, S. 176.
4. Gentzen: Untersuchungen über das logische Schließen. 1935, S. 184.
5. Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. 2001, S. 109.
6. Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. 2001, S. 110.
7. Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. 2001, S. 121.
8. Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. 2001, S. 124 f.
9. Pelletier: A History of Natural Deduction and Elementary Logic Textbooks. 2001, S. 129.