In principle, the answer can depend on the proof system, but as long as you stick to some of the usual Hilbert-style or sequent proof systems, this shouldn’t matter.

First, as explained in http://mathoverflow.net/questions/120106, the question is equivalent to provability of the consistency of FPA in $I\Delta_0+\Omega_1$. (The fact that you are using second order objects to encode proofs and formulas corresponds to using all numbers instead of just the logarithmically small ones in $I\Delta_0+\Omega_1$, hence you end up with the usual consistency statement.)

Now, working in $I\Delta_0+\Omega_1$ (or equivalently, Buss’s $S_2$), the consistency of FPA is equivalent to the consistency of the second-order theory of the model with one-element first-order universe (in whatever finite language, it’s all equivalent), since the two theories are interpretable in each other. This in turn can be reduced to the quantified propositional calculus: since there is only one first-order element (and only one $n$-tuple of elements for every $n$), you can ignore first-order quantifiers and variables, and replace second-order variables with propositional variables both in second-order quantifiers and in atomic formulas. (Purely first-order atomic formulas such as $t=s$ can be replaced with the constant $\top$ for truth.) Thus, the question becomes whether $I\Delta_0+\Omega_1$ proves the consistency of the quantified propositional calculus ($G$).

The answer is that this is one of the major open problems in the area, but it is conjectured to be false. There is a kind of correspondence of subsystems of bounded arithmetic to propositional proof systems; in particular, the fragments $T^i_2$ of $S_2$ (${}=I\Delta_0+\Omega_1$) correspond to the fragments $G_i$ of the quantified propositional calculus, obtained by restricting all formulas in the proof (or alternatively, all cut formulas in the sequent calculus formulation) to $\Sigma^q_i$ or $\Pi^q_i$ formulas (= formulas in prenex form with at most $i$ quantifier blocks). This means:

* $T^i_2$ proves the consistency (and even some form of reflection principle) of $G_i$.

* Conversely, $\mathrm{Con}_{G_i}$ implies over a weak base theory all $\forall\Delta^b_1$-consequences of $T^i_2$ (and more complex consequences of $T^i_2$ can be xiomatized by an appropriate reflection principle). A related fact is that if $T^i_2$ proves a $\forall\Sigma^b_i$ statement, one can translate it into a sequence of quantified propositional tautologies which will have polynomially bounded proofs in $T^i_2$.

* If $P$ is any propositional proof system whose consistency is provable in $T^i_2$, then $G_i$ polynomially simulates $P$.

$S_2$ is the union of its finitely axiomatizable fragments $T^i_2$. This means that $S\_2$ proves the consistency of each fragment $G_i$, but on the other hand, if it proved the consistency of the full quantified propositional calculus $G$, it would imply that $G\_i$ polynomially simulates $G$ for some $i$, and this is assumed to be false. To put it differently, the $\forall\Delta^b_1$-consequences of $S_2$ (as well as $S_2$ itself) are not assumed to be finitely axiomatizable.

The correspondence of theories and propositional proof systems also extends to complexity classes. Sets definable by $\Sigma^b_i$ formulas in the standard model of arithmetic are exactly those computable in the $i$-level $\Sigma^P_i$ of the polynomial hierarchy. The theories $T^i_2$ have induction for $\Sigma^b_i$ formulas, and their provably total $\Sigma^b_{i+1}$-definable functions are $\mathrm{FP}^{\Sigma^P_i}$, so these theories correspond to levels of the polynomial hierarchy. On the propositional side, satisfiability of $\Sigma^q_i$ formulas is a $\Sigma^P_i$-complete problem. Taking the union, $S_2$ corresponds to the full polynomial hierarchy $\mathrm{PH}$. However, the complexity class corresponding to $G$ is $\mathrm{PSPACE}$, as satisfiability of unrestricted quantified propositional formulas is $\mathrm{PSPACE}$-complete. Thus, asking $S_2$ to prove the consistency of $G$ is in the same spirit as collapsing $\mathrm{PSPACE}$ to $\mathrm{PH}$ (and therefore to some its fixed level). (Don’t quote me on this. While the collapse of the $T^i_2$ hierarchy does imply the collapse of $\mathrm{PH}$, for propositional proof systems this becomes only a loose analogy.)

In order to give also an upper bound on the consistency strength, the consistency of $G$, and therefore of FPA, is provable in theories corresponding to $\mathrm{PSPACE}$. The best known such theory is Buss’s theory $U^1_2$, which is a “second-order” extension of $S_2$ with comprehension for bounded sets defined by bounded formulas without second-order quantifiers, and *length* induction for bounded $\Sigma^1_1$-formulas. Notice that things get really messy here, as the first-order objects of $U^1_2$ correspond to second-order objects of FPA, and second-order objects of $U^1_2$ have no analogue in FPA. [Alan Skelley](http://www.cs.toronto.edu/~alan/papers/csl04.pdf) formulated an equivalent (technically, RSUV-isomorphic) theory $W^1_1$. This is syntactically a *third-order* arithmetic, and it is more directly comparable to FPA (as numbers of one theory correspond to numbers of the other, and sets correspond to sets). $W^1_1$ proves the consistency of $G$, and thus of FPA.