Gentzentypkalkül

aus Wikipedia, der freien Enzyklopädie
Dies ist die aktuelle Version dieser Seite, zuletzt bearbeitet am 17. Juli 2021 um 08:12 Uhr durch imported>Aka(568) (→‎Weblinks: https, Kleinkram).
(Unterschied) ← Nächstältere Version | Aktuelle Version (Unterschied) | Nächstjüngere Version → (Unterschied)

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.

Weblinks