Zur Bedeutung der Formalisierung

 In der Prädikatenlogik erster Stufe lassen sich alle mathematischen Sachverhalte in der größtmöglichen Exaktheit formulieren. Während man in der Mathematik Elemente der Prädikatenlogik oft nur als bequeme Abkürzungen ansieht (etwa: „∀“ steht kurz für „für alle“, „∧“ steht kurz für „und“), sind aus der Sicht der mathematischen Logik alle üblichen mathematischen Texte letztendlich informale (!) Versionen prädikatenlogischer Formeln. Sie erscheinen als umgangssprachliche Übersetzungen, die die Genauigkeit hinreichend wahren. Die mathematische Umgangssprache wird in jedem Fall hoch geschätzt, da erst sie in der Lage ist, komplexe Sachverhalte in einer menschlich lesbaren Form kompakt auszudrücken. Es ist aber von prinzipieller Bedeutung, dass sich die Prädikatenlogik erster Stufe zur peniblen Formalisierung der Mathematik eignet, auch wenn diese Formalisierung in den seltensten Fällen tatsächlich durchgeführt wird. Wir diskutieren zwei Gesichtspunkte:

 Zunächst wird eine größere Genauigkeit erreicht. Zum Beispiel kann der in der Mathematik an verschiedenen Stellen (etwa bei der Induktion oder in den Axiomen der Mengenlehre) naiv verwendete Eigenschaftsbegriff präzisiert werden: Eine Eigenschaft ℰ(x) ist einfach eine Formel φ(x) der Prädikatenlogik (einer bestimmten Signatur). Weiter können Axiome exakt formuliert werden: In welcher Signatur werden sie formuliert? Wie lauten sie genau?

 Zum anderen erlaubt die Formalisierung zu definieren, was ein mathematischer Beweis ist: Eine Folge von Formeln, die nach bestimmten syntaktischen Regeln gebildet ist, den Schlussregeln eines logischen Kalküls. Dadurch werden nicht nur die Spielregeln des mathematischen Beweisens offengelegt und zur Diskussion gestellt, sondern es wird auch möglich, mathematische Beweise mathematisch zu untersuchen. Erst so können grundlegende Ergebnisse wie die Nichtbeweisbarkeit bestimmter Aussagen in bestimmten Axiomensystemen erzielt werden. Zu diesen gehören allen anderen voran die Unvollständigkeitssätze von Kurt Gödel und die Resultate über die Grenzen der mengentheoretischen Axiomatik. Wir verweisen den interessierten Leser hierzu auf die Literatur zur mathematischen Logik und Mengenlehre.