New research on coding in reverse mathematics?

Question

Coding is obviously a fundamental tool in reverse mathematics, and practitioners take care to both demonstrate the correctness of their coding mechanisms and point out their limitations. Harvey Friedman posted on the FOM mailing list in 2004 (see [1] and [2]), prefacing the mathematical part of his first posting with the following.

For a wide variety of mathematical statements, the "correctness" or "appropriateness" of the coding used is completely unpoblematic, and goes virtually unnoticed. Part of the reason why it goes virtually unnoticed is that such coding mechanisms - in such unproblematic cases - are essentially the same as those that occur in virtually all aspects of recursion theory, in proof theory, and at least the finite part of set theory.

For other mathematical statements, the "correctness" or "appropriateness" of certain coding mechanisms is, in varying degrees, controversial. The main reason for this controversy is the presence of alternatives that seem equally reasonable, but are "substantially different".

The judging of the "correctness" or "appropriateness" of coding mechanisms has largely been of an informal, even sometimes polemical, nature. Here we wish to present some formal criteria that should go far in clarifying the issues, and open up new research programs.

I'm curious to know whether such new research programmes have indeed opened up, or whether there has been any further work in this area at all. I couldn't find anything by Googling "Coding in Reverse Mathematics" except an abstract for a talk by Friedman in October 2004.

[1] Friedman, H. Coding in Reverse Mathematics 1. FOM mailing list, 2004.

[2] Friedman, H. Coding in Reverse Mathematics 2. FOM mailing list, 2004.

Answer 1

I can offer a computational perspective. In computable mathematics we are interested in "computing with mathematical objects" such as integers, finite sets, real numbers, infinite-dimensional Banach spaces, compact subsets of $\mathbb{R}^n$, and many other "infinite" things. Some of these are pretty complicated, so the question arises how to represent them as a data structures, in other words, we face a coding problem, just like in Reverse Mathematics.

In computability theory we normally code everything with natural numbers. Another possibility is to code things with "reals", by which computability theorists mean infinite binary sequences. In actual implementations we code by elements of datatypes available to us in a programming language. But we always face the same question, namely what does it mean to correctly encode a given mathematical object.

To properly answer such a question we have to take a very important step: we must turn encodings themselves into honest mathematical objects and collect them all (even the allegedly senseless ones) into a manageable mathematical structure, say a category. We should be able to use the structure of the resulting category to bring some order and sense to the black art of "choosing appropriate codings".

When this is done in computable mathematics, the result is a realizability topos. This is great, as we can interpret higher-order (intuitionistic) logic in it, and that suffices to develop mathematics. To see how this works, consider an easy example, the natural numbers. Nobody ever questions encodings of natural numbers, but nevertheless it is possible to come up with some bad ones. Encodings are objects of a realizability topos. Thus, a candidate encoding for natural numbers lives inside the topos as an object $N$. If in the topos the object $N$ satisfies Peano axioms, then it correctly encodes natural numbers, otherwise it does not.

Our correctness criterion then is this: an encoding is correct when, seen as an object of the realizability topos, it corresponds to the expected mathematical object. Other examples are easy to come by:

• An encoding of real numbers is correct if the corresponding object in the topos is a Cauchy-complete Archimedean ordered field.
• An encoding of c.e. sets is correct if in the corresponding object in the topos is the object of countable subsets of $\mathbb{N}$.
• An encoding of functions $X \to Y$ is correct if in the topos it is the exponential object of $X$ and $Y$.
• An encoding of a group is correct if in the topos it corresponds to a group.
• etc.

As toposes and intuitionistic mathematics are often unfamiliar to mathematicians, and reverse mathematics happens in the context of classical logic anyway, realizability toposes are not going to be the right answer for Reverse Mathematics. Nevertheless, we have a plan: what category, or (non-standard) model of (weak) set-theory captures the idea of coding in Recursive Mathematics? If you can find it, and it has good enough properties, it should give some answers. This sounds like somebody's PhD.

Answer 2

Together with previous research by Ulrich Kohlenbach ([1]), a recent paper by Dag Normann and myself ([2]) provides the following pretty sharp answer.

In a nutshell, coding continuous functions in L$_2$, the language of second-order arithmetic, does not change the RM of WKL$_0$, one of the Big Five systems. By contrast, coding Riemann integrable functions (=continuous almost everywhere and bounded) dramatically changes the logical strength of basic theorems, like Arzela's convergence theorem for the Riemann integral from 1885.

In more detail, Kohlenbach shows in [1] that in RCA$_0^\omega +$ WKL, for any third-order $Y:\mathbb{N}^\mathbb{N}\rightarrow \mathbb{N}$ that is continuous on $2^\mathbb{N}$ (via the usual epsilon-delta definition), there is an RM-code $\alpha$ such that $(\forall f \in 2^{\mathbb{N}})(Y(f)=\alpha(f)$. This is based on a construction by Dag Normann and readily generalised to e.g. $[0,1]$.

In this way, as long as WKL is available, it does not matter whether one formulates a given theorem about continuous functions with or without codes.

Now consider Arzela's 1885 convergence theorem for the Riemann (see [0]):

Let $f$ and $(f_{n})_{n\in \mathbb{N}}$ be Riemann integrable on the unit interval and such that $\lim_{n\rightarrow \infty}f_{n}(x)=f(x)$ for all $x\in [0,1]$. If there is $M\in \mathbb{N}$ such that $|f_{n}(x)|\leq M+1$ for all $n\in \mathbb{N}$ and $x\in [0,1]$, then $\lim_{n\rightarrow \infty}\int_{0}^{1}f_{n}(x)dx=\int_{0}^{1}f(x)dx$.

With codes, this theorem is provable in WKL or weaker. Without codes, this theorem can be formulated in third-order arithmetic, but is not provable from third-order comprehension Z$_2^\omega$, which implies full second-order arithmetic Z$_2$. The stronger fourth order system Z$_2^\Omega$ does prove the above convergence theorem.

Here, Z$_2^\omega$ is Kohlenbach's RCA$_0^\omega$ extended with third-order functionals $S_k^2$ that decide $\Pi_k^1$-formulas (the latter formulated in $L_2$). Such functionals $S_k^2$ are highly similar to the functionals $\nu_k$ in [0b, p. 129]. Moreover, Z$_2^\Omega$ is RCA$_0^\omega$ plus Kleene's (fourth order) $\exists^3$. Note that Z$_2^\omega$ and Z$_2^\Omega$ are conservative extensions of Z$_2$.

In this light, the minimal comprehension axioms required to prove Arzela's convergence theorem for the Riemann integral are massively different depending on whether one uses codes. Moreover, we only need to go 'continuous almost everywhere/Riemann integration' for coding to break down: no need to drag in topology or other abstract stuff.

I note that term-by-term integration, which is similar to the above convergence theorem, can already be found in the work of e.g. Dini (1870).

References

[0] Cesaro Arzela, Sulla integrazione per serie, Atti Acc. Lincei Rend., Rome 1 (1885), 532–537

[0b] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg, Iterated inductive definitions and subsystems of analysis, LNM 897, Springer, 1981.

[1] Ulrich Kohlenbach, Foundational and mathematical uses of higher types, Reflections on the foundations of mathematics, Lect. Notes Log., vol. 15, ASL, 2002, pp. 92–116.

[2] Dag Normann and Sam Sanders, On the uncountability of $\mathbb{R}$, arxiv: https://arxiv.org/abs/2007.07560

Answer 3

Here is another place where coding becomes problematic: countable sets, the proverbial bread and butter of second-order RM. To see this, consider the following statement:

a countable RM-closed set $A\subset \mathbb{R}$ has finite measure. (1)

We do not need the Lebesgue measure to formulate (1), as is clear from the development of Lesbegue integration in RM.

The definition of "countable" in second-order RM is given in Simpson's SOSOA, Def. V.4.2. With this definition, (1) is provable in RCA$_0$, as one proves that $A$ has measure zero.

Now, "countable" is defined in Kunen's set theory textbook as "injection to $\mathbb{N}$''. In other words, `$A\subset \mathbb{R}$ is countable' is defined as follows:

$(\exists Y:[0,1]\rightarrow \mathbb{N})(\forall x, y\in A)(Y(x)=Y(y) \rightarrow x=_\mathbb{R}y)$

With this definition of countable set, (1) can be formulated in third-order arithmetic, but is not provable from third-order comprehension Z$_2^\omega$, which implies full second-order arithmetic Z$_2$. The former system is mentioned in my previous answer.

These results may be found in [2] of my previous answer.