mathematische Theorie, die in den 20er Jahren von D. Hilbert und seinen Schülern mit dem Ziel entwickelt wurde, die Bedenken einiger Mathematiker gegen gewisse Schlüsse der klassischen Mathematik, wonach z. B. eine Existenzaussage schon dann als bewiesen gilt, wenn ihre Negation zu einem Widerspruch führt, zu entkräften. Die Bedenken kamen insbesondere aus der intuitionistischen Mathematik, wo ein mathematisches Objekt nur dann als existent angesehen wird, wenn es mit finiten Mitteln wirklich „konstruiert“ werden kann.

Zur Umsetzung seines Programms gab Hilbert der klassischen Mathematik eine neue Deutung, indem er die jeweils betrachtete mathematische Theorie formalisierte und sie axiomatisch zu begründen versuchte. Beweiszusammenhänge erschienen nun als rein strukturelle Umformungen von Zeichenreihen. Ein mathematischer Beweis wurde damit zu einer endlichen Folge von Ausdrücken der zugrundegelegten elementaren Sprache, deren Folgeglieder formalen Regeln genügen, wobei diese Schlußregeln die inhaltlichen Schlußweisen der klassischen Mathematik widerzuspiegelten hatten. Zur praktischen Umsetzung des Programms sind mehrere grundlegende Voraussetzungen zu schaffen:

1. Die Grundbegriffe des zu axiomatisierenden mathematischen Gebietes sind anzugeben, auf die jeder weitere benutzte Begriff durch eine explizite Definition zurückzuführen ist. Durch diese Grundbegriffe ist eine elementare Sprache L festgelegt.
2. Die zulässigen Beweisregeln sind so zu wählen, daß sie mit finiten Mitteln auskommen. Diese Regeln stützen sich ausschließlich auf anschaulich evidente elementare logische und mathematische Beziehungen kombinatorischer Natur zwischen den Ausdrücken und Aussagen aus L. Insbesondere sind indirekte Beweise (Beweismethoden) unzulässig, und eine Existenzaussage gilt nur dann als bewiesen, wenn sich ein Objekt, dessen Existenz behauptet wird, effektiv angeben läßt.
3. Es ist eine „überschaubare“ (rekursive) Menge Σ von „gültigen“ Aussagen aus dem betrachteten Gebiet anzugeben, die als Axiomensystem dient. Von einem solchen Axiomensystem wird die Widerspruchsfreiheit gefordert, d. h., mit Hilfe der zulässigen Beweisregeln darf ein Ausdruck der Gestalt ϕ ∧ ¬ϕ nicht herleitbar sein.

Schließlich sollte das Axiomensystem Σ nach Möglichkeit vollständig sein, d.h., für jede L-Aussage (L-Formel) ϕ ist entweder ϕ oder ¬ϕ aus Σ (formal) beweisbar.

Um die Widersprüchlichkeit eines Axiomensystems Σ nachzuweisen, genügt es, einen Ausdruck ϕ und einen Beweis (ϕ₁,…,ϕ_n) aus Σ anzugeben, so daß ϕ_n = ϕ ∧ ¬ϕ. Dies läßt sich prinzipiell mit finiten Mitteln erreichen. Ein völlig anderes Problem ist der Nachweis der Widerspruchsfreiheit von Σ, da man sich hierbei eventuell auf weitere Voraussetzungen stützen muß, deren Widerspruchsfreiheit ebenfalls zu sichern ist.

Das Hilbertsche Programm erwies sich als nicht mehr realisierbar, als Gödel 1931 seinen Unvoll-ständigkeitssatz veröffentlichte, der im wesentlichen besagt, daß die Widerspruchsfreiheit nicht mit den logischen Hilfsmitteln bewiesen werden kann, die in dem betrachteten Kalkül formalisierbar sind. Insbesondere zeigte Gödel, daß es nicht möglich ist, die Widerspruchsfreiheit der elementaren Arithmetik in dem oben beschriebenen Sinne nachzuweisen, und daß es kein vollständiges (rekursives) Axiomensystem gibt, aus dem alle wahren Sätze der Arithmetik herleitbar sind. Dadurch waren gewisse Grenzen, aber nicht das Ende der Beweistheorie markiert, die sich nun als eigenständige mathematische Disziplin entwickelte.

Die moderne Beweistheorie untersucht die formalisierte Mathematik. Sie befaßt sich vor allem mit Problemen der folgenden Art: Mit welchen Mitteln ist die Widerspruchsfreiheit welcher formalisierter Theorien zu beweisen?