◄ UD0   ← Curry   LOGIKĒ · the modern foundations
LOGIKĒ · the modern foundations · undecidability

Emil Post

1897 – 1954 · Augustów, Poland & New York · City College & Columbia · production systems & the correspondence problem
Emil Post is the great almost-first of this lineage. Working alone in New York in the 1920s, he reached the core of [[kurt-godel]]'s incompleteness and [[alan-turing]]'s undecidability — before either — but, plagued by illness and a cautious editor, he didn't publish in time, and the credit went elsewhere. What is unquestionably his: production systems — the idea that all of computation is just rewriting strings by rules, a model as powerful as the Turing machine; and a single, devilish puzzle that became the workhorse for proving things impossible. The Post Correspondence Problem: you're given a set of dominoes, each with a string on top and a string on the bottom; can you lay some of them in a row so the top reads the same as the bottom? It sounds like a game. It is undecidable — no algorithm can solve it in general.
✓ STRONG

Foundational and exact. Post's production/rewriting systems are a complete model of computation; the Post Correspondence Problem is provably undecidable and is the standard tool for proving other problems undecidable across computer science.

◐ THE PRIORITY HE LOST

First, but not in print. Post anticipated Gödel's incompleteness (c. 1921) and the Turing-machine idea, but did not publish in time. His "anticipation" is real and acknowledged now — the formal credit, fairly, went to those who published.

◔ A LIFE OF OBSTACLES

Worked against the odds. Post lost an arm as a child, battled severe bipolar disorder his whole career, taught a heavy load at City College, and died at 57. The work survived conditions that would have ended most.

I · Play the Post Correspondence Problem

Each domino has a top string and a bottom string. Click dominoes to lay them in a row; the machine concatenates all the tops and all the bottoms. You win when the top string exactly equals the bottom string (and you've used at least one). Try it — some instances have a solution hiding in them, others have none, and there is no general method to tell which.

When the top and bottom finally read the same string, you've found a correspondence. The catch — Post's theorem — is that deciding whether any sequence works is undecidable: you can search (the "solve" button runs a bounded search), and if a short solution exists you'll find it, but no algorithm can always answer "no, there is none" in finite time. ⚑ It's [[alan-turing]]'s halting problem wearing a child's puzzle: the simplest-looking question — can these dominoes line up? — has no mechanical answer, which is exactly why PCP is the favourite tool for proving that grammar ambiguity, program equivalence, and a hundred other problems are impossible too.
"Solvability of a problem … is itself a problem that may be unsolvable." — in the spirit of Emil Post

II · Rewriting is everything

PRODUCTION SYSTEMS

Post's model of computation: a set of rules that rewrite strings of symbols. Apply rules until you stop. That's it — and it's exactly as powerful as a Turing machine. Computation as pure pattern replacement.

THE ANTICIPATION (c. 1921)

Years before Gödel and Turing, Post saw that such systems could express their own limits — that some questions about them must be undecidable, and that no formal system can be both complete and consistent. He glimpsed the whole landscape early.

Post's deepest idea is that computation is rewriting. Forget tapes and heads and λ's: give yourself strings of symbols and rules that say "replace this pattern with that one," and you can compute anything computable. This is the ancestor of every formal grammar (how programming languages are parsed), every term-rewriting system, and the production rules of classic AI. And because his systems could describe themselves, he ran straight into the same wall as everyone else in this lineage — incompleteness and undecidability — only earlier and more obscurely. The Post Correspondence Problem is the crystalline residue of that encounter: a problem so simple a child could play it, so deep that no machine can ever master it. ⚑ The man who saw the limits first, and turned them into a puzzle the whole field still uses. [[alan-turing]]'s machine, [[alonzo-church]]'s λ, [[haskell-curry]]'s combinators, and Post's rewriting are four roads to one place.

III · The first-comer who finished last

Gate kept on. The mathematics is first-rank and exact: production (rewriting) systems are a complete model of computation, the Post Correspondence Problem is rigorously undecidable, and it is the everyday instrument for proving undecidability throughout formal-language theory and verification. The honest centre of Post's story is priority. In the early 1920s, alone, he developed normal/production systems, recognised that they could encode their own decision problems, and concluded that there must be unsolvable problems and that no formal system could be complete and consistent — anticipating [[kurt-godel]] (1931) and [[alan-turing]] (1936). But his health, his teaching load, and his own perfectionism kept the work unpublished until far too late; the formal credit went, properly, to those who published first, and Post himself was scrupulous about acknowledging that. It is one of the most poignant near-misses in the history of thought — a man who saw the entire modern theory of computation in outline before anyone else and could not get it into print. He also gave us many-valued "Post logics" and the foundational "Post's problem" on degrees of unsolvability. He lost an arm at thirteen, lived with severe bipolar disorder, taught devotedly at City College, and died of a heart attack at 57, shortly after electroshock treatment. The credit was late; the work was early; both are true. ⚑ [[haskell-curry]] ← · next → Wittgenstein."