[FOM] What is a "non-constructive proof"?
Timothy Y. Chow
tchow at math.princeton.edu
Wed Feb 19 12:00:25 EST 2020
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.
More information about the FOM