Systeme natürlichen Schließens

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

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:

${\displaystyle \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).

${\displaystyle \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)).

${\displaystyle \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).

${\displaystyle \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)).

${\displaystyle \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“.

${\displaystyle \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).

${\displaystyle \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.

${\displaystyle \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).

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 (${\displaystyle \forall xA}$ oder ${\displaystyle \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.

${\displaystyle \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.

${\displaystyle \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“.

${\displaystyle \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“.

${\displaystyle \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“.

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

${\displaystyle =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.

${\displaystyle =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“.

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

Abhängigkeit(en)	Zeile	Aussage	Regel	angewendet auf
1	1	${\displaystyle A\rightarrow B}$	fixe Annahme
2	2	${\displaystyle \lnot B}$	fixe Annahme
3	3	${\displaystyle A\ }$	Annahme
1, 3	4	${\displaystyle B\ }$	${\displaystyle \rightarrow B}$	1, 3
1, 2, 3	5	${\displaystyle B\wedge \lnot B}$	${\displaystyle \wedge E}$	2, 4
1, 2	6	${\displaystyle \lnot A}$	${\displaystyle \lnot E}$	(3,) 5
1	7	${\displaystyle \lnot B\rightarrow \lnot A}$	${\displaystyle \rightarrow E}$	(2,) 6
	8	${\displaystyle (A\rightarrow B)\rightarrow (\lnot B\rightarrow \lnot A)}$	${\displaystyle \rightarrow E}$	(1,) 7

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, ${\displaystyle \lnot \lnot B}$, durch die Regel ex contradictione sequitur quodlibet, ${\displaystyle {\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, ${\displaystyle \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, ${\displaystyle \wedge E}$, so erhält man einen so genannten nicht adjunktiven parakonsistenten Logikkalkül.

Der Gentzensche Hauptsatz besagt, dass die Schnittregel

${\displaystyle \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. (${\displaystyle \Gamma }$ und ${\displaystyle \Delta }$ sind Listen von Formeln)