Eine Schlussregel, die erlaubt, aus einem Beweis eines der Disjunkte eine Disjunktion A ∨ B zu folgern (aus A folgere A ∨ B, oder aus B folgere A ∨ B).

Prinzip

Ein Beweis, dass ein bestimmtes Disjunkt wahr ist, reicht aus, um die Disjunktion zu etablieren, indem eine Alternative hinzugefügt wird; Disjunktionseinführung erhält die Wahrheit durch Abschwächung.

Demonstration

Aus einer Herleitung von A wende die Disjunktionseinführung an, um A ∨ B zu erhalten. Beispiel: aus ‚Es regnet‘ folgere ‚Es regnet ∨ Es schneit‘.

Fehlanwendung

Die Regel verwenden, um aus einer Disjunktion einen bestimmten Disjunkt zu wählen (A aus A ∨ B ableiten), oder irrelevante/täuschende Disjunkte einzuführen, die konstruktive Information für spätere Beweisschritte verschleiern.

Konsequenz

Ermöglicht das Erweitern von Möglichkeiten, das Erzeugen von Fallunterscheidungen und das Vorbereiten einer Beweisführung durch Fälle; in Programmiersprachen entspricht es dem Injizieren eines Werts in einen Summentyp (links- oder rechts-Injektion).

Umkehrung

Gegensatz zur Disjunktionselimination: Einführung schafft aus einer bestimmten Tatsache eine mehrdeutige Alternative, während Elimination verlangt, die Disjunktion durch separate Fallanalysen aufzulösen, um eine gemeinsame Konsequenz abzuleiten.

Abgrenzung

Gilt in klassischer und intuitionistischer Logik als grundlegende Strukturregel; in konstruktiven/typentheoretischen Umgebungen muss die passende Injektion (links oder rechts) als konstruktiver Beleg geliefert werden, und in manchen Kontexten kann willkürliches Hinzufügen von Disjunkten rechnerischen Gehalt vernichten.

Semantische Spannung

Es besteht Spannung zwischen der abschwächenden Natur der Disjunktionseinführung (sie macht die Aussage weniger informativ) und dem Bedarf in konstruktiven Kontexten, Belege zu erhalten; sie ist zwar zulässig, kann aber für spätere konstruktive Schritte wenig nützlich sein.

Synthese

Die Disjunktionseinführung ist der Mechanismus, der eine bestimmte Tatsache in eine breitere, wahrheits-erhaltende Alternativenaussage verwandelt, indem ein zusätzliches mögliches Disjunkt ergänzt wird; sie bereitet leichtgewichtig auf fallbasierte Beweise vor.