Gentzentypkalkül

Unter Gentzentypkalkülen versteht man Logikkalküle eines bestimmten Typs. Sie werden nach dem Mathematiker und Logiker Gerhard Gentzen genannt, weil diese Kalküle seinen Sequenzenkalkülen ähnlich sind.

Im Einzelnen handelt es sich um die Sequenzenkalküle LJ und LK, die Systeme des natürlichen Schließens NJ und NK (J ist jeweils der intuitionistische und K der klassische Kalkül), die Bethschen Baumkalküle (Tableaux) und die Dialogische Logik.

Im Gegensatz zu Logikkalkülen vom Hilberttyp gilt in den Gentzentypkalkülen der Gentzensche Hauptsatz, der besagt, dass die Schnittregel im jeweiligen Kalkül zulässig ist. Das bedeutet, dass die Schnittregel nicht extra zu den Kalkülregeln hinzugenommen werden muss.