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 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.