From the syllogism to incompleteness: twenty-three centuries of trying to mechanize reasoning, and the discovery that reason itself has limits.
Aristotle isolated form from content. A valid argument is valid because of its shape, not its subject matter. He catalogued the moods of the categorical syllogism — three terms, three propositions, fixed structure.
While Aristotle reasoned about classes of things, the Stoics reasoned about propositions. They built logic from whole sentences linked by connectives — and so anticipated the propositional calculus by two millennia.
Chrysippus is said to have written more than 700 logical treatises. Almost all are lost; only fragments survive in Diogenes Laertius and Sextus Empiricus.
The medievals took Aristotle and refined him with surgical care. Their central problem: how does a term refer in a proposition? Ockham's theory of supposition distinguished the modes by which a word stands for a thing.
Ockham insisted that universals are signs in the mind, not entities in the world — entia non sunt multiplicanda praeter necessitatem. The razor cuts in logic too.
Gottlob Frege's 88-page pamphlet of 1879 is the most important event in logic since Aristotle. He invented quantifiers — the ∀ and ∃ that bind variables — and with them, predicate logic.
For the first time, statements like "every prime greater than two is odd" could be written in a calculus where validity was a matter of mechanical form.
Frege's two-dimensional notation was unreadable; Peano and Russell rewrote it in the linear form we still use.
If logic is the form of all valid inference, perhaps mathematics is just logic in elaborate dress. Bertrand Russell and Alfred North Whitehead set out to derive arithmetic, analysis, and set theory from a handful of logical axioms.
The proof of 1 + 1 = 2 arrives on page 379 of Volume I. The project nearly broke them. And then it broke.
In 1901 Russell sent Frege a letter that destroyed Frege's life work just as Volume II of his Grundgesetze was at the printer.
Consider R, the set of all sets that are not members of themselves. Is R a member of itself?
David Hilbert proposed a rescue. We will rebuild mathematics on an unshakable formal base. Three demands:
If completed, mathematics would be a finite, mechanical game with no remaining mysteries. The famous Entscheidungsproblem: find the algorithm.
Kurt Gödel, age 25, demolished the program. By coding statements as numbers, he constructed a sentence G that says, in effect:
"This sentence has no proof in the system."
If G is provable, the system is inconsistent. If G is unprovable, the system is incomplete — and G is true.
Five years after Gödel, Alan Turing settled the third of Hilbert's demands. He invented an idealized machine — tape, head, finite states — and asked: is there a program that decides whether any given program will eventually halt?
From this it follows that first-order logic has no general decision procedure. The Entscheidungsproblem has a negative answer. And, incidentally, the modern computer was born.
Classical logic knows only that propositions are true or false. But ordinary speech distinguishes could be, must be, might have been. Modal logic adds two operators:
Kripke's masterstroke: a sentence is necessary iff true in every accessible world; possible iff true in some.
Russell's stratified hierarchy of types — rebuilt by Per Martin-Löf — gives a foundation in which terms inhabit types. Modern proof assistants (Coq, Lean, Agda) compute in it.
L. E. J. Brouwer rejected the law of the excluded middle: a proposition is true only when constructively provable. P ∨ ¬P is no longer free.
Propositions are types. Proofs are programs. To prove A → B is to write a function from A to B. Logic and computation are one structure seen twice.