TL;DR: classical Reverse Mathematics makes heavy use of so-called codes or representations. We observe a major problem with this coding practise, namely the connection between open sets and continuous functions, which is ‘brute-forced’ by the coding of these objects.
The long version: Reverse Mathematics needs no introduction on this blog and neither does , the language of second-order arithmetic. As is well-known,
contains a sort for natural numbers and a sort for sets of natural numbers. Using this frugal setup, one can represent higher-order objects via -often cumbersome- codes or representations.
First of all, as a case in point, here is the definition of ‘code for continuous function’, which looks nothing like the usual ‘epsilon-delta’ definition at first glance.
A (code for a) continuous function on
is a set of quintuples
which satisfies the following three conditions:
1) Ifand
then
,
2) Ifand
then
,
3) If
and
then
,
and the domain condition:
whereis an abbreviation for
.(see Simpson’s excellent SOSOA, II.6.1)
Complicated as such codes may look, they are ‘easy to find’: as shown here, one only needs weak Koenig’s lemma (WKL) to show that a third-order -function that is continuous has an RM-code in the above sense, working in Kohlenbach’s base theory for higher-order Reverse Mathematics. In this way, the use of codes for continuous functions does not (seem to) have a big influence on the Reverse Mathematics of the ‘Big Five’, the weakest system of which is WKL. In short:
codes for continuous functions are easy to find, namely the weakest Big Five system suffices.
Secondly, open sets of reals also are not available directly in and are represented as unions of open balls. We write ‘
‘ for
for an open set
. It is then a natural question how hard it is to prove the following ‘coding principle’ (Open), where open sets of reals are given by their characteristic functions (well-known from measure and probability theory):
(Open) For any open set
, there is a sequence of intervals
such that
.
One can show (see Remark 1.13 here) that open sets without any representation occur `in the wild’, namely in the study of regulated and bounded variation functions. The latter are rather tame and play an important role in e.g. Fourier analysis. In this way, (Open) is not just spielerei.
As shown here, none of the Big Five can prove the coding principle (Open), and the same for much stronger principles. In fact, (Open) is ‘explosive’ in that adding it to -CA
, the higher-order version of
-CA
, one can derive the much stronger
-CA
. In a nutshell, we have:
codes for open sets are hard to find, namely none of the Big Five systems suffice.
Thirdly, the above two paragraphs show that open sets and continuous functions are fundamentally different classes of objects. Since Reverse Mathematics is supposed to analyse theorems of ordinary mathematics as they stand (see I.8.9 and IV.2.8 in SOSOA for this very pov), this fundamental difference must be respected. Unfortunately, this fundamental difference is not reflected in second-order Reverse Mathematics in light of the following theorem.
Given a code RM-open set
(See Simpson’s excellent SOSOA, II.7.1 for a proof in the base theory RCA, we can effectively find a code for a continuous function
such that
for all real
. Vice versa, for a code for a continuous function
, we can effectively find a code for an open set
such that
.
.)
Now, the connection between codes for open sets and continuous functions is of course well-known from (Turing) computability theory, and enables the representation of third-order objects in . That is all well and good for computability theory, but Reverse Mathematics is supposed to deal with mathematics ‘as it stands’. As it stands, the coding of open sets and continuous functions ‘brute-forces’ the identification of two fundamentally different classes of objects, which is not acceptable if one stands by the grand foundational claims made in Reverse Mathematics.
In my opinion, the above observations are fundamentally more problematic than previous problems associated with coding, like in the case of the Nielsen-Schreier theorem (see here). As we will observe in a future post, coding similarly distorts the relation between well-known function classes, e.g. bounded variation and Baire 1, but that is for another day.
In conclusion, the coding practice of second-order Reverse Mathematics brute-forces the identification of two fundamentally different classes of objects, namely open sets and continuous functions. If one believes that Reverse Mathematics should analyse theorems ‘as they stand’, this kind of identification is not acceptable.