Das Kefk Network Wiki befindet sich im Testbetrieb.

Systeme natürlichen Schließens

Aus Kefk.

Wechseln zu: Navigation, Suche

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

Im Gegensatz zu axiomatischen Kalkülen enthält ein System natürlichen Schließens keine Axiome, sondern ausschließlich 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.

Mit Systemen natürlichen Schließens lässt sich zugleich der Anspruch einer „beweistheoretischen Semantik“ verbinden, die Bedeutung der logischen Operatoren (Junktoren) durch die Angabe der Schlussregeln festzulegen.

Üblicherweise werden die Schlussregeln so systematisiert, dass neben einer Annahmeregel, die es gestattet, jede beliebige Aussage anzunehmen, für jeden Operator 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.

Inhaltsverzeichnis

Die Regeln

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}


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


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


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

(Wenn es gelingt, aus jedem Disjunkt einer Disjunktion einen Satz P3 herzuleiten, dann folgt dieser Satz aus der Disjunktion.)


\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 Aussage P1 \rightarrow P2 herleitbar.)


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


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

(Wenn sich aus einer Aussage P1 ein beliebiger Widerspruch herleiten lässt, dann darf P1 verneint werden – Näheres siehe Reductio ad absurdum.)


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


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.

Nichtklassische Logik

Ebenso, wie man aus einem axiomatischen Kalkül für die klassische Logik nicht<span />klassische 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)

Siehe auch

Literatur

  • 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
  • Ingebrigt Johansson: „Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus“, Compositio Mathematica, 4(1937), Seite 119-136
Wikipedia
 Dieses Dokument entstammt in seiner ersten oder einer späteren Version der deutschsprachigen Wikipedia. Es ist dort zu finden unter dem Stichwort Systeme_nat%C3%BCrlichen_Schlie%C3%9Fens, die Liste der bisherigen Autoren befindet sich in der Versionsliste; die Originalfassung kann dort auch bearbeitet werden. Alle Texte der Wikipedia und ihre Derivate stehen unter der GNU-Lizenz für freie Dokumentation.
Von „http://www.kefk.org/wiki/Systeme_nat%C3%BCrlichen_Schlie%C3%9Fens“
Persönliche Werkzeuge
Andere Sprachen