Löb's Legacy

Richard Zach's Log Blog has brought to my attention the recent death of Martin Löb. It is fitting that we think here about his work. The famous Löb Theorem (in "Solution of a Problem of Leon Henkin" JSL, 1955) generates Löb's paradox (ibid.), which goes something like this:

(*) If this sentence is true, then so is A.
Notice that (*) is provable for an arbitrary proposition A. Here's the proof. Suppose (*) is true. Then it satisfies its own antecedent. So it follows that A. By conditional proof, if (*) is true then so is A. And that is just to say that (*) is true.

Notice also, that the provability of (*) underwrites the truth of any proposition A. For this reason and since both (*) and its proof are negation-free, Löb offers (*) as a test for inconsistency of negation-free languages (that allow self-reference).

Löb credits an anonymous referee for extracting the paradox and the insight about how to test for inconsistency without negation. Curry (1942), and not Löb (1955), usually gets credit for the above insights. Johan van Benthem ("FourParadoxes" JPL 1978), however, argues that the Löb+Referee insights were developed independently of Curry's work. Moreover, the Curry paradox is treated by Curry and his students as a feature of formal systems only, whereas Löb's paradox is a natural language paradox.

An interesting loose-end is the identity of the 1955 anonymous referee that extracted the paradox from Löb's Theorem.