 In contrast to the possibility of eliminating infinity as just described stand a number of results that show that some finitary statements can only be proved through infinitary considerations. These results originally emerge with Gödel’s incompleteness theorems (Gödel 1931) but have been recently refined by displaying statements of mathematical interest (whereas Gödel’s statements are of metamathematical interest but have no obvious mathematical interest). In order to understand the conceptual distinctions required, let us grant —as most logicians do—that all finitistic modes of reasoning are included in first-order Peano Arithmetic (henceforth PA).