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₀ there is an m₀ such that for all n₁ there is an m₁ such that … for all n_r there is an m_r such that P(n₀, m₀, …, n_r, m_r)” is true then there are witnessing functions f₀(n₀), …, f_r(n₀, …, n_r) such that for all n₀, …, n_r, P(n₀, f₀(n₀), …, n_r, f_r(n₀, …, 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 eth 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₀ there is an m₀ such that for all n₁ there is an m₁ such that … for all n_r there is an m_r such that P(n₀, m₀, …, 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₀, …, f_r each taking r arguments, the ith of which is a function from to satisfying the following: For any functions g₀, …, g_r such that g_i is from to ,

P(g₀, f₀(g₀, …, g_r), g₁(f₀(g₀, …, g_r)), f₁(g₀, …, g_r), …, g_r(f₀(g₀, …, g_r), …,f_{r – 1}(g₀, …, g_r)),f_r(g₀, …, 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 eth 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).