{"id":"cd00c960-e58b-41a4-9a9d-38b7f534e51c","arxiv_id":"1908.05676","paper_version":6,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A higher-order hierarchy built from net convergence and a bootstrap axiom maps via the ECF interpretation onto the Big Five of second-order Reverse Mathematics.","lead":"This paper constructs a new hierarchy of principles in higher-order arithmetic that corresponds, through a standard coding translation, to the Big Five of Reverse Mathematics. It shows that convergence theorems for nets are equivalent to a new comprehension axiom, offering a continuity-based 'return to Brouwer' perspective on these foundations.","discovery_kind":"unification","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The BOOT/MCTC_net mathematics appears sound, but the hierarchy-mapping claim rests on the informal ECF coding convention that the paper itself concedes in Remark 1.1.","rationale":"The reader's conditional verdict is appropriate. I found no concrete mathematical flaw in the BOOT/MCTC_net equivalence; the proof's use of the (exists2)-or-not(exists2) split is a standard technique in higher-order reverse mathematics, and the reductions in the negative case are consistent with the paper's own framework. The main substantive concern is that the big-picture hierarchy claim depends on the status of ECF as a canonical embedding, and the paper's Remark 1.1 itself limits that status. Since the paper already flags the interpretive nature of ECF, the conditional verdict remains justified and the mathematical core is not undermined.","tokens_in":50951,"tokens_out":37494,"duration_ms":388148,"concrete_test":"Formalize the ECF translation of Theorem 3.7 using the exact definition in [89, p.138] and verify in RCA0 whether [MCTC_net]^ECF is provably equivalent to ACA0. If the derivation requires an extra principle such as A1 from Section 5.2 to obtain total associates for continuous type-2 functionals, then the abstract's unconditional claim that the hierarchy 'maps to' the Big Five is too strong; if it goes through in RCA0 alone, the concern is terminological rather than substantive.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's central claim is that the Plato hierarchy 'maps to' the Big Five under ECF. The load-bearing point is not a mathematical error in Theorem 3.7, whose excluded-middle proof is standard in higher-order reverse mathematics. The fragility lies in the identification of ECF-translated statements with their second-order counterparts. Remark 1.1 explicitly admits that [BOOT]^ECF is not verbatim ACA0; the intended reading requires replacing type-2 objects by total associates and treating continuous objects as coded by their RM-codes. That coding step is familiar from second-order RM, but it is an additional interpretive layer. If ECF is accepted exactly as the paper intends, the hierarchy claim follows; if not, the result is a parallel hierarchy with an approximate correspondence rather than the claimed reflection. The mathematical equivalences, including MCTC_net <-> BOOT, survive either way.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a hierarchy in higher-order arithmetic, called the 'Plato hierarchy', built around the bootstrap comprehension axiom BOOT: (∀Y^2)(∃X^1)(∀n)(n∈X ↔ (∃f^1)(Y(f,n)=0)). Its central result is Theorem 3.7, which proves over RCA_0^ω that the monotone convergence theorem for increasing nets in Cantor space indexed by subsets of Baire space (MCTC_net) is equivalent to BOOT. The paper then derives a series of related equivalences involving the Bolzano-Weierstrass theorem for nets, moduli of convergence, the Moore-Osgood theorem, open sets given by uncountable unions, the Cantor-Bendixson theorem, the perfect set theorem, and Heine-Borel compactness. It also develops fragments of the neighbourhood function principle (NFP) and the axioms A_0, A_1, A_2, and claims that under the ECF translation the Plato hierarchy maps to the Big Five of second-order reverse mathematics.","tokens_in":51060,"tokens_out":21084,"duration_ms":211828,"significance":"If the results hold, this is a substantial contribution to higher-order reverse mathematics: it gives a genuinely new hierarchy based on convergence of nets and continuity principles, rather than on discontinuous functionals as in Kohlenbach's hierarchy. The proof of Theorem 3.7 is detailed and the equivalence MCTC_net ↔ BOOT is a striking and nontrivial result. The Specker-net lifting in Theorem 3.19, which recycles a classical second-order reversal, is also a valuable contribution. The paper is ambitious and will interest researchers in reverse mathematics, higher-order arithmetic, and the foundational interpretation of the Big Five. However, the manuscript's central 'mapping to the Big Five' claim depends on an informal coding convention that is only stated as a remark, and one of the derived equivalences (Corollary 3.14) has a proof gap in the ¬(∃2) case.","major_comments":[{"comment":"In the proof of Corollary 3.14, the case ¬(∃2) asserts that QF-AC^{0,1} 'is immediate from QF-AC^{0,0} (included in RCA_0^ω)'. This is not a valid inference: the statement that all functionals on Baire space are continuous does not give a uniform way to select a witness f ∈ N^N for each n, and QF-AC^{0,1} is not a theorem of ACA_0. Since Corollary 3.14 and Corollary 3.16 depend on this step, the authors must either supply a direct proof that CAUmod implies QF-AC^{0,1} in the ¬(∃2) case or weaken the statements of these corollaries.","section":"Section 3.2.2, Corollary 3.14"},{"comment":"The paper's central claim that the Plato hierarchy 'maps to' the Big Five under ECF is stronger than what is formally established. Remark 1.1 explicitly concedes that [BOOT]^ECF is not verbatim ACA_0 and that an additional step identifying continuous objects with their countable codes is needed. As stated, Figure 2 invites the reader to read the correspondence as a theorem, but it is an interpretive convention. The paper should state a precise preservation claim, such as: for each equivalence A↔B proved in the hierarchy, RCA_0 proves [A]^ECF↔[B]^ECF up to the coding conventions of Remark 1.1. Alternatively, the 'maps to' formulation should be explicitly downgraded to 'corresponds under ECF plus representation conventions'. The mathematical theorems, including Theorem 3.7, are unaffected by this point, but the paper's title and framing depend on it.","section":"Abstract and Section 1.3, Figure 2; Remark 1.1"}],"minor_comments":[{"comment":"There is a missing closing parenthesis in the definition of the directed set D: the condition should read '(∀i,j<|w|)(Y(w(i))=Y(w(j))→i=j)'. The current text 'Y(w(i) = Y(w(j)))' is a typo.","section":"Theorem 3.19 proof"},{"comment":"In the proof of Theorem 4.23, the text says 'Applying QF-AC^{1,1}, we obtain G : C → N'. Since the choice is of a natural number for each function in C, the principle used should be QF-AC^{1,0}, not QF-AC^{1,1}.","section":"Theorem 4.23 proof"},{"comment":"Remark 4.20 states that the generalisation to uncountable unions is '(technically) superfluous' because the open sets used in Section 4.2 can be expressed as countable unions under the mainstream definition of 'countable'. This sits uneasily with Section 4.2's claim that uncountable unions are the 'correct' notion of open set; the authors should clarify how the two statements are to be reconciled.","section":"Remark 4.20"},{"comment":"The notation QF-AC^{σ,τ} is used systematically, but in the base theory RCA_0^ω only QF-AC^{1,0} is included, while QF-AC^{0,1} is later used as an extra axiom. A short table or explanation fixing which instances are assumed and which are added would help avoid confusion, since the superscript order is easy to misread.","section":"Section 2.1, Definition 2.2"}],"recommendation":"major_revision","confidential_remarks":"The core mathematical contribution, especially Theorem 3.7, appears sound and is likely to be of genuine interest. The main risks are the proof gap in Corollary 3.14's ¬(∃2) case and the mismatch between the informal 'maps to the Big Five' claim and the actual ECF-based convention. Both are fixable in revision. The paper also relies heavily on the author's prior work, but the cited results appear published and not circular. I would not reject on these grounds."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: the mathematics is sound and the paper deserves serious refereeing. The genuinely new load-bearing result, Theorem 3.7, is real: over RCA_0^omega, MCTC_net for nets in Cantor space indexed by subsets of Baire space is equivalent to BOOT. The proof splits on (exists 2) and uses the standard higher-order RM fact that without (exists 2) all type-2 functionals are continuous. The same construction powers the later equivalences, including CAUmod with BOOT + QF-AC and the Moore-Osgood splitting, and those are also the real content.\n\nThe paper also does something worthwhile in Section 5: fragments of NFP, a classically valid continuity schema, are shown equivalent to BOOT/HBU and related principles. That genuinely contrasts with Kohlenbach's discontinuity hierarchy. The higher-type generalisations in Section 3.4.2 are more sketchy, but the paper labels them illustrative and they do not carry the main argument.\n\nThe soft spot is the packaging, not the proofs. The abstract says the Plato hierarchy 'maps to' the Big Five under ECF. The paper's own Remark 1.1 admits [BOOT]^ECF is not verbatim ACA0; you need the standard coding of continuous objects by associates and the usual RM-code identification. That coding step is bedrock of second-order RM, so I do not see it as a fatal gap. It is an interpretive layer, and the reader should calibrate the strength of the slogan accordingly. A second, smaller overstatement: the paper makes much of uncountable unions of open balls as the correct notion of open set, then Remark 4.20 concedes that the results go through for countable unions, with the real source of strength being that the union is not 'searchable'. Again the formal theorems survive; the conceptual billing is a bit inflated.\n\nOtherwise the citation pattern is ordinary for this area. Self-citations to Normann and Sanders are frequent, but the cited results are published and the non-provability of HBU is external, not circular.\n\nWho this is for: people working in higher-order reverse mathematics and the RM of topology and analysis. A nonspecialist can read the introduction and Figure 2, but the proofs are technical. I would send it to a competent referee. My own verdict would be conditional acceptance with a request to soften the ECF language in the abstract and make Remark 1.1 front-and-center.","headline":"Solid higher-order reverse mathematics: the BOOT/MCTC_net equivalences are genuine and the proofs look right; the only real caveat is that the 'maps to the Big Five' slogan depends on the ECF coding convention, which the paper itself qualifies in Remark 1.1.","tokens_in":51605,"tokens_out":2263,"would_cite":false,"duration_ms":24258,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B30","03D65","03F35"],"pacs":[],"model":"deepseek-v4-flash","headline":"A single higher-order axiom, BOOT, is equivalent to the monotone convergence theorem for nets and, under the ECF-translation, becomes arithmetical comprehension, anchoring a hierarchy that maps to the Big Five of reverse mathematics.","keywords":["reverse mathematics","higher-order arithmetic","nets","Moore-Smith sequences","bootstrap axiom","ECF-translation","Big Five","neighbourhood function principle"],"falsifier":"Build a model of $\\mathrm{RCA}_0^\\omega$ in which the monotone convergence theorem for increasing nets in Cantor space indexed by subsets of Baire space holds, yet for some type-two functional $Y$ no set $X$ collects exactly the $n$ with $(\\exists f^1)(Y(f,n)=0)$; Theorem 3.7 says such a model cannot exist. A forcing or realizability construction producing such a model would refute the central equivalence, and a computational check is whether the Specker-net reversal of Theorem 3.19 can be carried out without countable choice.","tokens_in":50690,"feed_emoji":"🏛️","tokens_out":12709,"duration_ms":108193,"temperature":0.7,"pith_summary":"The paper aims to show that the Big Five systems of second-order reverse mathematics are not the ground floor of foundations: they are the reflections, under a coding translation called ECF, of a hierarchy of principles stated in higher-order arithmetic. The engine of that hierarchy is the bootstrap axiom BOOT, which asserts that for every functional $Y$ from Baire space to numbers and every number $n$, the set of $n$ for which some $f$ satisfies $Y(f,n)=0$ exists. Over the higher-order base theory $\\mathrm{RCA}_0^\\omega$, BOOT is proved equivalent to the monotone convergence theorem for increasing nets in Cantor space indexed by subsets of Baire space. This single equivalence generates a parallel hierarchy in which convergence theorems for nets, Heine-Borel compactness for uncountable covers, the gauge integral, and open sets as uncountable unions replace their countable second-order counterparts. If the picture is correct, ordinary reverse mathematics is the ECF-shadow of a richer hierarchy that can be formulated through classically valid continuity principles from intuitionistic mathematics.","feed_headline":"The Big Five are shadows of a higher-order Plato hierarchy","feed_subtitle":"Monotone convergence for nets is equivalent to BOOT, which the ECF-translation maps to ACA0.","key_machinery":"The load-bearing machinery is the bootstrap axiom BOOT, a comprehension principle for type-two functionals, together with the ECF-translation that converts higher-order objects into countable continuous representatives. BOOT supplies the exact set-existence strength; ECF is what turns higher-order equivalences into second-order ones, which is why the Big Five appear on the second-order side. A second piece of machinery is the replacement of sequences by nets indexed by subsets of Baire space: directed sets of finite sequences in Baire space, ordered by inclusion, turn a functional $Y$ into an increasing net whose limit encodes the required set. Later sections add fragments of the neighbourhood function principle, a classically valid continuity schema, to re-express BOOT and Heine-Borel compactness without discontinuous functions.","core_discovery":"The paper's central result is Theorem 3.7: over $\\mathrm{RCA}_0^\\omega$, the monotone convergence theorem for increasing nets in Cantor space indexed by subsets of Baire space, $\\mathrm{MCTC}_{\\mathrm{net}}$, is equivalent to BOOT. BOOT is the comprehension axiom $(\\forall Y^2)(\\exists X^1)(\\forall n^0)(n\\in X \\leftrightarrow (\\exists f^1)(Y(f,n)=0))$. The proof splits by the law of excluded middle: if the discontinuous existential functional $\\exists^2$ is available, the BOOT-set is read off as the limit of an increasing net built from finite initial segments of witnesses; if not, all functionals on Baire space are continuous, and both BOOT and $\\mathrm{MCTC}_{\\mathrm{net}}$ reduce to arithmetical comprehension. Under ECF, which replaces higher-type objects by countable continuous codes, this equivalence becomes the classical equivalence between the monotone convergence theorem for sequences and $\\mathrm{ACA}_0$. The paper further shows that combining these convergence theorems with weak comprehension axioms produces a 'bootstrap' hierarchy, that the hierarchy has natural formulations via the neighbourhood function principle, and that it extends naturally to open sets given by uncountable unions and to index sets beyond Baire space.","pith_inferences":["Editorial inference: if the Plato hierarchy is taken as the intended object, the Big Five are artefacts of choosing countable codes, and one should expect natural theorems of analysis to change their classification when nets and uncountable unions are primitive.","Editorial inference: a testable extension is to replace the directed sets of finite sequences in Baire space by other directed sets, such as lexicographic orders on countable ordinals, and compare the resulting monotone convergence principles; the paper's Remark 4.8 already indicates that index-set structure, not cardinality, drives the strength.","Editorial inference: the lossiness of ECF, conceded in the paper, suggests that a refined translation preserving more higher-type information could produce intermediate hierarchies between this Plato hierarchy and the Big Five; whether such a translation exists is left open."],"forward_implications":["Over $\\mathrm{RCA}_0^\\omega$ plus $\\Pi^1_k$-comprehension, adding BOOT proves $\\Pi^1_{k+1}$-comprehension, so convergence theorems for nets bootstrap to the next comprehension level.","The monotone convergence theorem for nets in the unit interval indexed by subsets of Baire space is equivalent to BOOT, and its version with a modulus of convergence is equivalent to BOOT plus countable choice.","BOOT implies Heine-Borel compactness for uncountable canonical covers, and the ECF translation of this implication is the classical step from arithmetical comprehension to weak König's lemma.","The Cantor-Bendixson and perfect set theorems, formulated for open sets as uncountable unions of open intervals, split into $\\Pi^1_1$-comprehension plus BOOT and $\\mathrm{ATR}_0$ plus BOOT respectively.","Fragments of the neighbourhood function principle are equivalent to BOOT and to Heine-Borel compactness, giving the whole hierarchy a continuity-based formulation."],"supporting_citations":[{"why":"Supplies the higher-order base theory $\\mathrm{RCA}_0^\\omega$ and the dichotomy between the existential functional $\\exists^2$ and full continuity on Baire space used throughout.","marker":"[42]"},{"why":"Provides the second-order equivalence between the monotone convergence theorem for sequences and $\\mathrm{ACA}_0$ that ECF maps the net version onto.","marker":"[82]"},{"why":"Introduces the study of nets in reverse mathematics and the principles $\\mathrm{MCT}_{\\mathrm{net}}$ and $\\mathrm{BW}_{\\mathrm{net}}$ that Section 3 sharpens and reverses.","marker":"[74]"},{"why":"Supplies the Heine-Borel principle HBU, the gauge-integral equivalences, and the independence results for $Z_2^\\omega + \\mathrm{QF-AC}^{0,1}$ that frame the hierarchy.","marker":"[60]"},{"why":"Defines associates and RM-codes for continuous functionals, the concrete mechanism behind ECF.","marker":"[41]"},{"why":"Is the source of the neighbourhood function principle NFP used to give continuity-based equivalents for BOOT and HBU.","marker":"[91]"},{"why":"Provides the uniform Pincherle theorem and the equivalence between uniform weak König's lemma and HBU used in the compactness section.","marker":"[63]"}],"fun_headline_variants":["Plato hierarchy: Big Five's higher-order shadows","Big Five's shadows: Plato hierarchy in higher-order arithmetic","Plato hierarchy: the Big Five in higher-order code","From Plato's cave: Big Five as shadows of higher types","Plato's hierarchy: higher-order counterparts of Big Five"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The comparison between the higher-order hierarchy and the Big Five depends on treating the ECF-translation, which replaces uncountable objects by countable continuous codes, as the canonical embedding that preserves the intended meaning; if that identification is too lossy, the mathematical equivalences remain but the claim that the Big Five are shadows of the hierarchy weakens.","fun_headline_variants_meta":{"raw":{"variants":["Plato hierarchy: Big Five's higher-order shadows","Big Five's shadows: Plato hierarchy in higher-order arithmetic","Plato hierarchy: the Big Five in higher-order code","From Plato's cave: Big Five as shadows of higher types","Plato's hierarchy: higher-order counterparts of Big Five"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001338,"raw_usage":{"total_tokens":5487,"prompt_tokens":1043,"completion_tokens":4444,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":659,"completion_tokens_details":{"reasoning_tokens":4363}},"tokens_in":659,"tokens_out":4444,"duration_ms":28820,"temperature":1.0,"reasoning_tokens":4363,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T13:11:38.748365+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build a model of $\\mathrm{RCA}_0^\\omega$ in which the monotone convergence theorem for increasing nets in Cantor space indexed by subsets of Baire space holds, yet for some type-two functional $Y$ no set $X$ collects exactly the $n$ with $(\\exists f^1)(Y(f,n)=0)$; Theorem 3.7 says such a model cannot exist. A forcing or realizability construction producing such a model would refute the central equivalence, and a computational check is whether the Specker-net reversal of Theorem 3.19 can be carried out without countable choice.","supporting_citations":[{"cited_title":"Notes Log., vol","cited_arxiv_id":null,"evidence_quote":"Supplies the higher-order base theory $\\mathrm{RCA}_0^\\omega$ and the dichotomy between the existential functional $\\exists^2$ and full continuity on Baire space used throughout."},{"cited_title":"Nets and Reverse Mathematics, a pilot study","cited_arxiv_id":"1905.04058","evidence_quote":"Introduces the study of nets in reverse mathematics and the principles $\\mathrm{MCT}_{\\mathrm{net}}$ and $\\mathrm{BW}_{\\mathrm{net}}$ that Section 3 sharpens and reverses."},{"cited_title":"Notes Log., vol","cited_arxiv_id":null,"evidence_quote":"Defines associates and RM-codes for continuous functionals, the concrete mechanism behind ECF."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Is the source of the neighbourhood function principle NFP used to give continuity-based equivalents for BOOT and HBU."},{"cited_title":"Pure Appl","cited_arxiv_id":null,"evidence_quote":"Provides the uniform Pincherle theorem and the equivalence between uniform weak König's lemma and HBU used in the compactness section."}],"review_version":1}