ein konsistentes logisches System, für das der Gödelsche Vollständigkeitssatz gilt.

Zu einem logischen System gehört eine Menge Ax von logischen Axiomen, eine Menge von formalen Beweisregeln, die nur die Form, nicht aber den Inhalt der Axiome bzw. der zu beweisenden Aussagen berücksichtigen, und eine Folgerungsrelation ⊨ (logisches Folgern), die aus wahren Voraussetzungen nur wahre Behauptungen produziert. Das formale Beweisen wird durch ⊢ gekennzeichnet.

Ein logisches System heißt vollständig, wenn es konsistent ist (aus inkonsistenten Mengen sind alle Aussagen, insbesondere auch die falschen, beweisbar), und wenn für eine beliebige Menge T von Voraussetzungen und jede Aussage φ gilt:

\begin{eqnarray}T \vdash \varphi \iff T\models \varphi \end{eqnarray}

Das formale Beweisen, das nur eine Manipulation von Zeichenreihen zur Folge hat, spiegelt also das inhaltliche Folgern wider. Die Beweisregeln sind so gewählt, daß sie die Gültigkeit vererben, d. h., aus wahren Voraussetzungen sind nur wahre Behauptungen beweisbar, und die Beweisregeln sind in dem Sinne vollständig, daß alle Aussagen, die aus T inhaltlich folgen, auch aus T durch Anwendung der Regeln hergeleitet werden können. In der Prädikatenlogik haben sich die beiden Beweisregeln modus ponens und Generalisierung als ausreichend erwiesen.

Ein formaler Beweis für einen Ausdruck φ aus einer Menge T von Voraussetzungen ist eine endliche Folge (φ₁, …, φ_n) von Ausdrücken, so daß φ_n = φ gilt, und für jedes φ_i, i = 1, …, n, eine der folgenden vier Bedingungen erfüllt ist:

1. φ_i ∈ Ax (φ_i ist ein logisches Axiom).
2. φ_i ∈ T (φ_i gehört zu den Voraussetzungen).
3. Es gibt Indizes j, k< i, so daß \({\varphi}_{k}={\varphi}_{j}\to {\varphi}_{i}\)(Anwendung des modus ponens).
4. Es gibt einen Index j< i, so daß \({\varphi _i} = \forall x{\varphi _j}\) (Anwendung der Generalisierung).