Was "arithmetical translation" (that is, coding in the Goedel sense) ever a part of Hilbert's Program? I ask this question for several reasons:
i) it gives the numerals |, ||, |||,.... an ersatz 'meaning' in themselves and Hilbert (at least in his paper "On the Infinite") states that "These numerals, which are the object of our consideration, have no meaning at all in themselves."
ii) inasmuch as a formal first-order theory $T$ (containing enough arithmetic for Goedel numbering) was to be treated as a 'formula game' of 'meaningless symbols' for the purpose obtaining a finitary consistency proof of $T$, "arithmetical translation" of $T$ into itself gives these 'meaningless formulae' meaning, which produces self-reference (assuming $T$ proves multiplication to be total, following Dan Willard's results regarding self-verifying formal theories) which, assuming $T$ proves multiplication to be total, derives the incompleteness theorems. But then, what was the purpose of Hilbert requiring the formulae of $T$ to be 'meaningless'? Wasn't it the purpose of actually having a finitary proof of the consistency of $T$ (meaning that treating the formulae of $T$ as meaningless strings of symbols may allow one to avoid, say, the use of primitive recursive functionals of finite type to prove the consistency of $T$, as Goedel does for $PA$)?
iii) Consider also the following statement of Bernays from his survey article from 1935, "Hilbert's investigations on the foundations of arithmetic" (Bernays project: Text no. 14, translation by Dirk Schlimm, which can be found under title on the web) regarding Goedel's incompleteness theorems:
"The theorem mentioned [that is, the one that decides "whether it is possible to provide a proof for the consistency of number the theoretic formalism with elementary combinatorial methods in the sense of the 'finite standpoint' "] is one of the different important results of Goedels' paper ["On Formally Undecidable propositions of Principia Mathematica and Related Systems I], which has brought fundamental enlightenment with regards to the relation between contentfulness and formalism--whose investigation has been mentioned by Hilbert in "Axiomatisches Denken" as one of the aims of proof theory.
The basic message of the theorem is that a proof for the consistency of a consistent formalism, which encompasses the usual logical calculus and number theory, cannot be represented in this formalism itself, more precisely: it is not possible to deduce the elementary arithmetical theorem which represents the claim of the consistency of the formalism--based on a certain kind of enumeration of the symbols and variables and an enumeration of the formulas and of the finite series of formulas derivated from it--in the formalism itself.
To be sure, nothing is said hereby directly about the possibility of finite consistency proofs; but a criterion follows, which every proof of the consistency for a formalism of number theory or a more comprehensive formalism has to meet: a consideration must occur in the proof which can not be represented--based on the arithmetical translation--in the formalism mentioned."
If anyone can provide a cite from any of Hilbert's writings, letters, etc. stating that arithmetization (or any other form of coding) of some first-order theory $T$ in itself was a part of his program, I would be very grateful. Thanks in advance for your help.