FOM: my non-constructive proof

[Fred Richman]

Martin Davis wrote:
 
> Fred Richman wrote:

>> Would your story have had the same point if the constructive content
>> of your proof would have yielded a single Diophantine relation, but
>> it was too tedious to unwrap that content?
 
> No.

This situation is similar to the classic example of the existence of
two irrational numbers, x and y, such that x^y (exponentiation) is
rational. Let a = sqrt 2 and consider the two candidates a^a and
(a^a)^a = 2. If a^a is rational, the first candidate does it; if not,
the second does it. This is not a constructive proof even though the
construction is staring us in the face.

Would a constructivist take this as evidence that the theorem is true?
Of course. At the very least, it is a case where the conclusion holds
under stronger hypotheses (the law of excluded middle).

> > >> [F.R. again] Let P be a proposition (like "there is an odd
> > >> perfect number") and let's look for an integer n such that n = 1 
> > >> if P is true and n = 0 if P is false. Are you asking whether 
> > >> anyone should have the least doubt about the existence of such an 
> > >> integer?

> OK. If pressed I will say that yes, that is a definite integer, but we
> don't know whether its value is 0 or 1. But it seems silly. 1 just 
> stands for "true" and 0 for "false".

Yes, it does seem silly. And I suppose the point of contention is how
to resolve that silliness. An intuitionist might take the point of
view that a definite integer has not been specified, while you might,
justifiably, choose to ignore the question about what we know.

Personally, I am a little uneasy talking about "definite integers",
determinate properties, and what we know. Constructivists don't think
in terms of "definite integers" any more than anyone else does. That
is the kind of term introduced in an attempt to put constructivism in
a classical framework. For a constructivist, you have simply not
specified an integer in the situation above. Even from a classical
point of view, to specify an integer, you have to do more than just
give a predicate P(n). You also have to prove that there exists an
integer satisfying P(n) (and only one).

 
> So our disagreement comes down to terminology. I would say that I had
> proved the existence of a Diophantine relation with a non-Diophantine
> negation where a constructivist would say I had only proved the
> impossibility of every Diophantine relation having a Diophantine
> negation.

I think that's right. Just like in the sqrt 2 example above, where the
classical proof shows that it is impossible that x^y is always
irrational when x and y are irrational. But I would hesitate to
dismiss this as a terminological disagreement. If you prove "not not
A" and say that you have proved "A", you have rejected the whole
constructivist program. Whether this program is good or bad, I don't
think it is simply a question of terminology.

> Now remember the mathematical context: I wanted to know whether every
> r.e. relation is Diophantine. My belief that this might be true was
> strengthened by seeing that the two classes (Diophantine and r.e.
> relations) had the same closure properties: they were closed under
> "and, or, exists" but not under "not". If I had been converted to
> constructivism, would the evidence for my conjecture have been
> as compelling?

I would think that the actual context was that you wanted to *prove*
that every r.e. relation is Diophantine. If you were a constructivist,
you would have wanted to prove it constructively. If you could
construct an r.e. relation whose complement was not r.e., but you
could not construct a Diophantine relation whose complement was not
Diophantine, that wouldn't be a good sign. So the evidence provided by
the classical proof would not have been as compelling, although it
might very well have sufficed to keep you going.

--Fred