It's been suggested (e.g. by Pen Maddy, Philip Kitcher, and possibly by my advisor PK) that we can get some 'external evidence' for the truth of mathematical statements which are independent of our axioms, by noticing that they allow us to prove things which we already know to be true (because we can prove them directly from our axioms) much more quickly.
However, Godel's Speed Up Theorem seems to show that ANY genuine strengthening of our axioms would have this property. I quote from a presentation by Peter Smith:
"If T is nice theory, and γ is some sentence such
that neither T
⊢ γ nor T ⊢ ¬γ. Then the theory T + γ got
by adding γ as a new axiom exhibits ultra speed-up over T"
"Nice" here means all the hypotheses needed for Godel's theorem to apply to a theory, and "ultra speed up" means that for any recursive function, putatively limiting how much adding γ can speed up a proof, there's some sentence x whose proof gets sped up by more than f(x) when you add γ to your theory T.
Smith just points out that we shouldn't be surprised by historical examples of proofs using complex numbers of set theory to prove things about arithmetic.
But doesn't this theorem also raise serious problems for taking observed instances of speed up to be evidence for the truth of a potential new axiom γ ?