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 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", The Journal of Symbolic Logic 59, 1001-1011, 1994.

2. António Fernandes and Fernando Ferreira, "Groundwork for weak analysis", The Journal of Symbolic Logic 67, pp. 557-578, 2002.

3. António Fernandes and Fernando Ferreira, "Basic applications of weak König's lemma in feasible analysis", 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).

4. Fernando Ferreira and Gilda Ferreira, "The Riemann integral in weak systems of analysis", Journal of Universal Computer Science, 14, no. 6, pp. 908-937 (2008).

5. Samuel R. Buss, "Bounded Arithmetic", Bibliopolis, Revision of 1985 Ph.D. thesis.

6. Stephen G. Simpson, "Subsystems of Second Order Arithmetic", Second Edition, Perspectives in Logic, Association for Symbolic Logic, Cambridge University Press, 2009.

Post Undeleted by Kaveh
Post Deleted by François G. Dorais
Post Undeleted by François G. Dorais
Post Deleted by Kaveh
2 added 573 characters in body; deleted 21 characters in body
1