Im Jahr 1879 brachte ein bis dahin kaum bekannter deutscher Mathematiker namens Gottlob Frege ein dünnes Buch mit sperrigem Titel heraus — Begriffsschrift — und schlug etwas vor, was beim ersten Lesen wie ein Versehen aussah. Frege wollte, dass die Logik selbst eine Schreibweise erhält, so präzise wie die Algebra. Seine Diagramme waren typographisch verstörend, das Buch fand kaum Käufer. Doch in ihm steckte ein einziger Schritt, der die Mathematik neu begründen sollte: der Quantor. Die zwei kleinen Wörter für alle und es existiert, als formale Operatoren mit eigener Syntax und eigenen Regeln verstanden, erwiesen sich als genau das, was den zweitausend Jahren Logik davor — Aristoteles' Syllogismen, den mittelalterlichen Scholastikern, Booles Algebra — gefehlt hatte.
Die moderne Prädikatenlogik erster Stufe setzt sich aus vier Zutaten zusammen: Konstanten (bestimmte Objekte), Variablen (Platzhalter), Prädikate (Eigenschaften oder Relationen) und die Quantoren ∀ („für alle“) und ∃ („es existiert“). Mit ihnen lassen sich Aussagen formulieren, die der klassischen Logik verschlossen blieben: jede Primzahl größer als 2 ist ungerade, zwischen je zwei reellen Zahlen liegt eine ganze Zahl, für jedes ε existiert ein δ. Die Quantoren binden Variablen, wie das Integral der Analysis seine Hilfsvariable bindet, und die Disziplin, welche Variablen von welchen Quantoren gebunden werden, entscheidet, was eine Aussage eigentlich besagt.
Freges Rahmen wurde von Russell und Whitehead (die Principia Mathematica, 1910–13) verallgemeinert, von Hilbert formalisiert, von Tarski in den 1930er Jahren mit einer präzisen Semantik unterlegt und schließlich vom Gödelschen Vollständigkeitssatz (1929) gekrönt — dem Ergebnis, dass die Beweisregeln der Prädikatenlogik erster Stufe jede logische Folgerung aus jeder Axiomenmenge ableiten. (Nicht zu verwechseln mit Gödels Unvollständigkeits-Sätzen, die spezifische Theorien wie die Arithmetik betreffen, nicht die Logik selbst.) Die Hierarchie geht weiter: Aussagenlogik (keine Quantoren), erste Stufe (Quantoren über Individuen), höhere Stufe (Quantoren über Prädikate und Mengen). Die erste Stufe ist das Zugpferd: ausdrucksstark genug für nahezu die ganze praktizierte Mathematik, gutartig genug für ein vollständiges Beweissystem, und die natürliche Sprache axiomatischer Theorien von der Peano-Arithmetik bis zur ZFC-Mengenlehre.
Die Logik ist heute das Betriebssystem der formalen Verifikation: Beweisassistenten wie Coq, Lean, Isabelle und Agda erlauben es Mathematikern und Software-Ingenieuren, große Beweise maschinell prüfen zu lassen. Der Vier-Farben-Satz, Keplers Vermutung und Teile des Liquid Tensor Experiment sind auf diesem Weg verifiziert worden. Programmiersprachen-Semantik, Typentheorie, Datenbankabfragesprachen (SQL ist formal Prädikatenlogik erster Stufe mit Quantoren) und KI-Wissensrepräsentation ruhen sämtlich auf quantifiziertem Schließen. Der kulturelle Umbruch, den Frege anstieß — dass Argumente sich prüfen lassen, wie Arithmetik geprüft wird —, zählt zu den großen unvollendeten Projekten des geistigen Lebens.