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.


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.