 Gödel mentioned the possibility of the unsolvability of a question about the reals already in his 1929 thesis, in arguing against the formalist principle of Hilbert’s, that consistency is a criterion for existence. In fact, giving a finitary proof of the consistency of analysis was a key desideratum of what was then known as the Hilbert program, along with proving its completeness. Accordingly it was Gödel’s turn to these questions, especially the first, which led him to the two incompleteness theorems. (For a discussion of the Hilbert Program the reader is referred to the standard references: Sieg 1990, 1988, 1999; Mancosu 1998, Zach 2003, Tait 1981 and Tait 2002.)