Fixed Complexity Separations in Bounded Arithmetic

Definitions and mathematical statement

Let $\alpha$ denote the additional predicate parameter appearing in the source's relativized bounded-arithmetic notation. Write $S\vdash\sigma$ when the theory $S$ proves the sentence $\sigma$, and $S\nvdash\sigma$ when it does not. The symbols $T_m(\alpha)$ and $\mathrm{APC}_2(\alpha)$ retain their source meanings; the supplied record does not specify their languages or axioms. In particular, no identification of $T_m(\alpha)$ with a differently indexed standard hierarchy is assumed.

The notation $\Sigma_k^b(\alpha)$ refers to the source's intended level of the bounded-formula hierarchy relative to $\alpha$. Under the usual universal-closure interpretation, a $\forall\Sigma_k^b(\alpha)$ sentence has the form $\forall\vec{x}\,\theta(\vec{x})$, where $\theta\in\Sigma_k^b(\alpha)$ and all free variables of $\theta$ are included in $\vec{x}$. The exact language and syntactic hierarchy are not defined in the supplied record and require confirmation.

Question. Is there a fixed complexity level $k$ such that $T_{2n+1}(\alpha)$ can be separated from $T_{2n}(\alpha)$ by a $\forall\Sigma_k^b(\alpha)$ sentence?

To make the likely uniform reading explicit, let $I$ be the intended set of admissible indices $n$, and let $K$ be the intended set of complexity indices $k$; neither set is specified in the supplied record. If separation means provability in the higher indexed theory and nonprovability in the lower indexed theory, the uniform formulation is \[ \exists k\in K\;\forall n\in I\;\exists\sigma_n\in\forall\Sigma_k^b(\alpha)\quad \left(T_{2n+1}(\alpha)\vdash\sigma_n \ \land\ T_{2n}(\alpha)\nvdash\sigma_n\right). \] Here the separating sentence may depend on $n$, while $k$ is independent of $n$. This display is a conditional interpretation: the source leaves the quantifier over $n$, its range, and the direction of separation implicit. It must not be treated as an unqualified replacement for the source question.

The source additionally asks, under the words "in particular," whether \[ \exists n\in I\;\exists\tau\in\forall\Sigma_1^b(\alpha)\quad \left(T_{2n}(\alpha)\vdash\tau \ \land\ \mathrm{APC}_2(\alpha)\nvdash\tau\right). \] This second question has an explicit provability direction in the supplied record. Its asserted relationship to the first question cannot be checked without the intended theory definitions and comparison results.

Short English statement

The problem asks whether one fixed bounded-formula complexity suffices to distinguish the indicated successive theory levels. It also asks whether some even indexed theory proves a universally closed $\Sigma_1^b(\alpha)$ sentence that $\mathrm{APC}_2(\alpha)$ does not prove. The theory definitions and the first question's quantification over $n$ need clarification.

Sources

• Supplied local UnsolvedMath registry record, permanent ID $30003658$, source problem code catalogue entry; project registry data/unsolvedmath/problems.json, with catalog/problems.json designated for additional existing records. This draft uses the supplied complete record; the registry files were not independently inspected.
• Supplied report citation: Mathematical Logic: Proof Theory, Constructive Mathematics (2018), Oberwolfach Reports, pp. 3121--3183, DOI 10.4171/owr/2017/53. https://doi.org/10.4171/owr/2017/53. The record assigns proposed year 2017 and describes the material as collected from workshop open-problem discussions. No individual proposer is supplied.
• Supplied literature source: Kolodziejczyk--Thapen, Approximate counting and NP search problems. https://arxiv.org/abs/1812.10771.
• Supplied literature source: Oberwolfach Report 53, bounded arithmetic. https://doi.org/10.4171/owr/2017/53.
• Literature assessment dated exactly 2026-08-21: the supplied curation labels the problem open and states that later work gives partial separations but not the requested general result. This is supplied dated curation derived from the OWR record, not an independently verified assessment. The record expressly requests independent verification of time-sensitive status and cited claims.
• The supplied statement status is corrected_verified; its accompanying explanation says that mathematical content was preserved while notation, typography, and sentence structure were repaired. This is source metadata, not independent mathematical verification of this draft.