What did Hilbert actually want for his second problem?

When I read about the historical background of Gödel's incompleteness theorems, it is often mentioned that he was essentially responding to Hilbert, who was trying to prove the consistency of (Peano) Arithmetic. One textbook I read a while ago suggested he was trying to do this from within PA or some subset thereof, since a stronger system would be even more likely to contain an inconsistency than PA itself. In particular, this is described as Hilbert's second problem.

But that doesn't make any sense to me. If PA is inconsistent, then by the principle of explosion, PA proves that PA is consistent, so a consistency proof of PA written in PA is worthless (insofar as PA could still be inconsistent despite the proof). The principle of explosion is much older than Gödel's theorems, and surely Hilbert was aware of it.

What did Hilbert want as a solution to his second problem? Since $\mathrm{PA}\vdash Con(\mathrm{PA})$ would not be sufficient, what did he expect to see on the left side of the turnstile?

In other discussion of this problem, I sometimes encounter the word "finitistic," but I'm not sure what that actually means in this context. No matter what theory you use, you're still going to doubt its consistency, right? When does it end?

Solution 1:

What Hilbert wanted on the left side of the turnstile was something that was "obviously" consistent. History has been difficult for Hilbert's program, so it is not as easy to see what he was looking for from a modern perspective. But is it important to remember that the incompleteness theorems were, in a way, completely unexpected. The idea that some things might be forever unknowable or unjustifiable is still controversial, but to Hilbert it would have been unthinkable.

One example of a theory that is commonly accepted as finitistic is primitive recursive arithmetic (PRA). In one common axiomatization, this theory does not have any quantifiers in its language, just a large collection of function symbols with explicit definitions. The consistency of PRA is much less difficult to see than the consistency of PA -- PRA is, arguably, "obviously consistent". From Hilbert's viewpoint, it would not have been inconceivable that PRA could prove the consistency of PA. Only the incompleteness theorem showed this was impossible.

We can also look at the history of model theory, which as a field was also not well established in the time when Hilbert was active. The Lowenheim--Skolem theorem, for example, developed in fits and starts, and was not very well understood even in the 1930s. Henkin's method for generating models of consistent theories, which is now taught in basic courses, did not appear until 1949. Gödel's proof of the completeness theorem in 1929 was much more complicated and did not give the same clear conceptual picture as Henkin's proof. So our modern intuition about how easy it is to build nonstandard models would not have been clear to Hilbert.

Hilbert described the "obviously consistent" theories he was interested in as "finitistic". There is some general consensus that Hilbert's finitism corresponds to PRA, although this is not universally accepted among philosophers. In any case, PRA is an example of the sort of theory Hilbert was interested in.

Hilbert certainly would have realized that consistency proof of PA within PA is not very useful -- but he would have thought it should be possible to prove the consistency of PA in a weaker theory. Gödel showed this cannot be done even in PA, which covers Hilbert's goal and more.

A somewhat separate issue is that it probably was not clear, before the work of Gödel and Turing, that PA can formalize any finitistic theory, and so any finitistic theory will necessarily be weaker than PA. So it might have also been plausible that there could be a finitistic theory that could prove the consistency of PA without actually being weaker than PA in a formal sense. Some people still look for such theories today; see Hilbert's Program on the Stanford Encyclopedia of Philosophy.

We now know that we can trade the complexity of PA for a different sort of complexity, if we want to prove the consistency of PA in theories that are neither weaker nor stronger than PA. Gentzen's consistency proof of PA trades the induction scheme for quantifier-free transfinite induction. Gödel's Dialectica consistency proof of PA trades the induction scheme for a generalization of PRA to higher-type objects, in a quantifier-free theory known as System T. Neither of these is generally considered "finitistic", but both do reduce the consistency of PA to a theory that is, in some ways, more "obviously" consistent.