Beweisregeln

Beweisregeln sind formale Transformationen, die es erlauben, aus gegebenen Prämissen eine neue Aussage abzuleiten. Sie bilden zusammen mit Axiomen das Beweissystem einer mathematischen Theorie. Ziel ist es, die Gültigkeit einer Behauptung durch eine nachvollziehbare Folge logischer Schritte zu begründen.

Zu den bekanntesten Beweisregeln der Aussagenlogik gehören der Modus ponens (aus p und p→q folgt q) und der Modus tollens (aus ¬q und p→q folgt ¬p). Weitere grundlegende Regeln betreffen Einführungen und Eliminierungen von Konjunktionen sowie von Disjunktionen: Aus p und q folgt p∧q; aus p∧q folgt p bzw. q; aus p∨q lässt sich unter bestimmten Bedingungen q oder p ableiten. In der Prädikatenlogik kommen zusätzlich Regeln wie Allgemeine Einführung (von φ(x) zu ∀xφ(x), unter Nebenbedingungen) und Instanziierung (von ∀xφ(x) zu φ(t)) hinzu.

Beweisregeln finden sich in unterschiedlichen formalen Systemen, etwa im Natürlichen Deduktionssystem (Natural Deduction) mit Einführungs- und Eliminationsregeln für die logischen Verknüpfungen, oder in Hilbert-Systemen, die mit wenigen Axiomen arbeiten und Modus ponens als einzige Regel verwenden. Sequentenkalküle bieten eine weitere formale Darstellung von Beweisen.

Bedeutung und Grenzen: Beweisregeln gewährleisten, dass aus wahrheitsgetreuen Prämissen nur wahrheitskonforme Folgerungen entstehen. Sie ermöglichen eine strukturierte Beweisführung, die Nachprüfbarkeit und Formalisierung erleichtert. Induktion ist eine verbreitete Beweismethode, die oft als Beweisstrategie verwendet wird. Historisch prägten Beweisregeln Arbeiten von Frege, Hilbert und Gentzen; heute sind sie zentral in Mathematik, Logik und Informatik, auch in der automatisierten Beweisführung.