Arithmetics within the Linear Time Hierarchy

TL;DR

This paper explores specific fragments of arithmetic within the linear time hierarchy, defining new classes and proving their properties and relationships, with implications for complexity theory and foundational questions.

Contribution

It introduces new syntactic classes of arithmetic, defines associated arithmetics, and establishes their relationships and definability properties, advancing understanding of the linear time hierarchy.

Findings

Defined new classes $reve{S}^{i}_{1}$, $TLS^i_1$, $TSC^i_1$ within arithmetic.

Proved inclusion relations among these classes and their definability properties.

Established independence results related to complexity class separations.

Abstract

We identify fragments of the arithmetic $S_1$ that enjoy nice closure properties and have exact characterization of their definable multifunctions. To do this, in the language of $S_1$, $L_1$, starting from the formula classes, $\Sigma^{\mathsf b}_{i}$, which ignore sharply bounded quantifiers when determining quantifier alternations, we define new syntactic classes by counting bounded existential sharply bounded universal quantifiers blocks. Using these, we define arithmetics: $\breve{S}^{i}_{1}$, $TLS^i_1$ and $TSC^i_1$. $\breve{S}^{i}_{1}$ consists of open axioms for the language symbols and length induction for one of our new classes, $SIUT_{i,1}^{\{p(|id|)\}}$. $TLS^i_1$ and $TSC^i_1$ are defined using axioms related to dependent choice sequences for formulas from two other classes within $\Sigma^{\mathsf b}_{i}$. We prove for $i \geq 1$ that $$TLS^i_1 \subseteq TSC^i_1 \subseteq \breve{S}^{i}_{1} \preceq_{\forall B(SITT_{i+1}^{\{p(|id|)\}})} TLS^{i+1}_1$$ and that the $SITT_{i}^{\{p(|id|)\}}$-definable in $TLS^i_1$ (resp. $SITT_{i}^{\{2^{p(||id||)}\}}$-definable in $TSC^i_1$) multifunctions are $L_1$-$FLOGSPACE^{SIT_{i,1}}[wit]$ (resp. $L_1$-$FSC^{SIT_{i,1}}[wit]$). These multifunction classes are respectively the logspace or $SC$ (poly-time, polylog-space) computable multifunctions whose output is bound by a term in $L_1$ and that have access to a witness oracle for another restriction on the $\Sigma^{\mathsf b}_{i}$ formulas, $SIT_{i,1}$. For the $i=1$ cases, this simplifies respectively to the functions in logspace and $SC$, Steve's Class, poly-time, polylog-space. We prove independence results related to the Matiyasevich Robinson Davis Putnam Theorem (MRDP) and to whether our theories prove simultaneous nondeterministic polynomial time, sublinear space is equal to co-nondeterministic polynomial time, sublinear space.