On an alleged refutation of Hilbert's Program using Gödel's first incompleteness theorem (Q809063)

From his own ``instrumentalistic'' point of view the author criticizes arguments of \textit{C. Smoryński} [Self-reference and modal logic (1985; Zbl 0596.03001); CWI Q. 1, No.4, 3-59 (1988; Zbl 0665.03001)] claiming that already Gödel's First Incompleteness Theorem was a definite disproof of Hilbert's Program. The author's more formal arguments are convincing, his more philosophical ones rather debatable. Finally, he adds some quite speculative ideas on how also Gödel's Second Incompleteness Theorem may not be an argument against Hilbert's Program. Reviewer's Remark: Hilbert as a working mathematician offered his foundational program as a kind of long range research strategy. Therefore it seems quite preferable to look at his distinct formulations cum grano salis and not to take them as statements of a professional philosopher; this would open the way to interpret his program more freely and to avoid unnecessary debates about something like a ``true understanding'' of his program as well as on (ir)refutable refutations of it.