Anordnung der für mathematische Beweise notwendigen bzw. hilfreichen Teilschritte zu sog. Beweisketten.

Ein formaler Beweis für eine (formalisiert) dargestellte Aussage ϕ aus einer Menge) von (formalisierten) Voraussetzungen ist eine endliche Folge (ϕ₁, …, ϕ_n) so, daß jedes Folgeglied einen Beweisschritt in dem folgenden Sinne darstellt:

Für jedes ϕ_i mit 1 ≤ i ≤ n gilt:

• ϕ_i ist ein logisches Axiom (logische Axiome dürfen uneingeschränkt beim Beweisen benutzt werden),
• ϕ_i ∈ Σ (ϕ_i gehört zu den Voraussetzungen, aus denen ϕ zu beweisen ist),
• ϕ_i entsteht aus gewissen vorhergehenden Folgegliedern durch Anwendung einer der zuvor fixierten (formalen) Beweisregeln,
• ϕ_n = ϕ (den Abschluß des Beweises bildet die zu beweisende Aussage ϕ).

Die Beweisregeln können in unterschiedlichen Kalkülen zweckentsprechend verschiedenartig gestaltet sein, jedoch im allgemeinen immer so, daß aus wahren Voraussetzungen auch stets wahre Behauptungen herleitbar sind. In der klassischen Mathematik kommt man bei geeigneter Wahl der logischen Axiome stets mit den folgenden beiden Regeln aus: Abtrennungsregel und Generalisierung. Mit Hilfe der fixierten grundlegenden Beweisregeln lassen sich weitere abgeleitete Beweisregeln gewinnen; praktisch bedeutet dies, daß zuvor bewiesene Aussagen als Folgeglieder (Beweisschritte) in anderen Beweisen auftreten dürfen.

Da der Prädikatenkalkül nicht entscheidbar ist (d. h., es gibt keinen Algorithmus, der die Gültigkeit oder Ungültigkeit einer gegebenen Aussage überprüft), gibt es auch kein Verfahren, welches einen Beweis bzw. eine Widerlegung einer vorgelegten Aussage erzeugt. Demzufolge kann die Struktur von Beweisen für die gleiche Aussage aus gegebenen Voraussetzungen sehr unterschiedlich ausfallen. Siehe auch Beweismethoden.