A Scrabble on Cantor, Hilbert, and Zermelo (4)

何書こうとしてたか忘れてしまった。。。

Yes, as one well knows, Hilbert's attempt to show the existence of mathematical objects through proving the consistency of the theory is undermined by Gödel's second imcompleteness theorem (at least in usual arguments). What is important here is that one cannot prove consistency of theories, which at least is as strong as representing PA, with 'finistic' means. In saying 'finistic' means, we can separate two elements roughly: formulas should be finite, or, proofs should be finite. Following Grattan-Guiness, we can specify the former as 'horizontally finite', the latter as 'vertically finite'.

In this respect, what development of proof theory after Hilbert (especially, the theory of ordinal analysis) sees that allowing the vertically-infiniteness, we can prove relevant theories with still 'finistic' (or constructive) means. How about horizontally-infiniteness? Arguably, direct responces to Gödel's theorems were to find difficulties of Hilbert's program in horizontally-finiteness. At least one of Zermelo's point is this (he argued also vertically-infiniteness). His basic impression to Hilbert's attempt is such a kind:

If mathematics really deals with the infinities (and actually so), by no means finite language can represent all of that.