It is known that Hilbert proposed in the state of crisis of foundations of mathematics that we create formal theories which we analyze using "proof theory" or "metamathematics". He then also said that such analysis must be finitary in order to be convincing enough [Kleene "Introduction to Metamathematics" 1971].
I have some sort of intuition behind what finitary means just because I have seen a lot of metamathematical proofs. But the problem is that I have never found any source which said "Hilbert by finitary probably meant ... ". Also, I am confused about what logicians nowadays consider to be finitary in metamathematical reasoning.
When I worked through Godel's incompleteness theorem as presented in Kleene's "Introduction to Metamathematics" it used a lot of properties of natural numbers. Then I thought to myself - why would one formalize number theory if one uses it in metamathematics anyways? Then, my answer would be, because we would like to formalize even more abstract theories like real numbers (which are uncountably infinite) and set theory, and so forth. But then what makes natural numbers so reliable and other theories not? Recently I started learning about Turing machines and, even though Hilbert proposed finitary methods before the development of Turing machines, I feel like this is the closest that I have to being a finitary method. There, natural numbers play a special role because they are countable and each number can be represented as, say, finite amount of marks on the tape. For example, for the proof of Godel's incompleteness theorem we show that functions like predicate being a prime number are primitive recursive functions (which are therefore Turing computable functions). I feel like then the feeling of being secure with such operations (like, why + on natural numbers commutes) basically just means a statement that one might mechanically check for arbitrary two numbers certain property. So, we reduce proofs to being purely mechanical without intuition at all. Then it also makes sense why Turing machines are required to compute in finite steps because then it means that whenever someone doesn't believe me in metamathematical proof using natural numbers then one can check the statement by writing certain strings under certain well described rules (and if numbers are not too large) and just check it. This for me suffices to be finitary and convincing enough for metamathematics.
Why this is important to me? I just want to understand when one says "let us use finitary methods" what does that mean.
What do you think? I would appreciate your opinions and comments about this. I hope I made myself clear enough - if not please let me know.