Extracting an existential witness

Stream: IMO-grand-challenge

[Vlad Firoiu]

One of the issues with problems such as "Find the smallest integer N such that p(N)" is that the translation to an existential is too weak; a proof of the existential, even in a constructive logic, might require far too much time to normalize. We want the theorem prover to actually write down the bits that specify the integer, but there is no way to distinguish it from a brute-force program that is proven to terminate and give the right output.

Here is a slightly unorthodox solution to the problem; unorthodox because it requires interacting with the theorem prover multiple times. First, let's assume that the solution is known to be encodable in K bits. That is, we want to witness a K-bit integer N that satisfies p(N). We begin by querying (perhaps in parallel) the prover with two different propositions: that there exists a K-bit N s.t. p(N) with first bit 0, and the same but with first bit 1. If one of the queries is successful (say the 0-case), we query (twice) again about the second bit, fixing the first bit to be 0. This continues until we've produced all of the bits for the existential.

Lifting the restriction on K is a bit trickier. In principle there is a reasonable maximum M beyond which even writing M arbitrary bits would go beyond the time limit. We could use a similar querying strategy to binary search for the minimal K in the range [0, M].