# 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?

-

Here is a sketch of how the proof might go.

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
The definition of continuity gives "for all x in [0,1], there exists an open interval with rational endpoints such that x is in the interval and for all z in [0,1], if z is in the interval then -n < f(z) < n". I don't see how that can be used to show that "there exists a sequence of open intervals with rational endpoints such that for all x in [0,1], if -n < f(x) < n, then x is in one of the intervals". –  Ricky Demer Oct 8 '10 at 22:35
"Continuous function" has a special definition in reverse mathematics which does not seem to mentioned in Wikipedia yet, but which I allude to in my answer. For in-depth study of this subject one should get hold of Simpson's book Subsystems of Second Order Arithmetic. –  Bjørn Kjos-Hanssen Oct 8 '10 at 23:19
I can't vote up comments on an iphone, apparently, but Bjorn has the right point. In reverse mathematics a continuous function is accompanied by its coded representstion. That coded representation is key to defining sets relative to the continuous function. –  Carl Mummert Oct 9 '10 at 13:22