 Be that as it may, it seems that Gödel actually arrived at the first exact observations about incompleteness via a different route, during his attempts to contribute to Hilbert’s program, and not to undermine it (see Dawson 1997: Ch. IV). Namely, in 1930, Gödel made an effort to advance Hilbert’s program by attempting to prove the consistency of analysis (or, second-order arithmetic) with the resources of arithmetic, and thus reduce the consistency of the former to the consistency of the latter. In his attempted proof, he needed the notion of truth. Gödel soon faced various paradoxes (such as the Liar paradox), and had to conclude that arithmetical truth cannot be defined in arithmetic. Hence, Gödel first arrived at a version of the undefinability of truth theorem, usually associated with Tarski (cf. Murawski 1998). This also easily yields a weak version of the incompleteness result: the set of sentences provable in arithmetic can be defined in the language of arithmetic, but the set of true arithmetical sentences cannot; therefore the two cannot coincide. Moreover, under the assumption that all provable sentences are true, it follows that there must be true sentences which are not provable. This approach, though, does not exhibit any particular such sentence.