Separations of theories in weak bounded arithmetic (Q1344280)

\textit{P. Clote} and the author introduced [in: Feasible mathematics. II (to appear)] the first-order theories \(\text{TAC}^ i\), \(\text{TNC}^ i\) and TLS. \(\text{TAC}^ i\), \(\text{TNC}^ i\) and TLS correspond to \(\text{AC}^ i\), \(\text{NC}^{i+ 1}\) and LSPACE, respectively. TAC is the union of the \(\text{TAC}^ i\) and corresponds to AC. The author calls these theories, together with related theories, weak bounded arithmetic. In this paper, he proves the following separation results: (1) separation of \(\text{TLS}(\alpha)\) and \(\text{TAC}^ 1(\alpha)\); (2) separation of \(\text{TAC}(\alpha)\) and \(S^ 1_ 2(\alpha)\); (3) separation of \(\text{TNC}^ i(\alpha)\) and \(\text{TAC}^{i+ 1}(\alpha)\). \(\text{TAC}^ i(\alpha)\), \(\text{TLS}(\alpha)\), \(\text{TNC}^ i(\alpha)\) and \(\text{TAC}(\alpha)\) are obtained from \(\text{TAC}^ i\), TLS, \(\text{TNC}^ i\) and TAC, respectively, by introducing a free-order variable \(\alpha\).