\( \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{\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]{} \)

On the Finite Axiomatizability of Prenex $R^1_2$

Chris Pollett

Banff, Canada

Oct, 2011

Motivations

$S^1_2$ is a bounded arithmetic theory whose $\hat\Sigma^b_1$-definable function correspond to polynomial time computable functions, the class $FP$.
$R^1_2$ is a bounded arithmetic theory whose $\hat\Sigma^b_1$-definable function correspond to functions computable by polylog-depth polynomial-sized circuit families, the class $FNC$.
Although not as great maybe as showing $\NC \neq P$, proving a separation of $R^1_2$ from $S^1_2$ would imply new lower bounds on the provability of complexity problems. For instance, that $R^1_2$ can't prove $\NP = \coNP$ or that $R^1_2$ can't the collapse of polynomial hierarchy.
Unfortunately, both these classes of functions and bounded arithmetic theories seem difficult to separate.
However, if you look at the "prenex" version of $R^1_2$ you get a theory whose $\hat\Sigma^b_1$-consequences seem a fair bit weaker than $FNC$, so there seems to be some hope to separate this theory from $S^1_2$.
This talk is about trying to come up with a good way to describe the $\hat\Sigma^b_1$-consequences of prenex $R^1_2$ that might lead to a separation result.

First-order Bounded Arithmetic

The bounded arithmetic theories we will be looking at have BASIC axioms like: \begin{eqnarray} y\leq x &\IMP & y \leq S(x)\\ x+Sy &=& S(x+y)\\ &\ldots& \end{eqnarray} for the symbols $0$, $S$, $+$, $\cdot$, $x\# y := 2^{|x||y|}$, $|x| :=$ length of $x$, $\monus$, $\MSP{x}{i}$, $\leq$
We add to this base theory $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}|$.

String Manipulation, Collection/Replacement axioms

Because we have $\MSP{x}{i}$ 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 will also use later that we can define pairing and the function $\BIT(j, w)$ as a terms.
Besides induction another scheme known as $\BB_A$ or $\REPL_A$: $$(\forall x \leq |s|)(\exists y \leq t(x)) A(x,y) \IMP (\exists w \leq \bd(t^+, s))(\forall x \leq |s|) \beta_{|t^+|}(x,w) \leq t(x) \AND A(x,\beta_{|t^+|}(x,w)) $$ will also be considered in this talk as it allows us to do a limited amount of quantifier exchange. Here $t^+$ is a monotone term derived from $t$. $\bd(t^+, s)$ is a term used to a string of consisting of concatenating $|s|$ strings of length $|t^+|$.

Bounded Arithmetic Theories

$\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.
$\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 $\BB\Sigma^b_i$ 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$.

Definability

Let $\Psi$ be a class of formulas, we say a theory $T$ can $\Psi$-define a function $f$ if there is a $\Psi$-formula $A_f$ such that
$$T \proves \forall x \exists! y A_f(x, y)$$ and $$\nat\models \forall x A_f(x, f(x))$$

Recapping + What's Known

As we said earlier, the $\SIG{1}$-definable function of $\ST{1}$ and $\RT{1}$ are $\FP$ (Buss) and $FNC$ (Allen, Clote, Takeuti) respectively.
Multifunction algebras for the $\SIG{1}$-definable multifunctions of $\RR{1}$ and $\TR{1, \{|id|_m\} }$ are known from Pollett (2000).
That paper also used a Johannsen-style block counting argument to show for $m \geq 4$ the multifunction algebra one gets cannot define $\lfloor \frac{x}{3}\rfloor$.
Boughattas and Ressayre (2009) using a model theoretic technique then separated $\TR{1, \{|id|_3\} }$ from $\ST{1}$.

One Possible Separation Approach...

Jerabek (2006) showed $\ST{1}$ was $\Sigma^b_1$-convervative over $T^0_2$.
For $i \geq 1$, Pollett (1999) had a result that $\TT{i, \{2^{p(||id||)}\}} \preceq_{\forall\SIG{i+1}} \RT{i+1}$.
Here the $\{2^{p(||id||)}\}$ indicates the bound on induction.
So it was natural to conjecture Jerabek's techniques could be used to show that $\TT{0, \{2^{p(||id||)}\}} \preceq_{\forall\SIG{1}} \RR{1}$.
The hope would be then that some weaker notion of definability might then be used to separate $\TT{0, \{2^{p(||id||)}\}}$ from $\TT{0}$, and hence separating $\RR{1}$ from $\ST{1}$.

... That doesn't seem to work.

Pollett (2011) shows $\TT{0, \{2^{p(||id||)}\}}$, again by a block counting argument, can't define $\lfloor \frac{x}{3}\rfloor$.
It is unknown if $\RR{1}$ can define $\lfloor \frac{x}{3}\rfloor$. Certainly, $\RT{1}$, which can define all functions in $FNC$, can.
However, if you look take an $\TT{0, \{2^{p(||id||)}\}}$ induction axiom and prenexify it, it has an outer existential that is of size $2^{p(||id||)}$ which is too small to be able to express a string that codes the steps of a computation of the kind of functions $\RR{1}$ can $\SIG{1}$-define. So it is at least unlikely that $\TT{0, \{2^{p(||id||)}\}}$ is conservative under $\RR{1}$.
Pollett (2011) formulates a messy variant of a comprehension axiom called $\open_{\{||id||\}}$-$\COMP$ (will describe in a moment) which when added to $\LIOpen$ ($\BASIC$$+$$\open$-$\LIND$) suffice to carry out Jerabek's method and give a $\SIG{1}$-conservative subtheory of $\RT{1}$.
There were earlier $\SIG{1}$ theories for the functions in $\NC$. For example, $TNC$ of Clote Takeuti and RSUV isomorphisms of $VNC$ of Cook Nguyen. The point here was to be able to carry out a modified Jerabek's construction. A later hope was that this could be modified to $\RR{1}$ with the goal to come up with as simple and breakable an axiomatization of $\forall\SIG{1}(\RR{1})$ as possible.

A New Strategy on $\RR{1}$ and $\RT{1}$ versus $\ST{1}$

The function algebra for the $\SIG{1}$-definable functions of $\RR{1}$ consists of initial functions of the language, the functions $\mu i \leq |a| t(i,a, \vec{b}) = 0$ for some term in the language (use $\PI{0}$-$\LIND$ to get), closure under composition and under the following kinds of recursion:
$ \EQN{ F(0,x) &=&g(x)\\ F(n+1,x)&=&min(h(n,x,F(n,x)),r(n,x))\\ f(n,x) &=& F(||t(n,x)||,x) }$
To get the $\SIG{1}$-definable functions, $FP$, of $\ST{1}$ switch $|| \cdot||$ to $|\cdot|$. For $\RT{1}$, one adds to this closure under another kind of recursion called $CRN$.
Expressed as a function algebra it seems hard to do things like diagonalization to separate these algebras.
So ideally we want to get a normal form for the functions in these classes.
Even if we can't separate the classes, and hence the original theories, the normal form will at least tell us something about finite axiomatization in the theories.

Axiomatisations for $\forall\SIG{1}(\RR{1})$, $\forall\SIG{1}(\RT{1})$, and $\forall\SIG{1}(\ST{1})$

We begin with $BASIC$. To this we add the following $BITMIN$ axiom $(\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)].} $
This axiom can be proven in $\RR{1}$ using $\PI{0}$-$\LIND$, on the other hand it give us the sharply bounded $\mu$-operator for terms.
Next we add for each term $t$ a bounded dependent choice axiom, $\BDC_{\ell, t}$
$ \EQN{(\exists w \leq \bd(d, b))(\forall i < \ell(b))[\beta_{|d|}(0, w)= \min(a, d) \AND \\ \qquad\qquad t > 0 \IMP \beta_{|d|}(i+1, w) = min(t(\beta_{|d|}(i, w) , i, a, b, c) \monus 1, d) \AND\\ \qquad t = 0 \IMP LEASTON(\beta_{|d|}(i+1, w), \beta_{|d|}(i, w))].} $
where $\ell$ is $|x|$ if we want $\forall\SIG{1}(\ST{1})$ or of the form $||x||^k$ if we want $\forall\SIG{1}(\RR{1})$.
For $\forall\SIG{1}(\RT{1})$ you need in addition to add to $\BDC_{\ell, t}$ another clause to handle $CRN$.

Remarks

These are $\forall\SIG{1}$ axioms and can be proven in the theory they correspond to by a straightforward induction argument.
Let $ChoiceStr_{\ell}(w,a,b,c, d)$ the formula inside the $(\exists w \leq \bd(d, b))$ in a $\BDC_{\ell, t}$. Let $f(x,z)$ be a function, we say $f(x, z)$ is $\ell$-choice defined if
$$f(x, z) = y \IFF (\exists w \leq \bd(2^{|s|}, t))[ChoiceStr_{\ell}(w, x, t, z, 2^{|s|}) \AND OUT_f(w, x, z) = y]$$ for some terms $t, s$ not involving $w$, and for some term $OUT_f$.
To show the conservativity result, you need to show the class of $||\cdot||^k$- (resp. $|\cdot|$-)choice defined functions have the necessary closure properties to carry out a witnessing argument.
This gives that the $\SIG{1}$-definable functions of $\RR{1}$, $\RT{1}$, $\ST{1}$ are just projections of these kind of choice strings.
The main difference in the above and my 2011 Archive paper is that there I was working with open formulas rather than terms. This meant I had to define in an inductive fashion the open-formulas that would be suitable for the computation of a choice string.
The set-up above looks very promising for diagonalization provided we could come with a nice universal predicate for choice strings.

Finite Axiomatizations

Pairing, etc can be defined as terms in our language and using this we can give an encoding for terms as numbers.
You could imagine adding a parameter $e$ and modify our $ChoiceStr_{\ell}$ so that instead of having
$$\beta_{|d|}(i+1, w) = min(t(\beta_{|d|}(i, w) , i, a, b, c) \monus 1, d)$$
we say that after $\beta_{|d|}(i, w)$, $w$ codes a string which computes the operations according to the term coded by $e_t$ until we get to what would have been $\beta_{|d|}(i+1, w)$.
Writing this down, one would get a single $\SIG{1}$-formula $U(e_t, a, b, c, d)$ which for different codes $e_t$ would imply $\BDC_{|id|, t}$. This gives an alternative proof to Cook-Kolokolova (2003) that $\forall\SIG{1}(\ST{1})$ is finitely axiomatized.
In the case of $\RR{1}$ and $\RT{1}$ you get a sequence of formulas $U_k(e_t, a, b, c, d)$ for different values of $k$ in
$||\cdot||^k$.

Conclusion

I conjecture that the theory, which over the base theory has the axiom $U_{k+1}$, is strictly stronger than the theory with $U_k$. I.e., $\forall\SIG{1}(\RR{1})$ and $\forall\SIG{1}(\RT{1})$ are not finitely axiomatised.
For $\RT{1}$ these formulas probably correspond to hard problems at various levels of the $NC^k$ hierarchy, so are likely hard to separate.
The $d$ parameter in $U_k(e_t, a, b, c, d)$ would typically be of the form $2^{|x|^e}$ and bounds the intermediate terms occuring in the choice string computation. Since it depends on $e$ we can't immediately do diagonalization.
However, maybe in $\RR{1}$ there is some clever way to compress the intermediate steps (as they are just given by terms) to within some $2^{|x|^c}$ for fixed ??? I end my talk with that open problem.