Kompliziertheit mathematischer Beweise entsprechend eines Komplexitätsmaßes.

Die Präzisierung dieses Begriffs erfolgt in der Regel mit Hilfe formalisierter Sprachen L (siehe elementare Sprache). Den Wörtern (Zeichenreihen, L-Formeln, …) werden in eindeutiger Weise durch eine rekursive Funktion natürliche Zahlen, sogenannte Gödelzahlen, zugeordnet, so daß man aus diesen Zahlen die entsprechenden Wörter rekonstruieren (decodieren) kann. Der Vorgang selbst heißt Gödelnumerierung oder Gödelisierung der Sprache, und die zugrundegelegte rekursive Funktion kann als allgemeines Kompliziertheitsmaß für die Gödelisierung aufgefaßt werden. Wird dieser Vorgang von einem Automaten (TuringMaschine, Computer, …) ausgeführt, dann sind im allgemeinen zwei Berechnungsgrößen von Bedeutung: Die Zeitkomplexität (hier ist die Anzahl der benötigten Rechenschritte ausschlaggebend) und die Raumkomplexität (hier ist der für die Berechnung benötigte Speicherplatz entscheidend). Wird die Gödelnumerierung auf die zugrundegelegten formalen Beweisregeln (siehe formaler Beweis) erweitert, dann läßt sich eine Komplexität für formale Beweise definieren.

In den praktischen Anwendungen werden Komplexitätsbetrachtungen häufig mit Entscheidbarkeitsuntersuchungen elementarer Theorien T (Mengen von Aussagen der verwendeten Sprache L) verknüpft. Für die Entscheidbarkeit von T ist ein Algorithmus (Rechenverfahren) zu finden, mit dessen Hilfe die Gültigkeit oder Ungültigkeit jeder Aussage φ ∈ T überprüft werden kann. Hängt die Anzahl der benötigten Rechenschritte polynomial von der Länge der zu entscheidenden Aussagen φ ab, dann wird das Entscheidungsverfahren als günstig (weniger komplex) angesehen, ist jedoch die Abhängigkeit exponentiell, dann ist die Komplexität des Verfahrens ungünstig, es ist für längere Aussagen praktisch nicht mehr handhabbar.