{"id":"9adf2d72-1d2b-4fd6-8571-cc50ae4b2414","arxiv_id":"2411.16338","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"New uniqueness and finite dependent-choice axioms are placed inside hyperarithmetic analysis, and the class RFN^{-1}(ATR0) is shown to approximate hyperarithmetic analysis by closure properties and instance restrictions.","lead":"This paper introduces new versions of the dependent choice axiom in reverse mathematics and shows they belong to the special class called hyperarithmetic analysis. It also proposes a syntactic class, omega-model reflection, that approximates this class and proves several closure properties.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The proof of Theorem 5.12 and Corollary 5.13 relies on an unpublished reduction of arithmetic unique existence to Π1-0 uniqueness ([Suz24]); if that reduction is unavailable or wrong, the claimed exclusion of arithmetic unique-existence statements from RFN^{-1}(ATR0) is unsupported.","rationale":"The reader identified two gaps: the survey-based Remark 2.9 behind Proposition 5.8, and the [Suz24] dependency in Theorem 5.12. I focus on the [Suz24] dependency because it is the one that can be checked by a single re-derivation and because it attacks the exclusion direction of the approximation claim, which is advertised in the abstract and introduction. Proposition 5.8 with Remark 2.9 is indeed a cataloging assumption, but the paper is careful to phrase it as a survey ('To the best of the author's knowledge'), and the conditional statement Proposition 5.8 remains true regardless. The [Suz24] reduction, by contrast, is used as a black box inside a proof that is otherwise presented as complete. If the reduction is unavailable or subtly requires stronger induction, Corollary 5.13 fails; no part of the proof repairs it. The new DC variants and their hyperarithmetic-analysis membership appear supported by the cited literature and omega-model results, and I did not find an internal contradiction there. Therefore the paper should stay CONDITIONAL pending the check.","tokens_in":17877,"tokens_out":25022,"duration_ms":220417,"concrete_test":"Independently derive the reduction used in Claim 1: over ACA0, show that for every arithmetic formula ρ(n,Y) (with free set parameters) such that ∀n∃!Yρ(n,Y), there is a Π1-0 formula φ(n,Y) with the same uniqueness property and with ∀n∃!Yφ(n,Y) implying the existence of a sequence Z with ∀nρ(n,Z_n), all from unique Π1-0-AC0. A minimal check is to re-prove [Suz24, Theorem 6 and Remark 7] from first principles and then replace the single sentence 'Using unique Π1-0-AC0...' in the proof of Theorem 5.12 with an explicit construction. If the construction cannot be carried out without extra axioms or new induction, the proof of Theorem 5.12 is invalid and Corollary 5.13 should be withdrawn or re-proved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central 'difference' evidence for the approximation claim is Corollary 5.13, which asserts that no arithmetic statement of the form ∀X∃!Yθ(X,Y) lies in RFN^{-1}(ATR0). Its proof passes through Theorem 5.12. In the proof of Theorem 5.12, Claim 1 defines an arithmetic formula ρ (with a set parameter X) and then invokes unique Π1-0-AC0 to obtain a sequence Y. This invocation is valid only if the relation ρ is Π1-0. The paper does not prove that an arbitrary arithmetic uniqueness formula can be reduced to a Π1-0 uniqueness formula; it cites the unpublished note [Suz24] via Proposition 2.7(3) and the surrounding Remark 7. Since the cited source is not included, refereed, or replaced by a self-contained proof, the reduction is an unverified load-bearing step. If [Suz24]'s reduction requires additional induction or choice principles, or fails for formulas with set parameters, then Claim 1 collapses and with it the proof that RFN^{-1}(ATR0) excludes arithmetic unique-existence sentences. This is a concrete gap in a main advertised similarity/difference result, not merely a stylistic concern.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper investigates two themes in second-order arithmetic. In the first part (Sections 3 and 4), the author introduces unique and finite versions of the dependent choice axiom for Π1_0 and Σ1_1 formulas, shows that these variants imply ACA0+ but not Σ1_1 induction, proves that they belong to hyperarithmetic analysis, and compares them with known theories such as unique Π1_0-AC0, Δ1_1-CA0, Σ1_1-AC0, and Σ1_1-DC0. The main separation results use known ω-models, including Van Wesep's model Mw and Goh's model Mg. In the second part (Section 5), the author studies the class RFN^{-1}(ATR0), defined by equivalence of the ω-model reflection axiom with ATR0. The paper proves closure properties for this class (Theorem 5.11), shows that every theory between JI0 and Σ1_1-DC0 lies in RFN^{-1}(ATR0) (Proposition 5.8), and attempts to show that no arithmetic unique-existence sentence ∀X∃!Yθ(X,Y) belongs to this class (Theorem 5.12 and Corollary 5.13). These results are presented as evidence that RFN^{-1}(ATR0) approximates the class of theories of hyperarithmetic analysis.","tokens_in":18066,"tokens_out":22232,"duration_ms":206298,"significance":"If the main results are correct, the paper is a useful contribution to the study of hyperarithmetic analysis and ω-model reflection. The new DC variants give additional natural axioms in the hyperarithmetic-analysis area, and the structural results about RFN^{-1}(ATR0) provide a fresh perspective on a class that has not been extensively characterized. The paper is generally careful in its use of known ω-models and in the formalization of many implications, and it explicitly states open problems. A notable strength is the use of Goh's model Mg and Van Wesep's model Mw to produce a detailed satisfaction table, which is a convincing way to separate the new axioms. However, two load-bearing parts of the approximation claim rest on either an unpublished source ([Suz24]) or on an insufficiently justified inference; until those are repaired, the advertised 'difference' result between RFN^{-1}(ATR0) and hyperarithmetic analysis is not fully established. The paper also relies on a cataloging statement about all explicitly axiomatized theories of hyperarithmetic analysis, which should be clearly separated from proved theorems.","major_comments":[{"comment":"The proof applies unique Π1_0-AC0 to an arbitrary arithmetic formula ρ and relies on the assertion that unique Π0_2-AC0 is equivalent to unique Π1_0-AC0, citing the unpublished note [Suz24] (cf. Section 3). No self-contained proof is given that the particular arithmetic uniqueness formula ψ(X,Y), which contains clauses involving Turing functionals and the parameter X, can be reduced to Π1_0 or Π0_2 form. Since Claim 1 is the engine for the derivation of RFN^2 and hence for Corollary 5.13, the claimed exclusion of all arithmetic unique-existence sentences from RFN^{-1}(ATR0) is unsupported until this reduction is proved or replaced by a published source.","section":"Section 5, proof of Theorem 5.12, Claim 1"},{"comment":"The proof invokes König's lemma to obtain an infinite path f through the finitely branching tree T. König's lemma for finitely branching trees is equivalent to ACA0 over RCA0, but the ambient theory at that point is finite Π1_0-AC0 + Σ1_2-IND (or the analogous Σ1_{k+1} version). The text does not show that this theory proves ACA0, nor does it provide an alternative proof of the needed path existence. The construction of the sequence ⟨W_n⟩ therefore depends on an unstated comprehension principle. Please either prove the relevant instance of König's lemma from the available axioms or explicitly justify that finite Π1_0-AC0 (with the stated induction) implies ACA0.","section":"Section 4, proof of Theorem 4.5"},{"comment":"The first step of the proof infers 'Then ATR0⊢∀X∃!Yθ(X,Y)' from the assumption ATR0⊢RFN(∀X∃!Yθ)0. This inference is not justified by the definition of ω-model reflection: RFN(φ) asserts the existence of coded ω-models of φ+ACA0 containing any given set, and the existence of such models does not in general imply the truth of φ in the ambient universe. A separate argument, such as an absoluteness or reflection lemma, is needed before Theorem 5.12 can be applied to conclude ATR0⊢RFN^2(∀X∃!Yθ). Without this step, the contradiction with the second incompleteness theorem is not obtained.","section":"Section 5, proof of Corollary 5.13"},{"comment":"The covering claim 'all hyperarithmetic theories defined axiomatically lie between JI0 and Σ1_1-DC0' is presented as a survey assertion rather than as a proved theorem. This assertion is used to motivate the sense in which RFN^{-1}(ATR0) approximates the whole class HA. The paper should clearly label this statement as an open cataloging assumption, or provide evidence for it, because if a natural theory of hyperarithmetic analysis were outside this interval, the approximation claim would cover a strictly smaller class than advertised.","section":"Remark 2.9 and Proposition 5.8"}],"minor_comments":[{"comment":"The notation a∈O^X_+ and a∈O^X is dense and the distinction between O^X and O^X_+ is easy to miss; a short intuitive explanation of the intended meaning would help the reader.","section":"Section 2, Definition 2.2 and Definition 2.3"},{"comment":"The axiom schemes in Definition 3.1 are written without explicit universal closures; please add the universal closures for clarity and consistency with the surrounding text.","section":"Section 3, Definition 3.1"},{"comment":"In the proof of (1→3), the formula φ(X,Y) uses Y_L, Y_R, and Y_n without a consistent convention for the pairing of the components; please clarify whether X is always split as X_L⊕X_R and how Y_n refers to the n-th column of Y.","section":"Section 3, Proposition 3.4"},{"comment":"The abbreviation '∃ nonzero finitely many Xψ(X)' as ∃m∃X∀Y(ψ(Y)↔∃n≤m(Y=X_n)) already asserts that the X_n are exactly the solutions, so the word 'nonzero' is redundant and could be misleading; please rephrase or explain the intended nuance.","section":"Section 4, Definition of '∃ nonzero finitely many'"},{"comment":"The notation RFN(T)0 is introduced in a way that is easy to confuse with RFN(T)+ACA0; please consider simplifying the notation, for example by using a separate symbol for the one-fold reflection with base ACA0.","section":"Section 5, Definition 5.6"},{"comment":"Reference [Suz24] is an unpublished Google Drive document; since it is load-bearing for Theorem 5.12 and Proposition 2.7(3), it should either be replaced by a published source or its relevant content should be reproduced in the paper.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The paper has several solid parts, especially the systematic use of known ω-models to separate the new DC variants, and the closure properties in Theorem 5.11 are interesting. My main concern is the dependence of the central approximation/difference result on an unpublished note and on an unproved inference. If the author can supply a self-contained proof of the reduction used in Theorem 5.12, and justify the step in Corollary 5.13, the paper would be a valuable contribution. I also recommend that the editor ask the author to clarify the status of Remark 2.9, since it affects the claimed scope of the approximation. The paper seems well within the scope of the journal, so I do not see a fit problem, but the current version is not yet ready for acceptance."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth a look if you work on hyperarithmetic analysis. The paper introduces two new families of dependent choice axioms, the unique and finite variants of Π1-0-DC and Σ1-1-DC, and proves they sit in the hyperarithmetic analysis zone without implying Σ1-1 induction. It also proposes a syntactic approximation of the whole class via ω-model reflection, RFN^{-1}(ATR0). Both ideas are genuinely new relative to the cited literature, and the diagram of non-implications built on the known models Mw and Mg is a useful addition. The closure results in Theorem 5.11, mirroring the closure properties of HA, are clean and well proved.\n\nThe soft spot is the load-bearing use of the unpublished note [Suz24]. Theorem 5.12 needs to convert arbitrary arithmetic uniqueness formulas to Π1-0 uniqueness to apply unique Π1-0-AC0, and the paper simply cites [Suz24] for this. The conversion is not stated or proved. If that reduction is unavailable or requires extra induction principles, the proof of Corollary 5.13, which claims no arithmetic unique-existence sentence lies in RFN^{-1}(ATR0), collapses. This is a genuine gap in the advertised difference between the approximation class and HA, and a referee should ask for the reduction to be made explicit or replaced by a published source.\n\nSecond, the approximation claim rests on Remark 2.9, the survey assertion that every explicitly axiomatized theory of hyperarithmetic analysis lies between JI0 and Σ1-1-DC0. That is a cataloging statement, not a theorem. Proposition 5.8 uses it to conclude such theories all belong to RFN^{-1}(ATR0). It may be true of every known example, but it should be flagged as an empirical survey rather than a proven covering result.\n\nMinor point: Theorem 4.5 invokes König's lemma without saying that ACA0 provides it. Fine for the audience, but easy to spell out. The proof of Proposition 3.4 is dense, though the induction arguments in Lemmas 3.5 and 4.4 check out.\n\nOverall, the mathematics looks sound where I can check it. The new axioms and their basic implications are well supported; the reflection approximation is a promising organizing perspective even if the boundary is not yet fully mapped. I would send this to a referee with the instruction to focus on the [Suz24] dependency and the Remark 2.9 assumption.","headline":"New choice axioms for hyperarithmetic analysis and a fresh approximation idea, but the main difference result leans on an unpublished reduction.","tokens_in":18687,"tokens_out":2475,"would_cite":true,"duration_ms":22913,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03F35","03D55","03B30"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper shows that unique and finite dependent-choice axioms for $\\Pi^1_0$ and $\\Sigma^1_1$ formulas belong to hyperarithmetic analysis, and that the class $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$ approximates hyperarithmetic analysis in…","keywords":["hyperarithmetic analysis","reverse mathematics","dependent choice","omega-model reflection","ACA0+","Sigma-1-1 induction","ATR0","second-order arithmetic"],"falsifier":"Find an explicitly axiomatized theory of hyperarithmetic analysis that does not lie between $\\mathsf{JI}_0$ and $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$; this would break the covering argument. Alternatively, produce an arithmetic formula $\\theta(X,Y)$ such that the $\\omega$-model reflection of $\\forall X\\exists!Y\\,\\theta(X,Y)$ is equivalent to $\\mathsf{ATR}_0$, which would directly contradict Corollary 5.13.","tokens_in":2363,"feed_emoji":"🧮","tokens_out":3346,"duration_ms":141514,"temperature":0.7,"pith_summary":"This paper tries to pin down the structural boundary of hyperarithmetic analysis, the family of set-existence principles whose minimal $\\omega$-models are exactly the hyperarithmetic sets. It introduces unique and finite versions of $\\Pi^1_0$ and $\\Sigma^1_1$ dependent choice, shows they imply $\\mathsf{ACA}_0^+$ but not $\\Sigma^1_1$ Induction, and places them inside hyperarithmetic analysis between $\\mathsf{JI}_0$ and $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$. In a second line, it argues that the class $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$ approximates hyperarithmetic analysis: it shares the same closure properties and contains no arithmetic unique-existence statement. If correct, this gives a partial syntactic handle on a class usually defined semantically.","feed_headline":"Dependent-choice axioms join hyperarithmetic analysis","feed_subtitle":"Unique and finite variants prove ACA0+ but not Sigma-1-1 Induction; omega-model reflection approximates the class.","key_machinery":"The load-bearing mechanism is the $\\omega$-model reflection axiom $\\mathsf{RFN}(T)$, which asserts that for every set $X$ there is a coded $\\omega$-model containing $X$ and satisfying $T+\\mathsf{ACA}_0$. The class $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$ collects the theories $T$ for which $\\mathsf{RFN}(T)$ is equivalent over $\\mathsf{ACA}_0$ to $\\mathsf{ATR}_0$. The proof machinery also includes the equivalence of $\\mathsf{unique}\\,\\Pi^1_0\\text{-}\\mathsf{AC}_0$ and $\\mathsf{unique}\\,\\Pi^1_0\\text{-}\\mathsf{DC}_0$ under $\\Sigma^1_1$ induction, and the tree-indexing argument that upgrades finitely many choices to an infinite dependent-choice sequence.","core_discovery":"The central discovery is that two syntactic decorations of dependent choice, requiring the chosen object to be unique or allowing only finitely many choices, produce theories that sit inside hyperarithmetic analysis and strictly between $\\mathsf{ACA}_0^+$ and $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$, while remaining incomparable with $\\Sigma^1_1\\text{-}\\mathsf{AC}_0$ and $\\Delta^1_1\\text{-}\\mathsf{CA}_0$. The paper also proves that any theory whose strength lies between $\\mathsf{JI}_0$ and $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$ belongs to $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$, and that no arithmetic formula of the form $\\forall X\\exists!Y\\,\\theta(X,Y)$ with $\\theta$ arithmetic can belong to $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$. The latter exclusion is shown by proving from $\\mathsf{unique}\\,\\Pi^1_0\\text{-}\\mathsf{DC}_0$ the two-fold $\\omega$-model reflection of such a statement, which then triggers the second incompleteness theorem.","pith_inferences":["If the interval claim in Remark 2.9 is really a complete catalog, then $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$ contains all currently known theories of hyperarithmetic analysis; a natural test is to search for a hyperarithmetic-analysis theory whose $\\omega$-model reflection is not $\\mathsf{ATR}_0$.","The argument behind Theorem 5.12 may generalize: any sentence in $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$ that implies $\\mathsf{unique}\\,\\Pi^1_0\\text{-}\\mathsf{DC}_0$ would force its own consistency, so such theories must be weak in a precise proof-theoretic sense.","A plausible syntactic characterization of $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$ could be: theories $T$ with $\\mathsf{ACA}_0\\subseteq T\\subseteq \\Sigma^1_1\\text{-}\\mathsf{DC}_0$ plus enough induction; the open question about $\\Sigma^1_3$ instances suggests the class may be exactly those theories that are weak enough not to prove their own reflection.","The unique-versus-finite dichotomy may transfer to other formula classes: replacing $\\Pi^1_0$ by $\\Pi^1_k$ in the uniqueness antecedent could yield a hierarchy of intermediate hyperarithmetic-analysis theories."],"forward_implications":["Every explicitly axiomatized theory of hyperarithmetic analysis between $\\mathsf{JI}_0$ and $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$ has $\\omega$-model reflection equivalent to $\\mathsf{ATR}_0$, so $\\mathsf{RFN}(T)$ alone cannot separate those theories.","No purely arithmetic unique-existence sentence can axiomatize, via $\\omega$-model reflection, a theory equivalent to $\\mathsf{ATR}_0$; hence $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$ excludes an arithmetic core of hyperarithmetic analysis.","The new unique and finite dependent-choice axioms imply $\\mathsf{ACA}_0^+$ and therefore prove a stronger iteration of the Turing jump than $\\mathsf{ACA}_0$, yet they leave $\\Sigma^1_1$ Induction unprovable.","The closure properties of hyperarithmetic analysis, adjoining full induction, negating $\\mathsf{RFN}(T)$, or negating $\\mathsf{ATR}$, persist in $\\mathsf{RFN}^{-1}(\\mathsf{ATR}_0)$, so the two classes have the same global geometry under these operations.","Known $\\omega$-models separate the new axioms: one model satisfies the unique and finite $\\Pi^1_0$ choice axioms but fails $\\Delta^1_1\\text{-}\\mathsf{CA}_0$, while another satisfies $\\Delta^1_1\\text{-}\\mathsf{CA}_0$ but fails the finite $\\Pi^1_0$ choice axiom."],"supporting_citations":[{"why":"Supplies the base theories, the $\\mathsf{HYP}(X)$ models, the strong soundness theorem, and the equivalence of $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$ with $\\Sigma^1_3$ reflection used throughout.","marker":"[Sim09]"},{"why":"Defines hyperarithmetic analysis and the Jump Iteration axiom $\\mathsf{JI}$, and gives the model separating $\\mathsf{JI}_0$ from $\\mathsf{unique}\\,\\Pi^1_0\\text{-}\\mathsf{AC}_0$.","marker":"[Mon06]"},{"why":"Supplies the unpublished equivalence of $\\mathsf{unique}\\,\\Pi^1_0\\text{-}\\mathsf{AC}_0$ with $\\mathsf{unique}\\,\\Pi^0_2\\text{-}\\mathsf{AC}_0$ and the conversion of arithmetic uniqueness formulas to $\\Pi^1_0$ form used in Theorem 5.12.","marker":"[Suz24]"},{"why":"Introduces $\\mathsf{finite}\\,\\Pi^1_0\\text{-}\\mathsf{AC}_0$ and constructs the $\\omega$-model $\\mathsf{Mg}$ separating it from $\\Delta^1_1\\text{-}\\mathsf{CA}_0$.","marker":"[Goh23]"},{"why":"Constructs the $\\omega$-model $\\mathsf{Mw}$ satisfying $\\mathsf{unique}\\,\\Pi^1_0\\text{-}\\mathsf{AC}_0$ but not $\\Delta^1_1\\text{-}\\mathsf{CA}_0$, and proves the infinite descending chain theorem for hyperarithmetic analysis.","marker":"[Wes77]"},{"why":"Provides tagged tree forcing and the $\\omega$-model satisfying $\\Delta^1_1\\text{-}\\mathsf{CA}_0$ but not $\\Sigma^1_1\\text{-}\\mathsf{AC}_0$.","marker":"[Ste78]"},{"why":"Introduces $\\mathsf{unique}\\,\\Sigma^1_1\\text{-}\\mathsf{TDC}$, whose equivalence with $\\mathsf{ATR}_0$ grounds Proposition 3.2.","marker":"[Rüe02]"},{"why":"Provides detailed proofs for $\\mathsf{ABW}$ and $\\mathsf{SL}$ and shows the model $\\mathsf{Mw}$ satisfies $\\mathsf{ABW}$, used to locate $\\mathsf{finite}\\,\\Pi^1_0\\text{-}\\mathsf{AC}_0$.","marker":"[Con12]"}],"fun_headline_variants":["New DC variants navigate hyperarithmetic analysis","Unique and finite DC: from ACA0+ toward Sigma-1-1 Induction","Omega-model reflection narrows the hyperarithmetic gap","DC variants show ACA0+ not Sigma-1-1 Induction","Hyperarithmetic analysis refined by unique and finite DC"],"cache_read_input_tokens":20736,"weakest_assumption_plain":"The approximation result rests on Remark 2.9, the author's survey claim that every explicitly axiomatized theory of hyperarithmetic analysis lies between $\\mathsf{JI}_0$ and $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$; if a natural theory fell outside this interval, the covering argument of Proposition 5.8 would miss it.","fun_headline_variants_meta":{"raw":{"variants":["New DC variants navigate hyperarithmetic analysis","Unique and finite DC: from ACA0+ toward Sigma-1-1 Induction","Omega-model reflection narrows the hyperarithmetic gap","DC variants show ACA0+ not Sigma-1-1 Induction","Hyperarithmetic analysis refined by unique and finite DC"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000845,"raw_usage":{"total_tokens":3683,"prompt_tokens":956,"completion_tokens":2727,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":572,"completion_tokens_details":{"reasoning_tokens":2644}},"tokens_in":572,"tokens_out":2727,"duration_ms":20171,"temperature":1.0,"reasoning_tokens":2644,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-12T13:15:45.824272+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Find an explicitly axiomatized theory of hyperarithmetic analysis that does not lie between $\\mathsf{JI}_0$ and $\\Sigma^1_1\\text{-}\\mathsf{DC}_0$; this would break the covering argument. Alternatively, produce an arithmetic formula $\\theta(X,Y)$ such that the $\\omega$-model reflection of $\\forall X\\exists!Y\\,\\theta(X,Y)$ is equivalent to $\\mathsf{ATR}_0$, which would directly contradict Corollary 5.13.","supporting_citations":[],"review_version":1}