Construction of models of bounded arithmetic by restricted reduced powers (Q506954)

The paper is devoted to models of bounded arithmetic. The general aim is to construct extensions of models that preserve the set of lengths (and, consequently, polynomial-time computable properties) and satisfy some amount of bounded induction, yet are not elementary, so that they can be utilized, e.g., to prove independence results. Specifically, the author studies variants of \textit{restricted reduced powers}. He presents two constructions of such powers. Construction A is simple, but appears to be of limited applicability; nevertheless, the author shows how it can be used to reprove a form of Buss's witnessing theorem. Construction B is technically more complicated (both in the statement and in the proof), but it is more flexible than Construction A. The paper includes an interesting application of Contruction B to the open problem of separating the theory \(R^1_2\) from its strict variant: it is shown in the relativized setting that \(\mathrm{strict }R^1_2(\alpha)\neq R^1_2(\alpha)\), assuming that the existence of one-way permutations is hard for polynomial-size circuits (on any non-negligible subset of the domain). In fact, the author proves that under this assumption \(\mathrm{strict }R^1_2(\alpha)\) does not prove the bounded choice/collection/replacement schema \(\mathrm{BB }\Sigma^b_1(\alpha)\), which is well known to be provable in \(R^1_2(\alpha)\). Furthemore, if one can find such a one-way permutation definable by a term in the language of \(R^1_2\), we obtain even the unrelativized separation \(\mathrm{strict }R^1_2\neq R^1_2\).