FOM: Tait's question about classical existence proofs

[Arnon Avron]

In response to my examples concerning Tait's question Fred Richman wrote:
> 
> There is a difference between the "actual calculation" of an integral
> and "actually computing explicit formulas for integrals". The method
> used to prove that continuous functions have definite integrals, with
> some sophisticated refinements, may be all you have in certain cases,
> like the normal distribution function.

Of course. But my point was that just knowing the existence of 
certain integrals is sufficient for yielding useful algoritms,
which is what Tait's question was about, if I understood
it correctly (in this particular case it yields an algorithm
for finding explicit formulas for the antiderivatives of a certain
class of functions. Needless to say, these formulas can in turn be used
also for actually calculating integrals, but this is not the main issue).
 
 > Another example: define a function F on [1,2] by letting F(x) to be
> > the limit of the following sequence: a_0=x, a_{n+1}=SQRT(x+a_n). Here
> > it is very easy to compute the value of F(x)  once
> > it is proved that F is actually defined for x. The proof of this
> > on the other hand (at least the one I know) is purely existential.
> 
> I find this example more interesting. What you prove here is that if
> the limit b exists, then b^2 = b + x from which you get a formula for
> b. How do you know that the limit exists? We are iterating the
> function g(y) = SQRT(x + y) for fixed x, starting at y = x. But g'(y)
> is bounded by 1/2 for the values in question. So the difference of
> successive iterates of g on x goes down by a factor of at least 2 at
> each iteration, whence the iterates form a Cauchy sequence. In fact,
> if I'm not mistaken, the n-th iterate is within 1/2^n of the limit. As
> near as I can tell, this is a constructive proof.

The proof I had in mind was in fact much simpler (to my judgement, at least):
Prove by a straightforward induction that the sequences under consideration
are monotonic and bounded, and so each of them has a limit. Again I am not
sure to what extent this proof counts as "constructive". In any case,
it is almost certain that every simple existence fact of this kind can
be proved constructively (and it certainly should be extremely
difficult to come with a simple concrete example from basic calculus 
of classical existence claim for which one can demonstrate
that no constructive proof exists). The point is, however, that in this 
case (and in many similar ones) ANY existence proof, whether
constructive or not, has an immediate computational significance. 

 
To sum up: constructive existence proofs are usually taken to be
superior to nonconstructive ones because the former allow us to
actually compute the objects they claim to exist, while the latter
do not. What I have tried to show is that frequently once we know 
that something exists we can use other methods and knowledge to compute it
in the most efficient way (in the two examples I gave this was
done by finding a simple equation that only the relevant object
satisfies). When this is the case nonconstructive proofs are
as valuable as constructive ones, and if they are simpler
(as is usually the case) - they are in fact more useful. 

Arnon Avron