Parameter-free induction in bounded arithmetic

ABSTRACT. In the area of strong fragments of Peano arithmetic, it proved fruitful to study not just the usual induction fragments~$I\Sigma_i$, but also fragments axiomatized by \emph{parameter-free} induction schemata \[\tag{$\fii\text-\indf$}\fii(0)\land\forall x\,(\fii(x)\to\fii(x+1))\to\forall x\,\fii(x)\] where $\fii$ has no free variable other than~$x$, and theories axiomatized using the closely related induction \emph{inference rules} \[\tag{$\fii\text-\indr$}\frac{\fii(0,\vec y)\quad\fii(x,\vec y)\to\fii(x+1,\vec y)}{\fii(x,\vec y)}.\] See e.g.~\cite{kpd,bekl:indru,bekl:parfree}; in particular, the last two papers detail the connection of induction rules and parameter-free schemata to reflection principles.

In contrast, induction rules and parameter-free schemata have been largely ignored in bounded arithmetic literature. Apart from $IE_i^-$ briefly discussed in~\cite{kaye:dio}, the corresponding fragments of Buss's~$S_2$ were only studied in~\cite{bloch,cffmlm}. Many basic questions about these fragments were disregarded, in particular, neither paper even mentions $\pii i$-induction rules and parameter-free schemata, despite that they could be expected to behave rather differently from $\sig i$ rules by analogy with the case of strong fragments.

In this talk, we will try to systematically investigate parameter-free and inference rule versions of the theories $T^i_2$ and~$S^i_2$: that is, $\sih i\text-\indf$, $\pih i\text-\indf$, $\sih i\text-\indr$, $\pih i\text-\indr$, and the corresponding variants of~$\pind$. (While there are many other ways how to make parameter-free schemata or rules out of the various induction or minimization schemata equivalent to $S^i_2$ or~$T^i_2$, most turn out to be equivalent to one of those above; in particular, parameter-free \emph{rules} $\sih i/\pih i\text-\ppind^{R-}$ are equivalent to their versions with parameters.)

We will particularly focus on the following questions: \begin{itemize} \item Reductions between the various rules and schemata. (A rule $R$ reduces to a rule~$R'$ if $T+R\sset T+R'$ for every theory $T\Sset\tpv$.) See Fig.~\ref{fig:rules} for a summary. \item Conservativity results between the fragments, and the formula complexity of axioms. \item The number of instances (nesting) of~$R$ needed to generate the closure $T+R$, and finite axiomatizability of fragments. \item Reformulation of axioms and rules in terms of reflection principles for propositional proof systems. \item Conditional or relativized separations between the fragments. \end{itemize}