Gentzentypkalkül
aus Wikipedia, der freien Enzyklopädie
Dies ist die aktuelle Version dieser Seite, zuletzt bearbeitet am 21. Oktober 2023 um 14:31 Uhr durch Georg Hügler (Diskussion | Beiträge).
Eine gesichtete Version dieser Seite, die am 21. Oktober 2023 freigegeben wurde, basiert auf dieser Version.
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
[Bearbeiten | Quelltext bearbeiten ]- Gerhard Gentzen: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39 (1934). Nachdruck in: Karel Berka, Lothar Kreiser: Logik-Texte, Berlin (Ost) 1986. Teil 1 und Teil 2
- Sequent Calculus by Alex Sakharov MathWorld