Why and how do (classical) reverse mathematics and intuitionistic reverse mathematics relate?

This is a really big topic, as I'm sure you realize, so this answer is going to be fairly incomplete.

Is there a “big picture” explanation of the similarities? Can one explain, for example, why it is that computability plays such a major role in both classical and intuitionistic RM?

I think that it's important to take a historical perspective when asking a question like this. (That said, I am going to be a blatant revisionist and uniformly use the word 'computable' instead of 'recursive'.) There's some overlap in the list of important early figures in constructive metamathematics and computability theory, such as Kleene and Kreisel. There's also places where more specific cross-talk occurred (e.g., the Kleene-Brouwer ordering and the notions of Martin-Löf and Schnorr randomness). In the particular case of Kleene, this directly influenced constructive math by introducing computability-theoretic tools (i.e., realizability).

The other important thing to remember is that reverse mathematics as a discrete topic didn't arise in a vacuum. Harvey Friedman and Steve Simpson's advisor was Gerald Sacks, a major figure in computability theory. So with regards to reverse math in particular, one could be cynical and say that the reason computability plays such a central role is that the core questions of the field are defined in terms of computability (i.e., the base system is taken to be $\mathsf{RCA}_0$, rather than something a non-logician might write down if you locked them in a room and asked them to write a very minimalist formal theory of mathematics).

That said I don't think it's an entirely unmotivated perspective. Constructive math and computability theory both arise from some kind of intuition about the pre-formal notion of effectivity. Computability theorists sometimes describe the topic of their field as 'low-complexity definability,' which I think is reasonable. There's some sense in which computation is intimately linked to the most concrete aspects of mathematical reasoning.

Ideally: Can we make this similarity more precise, for example, by defining a procedure that takes a system of constructive mathematics (with full comprehension) and outputs a subsystem of classical second-order arithmetic (with excluded middle but only restricted comprehension) and/or perhaps in the other direction, that might preserve provability of certain kinds of statements?

I don't know of much work that has been done on this explicitly, but two ideas come to mind.

To go from classical reverse math to constructive reverse math, one approach might be to look at turning $\omega$-models (or maybe just arbitrary models) of $\mathsf{RCA}_0$ into partial combinatory algebras (or more generally the parameterized partial combinatory algebras in my paper with Andrej) and then looking at realizability over the resulting PCAs or PPCAs. (To me this is broadly similar to the idea of the construction in my paper with Andrej. Essentially what we're using is a kind of realizability that is relativized to a set of oracles (rather than a particular oracle), where realizers are required to work with some degree of uniformity relative to the particular choice of oracle.) Some very specific statements should be preserved by this (such as the existence of a non-computable real), although this will probably also depend on how specifically you define the (P)PCA from the model.

For the other direction, one thing that comes to mind is the work of Joan Moschovakis on unavoidable sequences in constructive theories. I can imagine a general procedure based on the ideas here:

• Take a constructive theory $T$ and fix some internal family of 'definable' or 'weakly definable' functions from $\omega$ to $\omega$ or from $\omega$ to $2$. (The most obvious choice would be the literal functions from $\omega$ to $\omega$, but Moschovakis is interested in the 'unavoidable' sequences, which are definable relations $A(x,y)$ on $\omega \times \omega$ satisfying $\forall x \neg\neg\exists y A(x,y)$ and $\forall x y y'(A(x,y) \wedge A(x,y') \to y = y')$.)

• Then look at the induced classical theory of the natural numbers and this family of (weakly) definable functions via a double negation translation.

For instance, I heavily suspect that if you did this with, say, $\mathsf{HA}^\omega$, the resulting classical theory would be precisely $\mathsf{RCA}_0$.

From the perspective of math philosophy, is it correct to say that classical arithmetic RM focuses on predicativism whereas intuitionistic RM focuses on constructivism, and that the similarities show that there is some connection between predicativism and constructivism (cf. this past question of mine)?

I actually wouldn't say this is correct, at least not without a lot of qualification. First of all, my understanding is that a lot of modern constructive mathematicians (especially people in the general sphere of constructive type theory) consider predicativity to be part of constructivism. People will sometimes say that theories like $\mathsf{IZF}$ aren't constructive because they're highly impredicative, for instance.

Secondly, the word 'predicative' is used in related but not fully compatible ways in classical mathematical logic and in constructive mathematical logic, although both uses trace back to Russell's use of the word as far as I can tell. (Even within classical mathematical logic, people can't agree about what 'predicative' should mean.) They both involve avoiding full power sets and (arguably) restricting comprehension but the details are different, and (amusingly to me) they both do things that the other finds objectionable: On the one hand, the classical predicative set theory $\mathsf{KP}$ avoids function sets entirely and is now often formulated without full $\in$-induction but can't really avoid propositional resizing because of its classicality (i.e., the power set of $1$ is always isomorphic to $2$ classically). On the other hand, predicative (extensions of) $\mathsf{MLTT}$ avoids propositional resizing more or less by design but really can't avoid the use of full function types and full induction (and often use large universes, which, while constructively weak, are classically comparable to large cardinals). The result of this incompatibility is that (classical) $\mathsf{KP}$ together with $\mathsf{CZF}$ (the constructive set theory that is naturally interpretable in predicative $\mathsf{MLTT}$) is equivalent to $\mathsf{ZF}$, a theory that is far, far stronger than either of them individually.

I don't think there is going to be an entirely formal correspondence, but there are formal fragments of correspondence, e.g., in proof mining, classical proof theory, and papers like [Uftring 2021], [Fujiwara 2021], [HM 2019].

My personal opinion is the phenomenon described in the question arises from looking at the same underlying phenomenon through multiple lenses, including computability theory, reverse math, Weihrauch and computable reducibility, constructive reverse mathematics, higher order reverse mathematics, and other perspectives. These provide different perspectives of an underlying phenomenon that is not fully captured by any one approach. It is not surprising that the perspectives seem related to each other, because they are looking at the same underlying phenomenon: the internal "structure" of particular mathematical theorems.

With that said, I think there are a few remarks I can make that might give some partial answers or insights.

• Classical reverse math was founded by Friedman but clearly foreshadowed by work of Weyl, Feferman and others on predicative analysis and theories of finite type - see [DW 2017]. There was also work well before reverse mathematics on effective classical analysis, e.g. Specker's work on computable sequences with uncomputable limits was published in 1949.

• Friedman realized many formalizations could be pushed as low as type $2$: subsystems of second-order arithmetic with restricted induction. Of course a key phenomenon in classical systems of that sort is computability, because Post's theorem links computability with definability in arithmetic.

• Friedman's work at the time emphasized "ordinary mathematics", which also linked it more closely with Bishop's work. Friedman wanted to show that systems with far lower consistency strengths than ZFC could be used to formalize significant portions of math. The analogous motivation in Friedman's and Bishop's projects is to demonstrate that something can be done (formalization in second-order arithmetic or in constructive mathematics) by using the most recognizable and famous theorems of elementary real analysis as case studies. Unsurprisingly, they studied many of the same theorems.

• Some researchers in constructive reverse mathematics reject the concept of formalized base systems. Similar to Bishop, they work in an informal system rather than choosing any particular formal base theory. Like Bishop-style constructive mathematics, many results of constructive reverse mathematics can be formalized in versions of higher-type Heyting arithmetic. But those most interested in constructive reverse mathematics may not be eager to study that particular formalization, or use it to compare with classical reverse mathematics. This is one of several reasons there are few direct concordances between constructive and classical reverse mathematics.

• I don't think "predicativity" has been a significant motivation in the low levels of reverse mathematics, where the analogies with constructive reverse mathematics are stronger. There is a focus on predicativity in systems like $\mathsf{ATR}_0$ for theorems which are already known to be at least as strong as $\mathsf{ACA}_0$. But the majority of reverse mathematics results are on theorems provable from $\mathsf{ACA}_0$, where there is no question of predicativity.

• Perhaps another perspective about regular and constructive reverse mathematics is they look at various kinds of uniformity, or at what principles beyond the base theory are needed to resolve the nonuniformity in proofs. Of course, computability theory is about one kind of uniformity. From this perspective, constructive proofs of implications enforce a very strong form of uniformity, Weihrauch reductions enforce a weaker kind, and provability of an implication in $\mathsf{RCA}_0$ or $\mathsf{ACA}_0$ establishes an even weaker form.

Citations

[DW 2017] Dean, Walter; Walsh, Sean, The prehistory of the subsystems of second-order arithmetic, Rev. Symb. Log. 10, No. 2, 357-396 (2017). ZBL1376.03005.

[Fujiwara 2021] Fujiwara, Makoto, Weihrauch and constructive reducibility between existence statements, Computability 10, No. 1, 17-30 (2021). ZBL1535.03294.

[HM 2019] Hirst, Jeffry L.; Mummert, Carl, Using Ramsey’s theorem once, Arch. Math. Logic 58, No. 7-8, 857-866 (2019). ZBL1475.03071.

[Uftring 2021] Uftring, Patrick, The characterization of Weihrauch reducibility in systems containing $\mathrm{E}\text{-}\mathrm{PA}^\omega+\mathrm{QF}\text{-}\mathrm{AC}^{0,0}$, J. Symb. Log. 86, No. 1, 224-261 (2021). ZBL1529.03224.

We can look a bit closer at $\mathrm{WKL}$ in both systems to see how excluded middle and comprehension contribute here. Let's take $\mathrm{WKL}$ to be the statement:

$$\forall (a_i) \in \mathbb{R}^\mathbb{N} \ \exists (z_i) \in \{-1,1\}^\mathbb{N} \quad \forall n \in \mathbb{N} \ \ z_na_n \geq 0$$

In its core, we have $\mathrm{LLPO}$ in the form $\forall a \in \mathbb{R} \ \exists z \in \{-1,1\} \ za \geq 0$ (or, easier to read, $\forall a \in \mathbb{R} \ a \geq 0 \vee a \leq 0$). In classical reverse math, $\mathrm{LLPO}$ is trivially true. However, $\mathrm{WKL}$ can fail since just because have every single bit of $(z_i)$ doesn't mean we have the entire sequence (lack of comprehension). On the other hand, $\mathrm{LLPO}$ does not hold constructively, so in intuitionistic reverse math we don't have the individual bits; but if we had them, we could collect them into the sequence.

This difference in where the problem lies exactly has consequences for concrete classifications: In intuitionistic reverse math, the Intermediate Value theorem is equivalent to $\mathrm{WKL}$, in classical reverse math the Intermediate Value theorem is provable in $\mathrm{RCA}_0$.

I am not an expert, but my impression is the same as Carl Mummert's, except that I wouldn't just say that the "the perspectives seem related to each other, because they are looking at the same underlying phenomenon: the internal "structure" of particular mathematical theorems", but also that interesting mathematical theorems tend to correspond to some level of computability, which therefore naturally shows up when we are trying to order them according to some kind of complexity hierarchy. There is also the straightforward connection between various notions in computability and logical principles or reasoning:

(In what follows I am referring to the principles and not the systems.)

1. Each Turing jump corresponds to being able to evaluate one more quantification over ℕ. That is why ACA corresponds to having all finite jumps.
2. Recursion along a well-ordering W implies induction along W and is equivalent once we have sufficient construction strength (e.g. can construct a function via union of approximations).
3. LEM for some sort of statements corresponds to an oracle for that sort of statements, so of course it is also related to computability.
4. WKL corresponds to recursive separability, which is a natural computability notion that is lower than the Turing jump.
5. ATR corresponds to Σ[1,1] separability, which is simply a higher-order analogue of recursive separability. Whether it should be considered predicative or not depends on what other assumptions you make about subsets of ℕ and quantification over subsets of ℕ.
6. Choice, like LEM, corresponds to choice oracles, which is why it can be obtained from sufficiently powerful comprehension principles when the choice can be expressed in some computational sense. This is why WKL can be viewed as a choice principle, which can be proven from ACA. And also why Σ[1,1] Choice can be proven from ATR.