Eine metatheoretische Eigenschaft eines deduktiven Systems, die besagt, dass immer wenn das System eine Disjunktion A ∨ B beweist, es entweder A oder B einzeln beweist; dies wird typischerweise von konstruktiven Systemen gefordert.

Prinzip

Konstruktive Beweise einer Disjunktion müssen Informationen enthalten, die aussagen, welcher Disjunkt gilt: Ein Beweis von A ∨ B muss effektiv einen Beweis von A oder einen Beweis von B liefern, statt lediglich ihre gemeinsame Falschheit auszuschließen.

Demonstration

In der intuitionistischen Aussagenlogik oder in bestimmten konstruktiven Typentheorien ergibt sich eine Herleitung von A ∨ B aus einem Beweis-Term, der entweder die linke oder die rechte Injektion in die disjunkte Summe ist; der Term selbst bezeugt, welcher Disjunkt beweisbar ist, und das System beweist diesen Disjunkt.

Fehlanwendung

Zu behaupten, die Disjunktions-Eigenschaft gelte in klassischen Systemen oder für beliebige metatheoretische Kodierungen; oder eine auf Metaebene beweisbare Disjunktion als unmittelbaren Beweis eines Disjunkts ohne internes konstruktives Zeugnis auszulegen.

Konsequenz

Hat ein System die Disjunktions-Eigenschaft, so lässt sich aus disjunktiven Beweisen konkrete algorithmische Information extrahieren; dies verbessert Programmextraktion und stellt sicher, dass Alternativbeweise nicht bloße nicht-konstruktive Widerspruchsargumente sind.

Umkehrung

Fehlt die Eigenschaft, so kann das System A ∨ B beweisen, ohne A oder B zu beweisen, typischerweise durch Rückgriff auf nicht-konstruktive Prinzipien wie das ausgeschlossene Dritte oder klassische Argumente.

Abgrenzung

Bezieht sich auf die Beweisbarkeit in der Objekttheorie und oft nur auf geschlossene oder arithmetische Formeln; sie behauptet nicht, dass jede metatheoretische Disjunktion in jedem Formalismus ein internes Zeugnis hat und kann in Erweiterungen mit klassischen Axiomen versagen.

Semantische Spannung

Spannung zum Prinzips des ausgeschlossenen Dritten: Dieses erlaubt das Beweisen von A ∨ ¬A ohne Angabe, welche Seite gilt, was dem konstruktiven Anspruch der Disjunktions-Eigenschaft entgegenläuft.

Synthese

Die Disjunktions-Eigenschaft fasst die konstruktive Forderung zusammen, dass Beweise von Alternativen informativ sein müssen: Beweist das System A ∨ B, so muss es innerhalb des Systems einen der Disjunkte beweisen und damit eine konkrete Auswahl liefern statt bloßer Nichtwidersprüchlichkeit.