For every true number-theoretic statement of the form “For all *n* there is an *m* such that *P*(*n*, *m*)” there is a witnessing function *f* such that for all *n*, *P*(*n, f*(*n*)) is true.

For example, a witnessing function for the statement “For all *n* there is an *m* such that *m > n* and *m* is prime” is any function which takes a number and returns a prime higher than that number, which certainly exists.

In general, if the statement “For all *n*_{0} there is an *m*_{0} such that for all *n*_{1} there is an *m*_{1} such that … for all *n*_{r} there is an *m*_{r} such that *P*(*n*_{0}, *m*_{0}, …, *n*_{r}, *m*_{r})” is true then there are witnessing functions *f*_{0}(*n*_{0}), …, *f*_{r}(*n*_{0}, …, *n*_{r}) such that for all *n*_{0}, …, *n*_{r}, *P*(*n*_{0}, *f*_{0}(*n*_{0}), …, *n*_{r}, *f*_{r}(*n*_{0}, …, *n*_{r})) is true.

Because it’s the case that if a number-theoretic statement is *true*, then its witnessing functions *exist*, we might hope that it woud be the case that if a number-theoretic statement is *provable*, then its witnessing functions are *computable*, that is, that we could extract a computer program for the witnessing functions from the proof.

For example, a computable witnessing function for the statement “For all *n* there is an *m* such that *m > n* and *m* is prime” can be easily extracted from Euclid’s proof that there are infinitely any primes.

Can this always be done? Unfortunately the answer is no, but Georg Kreisel’s No-Counterexample Interpretation gives an elegant piece of computational data that *can* be extracted from any provable number-theoretic statement.

For an example of a provable number-theoretic statement whose witnessing functions are not computable, consider the following: Let Halts(*e*, *s*) be the predicate which asserts that the *e*th Turing machine halts in *s* steps. (Note that Halts(e,s) is decidable—even primitive recursive.)

Clearly every Turing machine either halts or it doesn’t. It follows that “For all *e* there is an *s* such that for all *r*, (Halts(e,s) or ~Halts(e,r))” is provable (without any number-theoretic axioms even!) However, there can be no computable witnessing function *f*(*e*) for *s, *since if there were, we could solve the Halting problem: any e halts iff it halts in *f*(*e*) steps, which we can check computably.

Meditating on this example a bit may lead you to believe that there is no hope of extracting any computable information from this proof, which is one of the reasons why I think the no-counterexample interpretation is neat. It essentially says that although there may not be a sequence of computable witnessing functions for a provable statement, we may computably *simulate* a sequence of witnessing functions to someone who will only use them *once*, and who tells us in advance how he plans to use them.

Formally: Suppose that a statement of the form “For all *n*_{0} there is an *m*_{0} such that for all *n*_{1} there is an *m*_{1} such that … for all *n*_{r} there is an *m*_{r} such that *P*(*n*_{0}, *m*_{0}, …, *n*_{r}, *m*_{r})” is provable in Peano Arithmetic (a first-order formal system for proving number-theoretic statements) where *P* is quantifier-free and involves only primitive recursive predicates and function symbols.

Then there are computable *functionals* *f*_{0}, …, *f*_{r} each taking *r* arguments, the *i*th of which is a function from to satisfying the following: For any functions *g*_{0}, …, *g*_{r} such that *g*_{i} is from to ,

*P*(*g*_{0}, *f*_{0}(*g*_{0}, …, *g*_{r}), *g*_{1}(*f*_{0}(*g*_{0}, …, *g*_{r})), *f*_{1}(*g*_{0}, …, *g*_{r}), …,* g*_{r}(*f*_{0}(*g*_{0}, …, *g*_{r}), …,*f*_{r – 1}(*g*_{0}, …, *g*_{r})),*f*_{r}(*g*_{0}, …, *g*_{r}))

is true.

Here the functions *g*_{i} represent the way in which the witnessing functions were to be used, and the content of the claim is that we can write computer programs which, given these functions in advance can simulate the witnessing functions to the “satisfaction” of the functions *g*_{i}.

Let’s see how this works in our example above: Our statement is “For all *e* there is an *s* such that for all *r*, either Halts(*e*,*s*) or ~Halts(*e*,*r*).” We can’t write a program which determines if the *e*th Turing machine halts or not, but suppose we know that given *e* and *s*, our customer will only check that “Halts(*e*,*s*) or ~Halts(*e*,*r*)” is true for some specific *r = r*(*e*, *s*). Then we can satisfy him or her as follows: given *e*, check if Halts(*e*, *r*(*e*, 0)) holds. If so, return *s* = *r*(*e*, 0)), and the customer will be satisfied since Halts(*e*, *s*) will hold. If not, return, *s* = 0 and the customer will be satisfied since Halts(*e*, *r*) will not hold.

For more information, check out Jeremy Avigad and Solomon Feferman’s excellent article on Gödel’s functional interpretation in the Handbook of Proof Theory (also available here online).

I always liked the game-theoretic interpretation of Kreisel’s No-Counterexample Interpretation (and its big brother, Gödel’s Dialectica). This is related to the Fraïssé’s Theorem.

described in my post onThe witnessing functions form (the main part of) a winning strategy for True in the semantics game. While True’s winning strategy in that game is not computable in general, Kreisel’s No-Counterexample Interpretation says that there is a computable functional that witnesses that False does not have winning strategy in the semantics game associated to a true statement. Consequently, the existence of witnessing functions is equivalent to some form of determinacy (which depends on the base axioms).