Constructive proof of boundedness of continuous functions Consider the theorem for the continuous function:
Let $a<b$ be real numbers, and let $f:[a,b]\to{\bf R}$ be a function continuous on $[a,b]$. Then $f$ is a bounded function.
The proof in the classical textbook on real analysis uses the Heine-Borel theorem. It dose not say how to find the bound for $f$, but it show that having $f$ unbounded leads to a contradiction.
Here are my questions:


*

*Is there a direct [EDITED: constructive] proof for this theorem?


*More generally, can a theorem in mathematics always have a constructive proof? Or what kind of statements do not have any constructive proof, say, one has to use techniques such as "proof by contradiction" in order to prove it?

 A: There's a natural proof using sup. Consider the set $X=\{ x \in [a,b] : f \mbox{ is bounded in } [a,x] \}$. Then $X$ is non-empty and no $t<b$ is an upper bound for $X$. Hence $b=\sup X$ and $f$ is bounded in the whole interval. This argument is actually the same one used in Heine-Borel: for continuous functions in compact sets, locally bounded implies globally bounded. That $f$ is locally bounded comes from continuity and is used to prove that no $t<b$ is an upper bound for $X$.
A: There is no a-priori bound on the function: consider the constant function $f = M$. Also, the maximum can be attained at any given point - just take any appropriate quadratic.
As for the second question, that really depends on your notion of "directly".
In constructive mathematics, I believe that a continuous function is supplied with some "modulus of continuity" which immediately implies (directly) boundedness. Whether one can prove intuitionistically that the $\epsilon-\delta$ definition of continuity implies boundedness - probably not, but ask an expert!
A: As for your question about statements that can be proven "directly" or not, I find that this article by Tim Gowers and the resulting discussion in the comments is very interesting. It even addresses the Heine-Borel theorem.
A: Let $\{x_n\}_{n=1}^{\infty}$ be a sequence of points such that $|f(x_n)|$ converges to $M = \sup_x |f(x)|$. You can pass to a convergent subsequence $\{x_{n_k}\}_{k=1}^{\infty}$ which converges to some $y \in [a,b]$. Then by continuity of $f(x)$
$$|f(y)| = \lim_{k \rightarrow \infty} |f(x_{n_k})| = M$$
So $f(y) = \pm M$; therefore $M$ is finite and $|f(y)|$ achieves the value $M$. The proof of the existence of convergent subsequences as in the proof of the Bolzano-Weierstrass theorem, using divisions into halves and so on, is not by contradiction and is reasonably constructive. 
A: Would this be considered a direct proof?
Pick $x_n$ a sequence which is dense in $[0,1]$. Let $y_n =f(x_n)$ and $z_n =\max_{1 \leq i \leq n} y_i$.
Then $z_n$ is increasing, and thus has a limit.
Let $A:= \{ m | z_m > z_{m-1} \}$. If $A$ is finite, it has a maximum $k$ and since $y_n \leq z_k$ for each $n$, it follows that $z_m$ is the maximum of $f(x)$.
If $A$ is infinite, then order its elements incresingly $n_1 < n_2 < ..< n_k< ...$. Then by the definition of $A$, the sequence $y_{n_k}$ is increasing and 
$$y_{n_k}=z_{n_k}= \max_{1 \leq i \leq n_k} y_i (*) \,.$$
Finally pick a convergent subsequence $x_{m_l}$ of $x_{n_k}$. Let $a$ be the limit of this.
By continuity 
$$\lim_{l \to \infty} y_{m_l}= f(a) \,.$$
Since $y_{m_l}$ is a subsequence of $y_{n_k}$, and $y_{n_k}$ is increasing we get
$$\lim_{k \to \infty} y_{n_k}= f(a) \,.$$
But then, since $y_{n_k}$ is increasing, we get from $(*)$ that $y_n \leq f(a)$ for all $n$. Now the density of $\{ x_n \}$ completes the proof.
Note We actually used Heine-Borel theorem in the proof, when we picked a convergent subsequence of $x_{k_n}$ (unless of course one defines compactness that way). No matter what proof one tries, since the same theoremfails for $(0,1)$, somehow compactness is bounded to come in play....  
A: Choose $x_n=\inf\{x:|f(x)|>n\}$, and note that this is bounded by $b$ and (non-strictly) increasing by construction. Now consider:
$$\sup_n {x_n}=\lim_{n \rightarrow \infty} x_n=x_\infty$$
Since $f$ is a real valued function also defined on the end points, there is some $M$ such that $f(x_\infty)=M-1$. Furthermore, since $f$ is continuous
$$f(x_\infty)=\lim_{n \rightarrow \infty}f(x_n)=M-1.$$
Which concludes the proof. However, I would not consider this constructively acceptable since the least upper bound property is not constructively acceptable and we did not even construct the supremum. This is a direct proof, however.
Constructively the theorem may not even be true or relevant. According to Brouwer every function is uniformly continuous, while in Russian recursive mathematics it is possible to disprove the claim by use of Specker sequence. Hence Bishop's analysis (consistent with set theory) limits itself to uniformly continuous functions and the claim is unproved.
