Turing machines whose termination is unprovable? I have a naive question: does there exist a Turing machine whose termination is true but unprovable by any natural, consistent and finitely axiomatizable theory? I ask for a mere existence proof rather than a specific example. 

This might have some connection with ordinal analysis. Indeed, for a Turing machine $M$, we can define $O(M)$ as the least ordinal of a consistent theory proving its termination (or the infimum of these ordinals). So I guess it would be equivalent to ask whether there exists $M$ such that $O(M) \geq \omega_1^{CK}$?
Termination of a Turing machine (on a fixed input) is a $\Sigma^0_1$ sentence and all usual first-order arithmetic theories are complete for $\Sigma^0_1$ sentences, i.e. all true $\Sigma^0_1$ statements are provable in these theories.

If you look at totality in place of halting, i.e. a TM halts on all inputs, then that is a $\Pi^0_2$-complete sentence and for any computably axiomatizable consistent theory which is strong enough (e.g. extends say Robinson's $Q$ theory) there is a TM whose totality cannot be proven in that theory.