Systeme natürlichen Schließens
Kalküls der mathematischen und der philosophischen Logik
Systeme natürlichen Schließens sind ein Kalkültyp, der 1934 von Gerhard Gentzen (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.
Üblicherweise werden diese so systematisiert, daß 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 überzuehen; die Beseitigungsregel führt von einer Aussage mit O als Hauptoperator zu einer anderen Aussage. Für die Konjunktion gilt etwa:
- Konjunktionseinführung:
- p
- q
- Also: p & q
- Konjunktionsbeseitigung:
- p & q
- Also: p
- p & q
- Also: q