1.1 Brouwer’s Intuitionism and Hilbert’s Finitism

Brouwer’s Intuitionism is considered as the precursor of many varieties of constructivism and finitism which reject the law of excluded middle (LEM) for statements concerning infinite objects. It is said that even Hilbert, a most severe opponent of Brouwer’s, adopted a part of Brouwer’s idea in his proposal for meta-mathematics or proof theory, and this partial adoption is now called Hilbert’s Finitism. However, there are several essential differences between these two varieties of constructivism or finitism.

First, they are different in their original aims. Brouwer’s Intuitionism is a claim how mathematics in its entirety should be, and the mathematics practiced according to this is called Intuitionistic Mathematics (INT). On the other hand, Hilbert’s Finitism was intended to apply only to a particular part of mathematics, called proof theory or meta-mathematics. The aim of this part was “saving” the entirety of mathematics from the fear of inconsistency. The “entirety of mathematics” in Hilbert’s idea is far beyond finitism and now called Classical Mathematics (CLASS) in the context of comparison among kinds of mathematics.

This difference might explain why Hilbert’s Finitism is stricter than Brouwer’s Intuitionism: for example, the induction schema on numbers is granted for free in the latter whereas it is allowed only if restricted to finitely checkable statements in the former. The acceptance of the schema for properties not finitely checkable (even though LEM for such properties is not allowed) seems to be reason enough not to call Brouwer’s Intuitionism a finitism, and moreover Brouwer’s Intuitionism requires transcendental assumptions which basically assert that everything is to be constructed (cf. the notion of choice sequence) contradicting CLASS.

It is worth mentioning Bishop’s constructivism, a third variety of constructivism. Bishop-style constructive mathematics (BISH) is considered to be completely constructive, in the sense that it does not assume any transcendental assertion. Thus all the theorems of BISH, as formal sentences, are contained in those of CLASS and INT. Nonetheless, it does not seem plausible to call it a finitism either, for it also accepts the induction schema applied to properties not finitely checkable. It accepts the axiom of choice applied to such properties as well, which is also beyond the finitistically justifiable part of CLASS.

Another contrast between Brouwer and Hilbert is in their attitudes towards formalization: while Brouwer did not formalize INT, Hilbert tried to formalize CLASS and since then his Finitism (now identified with what is formalizable in Primitive Recursive Arithmetic $\textbf {PRA}$ ; see [Reference Tait47]Footnote ¹ ) has been established as the meta-theory of handling formalization, or, in which proof theory is practiced. This contrast has, however, been gradually losing significance: followers of Brouwer formalized INT, and now our interest is in how different it is, as a formal theory,Footnote ² from CLASS and from BISH as well as from Russian Recursive Mathematics RUSS. The last requires a different transcendental assumption asserting that everything is computable.

Unfortunately a difference is also in popularity: CLASS has been investigated extensively, e.g., identifying the finitistically secured part, while there seems to have been no similar systematic investigation for INT.

Given these contrasts, the aim of the present series of articles, the identification of the part of INT and addable axioms that Hilbert would recognize as secured, has multi-fold motivations. To repeat: from the viewpoint that Brouwer’s Intuitionism is the precursor of various kinds of constructivism and finitism; from the historical perspective that Brouwer and Hilbert were severe opponents of each other; and from the necessity of the identification as has been done for CLASS in order to develop INT in parallel to CLASS.

1.2 Reducibility and interpretability

By what criterion would Hilbert recognize a fragment of mathematics as secured according to his Finitism? We may distinguish two criteria: a fragment is said to be (i) finitistically guaranteed if it is consistent provably in $\textbf {PRA}$ ; and (ii) finitistically justifiable if it is consistent relative to $\textbf {PRA}$ provably in $\textbf {PRA}$ . It is likely that these were not distinguished in Hilbert’s original intention prior to Gödel’s incompleteness theorem.

Proof theory, to which Hilbert’s Finitism was originally intended to apply, has refined (ii) above (see [Reference Rathjen32, Section 2.5]): a formal theory $T_1$ is (proof theoretically) reducible to another $T_2$ over a class $\mathcal {C}$ of sentences if there is a primitive recursive function f such that provably within $\textbf {PRA}$ , for any sentence A from $\mathcal {C}$ , if x is a proof of A in $T_1$ then $f(x)$ is a proof of A in $T_2$ . Usually $\mathcal {C}$ contains the absurdum $\bot $ and so this notion yields the comparison of externally defined consistency strengths (namely, the consistency of $T_2$ implies that of $T_1$ or consistency-wise implication) provably in $\textbf {PRA}$ . In many interesting cases, the theories essentially contain a fragment of arithmetic and we can assume $\mathcal {C}$ includes $\Pi ^0_1$ or $\Pi ^0_2$ sentences. As the Gödel sentence (of a reasonable theory) is $\Pi ^0_1$ , it also yields the comparison of internally defined consistency strength: any reasonable formal theory consistent provably in $T_1$ is consistent provably also in $T_2$ . Now $\textbf {I}\boldsymbol {\Sigma }_1$ , $\textbf {RCA}_0$ and $\mathbf{WKL}_0$ are parts of Classical Mathematics that are known to be proof theoretically reducible to $\textbf {PRA}$ . As a subtheory is trivially reducible to a supertheory, these four theories are proof theoretically equivalent.

For our purposes, however, we can use a stronger notion, interpretability. We will prove reducibility results by giving concrete interpretations, among which are Gödel–Gentzen negative interpretation and realizability interpretation. Our notion of interpretability is slightly broader than that in some literature, in the sense that logical connectives can be interpreted non-trivially (as in the aforementioned examples).Footnote ³ An interpretation I is called $\mathcal {C}$ -preserving, if any $\mathcal {C}$ sentence A is implied by its interpretation $A^I$ in the interpreting theory $T_2$ . All interpretations in the present article are $\Pi ^0_1$ -preserving, and so imply reducibility with $\mathcal {C} = \Pi ^0_1$ . Whereas reducibility concerns only proofs ending with sentences in $\mathcal {C}$ , interpretability means that all mathematical practice formalized in one theory can be simulated in another. As each step of proofs in $T_1$ is transformed into a uniformly bounded number of steps in $T_2$ , the induced transformation f of proofs belongs to even lower complexity, and so the consistency-wise implication is proved in meta-theories weaker than $\textbf {PRA}$ .

The difference between reducibility and interpretability becomes essential when we talk about the relations between finitistically guaranteed theories (hence weaker than $\textbf {PRA}$ ): while the reducibility is proved typically by cut elimination, which requires commitment to superexponential functions, such a commitment yields the consistency of $\textbf {B}\boldsymbol {\Sigma }_1\textbf {ex}$ , $\textbf {RCA}_0^*$ and $\mathbf{WKL}_0^*$ , typical finitistically guaranteed theories, and so collapses the hierarchy of the externally defined consistency strengths of such weaker theories.

1.3 Characteristic axioms of Intuitionistic Mathematics

Up to the present, there seems to be a consensus on what axiomatizes (the characteristic part of) INT. An informal explanation of such characterizing axioms is as follows, where the terminology might differ from Brouwer’s original.

• Intuitionistic logic neither the law of excluded middle ( $A\lor \neg A$ ) nor double negation elimination ( $\neg \neg A \to A$ ) is accepted unless A is finitely checkable (while the explosion axiom $\bot \to A$ is accepted);

• Basic arithmetic basic properties, which are finitely checkable and which govern the natural numbers and fundamental operations, are accepted;

• Induction on natural numbers the induction schema on $\omega $ for all the legitimate propertiesFootnote ⁴ (not necessarily finitely checkable) is accepted;

• Bar induction transfinite induction along the well-founded tree (coded by a bar, which intersects any infinite sequence) of finite sequences of numbers, with various restriction, Footnote ⁵ is accepted;

• Fan theorem classically equivalent to a form of König’s lemma or weak fan theorem, restricted to binary trees but defined by any legitimate properties, is an important consequence of bar induction in many applications; either of them is taken as an axiom of INT instead of bar induction in some literature;

• Axiom of choice for any legitimate property A of sorts i and j, if for any x of sort i there is y of j such that $A[x,y]$ holds then there exists a function f of sort $i \to j$ such that $A[x,f(x)]$ holds for any x of i;

• Continuity principle a function on Baire space $\omega ^\omega $ defined by any legitimate property is locally continuous.

The last contradicts CLASS, and the others, except the first two and weak fan theorem, are classically beyond Finitism. Since Heyting arithmetic, consisting only of the first three, is mutually interpretable with Peano arithmetic, and hence already beyond Finitism, we need to restrict these axioms, as in CLASS.

The first half of the main purpose of the present series of articles is thus to clarify how large fragments of these axioms are jointly reducible to Hilbert’s Finitism (i.e., finitistically justifiable) or jointly consistent provably in Finitism (i.e., finitistically guaranteed). This article, the first in the series, addresses this question, in the language $\mathcal {L}_{\mathrm{F}}$ of function-based second order arithmetic (similar to that of $\textbf {EL}$ from [Reference Troelstra and van Dalen50, Chapter 3, 6.2]), where we need some twist to state the existence of choice functions on Baire space (see Section 2.5.5) or where we could say that the axiom of choice for such sorts is illegitimate at all (see f.n.12).

The expositions of axioms here are informal or pre-formal, and it is quite delicate how to formalize them. We follow a standard way, but some discussions are unavoidable and will be addressed in Section 2.

We define fragments of the axioms basically by requiring the relevant properties to be in classes of formulae, e.g., $\Sigma ^0_n$ ’s and $\Pi ^0_n$ ’s (which however do not exhaust all arithmetical formulae because of the lack of prenex normal form theorem), and by controlling the sorts in the axiom of choice.

1.4 Finitistically justifiable and guaranteed parts of Intuitionistic Mathematics

We will see that the following with $\textbf {EL}_0^-$ (i.e., the logic and basic arithmetic) are jointly reducible to $\textbf {PRA}$ :

• • induction on natural numbers restricted to $\Sigma ^0_2$ properties ( $\Sigma ^0_2\textsf {-Ind}$ );

• • bar induction restricted to $\Pi ^0_1$ properties ( $\Pi ^0_1\textsf {-BI}$ , see the exact formulation in Definition 2.26);

• • fan theorem for fans (decidable by definition) and bars defined by any legitimate properties ( $\mathcal {L}_{\mathrm{F}}\textsf {-FT}$ );

• • axiom of choice for all legitimate properties and dependent choice of numbers for $\Sigma ^0_2$ ones ( $\Sigma ^0_2\textsf {-DC}^0$ );

• • continuity principle for functions defined by any legitimate properties ( $\mathcal {L}_{\mathrm{F}}\textsf {-WC!}^0$ and $\mathcal {L}_{\mathrm{F}}\textsf {-WC!}^1$ ),

and that, with the following further restrictions, jointly consistent provably in $\textbf {PRA}$ : induction on numbers to decidable properties; dependent choice and bar induction omitted; fans to be complete binary ( $\mathcal {L}_{\mathrm{F}}\textsf {-WFT}$ ).

Besides the well known contrast with the classical situation concerning the continuity principle, we see further contrasts, as any of the following is, classically, beyond $\textbf {PRA}$ : $\Sigma ^0_2\textsf {-Ind}$ ; fan theorem restricted either to decidable bars $\Delta ^0_0\textsf {-FT}$ or to complete binary fans and $\Pi ^0_1$ bars $\Pi ^0_1\textsf {-WFT}$ ; and $\Pi ^0_1$ axiom of choice.

Our method is Kleene’s functional realizability, known to be able to interpret most part of INT in CLASS. We examine which fragments of INT are interpreted by this in $\mathbf{WKL}_0$ or $\mathbf{WKL}_0^*$ . As it is based on a $\Pi ^0_2$ -definable application “ $\,|\,$ ” for functions, unlike the number realizability, naïve attempts of proof easily rely on $\Pi ^0_2$ or higher induction. The proof is, in general, not straightforward from previously known one.

As a byproduct, we can add Markov’s principle $\textsf {MP}$ (i.e., $\Sigma ^0_1\textsf {-DNE}$ double negation elimination restricted to $\Sigma _1$ assertions) to the combinations above. $\textsf {MP}$ is accepted from some constructive views and called semi-constructive. While it seems agreed not to accept $\textsf {MP}$ in Intuitionism, it is not agreed to accept its negation.Footnote ⁶ We need no interpretations that exclude $\textsf {MP}$ , as the interpretability of $T{+}\textsf { MP}$ trivially implies that of T.

Moreover, we will see that these fragments are optimal: none of $\Pi ^0_2\textsf {-Ind}$ , $\Sigma ^0_1\textsf {-BI}_D$ (restricted to decidable bars), $\Pi ^0_2\textsf {-DC}!^0$ (with uniqueness in the premise) and $\Pi ^0_1\textsf {-DC}!^1$ (dependent choice of functions) can only with $\textbf {EL}_0^-$ be reducible to $\textbf {PRA}$ ; none of $\Pi ^0_1\textsf {-Ind}$ , $\Sigma ^0_1\textsf {-Ind}$ , $\Delta ^0_0\textsf {-BI}_D$ , $\Delta ^0_0\textsf {-DC}!^0$ and $\Delta ^0_0\textsf {-FT}$ only with $\textbf {EL}_0^-$ is consistent provably in $\textbf {PRA}$ . For the former, we interpret $\textbf {I}\boldsymbol {\Sigma }_2$ , which proves the consistency of $\textbf {PRA}$ , by generalizing Coquand and Hofmann’s method [Reference Coquand and Hofmann11]. For the latter, we interpret $\textbf {I}\boldsymbol {\Sigma }_1$ which is equiconsistent with $\textbf {PRA}$ .

Note that, by Gödel’s second incompleteness, if a theory $T_1$ proves the consistency $\textrm {Con}(T_2)$ of another $T_2$ , then $T_1$ is not reducible to (nor interpretable in) $T_2$ , since otherwise $T_1$ proves its own consistency.

1.5 Effects of semi-constructive or semi-classical principles

Hilbert’s Finitism did not intend to restrict the mathematics, but to maximize the set of acceptable axioms that are in the direct sense beyond Finitism but that are secured on his Finitistic ground through meta-mathematics. So we should continue to clarify which axioms beyond Intuitionism can be added to the secure parts of INT without losing finitistic guaranteedness or justifiability. The aforementioned byproduct on $\textsf {MP}$ is a part of answer, and it is natural to try to answer more generally: which part of classical logic, or even of CLASS, is finitistically guaranteed or justifiable jointly with major partsFootnote ⁷ of INT? As many classically valid principles are known not to imply full classical logic, the other half of our purpose is to ask: how does the secured part change from the intuitionistic situation to classical one, along the hierarchy of such semi-classical principles?Footnote ⁸

Among famous ones are limited principle of omniscience $\textsf {LPO}$ (i.e., $\Sigma ^0_1\textsf {-LEM}$ the law of excluded middle for $\Sigma ^0_1$ ) and lesser limited principle of omniscience $\textsf {LLPO}$ (i.e., $\Pi ^0_1{\lor }\Pi ^0_1\textsf {-DNE}$ double negation elimination for $\Pi ^0_1{\lor }\Pi ^0_1$ ). $\textsf {LLPO}$ is implied by $\textsf {LPO}$ and, as shown in [Reference Akama, Berardi, Hayashi and Kohlenbach1], independent of $\textsf {MP}$ . In the presence of full induction, $\textsf {LLPO}$ is equivalent to $\textsf {B}\Sigma ^0_2\textsf {-DNE}$ and to $\Sigma ^0_1\textsf {-GDM}$ , generalized De Morgan’s law $\neg (\forall x < y)A \to (\exists x\,{<}\,y)\neg A$ for $\Sigma ^0_1$ properties. With restricted induction, however, all the implications we know among these are as follows.

Unlike $\textsf {MP}$ , by weak counterexample argument Footnote ⁹ we can presume that Brouwer would reject the idea of $\textsf {LLPO}$ (and hence all principles above it). Thus the status of $\textsf {LLPO}$ in Intuitionism is as that of WKL in Finitism, since WKL is definitely directly unacceptable in Finitism, and actually they are equivalent in the presence of axiom of choice (cf. 3.9). Because accepting WKL indirectly by consistency proof was the core of Simpson’s “partial realizations of Hilbert’s Program” from [Reference Simpson44], $\textsf {LLPO}$ should be of particular interest in our context.

We show that adding $\Sigma ^0_1\textsf {-GDM}$ (and so $\textsf {LLPO}$ ), even jointly with $\textsf {MP}$ , does not change the intuitionistic situation described in Section 1.4, except the axiom of function-number and function-function choice. Though these choices cannot be formalized in $\mathcal {L}_{\mathrm{F}}$ , continuous choice (CC), whose $\Pi ^0_1$ fragment contradicts $\textsf {LLPO}$ , could be seen as conjunctions of them and continuity principle (cf. Section 2.5.5). Our main tool is van Oosten’s Lifschitz-style functional realizability from [Reference van Oosten31], in the definition of which, a bounded $\Sigma ^0_2$ property plays a central role. Thus the arguments on the finitistic ground is much more delicate than in van Oosten’s original context.

On the other hand, we will see that $\textsf {LPO}$ already makes the situation completely classical, that is, any of the following separately, but together with $\textbf {EL}_0^-\,{+}\textsf {LPO}$ , is already non-reducible to $\textbf {PRA}$ :

• • $\Sigma ^0_2$ induction on numbers ( $\Sigma ^0_2\textsf {-Ind}$ );

• • fan theorem restricted to $\Delta ^0_0$ bars but without the binary constraint ( $\Delta ^0_0\textsf {-FT}$ );

• • weak fan theorem restricted to (complete binary fans and) $\Pi ^0_1$ -bars ( $\Pi ^0_1\textsf {-WFT}$ ); and

• • $\Pi ^0_1$ axiom of choice even with the uniqueness assumption in the premise ( $\Pi ^0_1\textsf {-AC!}^{00}$ ).

For the second and fourth we will show the interpretability of $\textbf {ACA}_0$ with Gödel–Gentzen negative interpretation. For the others, we need the combination with intuitionistic forcing to interpret $\textbf {I}\boldsymbol {\Sigma }_2$ or $\textbf {ACA}_0$ .

1.6 Constructive reverse mathematics on consistency strength

Our study also contributes to the research field, called constructive reverse mathematics (cf. e.g., [Reference Ishihara19, Reference Ishihara20]). There implications, on a constructive ground, between (fragments of) axioms from CLASS, INT and RUSS, are investigated and, for the unprovability of these implications, questions of the following type are of interest:

Namely, it has been asked only whether a combination is consistent or inconsistent.

Now our investigation is on the proof theoretic or consistency strengths of combinations. In other words, we ask how consistent (or to which extent consistent) the combination is. Thus the question becomes refined:

The proof theoretic investigation of intuitionistic theories seems much less developed than classical ones.

Even the consistency strengths of $\Sigma _n$ or $\Pi _n$ induction schemata, the most basic targets of the study, were identified only in 1990s. Then Visser (in his unpublished note, see [Reference Wehmeier56]) pointed out that $\textbf {i}\boldsymbol {\Sigma }_{\infty }\,{=}\,\textbf {i}\boldsymbol {\Pi }_{\infty }$ , Heyting arithmetic with induction restricted to prenex formulae, is mutually $\Pi _2$ -preservingly interpretable with $\textbf {i}\boldsymbol {\Pi }_2$ , and so with classical $\textbf {I}\boldsymbol {\Sigma }_2$ . This shows the drastic contrast with the classical situation, as classical $\textbf {I}\boldsymbol {\Sigma }_n$ ’s form a strict hierarchy exhausting Peano arithmetic $\textbf {PA}$ . $\textbf {i}\boldsymbol {\Sigma }_1$ and $\textbf {I}\boldsymbol {\Sigma }_1$ are mutually $\Pi _2$ -preservingly interpretable (see [Reference Coquand and Hofmann11, Reference Avigad3]), and so are $\textbf {i}\boldsymbol {\Pi }_1$ and $\textbf {I}\boldsymbol {\Pi }_1\,{=}\,\textbf {I}\boldsymbol {\Sigma }_1$ as shown easily by Gödel–Gentzen negative interpretation (but only $\Pi _1$ -preserving, as shown in [Reference Wehmeier56]). Thus any of $\textbf {i}\boldsymbol {\Sigma }_n$ ( $n\,{\geq }\, 3$ ) and $\textbf {i}\boldsymbol {\Pi }_n$ ( $n\,{\geq }\, 2$ ) has the same strength as classical $\textbf {I}\boldsymbol {\Sigma }_2$ , and both $\textbf {i}\boldsymbol {\Sigma }_1$ and $\textbf {i}\boldsymbol {\Pi }_1$ as classical $\textbf {I}\boldsymbol {\Sigma }_1$ (and so $\textbf {PRA}$ ). What remains is $\textbf {i}\boldsymbol {\Sigma }_2$ , which [Reference Burr10, Corollary 2.27] interpreted in a fragment of Gödel’s $\textbf {T}$ of the same proof theoretic strength as $\textbf {I}\boldsymbol {\Sigma }_1$ by Dialectica interpretation. We will show these results by realizability but also that these strengths are not affected by adding the fragments of Brouwerian axioms. While for this goal we need functional realizability, our proof also shows that Kleene’s number realizability, used in [Reference Wehmeier56], interprets intuitionistic $\textbf {i}\boldsymbol {\Sigma }_2$ in classical $\textbf {I}\boldsymbol {\Sigma }_1$ . Here, realizing in a classical theory is essential; we do not know if $\textbf {i}\boldsymbol {\Sigma }_2$ is realizable in intuitionistic $\textbf {i}\boldsymbol {\Sigma }_1$ .

As mentioned in Section 1.5, $\textbf {i}\boldsymbol {\Sigma }_2$ and $\textsf {LPO}$ jointly have the same strength as classical $\textbf {I}\boldsymbol {\Sigma }_2$ . Generally, our method shows that $\textbf {i}\boldsymbol {\Sigma }_{n+1}{+}\Sigma _n\textsf {-LEM}$ is mutually $\Pi _{n+2}$ -preservingly interpretable with $\textbf {I}\boldsymbol {\Sigma }_{n+1}$ , whereas Gödel–Gentzen negative interpretation needs stronger $\textbf {i}\boldsymbol {\Sigma }_{n+1}{+}\Sigma _{n+1}\textsf {-DNE}$ to interpret $\textbf {I}\boldsymbol {\Sigma }_{n+1}$ .

Besides induction, there seem to have been no proof theoretic studies (in the sense of Section 1.2) on intuitionistic theories of the strength below $\textbf {HA}$ .Footnote ¹⁰ The present article leads to this large field of proof theoretic study.

1.8 A marriage of Brouwer’s Intuitionism and an ultrafinitism

After Hilbert’s Finitism in the early 20th century, ultrafinitisms, stricter kinds of finitism than Hilbert’s, have been proposed. Some are motivated by the development of computational complexity theory in the latter half of the century: only functions of a certain complexity are admitted, in the same sense as Hilbert’s (formalized as $\textbf {PRA}$ ) admits only primitive recursive ones. Which part of INT, with which semi-classical principle, is justifiable or guaranteed with respect to them? An abundance of complexity classes (not yet proved to be identical), and hence of ultrafinitisms, makes this question too big to answer in one article.

Here we consider only the easiest kind, which admits only Kalmár’s elementary functions.Footnote ¹³ This could be formalized as $\textbf {B}\boldsymbol {\Sigma }_1\textbf {ex}$ . All our finitistic guaranteedness results yield justifiability with respect to this kind of ultrafinitism, as they are proved via interpretability in $\textbf {B}\boldsymbol {\Sigma }_1\textbf {ex}$ . Recall that the notion of proof theoretic reducibility collapses the consistency of such weak theories but that of interpretability does not.

Theories for even stricter kinds of ultrafinitism require the distinction between large and small numbers (i.e., x’s and $|x|$ ’s), and therefore, in such a context, the natural formulations of some axioms, e.g., fan theorem, are not clear. The authors hope that they could treat these topics somewhere in the near future.

1.9 Outline and prerequisites

Section 2 introduces our base theory $\textbf {EL}_0^-$ and some variants, as well as semi-classical principles and Brouwerian axioms whose strengths we will investigate, with basic properties. Section 3 gives upper bounds of the strengths of combinations of them, with Kleene’s functional realizability and van Oosten’s variant for Lifschitz-style, whose characterization by axioms will be generalized extensively. Folklore results from classical arithmetic, refined in Section 3.1, play vital roles. Section 4 gives lower bounds, with Gödel–Gentzen negative interpretation and by generalizing Coquand–Hofmann forcing interpretation. Section 5 will present the results in final forms, with supplementary results, further problems and related works.

While Section 2 summarizes basic definitions and results on function-based second order arithmetic, the readers are assumed to be familiar with set-based counterpart from, e.g., [Reference Simpson45]. They are supposed to know the systems $\textbf {RCA}_0^*$ , $\mathbf{WKL}_0^*$ , $\textbf {RCA}_0$ , $\mathbf{WKL}_0$ and $\textbf {ACA}_0$ as well as the axiom schema $\Pi ^1_m\textsf {-TI}$ , which is known to be equivalent over $\textbf {ACA}_0$ to the transfinite induction along well-founded trees represented by sets. Comprehension axioms below are central in defining theories. By convention, we always assume that there are no collisions of free variables with bound ones. Thus below we implicitly assume that X is not free in $A[x]$ .

• ( $\mathcal {C}\textsf {-CA}$ ) $\exists X\forall x(x\,{\in }\,X\,{\leftrightarrow }\, A[x])$ for A from $\mathcal {C}$ .