Bounded-arithmetic provability of Arrow's theorem

Arrow's theorem concerns finite societies and social welfare functions, and its first-order formalisation is a sentence $\theta$ in the language of first-order arithmetic. The theory $\mathrm{I}\Delta_0+\mathrm{exp}$ is bounded arithmetic with induction for bounded formulas and an exponential function.

Bounded-arithmetic conjecture for Arrow's theorem. The first-order formalisation of Arrow's theorem is provable in

$$\mathrm{I}\Delta_0 + \mathrm{exp}.$$

The paper has established that the formalisation is provable in primitive recursive arithmetic and observes that its bounds are exponential; the conjecture asks for the corresponding proof in $\mathrm{I}\Delta_0+\mathrm{exp}$, but no resolution is supplied here.