Skip to content

The Proof Theory Blog

⊢ ∃x (D(x) → ∀yD(y))

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

What proof mining is about, Part I

Posted on June 6, 2020July 23, 2022 by Andrei Sipoș

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 \varphi in the language of first-order arithmetic (more generally, a primitive-recursively decidable formula), having x and y as its only free variables, and assume that the sentence

    \[\forall x \exists y\varphi\]

is true. This raises the question: is there a computable realizer for the sentence above, i.e. a program that outputs for any given x a corresponding y? Well, of course there is, just run through all the natural numbers and return the first one for which \varphi is satisfied — and by the truth of the sentence \forall x \exists y\varphi, 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 \varphi. 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:

    \[\mathsf{PA} \vdash \forall x \exists y\varphi.\]

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 \psi of the language of \mathsf{PA} another formula \psi^D in the language of a higher-typed quantifier-free logical system called System \mathsf{T} (whose details do not concern us for now), together with two tuples of variables \underline{x}_\psi and \underline{y}_\psi such that the sets underlying \underline{x}_\psi and \underline{y}_\psi are disjoint and their union is contained in the set of the free variables of \psi^D.

The usefulness of this mapping is given by the soundness theorem, which states that for any \psi such that \mathsf{PA} \vdash \psi there is a tuple of terms \underline{t} such that \mathsf{T} \vdash \forall \underline{x}_\psi \psi^D(\underline{x}_\psi, \underline{t}\underline{x}_\psi). This is proven, as expected, by structural induction on \mathsf{PA} 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 \psi to be \bot, then \psi^D is also \bot, so if \mathsf{PA} is inconsistent, then by soundness, \mathsf{T} 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 \mathsf{PA} to that of \mathsf{T}, a system which is judged as being more trustworthy, mainly because of its lack of quantifier complexity.

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

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 \psi to be our \forall x \exists y \varphi above, then the definition of the functional interpretation makes \psi^D to be \varphi, \underline{x}_\psi to be just x and \underline{y}_\psi to be just y, so if, as before,

    \[\mathsf{PA} \vdash \forall x \exists y \varphi,\]

then there is a term t (with no free variables) that denotes a function of signature \mathbb{N} \to \mathbb{N} such that

    \[\mathsf{T} \vdash \forall x (\varphi[y:=tx]),\]

so, in particular, t 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, <\varepsilon_0-recursive functions), and by examining the types of recursion that go into the construction of t, one may occasionally reduce this further — in particular, t 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 T is Kleene’s T predicate, i.e. for any m, n, p \in \mathbb{N}, T(m,n,p) is true iff the Turing machine with code m on input n terminates with run p, then if we consider the sentence

    \[\forall x \exists y \forall z (T(x,x,z) \to T(x,x,y)),\]

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 t that would give, as before, y in terms of x, since that would allow us to solve the special halting problem, simply by checking for any input n whether T(n,n,tn) 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 \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, who later extended this latter system even higher to System \mathsf{F}_\omega, 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.

6 thoughts on “What proof mining is about, Part I”

  1. Sam Sanders says:
    June 8, 2020 at 11:06 am

    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…

    Reply
  2. mario says:
    June 9, 2020 at 5:41 pm

    “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.

    Reply
    1. Andrei Sipoș says:
      June 9, 2020 at 5:54 pm

      This is some work in that direction: https://arxiv.org/abs/1804.00731

      Reply
      1. mario says:
        June 10, 2020 at 10:32 am

        Thanks, m.

        Reply
  3. Pingback: What proof mining is about, Part II: Structures and metatheorems - The Proof Theory Blog
  4. Pingback: What proof mining is about, Part III: The Heroic Age of Unwinding Proofs - The Proof Theory Blog

Leave a Reply Cancel reply

Your email address will not be published. Required fields are marked *

Meta

  • Register
  • Log in
  • Entries RSS
  • Privacy Policy

Search

© 2023 The Proof Theory Blog | Powered by Minimalist Blog WordPress Theme
The Proof Theory Blog uses cookies, but you can opt-out if you wish. For further information see our privacy policy. Cookie settingsAccept
Privacy & Cookies Policy

Privacy Overview

This website uses cookies to improve your experience while you navigate through the website. Out of these cookies, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may have an effect on your browsing experience.
Necessary
Always Enabled
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Non-necessary
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.
SAVE & ACCEPT