Beweisbarkeit

Beweisbarkeit bezeichnet in der Logik und Mathematik die Eigenschaft einer Aussage, aus den Axiomen eines formalen Systems durch eine endliche Folge von Anwendung von Beweisschritten herzuleiten zu sein. Sie ist eine relationale Eigenschaft, die von der Wahl der Theorie abhängt. Eine Aussage φ ist Beweisbar in einer Theorie T, wenn es eine formale Derivation gibt, die aus den Axiomen von T und den gültigen Inferenzregeln φ ableitet. In der Regel verwendet man die Notation ⊢T φ.

In formalen Theorien wird Beweisbarkeit durch Beweissysteme konkretisiert, etwa in Hilbert-Systemen oder im natürlichen Beweisverfahren. Die Beweisbarkeit ist eine zentrale Größe der Beweistheorie und der Metamathematik. Sie ermöglicht es, formale Gültigkeit unabhängig von der Interpretation der Objekte innerhalb einer bestimmten Struktur zu prüfen.

Gödels Unvollständigkeitssatz zeigt, dass Beweisbarkeit nicht mit Wahrheit gleichzusetzen ist. In jeder konsistenten, ausreichend mächtigen Theorie, die arithmetische Aussagen abbildet, gibt es Sätze, die wahr sind, aber innerhalb der Theorie nicht Beweisbar sind. Damit ist Beweisbarkeit eine relative Eigenschaft, die von der zugrunde liegenden Theorie abhängt, und sie kann in einer erweiterten Theorie anders sein.

Beweisbarkeit unterscheidet sich von Begriffen wie Verifizierbarkeit oder Falsifizierbarkeit. Beweisbarkeit bezieht sich auf formale Ableitbarkeit innerhalb eines Systems; Falsifizierbarkeit (Popper) und Verifizierbarkeit im wissenschaftlichen Sinn beziehen sich stärker auf empirische Prüfung und Beobachtbarkeit. In der Informatik und der formalen Verifikation ist Beweisbarkeit von Bedeutung für die automatische Beweisführung, Test und Verifikation von Software- und Hardware-Systemen.