On some subtheories of strong dependent choice

Juan P. Aguilera; Keita Yokoyama; Yudai Suzuki

REVIEW 2 major objections 5 minor 5 references

On some subtheories of strong dependent choice

T0 review · 2 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read This paper proves that the $\Pi^1_{e+2}$, $\Sigma^1_{e+1}$, and Boolean-combination consequences of $\Sigma^1_i$-$\mathsf{SDC}_0$ are exactly the sentences provable from specific $\beta$-model reflection schemes, so the provable fragments…

desk verdict Genuine progress on consequence classes of Sigma^1_i-SDC0, but Section 4's main proof has a gap that needs fixing. read the letter →

arxiv 2411.17415 v1 pith:3LHDWR3T submitted 2024-11-26 math.LO

Juan P. Aguilera , Yudai Suzuki , Keita Yokoyama This is my paper · ORCID

classification math.LO MSC 03F3503B3003E15

keywords strongdependentchoicebeta-modelsreflectionprinciplesreversemathematicssecond-orderarithmeticconservativityPi-1-1-CA0Booleancombinations

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper aims to identify exactly which sentences of limited logical complexity are provable from the theory $\Sigma^1_i$-$\mathsf{SDC}_0$, the strong dependent choice scheme for $\Sigma^1_i$ formulas in second-order arithmetic. The claimed answer is that each fragment is governed by a reflection principle built from finite chains of $\beta_i$-models: the $\Pi^1_{e+2}$ consequences are exactly the theorems of $\mathsf{ACA}_0$ plus the chain schemes $\beta^i_e\mathrm{RFN}(n)$, the Boolean combinations of $\Pi^1_{i+1}$ consequences are exactly the theorems of the parameter-free reflection scheme $\beta_i\mathrm{Rfn}(\Sigma^1_{i+1})_0$, and for $e

What carries the argument

The central objects are coded $\beta_i$-models: countable $\omega$-models that agree with the ambient universe on all $\Sigma^1_i$ formulas, equivalently that reflect $\Pi^1_i$ truths. The machinery is the finite chain $\beta^i_e(M_0,\dots,M_n)$, which requires $M_0\in M_1\in\cdots\in M_n$, makes each earlier model a $\beta_i$-model according to later members of the chain, and adds a $\beta_e$-condition on the last model; the corresponding reflection sentences $\beta^i_e\mathrm{RFN}(\sigma;n;\tau)$ assert that every set belongs to the first model of such a chain with prescribed sentences $\sigma$ and $\tau$ holding at the endpoints. The load-bearing step is a preservation lemma: a subuniverse closed under finding $\beta_i$-models is itself a $\beta_i$-submodel and a model of $\Sigma^1_i$-$\mathsf{SDC}_0$. This lemma is what lets the compactness argument convert a failure of provability into a model of $\Sigma^1_i$-$\mathsf{SDC}_0$ with the target sentence false.

What would settle it

A concrete falsifier is to construct a model $\mathcal{M}$ of $\mathsf{ACA}_0$ and a subcollection $\mathcal{S}'$ closed under $\mathcal{M}$'s $\beta_{i+1}$-models such that the induced $\omega$-submodel is not a $\beta_{i+1}$-submodel of $\mathcal{M}$ and does not satisfy $\Sigma^1_{i+1}$-$\mathsf{SDC}_0$; since the preservation lemma is the load-bearing step in the compactness arguments behind the characterizations, such a counterexample would refute the paper's central theorems.

Watch

Extended reading notes

Core claim

Working over $\mathsf{ACA}_0$, the paper proves that the $\mathsf{B}(\Pi^1_{i+1})$ sentences provable from $\Sigma^1_i$-$\mathsf{SDC}_0$ are exactly those provable from $\beta_i\mathrm{Rfn}(\Sigma^1_{i+1})_0$, whose axioms are all instances of $\sigma \to \exists M(\beta_i(M) \land M\models\sigma)$ for $\Sigma^1_{i+1}$ sentences $\sigma$, where $\beta_i(M)$ says that $M$ is a coded $\beta_i$-model: an $\omega$-model satisfying the same $\Sigma^1_i$ formulas as the ambient universe. It also proves that for $e<i$ the $\Pi^1_{e+2}$ consequences are exactly the theorems of $\mathsf{ACA}_0$ plus the chain reflection schemes $\beta^i_e\mathrm{RFN}(n)$, and that the $\mathsf{B}(\Pi^1_{e+1})$ and $\Sigma^1_{e+1}$ consequences are captured by the corresponding $\beta^i_e\mathrm{RFN}^-$ schemes. The direction from reflection to strong dependent choice is immediate from the known $\beta_i$-model reflection characterization of $\Sigma^1_i$-$\mathsf{SDC}_0$; the converse is the main work, carried out by a compactness argument that builds a $\beta_i$-submodel of a model of the reflection scheme and shows it satisfies $\Sigma^1_i$-$\mathsf{SDC}_0$.

Load-bearing premise

The whole characterization rests on a preservation lemma: any collection of sets closed under passing to $\beta_i$-models is itself a $\beta_i$-submodel and satisfies strong dependent choice; the induction proving that lemma assumes truth of a $\Pi^1_i$ formula inside a coded model is absolute between the subcollection and the ambient universe, and the base case is imported from an earlier paper rather than proved here.

Editorial extensions

If this is right

Every $\Pi^1_{e+2}$ sentence provable from $\Sigma^1_i$-$\mathsf{SDC}_0$ is already provable from $\mathsf{ACA}_0$ plus the chain reflection schemes $\beta^i_e\mathrm{RFN}(n)$, so the $\Pi^1_{e+2}$ fragment of strong dependent choice is exactly the union of those schemes.
The $\mathsf{B}(\Pi^1_{i+1})$ fragment is captured by the parameter-free reflection scheme $\beta_i\mathrm{Rfn}(\Sigma^1_{i+1})_0$, which is not finitely axiomatizable.
For $e<i$, the $\Sigma^1_{e+1}$ consequences are conservative over $\mathsf{ACA}_0$ plus $\beta^i_e\mathrm{RFN}^-(n)$; in the case $i=1,e=0$, this says the $\Sigma^1_2$ consequences of $\Pi^1_1$-$\mathsf{CA}_0$ coincide with iterated hyperjumps and with the determinacy levels $(\Sigma^{0,\emptyset}_1)^n$-$\mathsf{Det}$.
The finite levels of the reflection hierarchy are strictly increasing: $\beta^i_i\mathrm{RFN}^-(n)$ is properly $\Pi^1_{e+2}$-weaker than $\beta^i_e\mathrm{RFN}(n+1)$, so each additional rung of the $\beta$-model chain proves new $\Pi^1_{e+2}$ sentences.
Because $\Sigma^1_i$-$\mathsf{SDC}_0$ is $\Pi^1_4$-conservative over $\Pi^1_i$-$\mathsf{CA}_0$, the same characterizations transfer to $\Pi^1_i$-$\mathsf{CA}_0$ for $e=0,1,2$.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

A natural next step, not pursued here, is to apply the same chain-extraction compactness technique to other choice schemes such as $\Sigma^1_i$-$\mathsf{DC}$ or transfinite dependent choice, where the shape of the $\beta$-model chain would likely determine the exact consequence classes.
The strict inclusions among finite reflection levels suggest that the number of $\beta$-model rungs needed to prove a sentence could serve as a proof-theoretic rank measuring how far a sentence sits above the reflection base, analogous to ordinal ranks in first-order reflection hierarchies.
For $i=1$, the paper's identification of the $\Sigma^1_2$ consequences with iterated hyperjumps hints that the higher-$i$ hierarchies may correspond to iterated $\beta_i$-jumps, though no such correspondence is proved for $i>1$.
A testable extension is whether the parameter-free characterizations of Section 3 still hold when the ambient base theory is weakened below $\mathsf{ACA}_0$; the present proofs work over $\mathsf{ACA}_0$, and the exact strength needed for the compactness construction is not isolated.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

This is a real step forward in the program on Pi^1_2 consequences of Pi^1_1-CA0. It generalizes the earlier work [4] from the single case to arbitrary i, and adds Boolean combinations and Sigma consequences. The paper is mostly clean, but Section 4 has a genuine gap in the final step of Theorem 4.2 that the authors need to address.

The genuinely new material is concentrated in Sections 3 and 4. Theorem 3.7, equating the B(Pi^1_{i+1}) consequences of Sigma^1_i-SDC0 with the reflection scheme beta_iRfn(Sigma^1_{i+1})_0, is a nice result and the proof via Lemma 3.6 is clear. The conservativity result in Theorem 3.10, with the corollary about iterated hyperjumps and determinacy, is also valuable. And Lemma 2.13, which gives a computability-theoretic strengthening of the known Theorem 2.14, is a useful tool.

The problem is Claim 4.2.2 in the proof of Theorem 4.2. The proof says that since not-pi is a Sigma^1_{e+1} sentence true in A0 and A0 is a beta_i-submodel of M', M' also satisfies not-pi. That submodel property does not follow from the construction. The chain gives A0 in A1 and A1 |= beta_i(A0), and more generally A_n in A_{n+1} with A_{n+1} |= beta_i(A_n). That makes A0 a beta_i-model from the perspective of A1, not necessarily from the perspective of the union M'. The proof would need an upward transfer of Sigma^1_{e+1} truth from A0 to M'. That is plausibly provable by propagating Pi^1_e truth along the chain, but the paper does not supply the argument. As written, the step is a gap in the central theorem of Section 4, and the same compressed reasoning appears in Theorem 4.3. There are also some typos: tau appears where pi is meant, and the index A_{k+e+1} looks like it should be A_{k+n+1}. These are minor individually, but they do not help.

The stress-test note is accurate: the chain does not make A0 a beta_i-submodel of M'.

Who is this for? People working in reverse mathematics and the proof theory of second-order arithmetic. The results are plausible and likely correct, but Section 4 is not ready in its current form. The paper deserves a serious referee because the core ideas are good, the gap is localized, and the rest of the paper is careful. I would send it to review, with the expectation that the referees will ask the authors to fix Section 4.

Referee Report

2 major / 5 minor

Summary. The paper studies the sets of Π1_e-, Σ1_e-, and B(Π1_e)-consequences of the theory Σ1_i-SDC0 of strong dependent choice for Σ1_i formulas. It claims exact characterizations in terms of reflection principles over chains of coded β-models: Theorem 2.14 treats Π1_{e+2}-consequences for i>e, Theorem 3.7 treats B(Π1_{i+1})-consequences, and Theorems 4.2 and 4.3 treat B(Π1_{e+1})- and Σ1_{e+1}-consequences for e<i. The proofs use compactness/Barwise-Schlipf constructions with chains of β_i-models, together with a hierarchy of reflection schemata β^i_eRFN and β^i_eRFN^-.

Significance. If correct, these are sharp, elegant characterizations of the provable fragments of Σ1_i-SDC0, extending the authors' earlier work on the Π1_2-consequences of Π1_1-CA0 and connecting the subject to local reflection principles in the style of Beklemishev. The Section 2 argument is informative and the paper is explicit about the provenance of Theorem 2.14. However, the proofs of the central results in Sections 3 and 4 contain two nontrivial transfer steps that are not justified as written; hence the results should be regarded as not yet established.

major comments (2)

[Section 3, Lemma 3.5] The proof of Lemma 3.5 contains a load-bearing unsupported inference. After choosing a β_i-model Y with Y |= β^i_iRFN^-(φ;n), the proof states that the condition in the square brackets, which includes Y0 |= φ, "is Π1_i" and therefore holds in the ambient model. This is false for φ ∈ Σ1_{i+1}: the formula Y0 |= φ is Σ1_{i+1}, not Π1_i. Consequently, the conclusion that Y0,...,Y_n,Y_{n+1} witness β^i_iRFN^-(φ;n+1) in the ambient does not follow from Y |= β^i_iRFN^-(φ;n). Since Lemma 3.5 is used in Lemma 3.6 and hence in Theorem 3.7, this gap affects the central claim of Section 3. Please supply a correct proof, for example by constructing the chain inside a β_i-model and transferring only the Π1_i matrix via β_i-submodel absoluteness.
[Section 4, Proof of Theorem 4.2, Claim 4.2.2] The assertion that A0 is a β_i-submodel of M′ is not established by the construction. The theory T′ only yields A_{n+1} |= β_i(A_n) for each n, and Lemma 2.12 does not apply, since its hypothesis requires M |= β_i(A_n) for the relevant A_n. Therefore the upward transfer of the Σ1_{e+1} sentence ¬π from A0 to M′ is unproved. The same compressed step is used in Theorem 4.3. A lemma is needed showing that Π1_e truth propagates from A0 along the chain and then to the union M′, or otherwise that ¬π is true in M′. As written, this is a gap in the central Theorem 4.2.

minor comments (5)

[Section 4, Claim 4.2.1] In the statement of Claim 4.2.1, "σ∨τ" should presumably read "σ∨π", and the subscript "A_{k+e+1}" should presumably be "A_{k+n+1}".
[Section 1 heading] The heading "Introdcution" contains a typo.
[Section 2, Lemma 2.12] The base case i=1 is delegated to [4] without stating the exact result being invoked; please include the precise statement or a proof, since this lemma is central to the compactness arguments.
[Section 3, Lemma 3.5 proof] When applying the induction hypothesis to β^i_iRFN^-(φ;n), the proof says "also holds by the induction hypothesis", but the displayed implication is the n=0 case, not the induction hypothesis for the current n; please rephrase for clarity.
[Section 2, Proof of Theorem 2.14] The step "Mk+1 satisfies ACA0 ∧ X ∈ M0 ∧ β^i_i(M0,...,Mk)" is terse; a brief remark that the parameters M0,...,Mk and X lie in Mk+1 would improve readability.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the consequence characterizations are proved by compactness from independent β-model reflection; the self-citations are prior-work citations, and the flagged Section 4 issue is a proof gap, not a circular reduction.

full rationale

I found no self-definitional scheme, no fitted parameter later renamed as a prediction, and no ansatz whose content is the target theorem. The main equivalences (Theorems 2.14, 3.7, 4.2, 4.3) are established by compactness/Barwise-Schlipf arguments from the independent characterization Theorem 2.7 (cited to Simpson's textbook) together with Lemma 2.12. The only self-citations are [2] and [4]: Theorem 2.14 is explicitly said to be essentially mentioned in [2], and the i=1 base case of Lemma 2.12 is taken from [4]. These are prior results by overlapping authors, but the present paper supplies new proofs and extensions, so the load-bearing use is a normal citation of prior mathematical work rather than a reduction to the paper's own thesis. No equation in the paper is defined in terms of the consequence class it is supposed to characterize, and no 'prediction' is fitted from data. A separate, non-circular concern is that Claim 4.2.2 asserts that A0 is a βi-submodel of M′ without a proof from the stated chain conditions in Theorem 4.2; if that assertion is false, Theorem 4.2 would have a gap, but that is a soundness issue, not a circularity. Accordingly the circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The argument is purely proof-theoretic: no numbers are fitted to data, and no new particles, forces, or entities are postulated. The main external dependencies are standard results in reverse mathematics, the compactness theorem, and the authors' prior paper [4] for the base case of the key submodel lemma.

assumptions (4)

standard math Compactness theorem for first-order logic
Used to build models M of T in Lemma 2.13, Lemma 3.6, and the Section 4 compactness arguments.
standard math Theorem 2.7: Sigma^1_i-SDC0 is equivalent over ACA0 to beta_i-model reflection
Imported from Simpson's textbook; all characterizations of consequences are derived from this equivalence.
domain assumption Base case i=1 of Lemma 2.12 as proved in [4]
The paper cites [4] for the base case and does not reprove it; this is a load-bearing prior result by the same authors.
standard math ACA0 proves that every beta_e-model is a model of ACA0 for e>0
Used in Remark 2.10 and throughout Section 4 to omit explicit ACA0 satisfaction conditions for beta_e-models.

how reviews work

0 comments

Cite this review

Pith. "Pith review of On some subtheories of strong dependent choice." pith.science (2026). https://pith.science/paper/3LHDWR3T

@misc{pith2026241117415,
  author       = {Pith},
  title        = {Pith review of: On some subtheories of strong dependent choice},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3LHDWR3T}},
  note         = {Machine review of arXiv:2411.17415}
}

abstract

In this paper, we give characterizations of the set of $\Pi^1_{e}$-consequences, $\Sigma^1_{e}$-consequences and $\mathsf{B}(\Pi^1_{e})$-consequences of the axiomatic system of the strong dependent choice for $\Sigma^1_i$ formulas $\Sigma^1_i$-$\mathsf{SDC}_0$ for $i > 0$ and $e < i+2$. Here, $\mathsf{B}(\Gamma)$ denotes the set generated by $\land,\lor,\lnot$ starting from $\Gamma$.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

5 extracted references · 4 canonical work pages

[4]

On the $\Pi^1_2$ consequences of $\Pi^1_1$-$\mathsf{CA}_0$

Yudai Suzuki and Keita Yokoyama. On the Π 1 2 consequences of Π 1 1-CA0. arXiv preprint arXiv:2402.07136, 2024

work page Pith review arXiv 2024
[1]

Notes on local reﬂection principles

Lev Beklemishev. Notes on local reﬂection principles. v olume 63, pages 139–146. 1997. The arithmetization of metamathematics

work page 1997
[2]

Determinacy and re ﬂection principles in second-order arithmetic

Leonardo Pacheco and Keita Yokoyama. Determinacy and re ﬂection principles in second-order arithmetic. arXiv preprint arXiv:2209.04082 , 2022

arXiv 2022
[3]

Stephen G. Simpson. Subsystems of second order arithmetic . Perspectives in Logic. Cambridge University Press, Cambridge; Association for Sy mbolic Logic, Poughkeep- sie, NY, second edition, 2009

work page 2009
[5]

Partial impredicativity in reverse math ematics

Henry Towsner. Partial impredicativity in reverse math ematics. J. Symbolic Logic , 78(2):459–488, 2013. Institute of discrete mathematics and geometry, TU Wien. Wi edner Haupt- strasse 8-10, 1040 Vienna, Austria. Email address : aguilera@logic.at National Institute of Technology, Oyama College, Nakakuki 771, Oyama, Tochigi, Japan Email address : yudai.su...

work page 2013

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [4]

On the $\Pi^1_2$ consequences of $\Pi^1_1$-$\mathsf{CA}_0$

Yudai Suzuki and Keita Yokoyama. On the Π 1 2 consequences of Π 1 1-CA0. arXiv preprint arXiv:2402.07136, 2024

work page Pith review arXiv 2024

[2] [1]

Notes on local reﬂection principles

Lev Beklemishev. Notes on local reﬂection principles. v olume 63, pages 139–146. 1997. The arithmetization of metamathematics

work page 1997

[3] [2]

Determinacy and re ﬂection principles in second-order arithmetic

Leonardo Pacheco and Keita Yokoyama. Determinacy and re ﬂection principles in second-order arithmetic. arXiv preprint arXiv:2209.04082 , 2022

arXiv 2022

[4] [3]

Stephen G. Simpson. Subsystems of second order arithmetic . Perspectives in Logic. Cambridge University Press, Cambridge; Association for Sy mbolic Logic, Poughkeep- sie, NY, second edition, 2009

work page 2009

[5] [5]

Partial impredicativity in reverse math ematics

Henry Towsner. Partial impredicativity in reverse math ematics. J. Symbolic Logic , 78(2):459–488, 2013. Institute of discrete mathematics and geometry, TU Wien. Wi edner Haupt- strasse 8-10, 1040 Vienna, Austria. Email address : aguilera@logic.at National Institute of Technology, Oyama College, Nakakuki 771, Oyama, Tochigi, Japan Email address : yudai.su...

work page 2013