What proof mining is about, Part I

This is the first post in a series designed to introduce a working logician to the field of proof mining (for when you’ll want to know more than this hopefully gentle introduction will provide, the standard reference is the monograph of Kohlenbach). It will mainly focus on its motivations and logico-mathematical content, with historical information (at least in the beginning) more or less fading into the background.

Consider a quantifier-free formula in the language of first-order arithmetic (more generally, a primitive-recursively decidable formula), having and as its only free variables, and assume that the sentence

   

is true. This raises the question: is there a computable realizer for the sentence above, i.e. a program that outputs for any given a corresponding ? Well, of course there is, just run through all the natural numbers and return the first one for which is satisfied — and by the truth of the sentence , this program always terminates.

Somehow, this answer is not quite satisfying, mainly because all such programs look the same! We get absolutely no clue of the computational complexity or of any other issue germane to . On the other hand, why should one expect anything more since I didn’t say anything about the sentence? Excepting, of course, the fact that it is true.

How would one know in the first place that it is true? Well, usually it’s by being in possession of a proof, so suppose that we have such a proof in, say, first-order arithmetic:

   

This is where proof theory starts to come into play, specifically the tool known as the functional interpretation (also known as the Dialectica interpretation, after the journal it was first published in), devised by Gödel. This interpretation (what I’m sketching here is in fact known as the Shoenfield variant) is a mapping that associates to each formula of the language of another formula in the language of a higher-typed quantifier-free logical system called System (whose details do not concern us for now), together with two tuples of variables and such that the sets underlying and are disjoint and their union is contained in the set of the free variables of .

The usefulness of this mapping is given by the soundness theorem, which states that for any such that there is a tuple of terms such that . This is proven, as expected, by structural induction on proofs.

The original purpose of this apparently complicated mise en scène was proving the consistency of arithmetic (a theme which Anton touched upon recently), namely in the following manner. If we take to be , then is also , so if is inconsistent, then by soundness, is also inconsistent. Moreover, soundness may be proven in a primitive-recursive metatheory, so what we have here is a finitary reduction of the consistency of to that of , a system which is judged as being more trustworthy, mainly because of its lack of quantifier complexity.

In addition, the consistency of (in effect, the strong normalization of its underlying rewriting system) may be shown, as per Howard, by primitive-recursive induction along the ordinal , so the above strategy could be considered to be a refinement of the usual Gentzen-style proof of the consistency of .

It was Georg Kreisel’s idea to use these proof-theoretical tools (not only the functional interpretation, but also cut elimination, the epsilon calculus, and others) not just to obtain an (in his view) illusory feeling of trust by means of this kind of consistency proofs, but also to extract additional mathematical information out of concrete proofs — in other words, to answer what he later called the “recurring question”:

“What more do we know when we know that a theorem can be proved by limited means than if we merely know that it is true?”

Going back to where we started, if we take to be our above, then the definition of the functional interpretation makes to be , to be just and to be just , so if, as before,

   

then there is a term (with no free variables) that denotes a function of signature such that

   

so, in particular, is our desired program. (This particular instance of soundness is sometimes visible in this blog’s tagline.) We thus now know (to the extent that it is possible to “know”) its computational complexity, since it falls into the class of primitive-recursive functionals (or, equivalently, -recursive functions), and by examining the types of recursion that go into the construction of , one may occasionally reduce this further — in particular, may denote a primitive-recursive function.

Can we go higher — in terms of quantifier complexity? Not really, or at least (as we shall see later) not without severely downsizing our expectations. For if is Kleene’s T predicate, i.e. for any , , , is true iff the Turing machine with code on input terminates with run , then if we consider the sentence

   

which is true by pure first-order logic (it is basically a form of the drinker paradox — also in the tagline), we cannot hope to obtain a computable that would give, as before, in terms of , since that would allow us to solve the special halting problem, simply by checking for any input whether holds.

We can, though, go higher in another sense — higher on what is usually called the Gödel hierarchy of foundational theories. If we replace Peano arithmetic with the first-order, two-sorted theory commonly known as “second-order arithmetic”, we obtain programs in System as above but supplemented with the bar-recursive functionals of Spector, or, equivalently, programs in the language of System , due to Girard, who later extended this latter system even higher to System , which interprets simple type theory. In between them (as I was told), we also have a system of higher bar-recursive functionals due to Friedrich. What about the powerful foundation that almost all mathematicians, knowingly or not, are using nowadays: Zermelo-Fraenkel set theory with the axiom of choice? Well, proof mining techniques are not yet sufficiently advanced to deal with that: it is, as I like to say, proof mining for the twenty-fourth century.

So this is roughly all there is to it (exaggerating a little, of course) when all we have is numbers and arithmetic sentences. Next time, we’ll look at what happens when structures come into play.