Short Summary
Studying mathematics via logic implies one needs to choose a suitable logical language and represent part of mathematics therein. For instance, since everything is a set in set theory, one represents the natural numbers via the von Neumann ordinals: 0 corresponds to and
corresponds to the set
.
An obvious question raised by this practise is whether a given representation remains true to the original. The aim of this post is to show that for a rather common representation practise, namely coding objects in the language of second-order arithmetic, the answer is negative. In particular, we show that even representations of continuous functions change the logical strength of theorems with Big Names, like Weierstrass, Heine, and Tietze, attached to it.
Disclaimer: the below results may be found in full gruesome detail in [Sa19]; the interested reader should consult this paper before making grand (counter-)claims.
Representations/codes of continuous functions
Before providing the technical definition, I first provide an intuitive motivation for the coding/representation of continuous functions.
Now, the reader will be familiar with continuity, say on the unit interval as in the usual ‘epsilon-delta’ definition as follows:
.
A modulus of (pointwise) continuity is any function that outputs the above
in terms of the other data, i.e.
.
A moment of thought shows that can be taken to be continuous in the
variable.
While clearly dealing with uncountable things, a continuous function with a continuous modulus only contains countably much information as follows:
Since is continuous in the
-variable, the following union covers the union interval:
. By compactness, there is a finite sequence
such that
also covers
. By definition, the finite sequence
contains enough points to approximate
up to error
as follows:
.
Thus, we can reconstruct the function on
based on
for all
and all
, i.e. countably much information!
The previous observation is the idea underlying the representation or ‘coding’ of continuous functions in . Recall that the language
only involves variable for natural numbers and sets
and functions
.
The following definition is the standard in Reverse Mathematics (RM for short) and taken from Steve Simpson’s excellent Subsystems of Second-Order Arithmetic [Si09].

As it turns out, one does not need much beyond the computable to show that a (third-order) continuous function on has such a code/representation: the ‘Big Five’ system WKL from RM suffices, as shown by Kohlenbach [Ko02]. So far so good: continuous functions can be represented by countable codes, and one does not need much beyond the computable to make this work. Moreover, Kohlenbach’s base theory (see [Ko05])
proves that every code on
gives rise to a continuous (third-order) function.
Finally, people have proposed to study more complicated topics (measure theory, topology, …) via codes. The codes become rather complicated and showing that each higher-order object has a code, becomes hard compared to e.g. the Big Five of RM. Perhaps this observation would not come as a surprise, but we show next that even coding continuous functions has its problems.
Problems with coding continuous functions
We now discuss problems with the coding of continuous functions. The results in this section can be found in full detail in [Sa19]. The following table is taken from there. The notion of separably closed set is standard in RM (see e.g. [Bro05]).
In the first column, I have listed a number of well-known theorems from the RM literature. In the second column, one can observe the logical strength of these theorems when formulated in using RM-codes as in the above definition. The only difference with the third column is that we now use the usual definition of ‘third-order function that is continuous’.
The difference is quite extreme in some cases, less in others. Recall that the system is Kohlenbach’s base theory of higher-order RM from [Ko05].
I hope I have convinced you THAT a problem occurs: RM seeks to find the minimal axioms needed to prove theorems of ordinary mathematics and the above table suggests that introducing codes changes what these minimal axioms are/can be.
Too many codes
Let us now try to understand WHY this problem occurs, using the Tietze extension theorem as an example. This theorem is formulated as follows.
(TIE) For
continuous on the separably closed
, there is continuous
such that
for
.
Now let TIE be the theorem TIE interpreted in
using RM-codes. TIE
deals with codes for continuous functions defined on a separably closed set
. As is clear from the above table, TIE
is equivalent to ACA
.
Now let TIE be the theorem TIE interpreted without codes for continuous functions. Thus, TIE
deals with third-order functions
that are also continuous on a separably closed set
. As is clear from the above table, TIE
is provable in RCA
.
Recall from the above that codes defined on always define a third-order function in RCA
. For codes defined on separably closed sets, this is no longer the case! In fact, we have the following.
The following are equivalent over RCA
:
(a) ACA
(b) For an RM-code
defined on the separably closed
, there is a third-order function
such that
for
.
Note that from item (b) need not be continuous: this item only expresses that the second-order code
gives rise to a function
.
On a historical note, Tietze’s two main theorems in [Tie12] deal with functions that are everywhere defined on , as discussed in [Sa19].
From the equivalence between items a) and b), we may conclude that, working in RCA, there are ‘too many’ codes for continuous functions on separably closed sets. Indeed, we need ACA
to guarantee that every such code actually denotes a third-order object.
Thanks for the interesting post, Sam. Do you know if there is any tradition of showing the robustness of reverse mathematics results with respect to codings? E.g., can we say that your first column holds for any ‘reasonable’ first-order coding? In this way, a bit of a leap, perhaps the offset in logical strength can be calibrated with the order of the representation?