Systeme natürlichen Schließens

Im Gegensatz zu axiomatischen Kalkülen enthält System natürlichen Schließens keine Axiome sondern ausschließlich größere Zahl von Folgerungsregeln. Zusammen mit den von Gentzen entwickelten) Sequenzenkalkülen gehören Systeme des Schließens zur Familie der Regellogiken.

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

Üblicherweise werden die Folgerungsregeln so systematisiert neben einer Annahmeregel die es gestattet jede Aussage anzunehmen für jeden Operator eine Einführungs- eine Beseitigungsregel angegeben wird. Die Einführungsregel für Operator O erlaubt es zu einer Aussage O als Hauptoperator überzugehen; die Beseitigungsregel führt einer Aussage mit O als Hauptoperator zu einer Aussage.

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

<math>\wedge E:\ A \ B \Rightarrow\ \wedge B</math>

<math>\wedge B:\ A \wedge B \Rightarrow\ A \wedge B\ \Rightarrow\ B</math>

<math>\vee E:\ A \Rightarrow\ A \vee

<math>\vee B:\ A \vee B \ C \ [B]\ C\ \Rightarrow\ C</math>

<math>\rightarrow E:\ [A]\ B\ \Rightarrow\ A B</math>

<math>\rightarrow B:\ A \rightarrow B \ \Rightarrow\ B</math>

<math>\lnot E:\ [A]\ (B \wedge \lnot \Rightarrow\ \lnot A</math>

<math>\lnot B:\ \lnot \lnot A \Rightarrow\

Ersetzt man in einem solchen Kalkül Regel der Negationsbeseitigung <math>\lnot B</math> durch die ex falso quodlibet

<math>A \wedge \lnot A \Rightarrow B</math>

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

Bücher zum Thema Systeme natürlichen Schließens

Dieser Artikel von Wikipedia unterliegt der GNU FDL.