FOM: Tait's question about classical existence proofs

[Fred Richman]

Arnon Avron wrote:

>>> [Avron] 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).
>>> It is very easy to compute the value of F(x) once
>>> it is proved that F is actually defined for x.

>> [Fred] [ A constructive proof of the existence of the limit. ]

> [Avron] 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".

As it relies essentially on the least upper bound principle, this
proof would certainly be classified as nonconstructive. 

Two issues are raised here which are quite interesting. One has to do
with the oft made claim that constructive proofs are preferable but
not necessary. The other is the issue of certain statements made by
constructivists that have been characterized as "counterproductive and
needlessly provocative."

Professor Avron clearly prefers the nonconstructive proof: it's "much
simpler." I'm not sure that's true---the argument that the sequence is
increasing doesn't seem more straightforward to me than the argument
that the magnitude of the difference of successive terms goes down by
a factor of at least 2. However, let's say that it is. Then why would
the constructive proof be preferable?

It is easy to get a formula that a limit b must satisfy, namely bb = b
+ x, which leads directly to an algorithm to compute b. So we have a
way to compute the limit, if it exists. What good would it be to have
a *constructive* proof that the limit exists? As Professor Avron put
it:

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

But a constructivist is still going to feel that a constructive proof
that the limit exists is necessary. It would be difficult to defend
the constructivist program if he didn't. Why does he feel that way? It
seems to me that there can only be one reason: he does not think that
Professor Avron's argument constitutes a proof that the limit exists. 

One reason he doesn't buy the proof, even in conjunction with the
formula for the limit, is that "the objects they claim to exist" in
this case consist of more than simply the number which is the limit.
When you claim that a sequence converges to a number, you are claiming
(at least) that for each epsilon there is term in the sequence that is
within epsilon of the number. The argument via the least upper bound
principle does not tell you how to compute the index of such a term.

--Fred