Eliminationsregeln

Eliminationsregeln bezeichnet in der Logik die Inferenzregeln, mit denen aus einer zusammengesetzten Formel eine der beteiligten Komponenten oder eine einfachere Ableitung gewonnen wird. Sie dienen dem Entfernen eines logischen Konstrukts aus einer Formel, während die verbleibenden Informationen erhalten bleiben. In der natürlichen Deduktion bilden Eliminationsregeln das Gegenstück zu den Einführungsregeln und ermöglichen es, aus komplexen Aussagen konkrete Folgerungen abzuleiten.

Zu den häufigsten Eliminationsregeln gehören: ∧-Elimination, aus A ∧ B folgt A (und B); ∨-Elimination, aus A ∨ B folgt C, wenn aus A folgt C und aus B folgt C (Fallunterscheidung); →-Elimination, auch Modus ponens genannt: aus A → B und A folgt B; ∀-Elimination, aus ∀x φ(x) folgt φ(t) für jedes Term t; ∃-Elimination, aus ∃x φ(x) folgt ψ, sofern aus φ(c) die Folgerung ψ folgt, wobei c eine neu eingeführte Konstante ist.

Eliminationsregeln spielen eine zentrale Rolle in natürlichen Deduktionssystemen (zum Beispiel Gentzen-Natural Deduction) und stehen im engen Zusammenhang mit der semantischen Bedeutung der logischen Operatoren. Sie ermöglichen Beweise in normaler Form und strukturieren Ableitungen so, dass die nachfolgenden Schritte klar nachvollziehbar bleiben. In der Praxis werden Eliminationsregeln oft zusammen mit Einführungsregeln verwendet, um eine systematische Begründungsführung sicherzustellen.

In anderen logischen Kontexten, wie der Typentheorie oder programmbasierter Beweisführung, finden Eliminationsregeln ähnliche Formen, etwa beim Musterabgleich oder beim Ausführen von Fallunterscheidungen. Sie sind damit grundlegende Bausteine formaler Beweissysteme und erleichtern die Ableitung von Konsequenzen aus komplexeren Aussagen.