THE COLLAPSE OF THE HILBERT PROGRAM: A VARIATION ON THE GÖDELIAN THEME
Saul A. Kripke · Bulletin of Symbolic Logic · 2022
Abstract The Hilbert program was actually a specific approach for proving consistency, a kind of constructive model theory. Quantifiers were supposed to be replaced by ε-terms. εxA(x) was supposed to denote a witness to $\exists xA(x)$ , or something arbitrary if there is none. The Hilbertians claimed that in any proof in a number-theoretic systemS, each ε-term can be replaced by a numeral, making each line provable and true. This implies thatSmust not only be consistent, but also 1-consistent ( ${\Sigma}_1^0$ -correct). Here we show that if the result is supposed to be provable withinS, a statement about all ${\Pi}_2^0$ statements that subsumes itself within its own scope must be provable, yielding a contradiction. The result resembles Gödel’s but arises naturally out of the Hilbert program itself.