[FOM] re re re Harvey on "a very exciting claim."

[Harvey Friedman]

On 3/28/06 12:58 PM, "Gabriel Stolzenberg" <gstolzen at math.bu.edu> wrote:

>> So Corollary 7 can be proved constructively (under normal accounts), but
>> any proof must be grotesque - in that it must use at least 2^[1000]
>> symbols.
> 
>  What I first would like to know about is your proof that it can
> be proved constructively.  Your "So" suggests that you believe you
> have explained this already.  But, if you did, I didn't follow it.
> Could you please go over this crucial point again?

The proof that it can be proved constructively is NOT claimed to be
constructive. It turns out that the proof that it can be proved
constructively is a

(non grotesque) classical proof.

HOWEVER, your posting
http://www.cs.nyu.edu/pipermail/fom/2006-March/010270.html

at least OPENS the door for a claim by you that the statement in question
ACUTLALY HAS a non grotesque constructive proof.

If a SUFFICIENTLY liberal interpretation of "constructive" is indeed
maintained, then, as I indicated in my posting
http://www.cs.nyu.edu/pipermail/fom/2006-March/010268.html I can strengthen
the examples in various ways. How much of the wild impredicativity present
in ZF is deemed constructive will become the issue.

>  E.g., if Bishop claims to construct of a rational number with
> a certain property, we don't expect to see something of the form,
> m/n, in his proof.

Absolutely correct. If one gives a perfectly ordinary constructive proof
that there exists a rational number with a specific property, then even if
the rational number have completely grotesque numerators and denominators,
this will NOT be an example of the phenomenon I am illustrating.

> We assume that all he has done is to define
> (perhaps only implicitly) a program that if executed will yield
> such an m/n.  But the printout of the computation, if thought of
> as a proof, will almost surely be grotesque.

Any grotesque nature of associated computations is completely IRRELEVANT to
the issue of whether the existence proof is constructive, or is grotesquely
constructive, or is non grotesquely constructive. (However, there are some
metatheorems that, under certain circumstances, tell us a relationship of
certain kinds between the two. This is a mathematical discovery, not a
conceptual relationship).

On 3/28/06 5:18 PM, "Gabriel Stolzenberg" <gstolzen at math.bu.edu> wrote:
> 
>>   Examples where the known proof is nonconstructive, and where one
>> can give a constructive proof, but all known constructive proofs are
>> grotesque (e.g., extremely long, or extremely unpleasant, etc.).
> 
>  I don't understand.  Suppose a muddlehead makes a constructive
> proof that reflects his muddleheadedness.  (Or three muddleheads
> make three such proofs.)  What does this tell you?

Absolutely nothing.

But I was looking for examples like this where

1. With new insights, the proof can be made constructive, but people had no
idea how to do this previously; or

2. With new insights, we can prove that all proofs are grotesque, showing
that people couldn't do better.

Here is an example in an entirely different arena, nothing to do with
constructivity, where I know from personal experience that generally
mathematicians will all gravitate to a rather set theoretically exotic
proof:

THEOREM. Every countable algebraic system with a non finitely generated
subsystem, has a non finitely generated subsystem which is maximal among its
non finitely generated subsystems.

In fact, I showed that this is provably equivalent, over RCA0, to Pi11-CA0.
No axiom of choice at all, and relatively tame impredicativity. See

H. Friedman, Maximal nonfinitely generated subalgebras, in: Reverse
Mathematics, ed. S. Simpson, Lecture Notes in Logic, vol. 21, ASL, 189-200,
2005. 

As far as I can tell, there are many many Theorems very similar to this, and
mathematicians generally gravitate to the obvious proof that is conducted in
something like third order arithmetic with serious axiom of choice on top of
it.  

>>  Examples where the known proof is nonconstructive, and where one
>> can give a constructive proof, but it is known that all constructive
>> proofs are grotesque (e.g., extremely long, or extremely unpleasant,
>> etc.).
> 
>   What counts as a proof here?  Does everything have to be spelled
> out from first principles?  Or are you concerned only with a "normal"
> proof (one with things like "By lemma 2.7") that is long or grotesque?

What counts as grotesque is deliberately left open ended. BUT, for my
examples, it doesn't make any difference what grotesque means. The only
thing you need to know about grotesque is that a proof is grotesque if it
has more than 2^[1000] symbols.

It doesn't make any difference if you require that you go back to absolutely
first principals, or whether you allow this or that abbreviation power,
etcetera. With a number that big, even if you allow all kinds of standard
stuff, you aren't going to get anywhere near reducting it to 2^[999]
symbols.
 
>  More important, according to what you say above, for a case of
> this kind, you actually have a constructive proof that is extremely
> long or extremely unpleasant.  But if it's extremely long, how did
> you manage to make it?  It must have taken forever.  Also, how can
> you be confident that it is correct?  Who is going to check this
> monster?  Please explain.

I do NOT claim to have a constructive proof that there is a constructive
proof. I do claim to have a constructive proof that every constructive proof
is grotesquely long.

Again, see my remarks above about your posting
http://www.cs.nyu.edu/pipermail/fom/2006-March/010270.html
> 
>> Apparently there are quite a number of famous AEA theorems of
>> mathematics which people would like to prove constructively, but
>> can't.  Nobody knows if they can be proved constructively.
> 
>  Also, who are these people, what are some of these classical
> theorems and why do these folks want constructive proofs?  Is it
> just a game?  A challenge?

Here are just two famous examples. I saw a book listing more examples, and I
know that there are some FOM subscribers reading this who can help us with
mentioning more of them.

1. Roth's theorem about approximability of irrational algebraic real numbers
by rationals. Let x be any irrational real algebraic number, and let k > 2.
There exists c > 0 such that for all rationals p/q, q > 0, we have |x - p/q|
> c/(q^k). According to
http://www.ithaca.edu/osman/Courses/190Fa02/hw/history/Rot/Klaus%20Friedrich
%20Rot%5B1%5D.htm  Roth was awarded the Fields Medal for his proof of this
theorem. No constructive proof is known. No effective bounds are known. I
know that most leading number theorists are very much interested in
rectifying this situation.

2. Falting's theorem affirming Mordell's conjecture. There are finitely many
rational solutions for the polynomial expression p(x,y) = 0 when the genus
of p is at least 2. Faltings was awarded the Fields Medal for his proof of
this theorem. No constructive proof is known. No effective bounds are known.
I know that most leading number theorists are very much interested in
rectifying this situation.

Harvey Friedman