## [Sequentenkalkül](/de/node/59902) Definition Ein formales deduktives Rahmenwerk, in dem Sequents die primären syntaktischen Einheiten sind und Beweise durch Anwendung struktureller und logischer Inferenzregeln auf Sequents konstruiert werden; typischerweise enthält es eine Cut-Regel und ggf. strukturelle Regeln wie Schwächung, Kontraktion und Vertauschung. ## Prinzip Prinzip Der Sequentenkalkül organisiert Deduktion um lokale Manipulationen von Antezedens- und Sukzedens‑Komponenten; diese Lokalität unterstützt modulare Beweistransformationen (z. B. Cut-Elimination) und systematische Beweissuche. ## Demonstration Demonstration Im klassischen Sequentenkalkül LK leitet man etwa A∨B ⇒ A∨B über Identitätsaxiome und verwendet Links/Rechts‑Einführungsregeln, um größere Beweise zu bauen; eine Standarddemonstration ist die Cut‑Elimination, die einen Beweis mit Cut in einen ohne Cut überführt. ## Fehlanwendung Fehlanwendung Sequentenkalkül‑Regeln als semantische Umschreibungsregeln statt als syntaktische Inferenzschritte zu behandeln oder in Kontexten (z. B. linearer Logik) unbeschränkte strukturelle Regeln anzuwenden, was zu unsachgemäßen oder unzulässigen Ableitungen führt. ## Konsequenz Konsequenz Der Sequentenkalkül unterstützt metatheoretische Resultate (Cut‑Elimination, Konsistenz, Subformula‑Eigenschaft in bestimmten Formulierungen) und praktische Werkzeuge (systematische rückwärtsgerichtete Beweissuche, Grundlage für automatische Theorembeweiser und Beweistransformationen). ## Umkehrung Umkehrung Die Umkehr besteht darin, alternative Rahmen (natürliche Deduktion, Hilbert‑Systeme) zu verwenden, in denen Inferenzregeln auf Formeln statt auf Sequents wirken; der Vergleich zeigt unterschiedliche Kompromisse zwischen Symmetrie, Lokalität und Beweisgröße. ## Abgrenzung Abgrenzung Gilt für die syntaktische Beweistheorie und formale Systeme, die Folgerung durch Sequents darstellen; es liefert selbst keine semantischen Modelle und muss durch Signatur und Regelmenge instanziiert werden — unterschiedliche Wahl ergibt klassische, intuitionistische, lineare oder andere Varianten. ## Semantische Spannung Semantische Spannung Spannung besteht zwischen Sequentenkalkül und natürlicher Deduktion: Sequentenkalkül betont Symmetrie und strukturelle Manipulation von Kontexten, natürliche Deduktion betont Einführung/Elimination von Junktoren und oft kompaktere Beweise für menschliches Denken. ## Synthese Synthese Der Sequentenkalkül ist eine regelbasierte, sequentenzentrierte Deduktivarchitektur, die strukturelle Operationen explizit macht, rigorose Beweistransformationstheoreme ermöglicht und mechanisierte Beweissuche unterstützt, wobei die konkrete Logik durch Wahl der Regeln bestimmt wird.