Unavoidable Sequences and Brouwerian Theory $T_2$

Definitions and mathematical statement

The source poses two related tasks in constructive logic. First, for an arbitrary constructive theory $T$ in the report's language $L$ which includes the intended bar-induction principle, determine exactly which sequences are unavoidable over $T$. If $\operatorname{Seq}_L$ denotes the intended domain of sequences and $\operatorname{Unav}_T$ the report's unavoidability predicate, the classification target can be displayed as \[ \mathcal U(T)=\{\alpha\in\operatorname{Seq}_L:\operatorname{Unav}_T(\alpha)\}. \] This is notation for the requested class, not a definition of unavoidability: neither the sequence domain nor that predicate is given in the supplied record. The quantifier over $T$ is retained; the question is not restricted here to one specified constructive theory.

Second, the original source states the conjecture that the particular Brouwerian theory $T_2$ described in the report is recursively acceptable. Thus its intended assertion is \[ T_2\text{ is recursively acceptable}. \] The language and axioms of $T_2$ and the exact metamathematical definition of recursive acceptability are not reproduced. In particular, recursive acceptability is not silently equated with recursive axiomatizability, consistency, or any guessed realizability property. The supplied assessment mentions relevant Church--Kleene and Markov-rule properties, but does not give their rule schemata or assert a precise equivalence defining recursive acceptability.

The bar-induction schema, permitted formulas and sequence objects, background constructive metatheory, and any consistency or effectiveness restrictions on the arbitrary $L$-theories are also absent. These are essential source-dependent data: a self-contained characterization of $\mathcal U(T)$ or formal rule-admissibility statement for $T_2$ cannot be recovered by choosing conventional versions without confirmation.

The registry labels the statement corrected and verified after source checking. Its literature triage dated 2026-08-21 labels the problem open and says the recursive-acceptability claim and relevant Church--Kleene and Markov-rule properties remain conjectural. These are supplied dated qualifications rather than independent results.

Short English statement

Classify the sequences unavoidable over each constructive $L$-theory containing bar induction. In particular, retain the conjecture that the report's Brouwerian theory $T_2$ is recursively acceptable; the definitions and rule schemata needed to make both tasks self-contained are missing.

Sources

• Local UnsolvedMath registry, permanent ID 30000946, source code catalogue entry; supplied complete source record, including its corrected-verified source-check note and dated literature assessment.
• Mathematical Logic: Proof Theory, Constructive Mathematics (2009), Oberwolfach Reports, DOI 10.4171/owr/2008/18, pp. 907--952: https://doi.org/10.4171/owr/2008/18. The proposed-year field gives 2008.
• Moschovakis, unavoidable sequences: https://www.math.ucla.edu/~joan/MLQnote09topost.pdf, supplied as a literature reference; the record names no proposer for this entry.