\(
\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]{}
\)
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_{i1}$ (resp. $\Sigma^b_{i1}$) 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}\leqt_{i+1})A$$
where $A$ is an open formula. So we have $i+1$ alternations, innermost being
lengthbounded.
 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^{xy}$, $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_{m1}$.
 $\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 nonprenex
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
ptime 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 cutfree, $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 ptime 01 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 polysize,
polylog 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}$.
 CookKolokolova (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 1ary 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 1ary 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^+ \rceil1, 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:
 $\ST{1}$ is $\forall\SIG{1}$conservative over $\{\id\}$$\BDC$.
 $\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^+^kr^+}$
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\cdoty}$, 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.