FOM: nonconstructive existence proofs of algorithms

[Stephen G Simpson]

William Tait Tue, 11 Jul 2000 09:58:52 -0500 asks:

 > Is it impossible that, for example, there could be a classical but no 
 > constructive proof of an existence statement yielding an algorithm?

This question makes me think of certain nonconstructive extence proofs
of algorithms in graph theory.

For example, it is known that for each n there exists a finite set S_n
of finite graphs, such that a given finite graph G is of genus greater
than n if and only if G contains a minor isomorphic to one of the
graphs in S_n.  The proof of the existence of S_n is apparently
nonconstructive and rather difficult.  The existence of S_n is a
special case of the Robertson/Seymour Graph Minor Theorem.  No bounds
on the size of S_n are known, even for small values of n.

By other work of Robertson and Seymour, if we knew S_n explicitly, we
could explicitly write down a PTIME algorithm for deciding whether a
given finite graph is of genus greater than n.

Thus we have a nonconstructive proof that for each n there exists a
PTIME algorithm for deciding whether a given finite graph is of genus
greater than n.  We do not have the algorithms themselves.

-- Steve