Logikkalkül

Quelle: Wikipedia. Seiten: 40. Kapitel: Systeme natürlichen Schließens, Resolution, Sequenzenkalkül, Begriffsschrift, Existential Graphs, Termlogik, Lambda-Kalkül, Baumkalkül, Dialogische Logik, Charakteristische Zahlen, Hoare-Kalkül, Wp-Kalkül, Hilbert-Kalkül, Semi-Thue-System, Fitch-Kalkül, Davis-Putnam-Verfahren, Diskursuniversum, Termkalkül, Aussagenkalkül, Gentzentypkalkül, Normal Order Reduction, Applicative Order Reduction. Auszug: In der Beweistheorie und der mathematischen Logik bezeichnet man mit Sequenzenkalkül eine Familie formaler Systeme (oder Kalküle), die einen bestimmten Stil der Ableitung und gewisse gemeinsame Eigenschaften teilen. Die ersten Sequenzenkalküle, LK für die klassische und LJ für die intuitionistische Logik, sind von Gerhard Gentzen im Jahre 1934 als formaler Rahmen für die Untersuchung von Systemen des natürlichen Schließens in der Prädikatenlogik 1. Ordnung. Der Gentzensche Hauptsatz über LK und LJ besagt, dass die Schnittregel in diesen Systemen gilt, ein Satz mit weitreichenden Konsequenzen in der Metalogik. Die Flexibilität des Sequenzenkalküls zeigte sich später, im Jahr 1936, als Gentzen die Technik der Schnitt-Elimination verwendete, um die Widerspruchsfreiheit der Peano-Axiome zu beweisen. Die auf Gentzen zurückgehenden Sequenzenkalküle und die allgemeinen Konzepte, die dahinterstehen, werden in weiten Bereichen der Beweistheorie, mathematischen Logik und des maschinengestützten Beweisens standardmäßig verwendet. In diesem Artikel werden folgende Zeichen verwendet: Es werden folgende Konventionen eingeführt: Mittels einer Umformungsregel lässt sich der Quantor (Allquantor) wie folgt darstellen: Von diesen Umformungen wird in den Beispielen Gebrauch gemacht. Der Sequenzenkalkül dient dazu, das Vorgehen beim mathematischen Beweisen von Theoremen möglichst genau abzubilden. Ein Bestandteil dieser Beweismethode ist, dass an jeder Stelle des Beweises Zusatzvoraussetzungen eingebracht werden können, die dann entweder bis zum Schluss stehen bleiben oder aber wieder eliminiert werden können. Die Grundeinheit des Sequenzenkalküls ist eine Zeichenfolge (eine Sequenz) aus Variablen , die jeweils für Ausdrücke des jeweils betrachteten logischen Systems stehen; z.B. für Ausdrücke einer Sprache erster Stufe. Eine solche Sequenz bezeichnen wir mit oder kürzer mit wobei für die Folge der Ausdrücke steht. Die Idee dabei ist, dass in die Voraussetzungen stehen und das letzte Gl