FOM: my non-constructive proof

[Fred Richman]

Martin Davis wrote:
 
>>> The constructive content of my proof if
>>> I cared to pay attention, would yield a pair of Diophantine
>>> relations at least one of which does not have a Diopahntine
>>> complement. For an actual example, I had to wait twenty years.

>> [Fred Richman's response] Why don't you believe that your proof
>> furnishes an "actual example"?
 
> Should I have said a specific example? My proof showed that there is a
> Diophantine relation whose negation is not Diophantine. But I was
> unable to furnish an example of such.

You said the constructive content of your proof would yield a pair of
Diophantine relations. I assumed that meant you could have produced
two specific relations if you wanted to. 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?

>> [F.R. again] I'd like to clarify this situation by possibly
>> simplifying it a bit. 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?
 
> I don't agree that this is a simplification. I introduced my example
> into the discussion precisely to avoid this kind of artificiality. My
> example came up in my research, and my challenge remains: should I
> have entertained the least doubt about the correctness of my
> conclusion even though the means for obtaining it was (and remained
> for 20 years, non-constructive?

It seems simpler to me: I don't have to know anything about
Diophantine relations, just perfect numbers. But whether or not it is
simpler, and whether or not it is unnatural, it would be interesting
to me to know your take on this example. Then I might understand what
the nature of your challenge is. There are lots of reasons why
mathematicians are sure that certain conclusions are correct, and most
of these reasons have nothing to do with constructivity.

Your result showed that it was impossible for the negation of every
Diophantine relation to be Diophantine. So nobody was going to be able
to disprove your conclusion. Are you asking constructivists whether
that is enough to establish your conclusion in their eyes? They would
say no. Are you asking whether they would doubt the conclusion? That
question is not so clear cut given the subjective nature of what makes
us sure things are true. Certainly they can't form an opinion as to
whether *you* should have doubted it.

> My "challenge" has to do with whether a constructivist would really
> doubt or deny the truth of my conclusion.

Constructivists are constantly being badgered to choose between A and
not A. Inasmuch as a constructists would feel that your proof does not
establish your conclusion, he would doubt your conclusion. He
certainly wouldn't *deny* your conclusion any more than he would deny
"A or not A". After all, "not not (A or not A)" is a theorem in
intuitionistic propositional calculus.

--Fred