11
$\begingroup$

Blum's speedup theorem is a statement about a certain class of computable functions for which it is always possible to find a program of lower complexity. Gödel's speed-up theorem is a statement about the possibility of drastically reducing the size of a theorem proof, by going to a more powerful axiomatic system.

Is Gödel's speed-up theorem an instance of Blum's speedup theorem, in which the computable function takes as input the axioms and outputs the theorem? Such a function could concretely be built in theorem proving programming languages, say for instance with Coq.

Additional info: I found this that looks related, but it doesn't clearly answer my question.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ There is a difference between static complexity measures (like program size or proof length) and dynamic complexity measures (like running time); the latter depend on the input as well. Blum axiomatized both; the speedup theorem you cite refers to dynamic measures. There is a theorem to the effect of: if a programming language L can diagonalize over K, then L has shorter programs than K even for K-computable functions. This resembles Gödel's speedup theorem and I wouldn't be surprised if there was a formal connection. Odifreddi's Classical Recursion Theory vol. 2 is an excellent reference. $\endgroup$
    – Siddharth
    Commented Oct 3, 2023 at 21:25
  • 1
    $\begingroup$ On History of Science and Mathematics, there is a related question whose answer elaborates a bit on the resemblance mentioned by @Siddharth: hsm.stackexchange.com/questions/12317/… $\endgroup$
    – Hermann Gruber
    Commented Oct 4, 2023 at 9:18

1 Answer 1

Reset to default
-1
$\begingroup$

No, it is not, although I have admittedly never heard of either theorem before so I'm just going off the definitions you posted, of which the one for Gödel's theorem is rather lackluster.

Gödel's theorem, as stated on the linked Wiki page, seems to talk about specific theorems having shorter proofs. There are actual examples stated on the page.

On the other hand, Blum's theorem just states that there exists some function which can be sped up as much as you want. In no way is it guaranteed that that function relates to your statement or proof.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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