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:
(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.