# Proving boundedness of continuous images of [0,1] in WKL0

I've been reading about reverse mathematics (mostly on wikipedia), and I had been thinking that I understood how to prove the equivalences to WKL0 and ACA0 mentioned in the its article. However, I now realize that my idea of how WKL0 can prove that every continuous real valued function on [0,1] is bounded. My idea would have started "since f is continuous, there f is locally bounded near each point, so there is an open cover of [0,1] such that f is bounded on each member of the cover", but I can't figure out how to express "f is bounded on the interval with rational endpoints (q,r)" as a Sigma_1 property, and I can't figure out how to get around this issue, either.

How does WKL0 prove that every continuous real valued function on [0,1] is bounded?

-

If $f:[0,1]\rightarrow\mathbb R$ is continuous but not bounded then the sets $S_n=[0,1]\setminus f^{-1}[(-n,n)]$ are closed with $S_n\ne\emptyset$ for all $n\in\mathbb N$. According to the definition of continuous function the sets $f^{-1}[(-n,n)]$ are represented as $\Sigma_1$ sets of (endpoints of) rational intervals ($\Sigma_1$ definable in the model). So the closed dyadic rational intervals intersecting $S_n$ for $n\in\mathbb N$ can be represented as an infinite $\Pi_1$ (or by a standard trick, equivalently $\Delta_1$) tree, which by Weak König's Lemma must have a path, so $\cap_n S_n\ne\emptyset$ which is absurd.
How are the definition of continuity show that the sets $f^{-1}([-n,n)]$ are represented as the union of $\Sigma_1$ collections of open intervals with rational endpoints? (I'm also not sure how it's provable that those collections are sets, but that's not needed.) –  Ricky Demer Oct 8 '10 at 20:43
I think that's basically the definition of continuity. Since every object in reverse math that belongs to the model must be represented by an element or a subset of $\mathbb N$, one cannot just use the set-theoretical definition of a function. You're right, a set being $\Sigma_1$ definable in the model does not imply the set is in the model, just that there is a $\Sigma_1$ formula with parameters from the model that defines the set. –  Bjørn Kjos-Hanssen Oct 8 '10 at 21:40