Mathematical logic

Before Frege, logic was Aristotle's syllogisms — subjects and predicates, "all men are mortal, Socrates is a man." Frege's *Begriffsschrift* ("concept-script," 1879) swept that aside for a function-and-argument analysis and, decisively, for *quantifiers* binding *variables*: "for every x, if x is a man then x is mortal." This let logic express relations and layered generality that syllogisms simply could not reach — "every person has a mother," "for every number there is a larger prime." Frege laid down explicit axioms and explicit rules of inference, so that a proof became a purely formal chain, checkable by its shape alone, with no appeal to meaning. That is first-order predicate logic, still the standard notation of mathematics.

Making proof a formal object is what lets you ask mathematical questions *about* mathematics: Is this system consistent? Is it complete? Is there a procedure to decide its truths? Frege's own aim was logicism — to show that arithmetic is nothing but logic in disguise. That dream was wounded by Russell's paradox (consider the set of all sets that do not contain themselves — does it contain itself?), which struck at Frege's rule for forming sets from properties. It was bounded for good by Gödel's incompleteness theorems (1931), which used precisely this formal machinery to prove that any consistent system strong enough for arithmetic must contain true statements it cannot prove. Logic had become powerful enough to map its own limits.

Mathematical logic is the direct parent of the theory of computation: Turing and Church were answering the Entscheidungsproblem, a question posed in this language. It underlies every programming language and type system, automated theorem proving and formal verification, and the relational query languages of databases, which are predicate logic in commercial dress. And it gave the modern world its sober understanding of both the enormous reach and the hard, permanent limits of formal reasoning.