This paper solves an open problem in the field of bounded arithmetic. Bounded arithmetic is an area developed for the logical analysis of the expressive properties of the polynomial hierarchy in theoretical computer science [1]. Fragments of bounded arithmetic can express exactly the problems/functions expressible in the hierarchy, which contains, among many others, the classes P, NP, and PSPACE. In particular, there are two families of theories in bounded arithmetic that are of interest, namely the families Si2 and Ti2 [2], which differ by the induction schema allowed. The main problem in this setting is to separate the elements of these families by means of a formula that can be proved in a theory of order i, but cannot be proved at an earlier order i’ < i. It is not known, for instance, if the first element S12 is separable from any other element in the S12 hierarchy, but it is known that Ti2 proves S12 and S{i+1}2 proves Ti2 for i ≥ 0.
The polynomial hierarchy can be relativized by allowing queries to an oracle &agr;; similarly, the bounded arithmetic families can also be relativized to Si2&agr; and Ti2&agr;. This paper deals with the relativized setting in which the oracle &agr; can answer any polynomial time query, and the class T12&agr;. It is assumed that the elements of the relativized families differ in their capability of performing approximate counting.
In fact, this approach for trying to show separation results based on approximate counting started in [3]. Prior to that, separation was attempted based on the expressivity of the theories in the families Si2 and Ti2. There are many theories of approximate counting; this paper deals with two of them.
One form of counting is a weak version of the pigeonhole principle (sWPHP), which states that there is no way of subjectively mapping n pigeons to n2 holes. The other form of counting is called the Herbrandized order principle (HOP), which basically states that if there is a strict linear order on the elements of the integer interval [1, n] and a function h on that interval into itself, then some element of the interval is not h-mapped to its immediate predecessor.
The main result of the paper shows that, in the relativized setting over polynomial time oracle &agr;, T12&agr; + sWPHP&agr; cannot prove HOP&agr;. This implies that there is a separation in the polynomial hierarchy, in the relativized setting. In fact, Buss et al. show such a result with a different, stronger version of the WPHP problem [3]. Furthermore, it was conjectured there if separation holds for a weaker version of the PHP, namely sWPHP.
The paper solves positively that conjecture, so that separation with a weaker form of the PHP problem yields a stronger result of separation. The main strategy for the proof is to show some properties about the universal formulas that can be proved by T12&agr; + sWPHP&agr;. The larger part of the paper is dedicated to showing that proving HOP would contradict such properties. The proof is quite technical, as expected, and uses several results from the literature on proof theory and bounded arithmetic. It also introduces a particular kind of tree to compute a function whose existence leads to the impossibility of proving HOP.
The paper closes by presenting two statements about the existence of “narrow proofs” for the propositional version of HOP, obtained from the bounded arithmetic version used in the body of the paper. It is claimed that one such property can be falsified by the techniques of the paper, while nothing can be said about the second property, thus showing possible ramifications and applications of the proof theoretical techniques developed in this paper.
