Eine Schlussregel, die es erlaubt, jeden Konjunkt aus einer Konjunktion A ∧ B abzuleiten; formal: aus A ∧ B folgere A (und symmetrisch B).

Prinzip

Eine Konjunktion behauptet beide ihrer Konjunkte; daher ist jeder Konjunkt einzeln aus der Konjunktion als Prämisse ableitbar.

Demonstration

Aus einer Herleitung von A ∧ B wende die Konjunktionselimination an, um A zu erhalten. Beispiel: Aus ‚Es regnet ∧ der Boden ist nass‘ folgere ‚Es regnet‘.

Fehlanwendung

Anwenden der Elimination auf eine Formel, die keine echte Konjunktion ist (z. B. eine materielle Implikation oder Disjunktion), oder zu erwarten, dass Elimination Konjunkte erzeugt, die nicht vorhanden waren (z. B. B aus A allein folgern).

Konsequenz

Ermöglicht das Extrahieren und lokale Verwenden spezifischer Fakten innerhalb einer zusammengesetzten Aussage und unterstützt modulares Denken und fokussierte Teilbeweise.

Umkehrung

Die Umkehrung ist die Konjunktions-Einführung (Komposition): während die Elimination ein Zusammengesetztes in Teile zerlegt, setzt die Einführung Teile zu einem Ganzen zusammen; ihre Verwechslung führt zu unbegründeten Schlüssen.

Abgrenzung

Gilt in klassischer, intuitionistischer und den meisten Standard-Systemen; kann eingeschränkt sein in Logiken, in denen Konjunktion anders verstanden wird (z. B. in linearer Logik mit Ressourcen-Tracking) oder wenn Konjunktion extensionell statt beweistheoretisch definiert ist.

Semantische Spannung

Spannung entsteht durch Distribution oder durch zusammengesetzte Operatoren, deren Oberflächensyntax wie eine Konjunktion aussieht, aber zusätzliche Struktur besitzt; die Gültigkeit der Elimination hängt von der Semantik des Operators ab.

Synthese

Die Konjunktionselimination ist die Regel, die Beweisen den Zugriff auf die einzelnen durch eine Konjunktion garantierten Komponenten erlaubt und eine gemeinsame Aussage in nutzbare einzelne Prämissen für weiteres Schließen verwandelt.