**EDIT**: I noticed that I misunderstood the question after posting the answer, so this is not a answer to the question. I am leaving it here just in case it might be interesting to others.

----

This is studied in bounded reverse math by people like [Fernando Ferreira](http://www.ciul.ul.pt/~ferferr/index_english.html) and colleagues.

The base theory BTFA [Fer'94] is a two sorted theory version of Sam Buss's bounded arithmetic theory $S^1_2(\alpha)$ [Bus85, ch. 9] plus bounded collection/replacement for $\Sigma^b_\infty $ formulas ($B\Sigma^b_\infty$) plus a form of comprehension axiom for $\Delta_1$ sets ($\nabla^b_1CA$):

$$\forall x (\forall z \ \varphi(x,z) \leftrightarrow \exists y \ \psi(x,y)) \Rightarrow \exists Z \ \forall x \ (x \in Z \leftrightarrow \exists y \ \psi(x,y))$$
 
where $\varphi$ and $\psi$ are respectively $\Pi^b_1$ and $\Sigma^b_1$ formulas. This is a modification of Simpson's axiom in his book [Sim'09]. Because of its special form the first order part is conservative over $S^1_2$ and is incapable of using the full power of comprehension for $\Delta_1$ sets. On the other hand, the second order part of the smallest model of the theory is $\Delta_1$ sets.

In [FF'02, thm. 4], a version of the Intermediate Value Theorem is proven in BTFA. Some caution is needed here in formalizing the IVT. Also the proof is not constructive (either there is a rational number which is the root of the function or we can continue a process getting arbitrary close to a root. Deciding that a given rational number is not a root of the function is not decidable and this is required since we need to stop the process of dividing the current interval into two halves if we reach a root, i.e. we need this assumption so we have $f(m)<0 \ \lor \ f(m)>0$ where $m$ is the rational mid-point of the current interval). As far as I remember WKL is not provable in BTFA. See also [FF'05] and [FF'08].

----
References:

  1. Fernando Ferreira, "[A feasible theory for analysis](http://www.ciul.ul.pt/~ferferr/feasible.pdf)", The Journal of Symbolic Logic 59, 1001-1011, 1994.

  2. António Fernandes and Fernando Ferreira, "[Groundwork for weak analysis](http://www.ciul.ul.pt/~ferferr/groundwork.pdf)", The Journal of Symbolic Logic 67, pp. 557-578, 2002.

  2. António Fernandes and Fernando Ferreira, "[Basic applications of weak König's lemma in feasible analysis](http://www.ciul.ul.pt/~ferferr/basic.pdf)", in "Reverse Mathematics 2001", edited by Stephen Simpson. Lecture Notes on Logic (Association for Symbolic Logic), vol. 21, pp. 175-188 (A K Peters, 2005).

  3. Fernando Ferreira and Gilda Ferreira, "[The Riemann integral in weak systems of analysis](http://www.ciul.ul.pt/~ferferr/riemann_ff.pdf)", Journal of Universal Computer Science, 14, no. 6, pp. 908-937 (2008).

  4. Samuel R. Buss, "[Bounded Arithmetic](http://www.math.ucsd.edu/~sbuss/ResearchWeb/BAthesis)", Bibliopolis, Revision of 1985 Ph.D. thesis.

  5. Stephen G. Simpson, "[Subsystems of Second Order Arithmetic](http://www.math.psu.edu/simpson/sosoa/)", Second Edition, Perspectives in Logic, Association for Symbolic Logic, Cambridge University Press, 2009.