Was "arithmetical translation" (coding in the Goedel sense) ever a part of Hilbert's Program?

Question

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.

Answer 1

The following quote from Dan Willard's preprint "On the Broader Epistemological Significance of Self-Justifying Axiom Systems" (found on his Homepage) is, I believe, of some small significance:

"In any case some years after he wrote *'s initial statement

[* 'It must be expressly noted Proposition XI represents no contradiction of the formalistic standpoint of Hilbert. For this standpoint presupposes only the existence of a consistency proof by finite means, and there might conceivably be finite proofs which cannot be stated in P or in...'],

Goedel gave a 1933 lecture..., where he told his audience that Hilbert's initial 1926 objectives, summarized formally by ** below, had 'unfortunately' no 'hope of suceeding along' its originally intended plans.

** (Hilbert ['On the Infinite', pp. 375-6 of van Heijenoort] 1926): ' Let us admit that the situation in which we presently find ourselves with respect to paradoxes is in the long run intolerable. Just think: in mathematics, this paragon of reliability and truth, the very notions and inferences, as everyone learns, teaches, and uses them, lead to absurdities. And where else would reliability and truth be found if even mathematical thinking fails?' (It is evident that Hilbert is advocating in this 3-sentence passage a version of his Consistency Program that modern mathematicians consider over-simplistic in light of the strength of the Second Incompleteness Theorem. This is because Item 2 of Hilbert's next pargraph is clearly making an excessive promise when it attaches no reservation to its declaration that: 'It is necessary to make inferences everywhere as reliable as they are in ordinary elementary mathematics, which no one questions and in which contradictions and paradoxes arise only through our carelessness'.)

Prof. Willard, I believe, speaks for the majority of the mathematical community with this statement. As Andrej Bauer (in his comments to this question) rightly points out, :"...Goedel did exactly what Hilbert wanted...". In what sense did Goedel do exactly what Hilbert wanted? Well, if one wants to make "inferences everywhere as reliable as they are in ordinary elementary arithmetic", what better way to do this is to see if one can reformulate these inferences as statements of elementary arithmetic itself--if one could, then these inferences would be shown to be completely reliable, according to Hilbert's stated belief. This Goedel did, and as Andrej Bauer again rightly points out, Goedel "...proved a neat result. It just happened to be a result not anticipated by Hilbert."

However, is this precisely what Hilbert wanted (or even required)? The following statement by his assistant, Paul Bernays, in his 1930 report (Bernays Project: Text no. 9, pp.57-8) "The Philosophy of Mathematics and Hilbert's Proof Theory", suggests otherwise:

" We believe that number theory as determined by Peano's axioms with the addition of definition by recursion is deductively closed ["a theory is deductively closed... if it is impossible to add a new axiom expressible in terms of the theory but not already derivble with out producing a contradiction--or, which amounts to the same thing: if every statement formulatable in the framework of the theory is either provable or refutable"--this from the previous paragraph (my comment)]; but the task of giving a real proof of this belief is still completely unsolved. The question becomes even more difficult if we go beyond the domain of number theory to analysis and further set theoretic ways of constructing concepts.

In the region of these and related questions there is a considerable field of open problems. But these problems are not of such a kind that they represent an objection to the standpoint we have adopted. we must only keep in mind that the formalism of statements and proofs which we use to represent ideas are notidentical with the structure which we have in our mind in our conceptual thinking. The formalism suffices for formulating our ideas about infinite manifolds and for drawing out the logical consequences of these ideas; but in general it [the formalism--my comment] is not able, so to speak, to produce the manifold out of itself combinatorially."

Two points should immediately jump out at the reader from this rather long quote from Bernays: i) the notion that $PA$+"Definition by recursion" is deductively closed was a "belief" of which "a proof of this belief is still completely unsolved"); and ii) that "The formalism suffices for formulating our ideas about infinite manifolds and for drawing out the logical consequences of these ideas; but in general it [the formalism--my comment] is not able, so to speak, to produce the manifold out of itself combinatorially." As to i), it seems (to me, at least) that such an unproven belief could not really be part and parcel of any 'program' (i.e. Hilbert's program should be able to exist with or without the deductive closure of $PA$+"Definition by recursion"); and as regards ii), this suggests (rather metaphorically) that "the structure which we have in our mind in our conceptual thinking..." is not "identical" to the "formalism of statements and proofs which we use to represent our ideas...". If it is not, then both Hilbert and Bernays (by this statement) seemed to understand that there might be statements formulatable in $PA$+"Definition by recursion" that would not be provable in the formalism and that there would be 'finitary proofs' not formulatable in the formalism. Evidence for this viewpoint might be Hilbert's proof of the consistency of $PRA$ (whose proof-theoretic ordinal is $\omega^{\omega}$).

Answer 2

It should be noted also that Goedel said (according to a personal communication between Gerald Sacks and Piergiorgio Odifreddi (1987) as reported by Odifreddi in his paper "Goedel's Mathematics of Philosophy", chapter 13 of Kurt Goedel and the Foundations of Mathematics) that "he got the idea of arithmetization from Leibniz. Sacks seemed to be skeptical about the causal effect and suggests that Goedel may have only thought of it after the fact.

Be that as it may, it cannot be denied that in Leibniz's (1666) Dissertatio de arte combinatoria, one indeed finds a detailed exposition of a method to associate numbers with linguistic notions. However, one also finds a quite surprising naivety: to associate composite numbers with composite notions, Leibniz proposes (in sect. 69) to use multiplication, thus making decomposition uncertain (because a number may have multiple decompositions).

Goedel's improvement on Leibniz was the use of prime exponentiation in place of multiplication. This made decomposition unique by the prime factorization theorem."

Although Odefreddi states at the outset that " I claim that some of Goedel's main results can be interpreted as being mathematically precise formulations of Aristotle, Leibniz, and Kant.", Sacks' personal communication (regardless of his skepticism regarding the causal effect of Leibniz on Goedel) and Odifreddi's report that Leibniz wanted to use multiplication to associate composite numbers with composite ideas suggests that this notion (because of Goedels use of prime exponention to make the decomposition unique) that Goedel was inspired by Leibniz to arithmetize Russell's Principia Mathematica in itself is, at least, plausible.

But where, then, does this leave Hilbert, Bernays, and arithmetization?