Systeme natürlichen Schließens

Systeme (oder Kalküle) natürlichen Schließens sind ein Kalkültyp, der 1934 von Gerhard Gentzen ("Untersuchungen über das logische Schließen", in: Mathematische Zeitschrift 39, 1934-1935) und etwa zeitgleich von Stanislaw Jaskowski 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 Folgerungsregeln. Zusammen mit den (gleichfalls von Gentzen entwickelten) Sequenzenkalkülen gehören Systeme des natürlichen Schließens zur Familie der Regellogiken.

Mit Systemen natürlichen Schließens kann zugleich der Anspruch verbunden werden, in Form einer "direkten Semantik" durch Angabe der Regeln zugleich die Bedeutung für logische Operatoren festzulegen.

Üblicherweise werden die Folgerungsregeln so systematisiert, dass neben einer Annahmeregel, die es gestattet, jede beliebige Aussage anzunehmen, für jeden Operator eine Einführungs- und eine Beseitigungsregel angegeben wird. 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.

Für die (klassische) Aussagenlogik gelten dabei folgende Regeln (Prämissen sind durch Kommata abgetrennt, der Doppelpfeil steht für den Übergang von den Prämissen zur Konklusion, eckige Klammern markieren Abhängigkeiten):

$\wedge E:\ A,\ B\Rightarrow \ A\wedge B$

$\wedge B:\ A\wedge B\Rightarrow \ A;\ A\wedge B\ \Rightarrow \ B$

$\vee E:\ A\Rightarrow \ A\vee B$

$\vee B:\ A\vee B,\ [A]\ C,\ [B]\ C\ \Rightarrow \ C$

$\rightarrow E:\ [A]\ B\ \Rightarrow \ A\rightarrow B$

$\rightarrow B:\ A\rightarrow B,\ A\Rightarrow \ B$

$\lnot E:\ [A]\ (B\wedge \lnot B)\ \Rightarrow \ \lnot A$

$\lnot B:\ \lnot \lnot A\Rightarrow \ A$

Ersetzt man in einem solchen Kalkül die Regel der Negationsbeseitigung $\lnot B$ durch die Regel ex falso quodlibet

$A\wedge \lnot A\Rightarrow B$

ergibt sich ein dem Intuitionismus entsprechender Kalkül, streicht man die Regel vollständig, erhält man einen Minimalkalkül.