\(\text{Count}(q)\) does not imply \(\text{Count}(p)\) (Q1377601)

For a natural number \(p\), Count\((p)\) is the principle: if the set \(\{1,\dots ,n\}\) is partitioned by a \(\Delta_0\)-formula into disjoint sets, each of cardinality \(p\), then \(p\) divides \(n\). Ajtai proved that Count\((2)\) is not a theorem of \(I\Delta_0(f)\) -- bounded induction in the language of arithmetic with one additional function symbol [\textit{M. Ajtai}, Ann. Pure Appl. Logic 24, 1-48 (1983; Zbl 0519.03021)]. Ajtai also asked, for which \(p\) and \(q\) Count\((p)\) implies Count\((q)\) over the same theory. Riis answers the question completely by proving the following theorem: Let \(\mathcal T\) be any system of Bounded Arithmetic over some countable language \(L\) which contains at least one undefined relational symbol. Suppose that all terms in \(\mathcal T\) have polynomial growth rate. Then, for all \(p,q\in\mathbb{N}\) the following are equivalent: (a) There is a model \(M\) of \(\mathcal T\) in which Count\((q)\) holds and Count\((p)\) fails; (b) There exists a prime factor of \(p\) which does nor appear in \(q\). Corollaries include a variant of the theorem formulated for \(\text{ACA}^{\text{top}}\) -- a system of second order arithmetic with a top element, and a result concerning the size of proofs of ``Count\((q)\) implies Count\((p)\)'' in Frege proof systems. The main idea of the paper is the reduction of Count\((p)\) to properties of forests of some special labelled trees. Then, to solve the problem, purely combinatorial techniques are applied to prove the existence of some ``exceptional'' forests. The result is a highly nontrivial solution of a difficult problem. It uses an array of tools combining forcing in arithmetic and boolean circuit theory. It is a very interesting paper, the reader should be warned however, this is not an easy reading. Some more careful proofreading and editing could have helped.