FOM: Tait's question about classical existence proofs

[Fred Richman]

Arnon Avron wrote (regarding the possibility of a classical but not
constructive proof of an existence statement yielding an algorithm):
 
> My answer is that the calculus is full of examples which indicate
> that this is quite possible, because frequently the existence of
> an object and its actual calculation is totally separated there.
> A good example is provided by the theorem that every continiuous
> function has an indefinite Integral (primitive function).

> when it comes to actually computing explicit formulas
> for integrals, nobody uses the proof of this abstract existence
> theorem, or the method it employs.

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.

> The fact that the integral exists IS, on the other hand, used quite
> frequently. Thus an algorithm for computing the Integral of (sin x)^n
> (in the form of a recurrent formula) is obtained by an integration by
> parts, which relies in a crucial way on the fact that the relevant
> integrals exist.

This is really a question of finding antiderivatives, not indefinite
integrals. The product rule ("integration by parts") allows you to
change the problem of finding an antiderivative of f'g to finding an
antiderivative of fg'. This, and some algebraic maneuvers---it's not a
completely straightforward integration-by-parts problem---give the
recursion formulas. It's all about formulas for derivatives, nothing
about existence of integrals.

> 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.

There remains the question as to whether this proof that the limit
exists is "purely existential". It doesn't give you a formula for the
limit. That seems to be the distinction that Professor Avron is
interested in, both here and in his previous example. It's a real
distinction, but I don't think it is what is commonly thought of as
the distinction between constructive and purely existential proofs.

--Fred