□(□p → p) → □p. Incompleteness becomes a one-line modal fact: the system cannot prove its own consistency, ¬□⊥. And the strange self-referential sentences at the heart of Gödel's proof become two clean fixed points with opposite fates. Boolos made the deepest theorem in logic legible.Rigorous and clarifying. Provability logic (the system GL) is a precise, complete modal account of provability in arithmetic; Boolos's "The Logic of Provability" is the standard text. It re-derives Gödel and Löb in a few clean modal lines.
Recasting, brilliantly. The core results are Gödel's and Löb's; Boolos's gift was the modal framework that makes them transparent and connects them to [[saul-kripke]]'s semantics. Synthesis of the first order, not a fresh incompleteness.
The popular Boolos. He wrote Gödel's second theorem "in words of one syllable," and devised "The Hardest Logic Puzzle Ever" (three gods: True, False, Random). Beloved feats of exposition — refinements of Smullyan, not his deepest math.
Provability logic lives or dies on self-reference. By Gödel's fixed-point trick, a system can build a sentence that asserts something about its own provability. There are two natural ones — and they could not end more differently. Click each to follow its logic to the end. The box □ means "this is provable in the system."
¬□⊥ ("falsehood is not provable") is exactly a sentence the system cannot prove about itself — Gödel's second theorem, now a one-line modal fact. Boolos's framework turns a forest of arithmetic into a handful of modal axioms with [[saul-kripke]]-style worlds (here: provability-worlds, a transitive well-founded frame)."… we cannot prove that we cannot prove a contradiction — unless we can." — the shape of Gödel's second theorem, à la Boolos
Modal logic with □ = "provable," the transitivity axiom, and Löb's axiom □(□p→p)→□p. It is sound and complete for provability in Peano Arithmetic — every modal theorem corresponds to a real fact about proofs, and vice versa.
Three gods — True, False, and Random — answer yes/no in a word whose meaning ("da"/"ja") you don't know. Identify them in three questions. Boolos's celebrated hardening of a Smullyan puzzle, solved by self-referential questions.
Boolos's achievement is to make the summit transparent. Gödel's and Löb's theorems are notoriously slippery; recast as the modal system GL — provability as a box operator over a [[saul-kripke]] frame of "worlds you can prove your way to" — they become almost mechanical, and the connection between incompleteness (Gödel), self-reference (Löb), and possible-worlds semantics (Kripke) becomes one picture. The same man who wrote the standard graduate logic textbook and the definitive monograph on provability logic also delighted in proving the second incompleteness theorem in words of one syllable and inventing puzzles that are genuinely the hardest known — because he believed, rightly, that if you truly understand a deep thing you can make it clear. ⚑ He took the hardest theorem in this lineage and handed it back as a small, clean modal logic. [[ludwig-wittgenstein]] ← · the lineage rests here.
Gate kept on. The work is rigorous and important: provability logic — the modal system GL, with □ read as "provable in arithmetic," made sound and complete by the Solovay theorems — is a real and beautiful corner of mathematical logic, and Boolos's The Logic of Provability (1993) is its standard treatment; it re-derives [[kurt-godel]]'s incompleteness and Löb's theorem as clean modal facts and ties them to [[saul-kripke]]'s semantics. The honest framing is that this is a profound reorganisation, not a new incompleteness theorem — the deep results are Gödel's and Löb's (and the completeness is Solovay's); Boolos's genius was the unifying modal view and an unmatched gift for making it understandable. His popular feats — the "Hardest Logic Puzzle Ever" (a refinement of [[raymond-smullyan]]'s gods puzzles) and proving Gödel's second theorem in words of one syllable — are dazzling exposition rather than his deepest mathematics, and he'd have said so. The man: George Boolos was, by wide agreement, one of the great teachers of logic, co-author of the standard text Computability and Logic, a national crossword champion and Joyce scholar, who died of pancreatic cancer at 55, far too soon. He spent his life on the conviction that the hardest truths can be made clear — and proved it on the hardest one there is. ⚑ With Boolos the lineage rests: from [[thales-of-miletus]]' first proof to the modal logic of proof itself. [[ludwig-wittgenstein]] ←."