The MSO counting-logic conjecture for bounded arithmetic

Let $\mathsf{MSO}^\phi(\sharp)$ be monadic second-order logic with the Härtig quantifier, and call an arithmetical predicate directly definable when it is defined by the logic in the intended coding structure. Let $\Delta_0$ denote bounded arithmetic, containing equalities between polynomial terms, Boolean operations, and bounded numerical quantifiers of the form

$$\exists x < t.\,\varphi(x,\mathbf{y}),$$

where $t$ is a polynomial term. The MSO counting-logic conjecture. The arithmetical predicates directly definable in $\mathsf{MSO}^\phi(\sharp)$ can be defined in $\Delta_0$. This conjecture asks whether the direct expressive power of the second-order counting extension remains within bounded arithmetic, despite its ability to define all recursively enumerable trace sets; the source provides no resolution.