Arithmetics within the Linear Time Hierarchy

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 }_i^{\mathsf{b}}$, 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}}_1^i$, $TL{S}_1^i$ and $TS{C}_1^i$. ${\breve{S}}_1^i$ consists of open axioms for the language symbols and length induction for one of our new classes, $SIU{T}_{i,1}^{\{p(|id|)\}}$. $TL{S}_1^i$ and $TS{C}_1^i$ are defined using axioms related to dependent choice sequences for formulas from two other classes within ${\Sigma }_i^{\mathsf{b}}$. We prove for $i\ge 1$ that $$TL{S}_1^i\subseteq TS{C}_1^i\subseteq {\breve{S}}_1^i{⪯}_{\forall B(SIT{T}_{i+1}^{\{p(|id|)\}})}TL{S}_1^{i+1}$$ and that the $SIT{T}_i^{\{p(|id|)\}}$-definable in $TL{S}_1^i$ (resp. $SIT{T}_i^{\{2^{p(||id||)}\}}$-definable in $TS{C}_1^i$) multifunctions are $L_1$-$FLOGSPAC{E}^{SI{T}_{i,1}}[wit]$ (resp. $L_1$-$FS{C}^{SI{T}_{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 }_i^{\mathsf{b}}$ formulas, $SI{T}_{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.

Need to fix proofs