\( \def\lefteqn#1{\rlap{\displaystyle{#1}}} \newcommand{\Hajek}{H\'{a}jek} \newcommand{\Hastad}{H{\aa}stad} \newcommand{\Pudlak}{Pudl\'{a}k} \newcommand{\Krajicek}{Kraj\'\i\v{c}ek} \newcommand{\Jerabek}{Je\v{r}\'{a}bek} \newcommand{\Kolodziejczyk}{Ko{\l}odziejczyk} \newcommand{\compfont}{\mathsf} \newcommand{\SIG}[1]{\hat\Sigma^{\compfont b}_{#1}} \newcommand{\SIB}[1]{\Sigma^{\compfont b}_{#1}} \newcommand{\SIGINFTY}[1]{\Sigma^{\compfont #1}_{\infty}} \newcommand{\ASIGINFTY}[1]{\mathcal{A}\Sigma^{\compfont #1}_{\infty}} \newcommand{\pSIB}[1]{p\Sigma^{\compfont b}_{#1}} \newcommand{\PI}[1]{\hat\Pi^{\compfont b}_{#1}} \newcommand{\PIB}[1]{\Pi^{\compfont b}_{#1}} \newcommand{\DELT}[1]{\hat\Delta^b_{#1}} \newcommand{\DELTB}[1]{\bigtriangledown_{#1}} \newcommand{\BOOL}{\compfont B} \newcommand{\UNIV}{\compfont U} \newcommand{\EXIST}{\compfont E} \newcommand{\LEX}{\compfont L} \newcommand{\PLS}{\compfont{PLS}} \newcommand{\FP}{\compfont{FP}} \newcommand{\PTIME}{\compfont{P}} \newcommand{\NP}{\compfont{NP}} \newcommand{\NC}{\compfont {NC}} \newcommand{\coNP}{\compfont{co}-\compfont{NP}} \newcommand{\PH}{\compfont{PH}} \newcommand{\polylog}{\compfont{polylog}} \newcommand{\SigmaP}[1]{\Sigma^{\compfont p}_{#1}} \newcommand{\SiP}[1]{\Sigma^{\compfont p}_{#1}} \newcommand{\PiP}[1]{\Pi^{\compfont p}_{#1}} \newcommand{\theoryfont}{\mathit} \newcommand{\BASIC}{\theoryfont{BASIC}} \newcommand{\LKB}{\theoryfont{LKB}} \newcommand{\LK}{\theoryfont{LK}} \newcommand{\EBASIC}{\theoryfont{EBASIC}} \newcommand{\IOpen}{\theoryfont{IOpen}} \newcommand{\LIOpen}{\theoryfont{LIOpen}} \newcommand{\TOCOMP}{\theoryfont{TOComp}} \newcommand{\TCOMP}[1]{\theoryfont{TComp}^{#1}} \newcommand{\IDelta}{\mbox{$\theoryfont{I}\Delta_0$}} \newcommand{\TT}[1]{\theoryfont{T}^{#1}_2} \newcommand{\TR}[1]{\theoryfont{\hat{T}}^{#1}_2} \newcommand{\ST}[1]{\theoryfont{S}^{#1}_2} \newcommand{\RT}[1]{\theoryfont{R}^{#1}_2} \newcommand{\RR}[1]{\theoryfont{\hat R}^{#1}_2} \newcommand{\CT}[1]{\theoryfont{\hat{C}}^{#1}_2} \newcommand{\quasip}{\theoryfont{\{2^{ \mathbf{ \dot{(||\id||)} } } \} }} \newcommand{\RFN}{\theoryfont{RFN}} \newcommand{\BPR}{\theoryfont{BPR}} \newcommand{\BDC}{\theoryfont{BDC}} \newcommand{\LLIND}{\theoryfont{LLIND}} \newcommand{\LIND}{\theoryfont{LIND}} \newcommand{\IND}{\theoryfont{IND}} \newcommand{\COMP}{\theoryfont{COMP}} \newcommand{\REPL}{\theoryfont{REPL}} \newcommand{\BB}{\theoryfont{BB}} \newcommand{\open}{\theoryfont{open}} \newcommand{\WIT}{\theoryfont{WIT}} \newcommand{\mathfnfont}{\mathrm} \newcommand{\K}{\mathfnfont{K}} \newcommand{\cons}[1]{\mathfnfont{cons}(#1)} \newcommand{\car}[1]{\mathfnfont{car}(#1)} \newcommand{\cdr}{\mathfnfont{cdr}} \newcommand{\cond}{\mathfnfont{cond}} \newcommand{\PAD}{\mathfnfont{PAD}} \newcommand{\CAT}{\mathfnfont{CAT}} \newcommand{\LSP}{\mathfnfont{LSP}} \newcommand{\MSP}[2]{\mathfnfont{\lfloor\frac{#1}{2^{#2}}\rfloor}} \newcommand{\MULT}{\mathfnfont{MULT}} \newcommand{\Interval}[3]{\mathfnfont{#1 \in [#2, #3)}} \newcommand{\BLK}{\mathfnfont{BLK}} \newcommand{\BIT}{\mathfnfont{BIT}} \newcommand{\OUT}{\mathfnfont{OUT}} \newcommand{\DMSB}{\mathfnfont{DMSB}} \newcommand{\PREV}{\mathfnfont{PREV}} \newcommand{\bit}[1]{\mathfnfont{BIT}(#1)} \newcommand{\bool}[1]{\mathfnfont{bool}(#1)} \newcommand{\longBool}[1]{\mathfnfont{lbool}(#1)} \newcommand{\Pair}[1]{\mathfnfont{pair}(#1)} \newcommand{\NOP}{\mathfnfont{NOP}} \newcommand{\Seq}{\mathfnfont{Seq}} \newcommand{\RIGHT}{\mathfnfont{right}} \newcommand{\ispair}{\mathfnfont{ispair}} \newcommand{\Len}{\mathfnfont{Len}} \newcommand{\modtwo}{\mathfnfont{mod2}} \newcommand{\id}{\mathfnfont{id}} \newcommand{\cl}{\mathfnfont{cl}} \newcommand{\proj}[2]{(#1)_{#2}} \newcommand{\vec}[1]{\mathbf{#1}} \newcommand{\bd}{\mathfnfont{bd}} \newcommand{\LAST}{\mathfnfont{LAST}} \newcommand{\SUB}{\mathfnfont{SUB}} \newcommand{\ov}{\overline} \newcommand{\proves}{\vdash} \newcommand{\sequent}{\rightarrow} \newcommand{\monus}{\frac{\cdot}{ }} \newcommand{\bigvw}{\mathop{\mathchoice% {\makebox[0pt][l]{$\displaystyle\bigvee$}\mbox{$\displaystyle\bigwedge$}}% {\makebox[0pt][l]{$\textstyle\bigvee$}\mbox{$\textstyle\bigwedge$}}% {\makebox[0pt][l]{$\scriptstyle\bigvee$}\mbox{$\scriptstyle\bigwedge$}}% {\makebox[0pt][l]{$\scriptscriptstyle\bigvee$} \mbox{$\scriptscriptstyle\bigwedge$}}}\limits} \newcommand{\IFF}{\Leftrightarrow} \newcommand{\AND}{\mathrel{\land}} \newcommand{\OR}{\mathrel{\lor}} \newcommand{\NOT}{\neg} \newcommand{\IMP}{\supset} \newcommand{\DAND}{\wedge\!\!\!\!\wedge} \newcommand{\DOR}{\vee\!\!\!\!\vee} \newcommand{\GN}[1]{\,\!^{\lceil}\!#1\,\!^{\rceil}} \newcommand{\HALF}[1]{\lfloor\frac{1}{2}#1\rfloor} \newcommand{\DIV}[2]{\lfloor\frac{#1}{#2}\rfloor} \newcommand{\LEQ}{\leq_l} \newcommand{\nat}{\mathbb{N}} \newcommand{\EQN}[1]{\begin{eqnarray*}#1\end{eqnarray*}} \newcommand{\EQ}[1]{\begin{eqnarray}#1\end{eqnarray}} \newcommand{\TQ}[1]{\hbox{$#1$}} \newenvironment{proof}% {\medskip \noindent {\it Proof.} }{$\Box$} \newcommand{\ignore}[1]{} \)

Normal Forms from Witnessing Arguments

Chris Pollett

Prague, Czech Republic

Nov, 2017

Introduction

One of the goals of bounded arithmetic is to develop logical theories capable of formalizing arguments from computational complexity in a uniform way.
Ideally, we want to find a minimal theory capable of carrying out an argument and, with luck, say that the argument is equivalent to the underlying principle used to define the theory.
Structurally classifying the kinds of formulas provable in a bounded arithmetic theory can help us with this task, and it can allow us to say when a theory is likely to be weaker than another.
Today, I'd like to look at some concrete normal forms for formulas provable in various bounded arithmetic starting from one that can be derived from an early result of Sam Buss, and then look at how these forms shed light on the relationships between weak theories of arithmetic.

Bounded Arithmetic Refresher

$\Sigma^b_0$ (aka $\Pi^b_0$) are the bounded arithmetic formulas whose quantifiers are all of the form
$(\forall x \leq |t|)$ or $(\exists x \leq |t|)$.
For $i>0$, $\Sigma^b_i$ (resp. $\Pi^b_i$) are the closure of the $\Pi^b_{i-1}$ (resp. $\Sigma^b_{i-1}$) formulas under conjunctions, disjunctions, $(\exists x \leq t)$ and $(\forall x \leq |t|)$ (for $\Pi^b_i$, $(\forall x \leq t)$ and $(\exists x \leq |t|)$).
The prenex variant of the $\Sigma^b_i$ formulas, the $\SIG{i}$-formulas, look like: $$(\exists x_1 \leq t_1) \cdots (Qx_i \leq t_i) (Qx_{i+1}\leq|t_{i+1}|)A$$ where $A$ is an open formula. So we have $i+1$ alternations, innermost being length-bounded.
A $\PI{i}$-formula is defined similarly but with the outer quantifier being universal.
BASIC is a fixed set of open formula axioms for the symbols $0$, $S$, $+$, $\cdot$, $x\# y := 2^{|x||y|}$, $|x| :=$ length of $x$, $\monus$, $\MSP{x}{i}$, $\leq$.
Because we have $\MSP{x}{i}$ and $\monus$ in the language, it is possible to define as a term $\beta_{a}(i, w)$, the function which projects out the $i$th block of $a$ bits out of $w$.
We can also define pairing and the function $\BIT(j, w)$ as a terms.
We add to BASIC, $L^mIND_{A}$ induction axioms of the form: $$A(0) \wedge \forall x<|t|_m[A(x) \IMP A(S(x))] \IMP A(|t|_m)$$ Here $t$ is a term made of compositions of variables and our function symbols and where we are using the definition $|x|_0=x$, $|x|_m=| |x|_{m-1}|$.
$\TT{i}$ is the theory $\BASIC$$+$$\Sigma^b_i$-$\IND$.
$\ST{i}$ is the theory $\BASIC$$+$$\Sigma^b_i$-$\LIND$.
$\RT{i}$ is the theory $\BASIC$$+$$\Sigma^b_i$-$\LLIND$.

Prenex Theories

It seems natural to ask if it makes any difference to define $\TT{i}$, $\ST{i}$, or $\RT{i}$ using $\SIG{i}$-$L^mIND$ rather than $\Sigma^b_i$-$L^mIND$.
For $\TT{i}$ and $\ST{i}$ it makes no difference as the prenex theory can prove the necessary sharply bounded quantifier exchnage principle and so can convert between prenex and non-prenex formulas. For $R^i_2$, it is not known.
We denote the prenex version of $\RT{i}$ by $\RR{i}$.
We write $\TR{i, \{|id|_m\} }$ for the theories $\BASIC$$+$$\SIG{i}$-$L^mIND$.

$\forall\Sigma^b_{i+1}$-Conservativity of $S^{i+1}_2$ over $T^i_2$

To show every $\Sigma^b_{i+1}$ formula provable in $S^{i+1}_2$ is in $T^i_2$ for $i \geq 1$, Buss 1990 (1987 Workshop Proceedings) introduced the notion of query definability:

A theory $R$ can $Q_i$-define the function $f(\vec{x})$ if and only if there is a $\Sigma^b_i$-formula $U(w,j, \vec{x})$, a term $t(\vec{x})$ and a $\Sigma^b_1$-defined function $f_{\star}$ of $S^1_2$ such that $R \proves (\forall x)(\exists w)DEF_{U,t}(w, \vec{x})$, where $DEF_{U,t}$ is the formula $$(\forall j < |t|)[\BIT(j,w) = 1 \IFF U(\LSP(w,j),j, \vec{x})],$$ and such that, for all $\vec{n}$, $w$ in `NN`, if $DEF_{U,t}(w, \vec{n})$ then $f(\vec{n}) = f_{\star}(w, \vec{n})$.
You can think of `w` in $DEF_{U,t}$ as encoding the answers to a sequence of queries to a $\Sigma^b_i$-oracle from which $f_{\star}$ computes in polynomial time an output.
Buss shows that all $FP^{\Sigma^p_i}$ functions are $Q_i$-defined in $T^i_2$.
As for $i \geq 1$, $S^1_2 \subseteq T^i_2$, and $S^1_2$ can define any p-time function, this amounts to showing $T^i_2 \proves (\forall x)(\exists w)DEF_{U,t}(w, \vec{x})$ for any $\Sigma^b_i$-formula $U$ and term $t$.
If we replace $\IFF$ in $DEF_{U,t}$ with $\IMP$, the formula becomes $\Sigma^b_i$, and we can use $\Sigma^b_i$-IND to get a maximal `w` satisfying this formula. Such a `w` not only has to have its `1` bits correct, but also its `0` bits and so gives us the result.
Buss then showed that the $Q_i$-definable functions are closed under composition, limited recursion, and bounded minimization.
These closure properties were used to show $T^i_2$ can carry out a witnessing argument with $Q_i$-definable witnesses based on any free cut-free, $S^{i+1}_2$ proof of a sequent $\Gamma \rightarrow \Delta$ of $\Sigma^b_{i+1}$-formulas, giving the conservativity result.

Extracting a Normal Form for $\Delta^b_{i+1}$-predicates

The following was not in Sam's paper, but follows from it.
A formula $A(\vec{x})$ is a $\Delta^b_{i+1}$ in $T^i_2$ if $T^i_2 \proves A(\vec{x}) \IFF A_\Sigma(\vec{x})$ and $T^i_2 \proves A(\vec{x}) \IFF A_\Pi(\vec{x})$ where $A_\Sigma(\vec{x})$ is $\Sigma^b_{i+1}$ and $A_\Pi(\vec{x})$ is $\Pi^b_{i+1}$.
In which case, $T^i_2 \proves \exists! y \leq 1 (\NOT A_\Pi(\vec{x}) \AND y = 0) \OR (A_\Sigma(\vec{x}) \AND y=1)$
As this is a $\Sigma^b_{i+1}$-formula, by Buss' result the existential is witnessed by a $Q_i$-definable function in $T^i_2$.
Let $A_{f_{\star}}(w, \vec{x}, y)$ be the $\Sigma^b_1$-graph of $f_{\star}$ used in this $Q_i$-definition.
Then the witnessing argument shows $A$ is provably equivalent to a formula of the form $C(\vec{x}, 1)$ and to $\NOT C(\vec{x}, 0)$ where $C(\vec{x}, y)$ is $$(\exists w \leq t)(DEF_{U,t}(w, \vec{x}) \AND A_{f_{\star}}(w, \vec{x}, y)).$$
On the other hand, given any $\Sigma^b_i$-formula, U, and any p-time 0-1 valued $f_{\star}$, $T^i_2$ can show the predicate defined as above by these is $\Delta^b_{i+1}$.

Related uses of Query Definability and Syntactic Normal Forms

Krajicek 1993 showed for $i\geq 1$ the $\Delta^b_{i+1}$-predicates $S^i_2$ are the class $P^{\Sigma^p_{i}}(\log)$.
Buss Hay 1991 showed $P^{\NP}(\log)$ predicates are exactly those computable by formulas of the form $\exists j \leq |k(x)|(A(j, x) \AND \NOT B(j+1, x))$ where $A$, $B$ are $\Sigma^b_1$.
Buss Krajicek and Takeuti 1993 showed $\forall\Sigma^b_{i+1}$-conservativety of $R^{i+1}_3$ over $S^i_3$ using a notion of query definability. Here the 3 indicates a language with $x \#_3 y = 2^{|x|\#|y|}$.
Pollett 1999 used a variant of query definability to characterize the $\hat\Sigma^b_{i+1}$-definable functions of $\hat{T}^{i, \tau}_2$ where $\tau$ is a collection of terms $\ell(x) \in O(|x|)$ these theories have induction up to.
This result shows these theories $\hat\Delta^b_{i+1}$-predicates can be provably converted in the theory to the form $(\exists v \leq \ell(s(x)))[A(x,v) \AND \NOT B(x,v + 1)]$ where where $A$, $B$, are $\hat\Sigma^b_{i}$, $\ell\in \dot \tau$. Here $\dot \tau$ is the closure of $\tau$ under polynomials.
For $S^i_2$ this shows its $\hat\Delta^b_{i+1}$-predicates can be written as $$(\exists v \leq |s(x)|)[A(x,v) \AND \NOT B(x,v + 1)]$$ and those of $\hat R^i_2$ can be written as $$(\exists v \leq ||s(x)||^k)[A(x,v) \AND \NOT B(x,v + 1)]$$ for some $k$.
Jerabek 2006 showed $S^1_2$ is $\forall\Sigma^b_1$-conservative over $T^0_2$ (in the language with $\lfloor x/2^i \rfloor$) by using a notion of definability by bit recursion which is related to query definability. This proof does not give a normal form for the $\Delta^b_1$-predicates of $S^1_2$ because the safe for bit recursion formula notion used do not seem to have a nice syntactic characterization.

$\ST{1}$ versus $\RT{1}$ and $\RR{1}$

Normal forms such as those on the previous slide point out structurally suggestive differences between theories.
They also make it easier to come up with universal encodings for the classes in question as one can just use a tuple of the encodings for the finite list of terms in the quantifiers in the prenex formulas as well as a term representing the open matrix.
Having such an encoding facilitates finite axiomatization results.
The results mentioned earlier don't apply to $\ST{1}$ and $\RT{1}$ whose $\SIG{1}$-definable formulas are $FP$ (Buss) and $FNC$ (Allen, Clote, Takeuti) respectively. Here $FNC$ are those functions computable by poly-size, poly-log depth circuit families.
Multifunction algebras for the $\SIG{1}$-definable formulas of $\RR{1}$ and $\TR{1, \{|id|_m\} }$ are known from Pollett (2000), but these complexity classes are not well studied and may be substantially weaker than $NC$.
Boughattas and Ressayre (2009) using a model theoretic technique have separated $\TR{1, \{|id|_3\} }$ from $\ST{1}$.
Cook-Kolokolova (2003), using a secord order theory, showed the $\forall\hat\Sigma^b_1$-consequences of $S^1_2$ are finitely axiomatized, but no such result is known for $\RT{1}$ or $\RR{1}$.
A normal form result for the $\forall\Sigma^b_1$-formulas of $\ST{1}$, $\RT{1}$, and $\RR{1}$ might help yield both finite axiomatization results as well as shed light on the relationships between these theories.

Bounded Choice Defined Theories

In a paper to appear in MLQ, I came up with theories for the $\forall\SIG{1}$-consequences of $\ST{1}$ and $\RR{1}$ based on bounded dependent choice axioms.
Let $\tau$ be a set of 1-ary nondecreasing terms $\ell(x) \leq |x|$, let $k \in \nat$. We write $\tau$-$\BDC$ for the theory consisting of $\hat{S}^{0}_2$ together with axioms $\BDC[\ell, t_{init}, t_{sel}, t_{rec}, t_{\mu}, b]$ of the form: \begin{eqnarray*} \lefteqn{(\exists w \leq 2^{\ell(b)\cdot(|b| +1)})(\forall i < \ell(b)) [(\beta_{|b|}(0, w) = \min(t_{init}(\vec{a}), b) \AND} \\ &&(t_{sel}(\beta_{|b|}(i, w), i, \vec{a}) > 0 \IMP \beta_{|b|}(i+1, w) = \min(t_{rec}(\beta_{|b|}(i,w),i,\vec{a}),b))\AND\\ &&(t_{sel}(\beta_{|b|}(i, w), i, \vec{a}) = 0 \IMP \beta_{|b|}(i+1, w)= \mu j<|b|( t_{\mu}(j,\beta_{|b|}(i,w),\vec{a})>0))]. \end{eqnarray*} where $\ell\in\tau$ and $t_{init}$, $t_{sel}, t_{rec}, t_{\mu}$ are $L_2$ terms.
$\BDC[\ell, t_{init}, t_{sel}, t_{rec}, t_{\mu}, b]$ roughly asserts the existence of a computation sequence whose members are computed from earlier members either by term application or by a $\mu$ operation.
We are using $\mu$ in the above to be suggestive, but it is an abbreviation. $a = \mu j < |b|(t(j, c) > 0)$ is shorthand for $$(\forall i \leq |b|)[((a <|b| \AND i < a) \IMP t(a,c)>0 \AND t(i, c) = 0) \AND \\(a =|b|\IMP(\forall k < |b|)(t(k,c) = 0))]$$

Bounded Choice Defined

We call our analog of query definability in this setting, bounded choice defined.
Let $\tau$ be a set of 1-ary nondecreasing terms, $\ell(x) \leq |x|$ and let $r(\vec a)$ be an $L_2$ term. We view $w$ as a sequence of $|r^+|$-bit long blocks.
To get the last block of bits from this sequence, define $$\LAST(w, r) = \min(\beta_{|r^+|}(\lceil |w|/|r^+| \rceil-1, w), r).$$
We say a function $f(\vec a) = y$ in a bounded arithmetic theory $T$ is $\tau$-bounded choice defined if there is a formula $\psi_f(w, \vec a, r)$ of the form: \begin{eqnarray*} \lefteqn{(\forall i < \ell(r^+))[(\beta_{|r^+|}(0, w)= \min(t_{init}(\vec a), r) \AND} && \\ &&(t_{sel}(\beta_{|r^+|}(i, w), i, \vec a) > 0 \IMP \beta_{|r^+|}(i+1, w) = \min(t_{rec}(\beta_{|r^+|}(i, w), i, \vec a), r)) \AND \\ &&(t_{sel}(\beta_{|r^+|}(i, w), i, \vec a) = 0 \IMP \beta_{|r^+|}(i+1, w) = (\mu j < |r^+|)( t_{\mu}(j,\beta_{|r^+|}(i, w), \vec a) > 0))]. \end{eqnarray*} where $\ell \in \tau$, $r(\vec a)$ and $t_{init}(\vec a)$, $t_{sel}(v, i, \vec a)$, $t_{rec}(v, i, \vec a)$, $t_{\mu}(j, v, \vec a)$ are terms, and if there is a term $\OUT_f(v, \vec a)$, computing from the last block $v$ of $w$ the output of $f$, such that $T$ proves $$\forall \vec a \exists! y \leq 2^{|r^+|}\exists! w \leq 2^{\ell(r^+)\cdot (|r^+| +1)} \psi_f(w, \vec a, r)\AND \OUT_f(\LAST(w, r), \vec a) = y$$ and $$\nat \models \exists w \leq 2^{\ell(r^+)\cdot (|r^+| + 1)} \psi_f(w, \vec a, r)\AND \OUT_f(\LAST(w, r), \vec a) = f( \vec a).$$

Conservativity and Normal Forms

By concatenating the computation sequences or by repeatedly carrying out such concatenations, one can get computation sequences for the closure of $\tau$-bounded choice defined functions closed under composition or $\tau$-limited recursion.
We can find single terms $t_{init}(\vec a)$, $t_{sel}(v, i, \vec a)$, $t_{rec}(v, i, \vec a)$, $t_{\mu}(j, v, \vec a)$ which compute the appropriate subsequence of these computation sequences based on $i$, hence, showing $\tau$-BDC proves its $\tau$-bounded choice defined functions closed under these operations.
The $\mu$-clause built into the bounded choice defined definition allows it to handle the sharply bounded $\forall$ cases of a witnessing argument.
Given this we can prove the following:
1. $\ST{1}$ is $\forall\SIG{1}$-conservative over $\{|\id|\}$-$\BDC$.
2. $\RR{1}$ is $\forall\SIG{1}$-conservative over $\cup_k\{||\id||^k\}$-$\BDC$.
We also get normal forms. Let $T$ be $\ST{1}$ or $\RR{1}$. Then $T$ proves every $\DELT{1}$-formula is equivalent to a $\SIG{1}$-formula of the form $C(\vec a, 1)$ and to a $\PI{1}$-formula equivalent to $\neg C(\vec a, 0)$ where $C(\vec a, b)$ is: \begin{eqnarray*} \lefteqn{(\exists w \leq 2^{\ell(r^+)|r^+ + 1|})(\forall i < \ell(r^+)))[ (\beta_{|r^+|}(0, w)= \min(t_{init}(\vec a), r(\vec a)) \AND} && \\ &&(t_{sel}(i, \vec a) > 0 \IMP \beta_{|r^+|}(i+1, w) = \min(t_{rec}(\beta_{|r^+|}(i, w), i, \vec a), r(\vec a))) \AND \\ &&(t_{sel}(i, \vec a) = 0 \IMP \beta_{|r^+|}(i+1, w) = \mu j < |r^+|( t_{\mu}(j,\beta_{|r^+|}(i, w), \vec a) > 0)) \AND \\ && \BIT(0, \LAST(w,r(\vec a))) = b]. \end{eqnarray*} where is $\ell := |id|$ when $T = \ST{1}$, and $\ell$ is of the form $||id||^k$ for some $k$ when $T=\RR{1}$, and where $r$, $t_{init}$, $t_{sel}, t_{rec}, t_{\mu}$, $\OUT$ are $L_2$ terms.

Finite Axiomatizations

To get our finite axiomatization result we defined a theory between a finitely axiomatize theory between $\hat{S}^0_2$ and $R^1_2$.
We showed both $\{|\id|\}$-$\BDC$ and $\cup_k\{||\id||^k\}$-$\BDC$ can bounded choice define a function $term(E, z, \vec{a})$ which provided $E$ is the code of a term in the language, $z$ is large enough, computes that term applied to $\vec{a}$.
From this we derived an axiom $UC$ which roughly says the $y$ computed as the output of the function $term$ exists.
Another axiom we used used was $BITMIN$ := $(\exists i \leq |a|)LEASTON(i, a)$
where $LEASTON(i, a)$ is:
$ \EQN{(\forall j < i)[ ( i < |a| \IMP \BIT(i, a) = 1 \AND \BIT(j, a) = 0) \AND \\ (i = |a| \IMP (\forall k < |a|) \BIT(k, a) = 0)].} $
We showed our variant of $BASIC$$+$$BITMIN$$+$$UC$ proves $\hat{S}^0_2$ and is contained in the $\forall\SIG{1}$-consequence of $R^1_2$.
From this we modified the $\BDC$ axioms to work with encoding of terms, $\BDC'$, and then got single $\SIG{1}$-axioms, $U$ and $U_k$ which respectively imply $\{|\id|\}$-$\BDC'$ and for fixed $k$, $\{||\id||^k\}$-$\BDC'$.
This allowed us to show the $\forall\Sigma^b_1$-consequences of $\ST{1}$ are finitely axiomatized, and if we add $\#_3$ to the language, that $\forall\Sigma^b_1(\hat{R}^1_3)$ is finitely axiomatized.

Conclusion

I tried to show $\RR{1}$ is not finitely axiomatized by showing $U_{k+1}$, is strictly stronger than the theory with $U_k$.
I was able to get a weak diagonalization result in the paper, but otherwise, didn't succeed.
One reason why I hoped this might be possible was the outermost quantifier for $U_k$ was bounded by a term of the form $2^{||r^+||^k|r^+|}$ as compared to one of the form $2^{||r^+||^{k+1}|r^+|}$ for $U_{k+1}$.
I hoped, without being able to prove, that there might be some kind of compression one could perform on the computation sequences (short iterations of $L_2$-terms) that might allow one to restrict the term $r$ in these bounds, and hence, prove a diagonalization result based on the length of the computation sequences the two theories could handle.
If you replace $\#$ with $x \#'y = 2^{||x||\cdot|y|}$, you can define a variants of $S^1_2$ and $\hat{R}^1_2$.
The variant of $S^1_2$ would roughly correspond to quasilinear time, the analog of $\hat{R}^1_2$ is now even weaker.
I think the BDC results I have given still go through, so I conjecture it might be easier to show the resulting $S^1_2$ and $\hat{R}^1_2$ variants are not finitely axiomatized.
Let me conclude by saying, I think these normal forms extracted from witnessing arguments are promising baby steps towards separations.