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

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.

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

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

Leave a Reply Cancel reply