9
$\begingroup$

Blum's speedup theorem is a statement about a certain class of computable functions for which it is always possible to find a faster algorithm. 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.

$\endgroup$

Your Answer

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

Browse other questions tagged or ask your own question.