[FOM] What is a "non-constructive proof"?

[Timothy Y. Chow]

On Wed, 19 Feb 2020, Joe Shipman wrote:
> My 2nd category guarantees a solution but with no bound, and my 1st 
> category (worse still) guarantees finitely many (possibly 0) solutions 
> with no way of knowing when to stop searching.

This isn't a perfect example, but how about Levin universal search?  We 
can explicitly write down an algorithm A with the following property:

   (*)  If P = NP then A solves SAT in polynomial time.

There is no bound on the degree of the polynomial.  But in some sense we 
are "guaranteed a solution."  Of course the big catch is that we don't 
know that P = NP.

Tim