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




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.
Thanks for the interesting post; looking forward to the rest of the series!
Serendipitously, one of the three existent papers by W. Friedrich (whom you mention) has some higher-order Reverse Mathematics in it. Unfortunately, it is written in German…
“we obtain programs in System \mathsf{T} as above but supplemented with the bar-recursive functionals of Spector, or, equivalently, programs in the language of System \mathsf{F}, due to Girard”
Has somebody worked out the details of direct proofs that the the former ones are definable as the latter ones, and viceversa? Thanks.
This is some work in that direction: https://arxiv.org/abs/1804.00731
Thanks, m.