##  [Display-Logik](/de/node/60966) 

 Definition

Ein strukturaler Beweiskalkül, der durch Display-Axiome gekennzeichnet ist, welche es erlauben, jede Teilstruktur eines Sequents auf eine Seite des Turnstils zu 'displayen' (isolieren), so dass die jeweilige Hauptregel angewandt werden kann; Display-Logik bietet einen einheitlichen Mechanismus zur Handhabung vielfältiger Konnektive und struktureller Manipulationen.

 

 

 

 

 

 





## Prinzip

Prinzip

Verwende strukturelle Konnektive und Display-Axiome, um Sequents so umzuordnen, dass eine gewählte Teilstruktur in Fokusposition gebracht werden kann; ist sie einmal displayed, wirken logische Regeln lokal auf diese Teilstruktur, und Metatheoreme wie Cut-Elimination folgen aus der einheitlichen Strukturverwaltung.

 

 

 

 

 





## Demonstration

Demonstration

Um eine Implikationsregel auf eine tief eingebettete Teilformel in einem komplexen Antezedens anzuwenden, schreiben Display-Axiome die umgebende Struktur so um, dass die Teilformel allein links vom Turnstil erscheint; die Implikationsregel wird dann direkt angewandt und der Sequent bei Bedarf wieder zurückgeordnet, womit das Vorgehen für verschiedene Konnektive systematisch wird.

 

 

 

 

## Fehlanwendung

Fehlanwendung

Zu glauben, Display-Logik vereinfache automatisch jeden Beweis oder die Kosten wiederholter struktureller Umordnungen zu ignorieren, kann irreführend sein: naiver Einsatz kann Komplexität verbergen, und Display-Axiome ohne Sicherstellung der Zulässigkeit struktureller Regeln für die Ziellogik anzuwenden, kann inkorrekte oder nicht-konservative Erweiterungen erzeugen.

 

 

 

 

 





## Konsequenz

Konsequenz

Display-Logik liefert eine einheitliche, modulare Darstellung vieler Konnektive und Strukturregeln, erleichtert häufig metatheoretische Beweise (Cut-Elimination, Konservativität) und erlaubt den Transfer struktureller Erkenntnisse zwischen Logiken mit displaybarer Struktur.

 

 

 

 

## Umkehrung

Umkehrung

Die Umkehrung ist das Arbeiten ohne Displaybarkeit, also sequentielle Kalküle, in denen Teilstrukturen nicht immer durch allgemeine Axiome isolierbar sind; solche Kalküle können in bestimmten Fällen einfacher zu implementieren sein, verlieren jedoch den einheitlichen Mechanismus zur Handhabung beliebiger struktureller Kontexte.

 

 

 

 

 





## Abgrenzung

Abgrenzung

Display-Logik ist anwendbar, wenn strukturelle Konnektive und Axiome definiert werden können, um Teilstrukturen zu verschieben; sie ist weniger nützlich für Logiken, deren strukturelles Verhalten sich gegen Display-Axiome sperrt, oder wenn der Aufwand der strukturellen Manipulation den Nutzen an Uniformität übersteigt.

 

 

 

 

 





## Semantische Spannung

Semantische Spannung

Spannung zwischen Display-Logik und anderen strukturellen Kalkülen (Sequent, Hypersequent, gelabelte Systeme): Display-Logik betont eine universelle strukturelle Algebra und Axiome zur Isolierung von Teilstrukturen, während Alternativen Generalität gegen einfachere Syntax oder direktere semantische Repräsentationen abwägen.

 

 

 

 

 





## Synthese

Synthese

Display-Logik bietet eine strukturelle Algebra und Display-Axiome, die jede Teilstruktur für Regelanwendung zugänglich machen: durch systematisches Umordnen von Sequents in Display-Form erreicht man eine einheitliche Behandlung von Konnektiven und Strukturen, die modulare Metatheorie ermöglicht, allerdings mit expliziter struktureller Buchführung.