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.

unrestrictedFPA is an open problem. There is a chance that its provability inrestrictedFPA may be refuted unconditionally, because this breaks the connection to $I\Delta_0+\Omega_1$. $\endgroup$ – Emil Jeřábek Jan 30 '13 at 12:29consistencyof RCons(FPA + E(n)), you need to specify what kind of consistency, and how one should understand the consistency of the bare formula RCons(FPA + E(n)) without a background theory (i.e., should it really be the consistency of FPA + RCons(FPA + E(n)), or something else). $\endgroup$ – Emil Jeřábek Jan 30 '13 at 12:34