Skip to content

The Proof Theory Blog

α < β ⇒ φα(φβγ) = φβγ

Menu
  • Home
  • About
  • Contribute
  • Resources
Menu

What proof mining is about, Part II: Structures and metatheorems

Posted on June 14, 2020July 3, 2020 by Andrei Sipoș

As I said last time, it is time to raise the stakes and start dealing with sentences involving structures, which at first will be the structures of first-order logic. Let, then, \sigma be a first-order signature and \{\varphi_{n,m}\}_{n,m\in\mathbb{N}} be a family of \sigma-sentences. For the purposes of this post, we shall say, for any \sigma-structure M, that M \models \forall x \exists y \varphi_{x,y} if for all n \in \mathbb{N} there is an m \in \mathbb{N} such that M \models \varphi_{n,m}.

Let now \mathcal{K} be a class of \sigma-structures and assume that \mathcal{K} \models \forall x \exists y \varphi_{x,y}. We may now ask the same question as last time: can we find a computable realizer of y in terms of x? First, I want you to see that the way the assumption is written is a bit eye-deceiving, since it only means that for every M \in \mathcal{K} and every n \in \mathbb{N}, there is an m \in \mathbb{N} such that M \models \varphi_{n,m}, whereas a realizer, be it computable or not, would mean something stronger, more uniform, namely that for every n \in \mathbb{N} there is an m \in \mathbb{N} such that for every M \in \mathcal{K}, M \models \varphi_{n,m}.

The way out of this dilemma is to require only a uniform bound on y in terms of the x (this will be a recurring motif from now on), and we will now show that if the class \mathcal{K} is in addition axiomatizable, then our apparently weak assumption is enough to guarantee that.

Let, then, \Gamma be an axiomatization for \mathcal{K}, and fix an n \in \mathbb{N}. We know that for every M \in \mathcal{K}, there is an m \in \mathbb{N} such that M \models \varphi_{n,m}. In other words, we have that the set \Gamma \cup \{\neg\varphi_{n,m} \mid m \in \mathbb{N}\} is inconsistent. By compactness, there is a k\in \mathbb{N} such that \Gamma \cup \{\neg\varphi_{n,m} \mid m \leq k\}, or simply

    \[\Gamma \cup \left\{\neg\bigvee_{m \leq k} \varphi_{n,m}\right\}\]

is inconsistent, so

    \[\Gamma \models \bigvee_{m \leq k} \varphi_{n,m},\]

that is, for any M \in \mathcal{K} there is a m \leq k such that M \models \varphi_{n,m}. Thus k is our desired bound.

The above argument also tells us immediately when and why k is computable — if we assume that \sigma is a decidable signature, the function (n,m) \mapsto \varphi_{n,m} is computable and \Gamma is recursively enumerable, then we may simply enumerate the consequences of \Gamma, and wait until we certify one as being of the form

    \[\bigvee_{m \leq k} \varphi_{n,m},\]

in which case we simply return the k — and it is guaranteed that such a sentence will show up. Note that this is not pure search, as in the number-theoretic case, but a rather metamathematical sort of search.

Of course, if we follow the plan from the previous post, now would be the time to say how proof theory gets involved in this. I could tell you that in terms of what you already know (or could I?), but I prefer to tell you the way it is actually done. To do that, though, I have to patch up a bit what I’ve told you so far.

Firstly, instead of \mathsf{PA}, one typically uses a higher-order system that has the same proof-theoretic strength, that I will denote here as \mathcal{T}^\omega, even though that designation hasn’t been commonly used lately. (Ulrich Kohlenbach later initiated the reverse-mathematical investigation of these systems, which in recent years Sam Sanders, together with Dag Normann, turned into a fully-fledged field of study.) Since the goals of proof mining are orthogonal to consistency, we do not care as much about the target system’s complexity and thus the implicit trust in it, and so one may also replace Gödel’s System \mathsf{T} with the same system \mathcal{T}^\omega. Therefore the soundness result that I have talked about in the previous post now takes the following form (a slightly weaker variant of Theorem 10.8 in Kohlenbach’s book): if we have that

    \[\mathcal{T}^\omega \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} and that one extracts by structural induction over the proof, such that

    \[\mathcal{T}^\omega \vdash \forall x (\varphi[y:=tx]).\]

Secondly, in order to be able to adapt the model-theoretic arguments above as to explain the results of proof mining in nonlinear analysis, one must replace first-order logic by a more powerful one, called positive-bounded logic, which is designed to deal with metric structures like Banach spaces and where a lot of the arguments used to show the nice properties of first-order logic carry through, such as the ones for compactness or Löwenheim–Skolem, or even the famous proof of Shelah, that avoids the use of GCH, of the ultrapower isomorphism theorem (a good reference is these notes; see Chapter 10 for the latter result) — it escapes the Lindström phenomenon essentially by talking about a different kind of structures than first-order logic. That the arguments I presented do indeed make sense for the kind of sentences usually studied in proof mining was first observed by Jeremy Avigad and José Iovino for the uniformity argument in this paper (see also my treatment of their results that avoids any mention of logic) and by Jason Rute for the computability argument in these slides. (All this is not to say that first-order logic is just a toy case, as reasoning of this sort has been featured e.g. in the work of Lou van den Dries and his collaborators, see Section 6 of this paper.)

To sum up, we have on the one hand a foundational theory \mathcal{T}^\omega and on the other a theory \Gamma in a first-order-like language that axiomatizes the class of structures that a mathematical theorem refers to. (The distinction between whether a theory aims to capture a “standard” model or a whole class is something which some philosophers, specifically mathematical structuralists, care about — see e.g. this book of Shapiro, where he calls such theories “non-algebraic” and “algebraic”, respectively, as examples of the latter type tend to show up in basic abstract algebra: group or ring theory.) The question is now how do we put them together. The answer, found by Kohlenbach at the turn of the century, is: by literally putting them together. Specifically, one (i) adjoins to the algebra of types of \mathcal{T}^\omega a new basic type X representing the (metric) structure — forming thus new composite types such as X \to X or \mathbb{N} \to (X \to \mathbb{N}); (ii) adds to the resulting system the axioms of \Gamma in a form that makes sense; and (iii) attempts to extend the proof of the soundness theorem for the functional interpretation. This can be a bit messy, especially when bar recursion (see the last post) gets involved and one has to juggle with multiple models for higher-order functionals. When it works, this yields results which are usually called “general logical metatheorems”, featured in those three papers of Kohlenbach (two of these with his student Gerhardy), and which, above all, as we shall later illustrate, brought more confidence in the kind of problems that proof mining could hope to make a dent in. To close the loop, Kohlenbach later showed with another student of his, Günzel, that this procedure always works when the structures under discussion are axiomatizable in positive-bounded logic.

I reckon this makes up all the basic vocabulary that you need in order to understand the discourse of proof mining. Next time, we’ll talk about how all this theory meets practice (which here also means theory, though of a less logical sort), along with some long-overdue historical overview.

2 thoughts on “What proof mining is about, Part II: Structures and metatheorems”

  1. Pingback: What proof mining is about, Part I - The Proof Theory Blog
  2. 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