FOM: Tait's question about classical existence proofs

[Arnon Avron]

Only recently I came accross the Following question of Tait:

>Is it impossible that, for example, there could be a classical but 
>no 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). Not being
a specialist on constructive Mathematics, I am not sure to what extent
the usual proof is constructive. This does not matter, however,
because when it comes to actually computing explicit formulas
for integrals, nobody uses the proof of this abstract existence 
theorem, or the method it employs. 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. 
Now in this case one can easily prove the correctness of
the resulting formula by ordinary induction, but this is
not necessary from a classical point of view. More important: in this
case the "constructive" proof is given only after the formula is found
(not guessed!) by classical reasoning.
 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.

Arnon Avron, Professor
School of Computer Science
Tel-Aviv University, Israel