If a language L is decidable, does that imply that the is a computable function f such that L is in O(f(n)) ?
For example what would be the complexity class of the language of "provably halting Turing machines that halt in an even number of steps"
If a language L is decidable, does that imply that the is a computable function f such that L is in O(f(n)) ?
For example what would be the complexity class of the language of "provably halting Turing machines that halt in an even number of steps"
The answer to your first question is yes: if $L$ is decidable, there is an algorithm that decides it, and this algorithm has a time complexity which is in $O(f(n))$ for $f(n)=$``maximal running time of the algorithm on entries of length $n$''.
As for your second question, I'm not sure your language is decidable: what would be your algorithm ? Trying all proofs of halting only works if a proof exists, and we'll get stuck if the halting problem for this machine is undecidable. Anyway if an algorithm exists, the above construction for $f(n)$ answers your question.
The answer to your second question is that this problem is not decidable, since in fact that language is equivalent to the halting problem. First of all, every halting program is provably halting (in very weak systems, such as PA), since the computation itself can be turned into a proof of halting. Another way to say this is that every true $\Sigma^0_1$ assertion is provable. So you are really just asking about the language of programs that halt in an even number of steps. But this is equivalent to the halting problem, since we can reduce the halting problem to it: given any Turing machine program $p$, design a new program $p'$ that operates just like $p$, but inserts a redundant step between each step of $p$. So $p$ halts on a given input if and only if $p'$ halts on that input in an even number of steps. So if we could decide your problem, then we could decide the halting problem.
Let me add something on the second question. As D K wrote, the way you formulated it it is undecidable. However, if you take a fixed Turing machine $M$ such that a ($\Sigma^0_1$-sound) theory $T$ proves “for every $x$, $M$ halts on input $x$”, then the language accepted by $M$ is indeed decidable, which means there is a recursive bound on its running time. While this is just about everything one can say in general, quite a lot more is known for some particular theories $T$. For example, if Peano arithmetic proves that $M$ halts on every input, then its running time is eventually bounded by a function $f_\alpha$ in the fast-growing hierarchy with $\alpha<\epsilon_0$.