7
$\begingroup$

Blum's speedup theorem seems to me that bears at least some superficial resemblance to Godels research on the length of proofs under certain axiomatic systems. Does Blum's speedup theorem has any conceptual predecessors?

$\endgroup$
9
$\begingroup$

The resemblance is not superficial. There is a precise relation between computer programs and formal proofs known as the Curry–Howard correspondence that took shape in 1960s. And Godel's results on proof length were a direct inspiration for speed-up theorems starting with Blum's 1967 result, see Dawson, The Godel Incompleteness Theorem from a Length-of-Proof Perspective:

"In one year (1936) three important papers appeared, all based on considerations of the length or complexity of proofs in formal systems. One, Rosser's improvement of the Incompleteness Theorem, has already been mentioned. The others were Gentzen's consistency proof for arithmetic ([7], translated in [23, pp. 132-213]), the first of its kind, employing a transfinite induction on the complexity of derivations; and a brief and little-noticed article by Godel himself ([10], translated in [5, pp. 82-83]). The latter, titled simply "On the Length of Proofs," pointed out that, by passing to systems of "higher type" (allowing sets of integers, sets of sets of integers, etc.), not only can new theorems be proved, but "it becomes possible to shorten extraordinarily infinitely many of the proofs already available."

Translated only in 1965, Godel's length-of-proof paper was largely ignored until after the advent of the computer revolution, when concern for efficiency of computation led to Manuel Blum's creation of computational complexity theory, and Godel's proof-shortening result was resurrected to become the progenitor of a whole class of speed-up theorems (see [1, pp. 253 and 261-263])."

[1] is Arbib, Theories of Abstract Automata (1969).

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.