# Bounded Arithmetic and Counting

Let $\mathcal{L}=\{0,S,+,\cdot,=,<,X,R,S\}$ be the language of arithmetic with three additional predicate symbols $X(v)$, $R(v,u)$ and $S(v,u)$.

Let $\phi(x),\psi(x,y)$ and $\eta(x,y)$ be formulas in $\mathcal{L}$. Define the formula $\Theta_e(\phi,\psi,\eta)$ in $\mathcal{L}$ for some $e\in \mathbb{N}$ which says:

1. $\phi(0)$
2. $\psi$ is a partition of $\{x:\phi(x)\}$ into classes of size $e$.
3. $\eta$ is a partition of $\{x:\phi(x)\land \neg x=0\}$ into classes of size $e$.

Theorem. For every fix prime number $p,q\in \mathbb{N}$, ${\bf I}\Delta_0(R,S,X)+\Theta_p(R,S,X)+\{\neg \Theta_q(R',S',X'):R',S',X'\in \Delta_0(R,S,X)\}\not \vdash \bot$

Proof. One of the proofs of this theorem can be found here.

Q1. Is there any similar result for counting modulo a composite number? For example is ${\bf I}\Delta_0(R,S,X)+\Theta_7(R,S,X)+\{\neg \Theta_6(R',S',X'):R',S',X'\in \Delta_0(R,S,X)\}$ consistent?

Q2. Suppose that the theory above is consistent. Does it imply separation of complexity classes like $AC_0[6]$ and $NP$?

Q1: Yes. The paper you linked to in the question actually proves the theorem for every pair of natural numbers $p,q$ such that $p$ has a prime factor that does not divide $q$ (in other words, $p$ does not divide any power of $q$).
Q2: No. Even at the best of times, you'd only get the conclusion that the classes are different in some model of the theory, not necessarily the standard model. However, the theory here is too weak even for that. Passing to the second-order language as used e.g. by Cook and Nguyen, you'd need to prove separation from the theory $V^0(6)$ to make things work. Your schema consists of instances of the $\forall\Sigma^B_0$ mod-6 counting axiom, which is weaker than the $\forall\Sigma^B_1$ axiom of $V^0(6)$ asserting the existence of suitable mod-6 counting functions.
• Ah! you are right!. I thought that paper proves the case for $p$ and $q$ are both prime. By the way, by separation from $V^0(6)$, you mean proving consistency $V^0(6)+\Theta_7(R,S,X)$ or separating it from another theory? Jan 23, 2017 at 15:13
• Depends on what exactly you want. If $V^0(6)\ne V^1$, then $V^0(6)$ has a model in which $\mathrm{AC^0[6]\ne NP}$. If $V^0(6)\nsupseteq V^0(7)$ (which is a stronger assumption), it even has a model where $\mathrm{AC^0[6]\nsupseteq AC^0[7]}$. Since $V^0(7)\vdash\neg\Theta_7$, the consistency of $V^0(6)+\Theta_7$ is a yet stronger assumption. Jan 23, 2017 at 16:57
• Thank you very much. Do you know why something like Ajtai forcing or similar arguments do not work for proving $V^0(6) \not = V^1$? Jan 23, 2017 at 17:53