In 1879, an obscure German mathematician named Gottlob Frege published a thin book with an awkward title — Begriffsschrift, "concept-script" — and proposed something that looked, on first reading, like a mistake. Frege wanted logic itself to have a notation as precise as algebra. His diagrams were typographically baffling and the book sold almost no copies. But inside it was a single move that would re-found mathematics: the quantifier. The two little words for all and there exists, treated as formal operators with their own syntax and rules, turned out to be exactly what the previous two thousand years of logic — Aristotle's syllogisms, the medieval scholastics, Boole's algebra — had been missing.
Modern first-order logic combines four ingredients: constants (specific objects), variables (placeholders), predicates (properties or relations), and the quantifiers ∀ ("for all") and ∃ ("there exists"). With these you can write things classical logic could not: every prime greater than 2 is odd, there exists an integer between any two reals, for every ε there exists a δ. The quantifiers bind variables the way a calculus integral binds its dummy variable, and the discipline of which variables are bound by which quantifiers turns out to control what statements actually mean. Frege's framework was generalized by Russell and Whitehead (the Principia Mathematica, 1910–13), formalized by Hilbert, given a precise semantics by Tarski in the 1930s, and crowned by Gödel's completeness theorem (1929) — the result that says first-order logic's proof rules can derive every logical consequence of any set of axioms. (Not to be confused with his incompleteness theorems, which are about specific theories like arithmetic, not about logic itself.) The hierarchy goes higher: propositional logic (no quantifiers), first-order (quantifiers over individuals), higher-order (quantifiers over predicates and sets). First-order is the workhorse: expressive enough for almost all of working mathematics, well-behaved enough to have a complete proof system, and the natural language of axiomatic theories from Peano arithmetic to ZFC set theory.
Logic is now the operating system of formal verification: proof assistants like Coq, Lean, Isabelle, and Agda let mathematicians and software engineers check large proofs by machine. The four-color theorem, Kepler's conjecture, and parts of the Liquid Tensor Experiment have been verified this way. Programming-language semantics, type theory, database query languages (SQL is, formally, first-order logic with quantifiers), and AI knowledge representation all run on quantified reasoning. The cultural shift Frege initiated — that argument can be checked the way arithmetic is checked — is one of the great unfinished projects of intellectual life.