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?



Proving boundedness of continuous images of [0,1] in WKL0
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.


