Hilbert's program is popularly understood as an attempt to justify infinitary mathematics with a finitary consistency proof. Godel's Second Theorem is usually considered as showing this is not possible.
Question (to be made precise below): Can finitary mathematics be justified with a ultrafinitistic consistency proof?
Consider FPA, a multi-sorted first-order theory, with lower-case or small letters (for numbers) and upper-case or big letters for relations of n-arity (n >= 1). (Practically, I think one can limit the theory to relations where n = 1, 2, or 3.)
Full comprehension is assumed.
FPA has a constant symbol 0, a 1-ary relationship N (natural number), and a 2-ary relationship symbol S (successoring).
In this context the Peano Axioms can be written:
(PA1) N0
(PA2) $\forall$n (Nn $\Rightarrow$ $\exists$m (Nm & Sn,m))
(PA3) $\forall$n$\forall$m$\forall$m' (Nn & Nm & Nm' & Sn,m & Sn,m' $\Rightarrow$ m = m')
(PA4) $\forall$n$\forall$m$\forall$n' (Nn & Nm & Nn' & Sn,m & Sn',m $\Rightarrow$ n = n')
(PA5) $\forall$n (Nn $\Rightarrow$ $\neg$ Sn,0)
(PA6) $\forall$P (P0 & $\forall$n$\forall$m(Pn & Sn,m $\Rightarrow$ Pm) $\Rightarrow$
$\forall$n(Nn $\Rightarrow$ Pn))
FPA assumes all the Peano Axioms except (PA2), that is, everything except the totality of the successor relationship. It has as its standard models all the initial segments as well as the standard model of the natural numbers. {0} is a model. It is therefore agnostic as to whether the natural numbers go on and on. Let's call it "ultrafinitistic" even if it's not always clear to me what "ultrafinitistic" means.
Now an ultrafinitistic Hilbert's Program might be the following. Let E(n) be the wff
$\exists x_1 \exists x_2 … \exists x_n$(N$x_1$ & S0,$x_1$ & N$x_2$ & S$x_1,x_2$ & … & S$x_{n-1},x_n$)
i.e. the assertion that the number n exists. The ultrafinitistic hope would be that FPA can prove the consistency of FPA + E(n) for any n, or even (this would be magical) prove the assertion
$\forall$n Cons(FPA + E(n)).
Now in one sense of consistency, where like Godel one uses numbers to represent sequences, one can actually get started on this. Restricting the arities of the upper-case letters to no more than 3 (which is sufficient to develop the appropriate apparatus), it seems that FPA can prove the Godel consistency of FPA + E(1) and FPA + E(2).
However, the proof works with a certain cheat; Godel numbering uses numbers so big that the assumption that there is a proof leading to a contradiction implies the existence of a truly big number, which provides enough space for creating a model of true-in-{0,1} or true-in-{0,1,2} for propositions whose length are <= the length of the longest proposition appearing in the proof of contradiction. A more appropriate manner of representing consistency would surely be to use the upper-case letters, since then a sequence of length n only implies the existence of n, which is obviously much smaller than the Godel number. Let RCons(FPA) and the like represent this notion of consistency.
According to
Can FPA really prove its consistency?
whether FPA can prove RCons(FPA) is equivalent to a well-known open problem which is conjectured to be false. Obviously, this does not bode well for FPA proving stronger systems to be RCons consistent. Still, "open" brings hope, so my questions are:
(1) Can it be shown, for any n, that FPA does not prove RCons(FPA + E(n))?
(2) If so what is the smallest n?
(3) If not can it be shown that FPA cannot prove $\forall$n Cons(FPA + E(n)) ?
If something significant can be said with a different formula asserting the existence of a number other than E(n) (e.g. defined using an exponential), that would obviously be of interest. (EDITED ADDITION: The restriction of upper-case letters to arity 3 or less is welcome, especially if a "yes" answer plays on unbounded arity.)
Since this is my third question about this theory, I would also like here to refer to this question/answer, where the models (and other details) of FPA are described:
Provability in Second-Order Arithmetic without the Successor Axiom
so with one search I can later find everything.
Thanks for your time.
Best Answer
Ulrich Kohlenbach with his coworkers in proof mining has perhaps the best modern nonfatalist position about Hilbert program. Rather than stressing over Gödel's demolition of Hilbert's ideal, we can analyze the extent to which "non-finitary" methods play a role. This has lead to some very nice results and applications of proof theory. Lecture 1 of Ulrich's notes on "Proof mining" provides a quick but more careful explanation of the idea that proof mining is the natural outcome of Hilbert's program.