Ein syntaktisches Objekt der Form Γ ⇒ Δ (wobei Γ und Δ typischerweise endliche Multimengen oder Folgen von Formeln sind), das ausdrückt, dass die Konjunktion der Formeln in Γ die Disjunktion der Formeln in Δ in einem sequentiellen Kalkül impliziert.

Prinzip

Ein Sequent internalisiert Folgerung als ein einzelnes formelartiges Token, sodass Inferenzregeln lokal auf Antezedens- und Sukzedens‑Komponenten wirken und so systematische Manipulation der Folgerungsstruktur erlauben.

Demonstration

Sequent-Beispiel: {A, A→B} ⇒ {B}. Im klassischen Sequentenkalkül erlauben die Regeln die Transformation der Prämissen in das Sukzedens; dieses einzelne Sequent repräsentiert die Behauptung, dass A und A→B zusammen B implizieren.

Fehlanwendung

Ein Sequent Γ ⇒ Δ einfach als materiale Implikation (∧Γ)→(∨Δ) zu lesen, ohne strukturelle Regeln oder Kontext zu beachten, oder Sequents als semantische Konditionale zu behandeln, wo der Kalkül strukturelle Regeln einschränkt (z. B. intuitionistische Sequents mit Einzelconclusion).

Konsequenz

Die Verwendung von Sequents macht strukturelle Phänomene (Schwächung, Kontraktion, Vertauschung, Cut) explizit; die Sequentdarstellung unterstützt Metaergebnisse wie Cut-Elimination und systematische Strategien zur Beweissuche.

Umkehrung

Die Umkehr besteht darin, Antezedens und Sukzedens zu vertauschen (Δ ⇒ Γ) oder sequentielle Urteile zurück in Formeltheoreme eines Hilbert‑Systems zu überführen; solche Umkehrungen heben Asymmetrien hervor (etwa intuitionistische Ein-Schluss-Sequents).

Abgrenzung

Gilt innerhalb von Sequentenkalkülen und verwandten syntaktischen Rahmen; es ist ein formales Mittel und selbst keine semantische Bewertung oder ein Modell; Sequents setzen eine Entscheidung darüber voraus, ob Γ/Δ Mengen, Multimengen oder Folgen sind und welche strukturellen Regeln gelten.

Semantische Spannung

Spannung besteht zwischen dem Sequent als syntaktischem Folgerungs‑Token und alternativen Darstellungen der Folgerung (Hilbert‑Beweise, natürliche Deduktion, Tableaux): alle drücken Konsequenz aus, verteilen aber die logische Arbeit unterschiedlich über Regeln und Kontexte.

Synthese

Ein Sequent ist eine konzentrierte syntaktische Repräsentation von Folgerung Γ ⇒ Δ, entworfen, damit lokale Inferenzregeln Antezedens- und Sukzedens‑Teile manipulieren und so strukturelle Analyse und algorithmische Beweisumformungen ermöglichen.