# Proofs in $S_{2}^{1}$

In a talk by Razborov, a curious little statement is posted.

If FACTORING is hard, then Fermat’s little theorem is not provable in $S_{2}^{1}$.

What is $S_{2}^{1}$ and why are current proofs not in $S_{2}^{1}$?

$S^1_2$ is a theory of bounded arithmetic, that is, a weak axiomatic theory obtained by severely restricting the schema of induction of Peano arithmetic. It is one of the theories defined by Sam Buss in his thesis, other general references include Chapter V of Hájek and Pudlák’s Metamathematics of first-order arithmetic, Krajíček’s “Bounded arithmetic, propositional logic, and complexity theory”, Buss’s Chapter II of the Handbook of proof theory, and Cook and Nguyen’s Logical foundations of proof complexity.

You can think of $S^1_2$ as a theory of arithmetic which has induction only for polynomial-time predicates. In particular, the theory does not prove that exponentiation is a total function, the theory can prove to exist only objects of polynomial size (loosely speaking).

All known proofs of the Fermat Little Theorem utilize either exponential-size objects, or they rely on exact counting of sizes of bounded sets (which is probably not definable by a bounded formula, i.e., in the polynomial hierarchy, because of Toda’s theorem).

The result on FLT, $S^1_2$, and factoring stems from Krajíček and Pudlák’s paper Some consequences of cryptographical conjectures for $S^1_2$ and EF, and in my opinion it is fairly misleading. What Krajíček and Pudlák prove is that if factoring (actually, IIRC they state it for RSA instead of factoring, but it’s known that a similar argument works for factoring too) is hard for randomized polynomial time, then $S^1_2$ cannot prove the statement that every number $a$ coprime to a prime number $p$ has finite exponent modulo $p$, that is, there exists $k$ such that $a^k\equiv1\pmod p$.

It’s true that this is a consequence of FLT, but in fact it is a much, much weaker statement than FLT. In particular, this statement follows from the weak pigeonhole principle, which is known to be provable in a subsystem of bounded arithmetic (albeit a stronger one than $S^1_2$). Thus, Krajíček and Pudlák’s argument shows that $S^1_2$ does not prove the weak pigeonhole principle unless factoring is easy, and as such provides a conditional separation of $S^1_2$ from another level of the bounded arithmetical hierarchy, say $T^2_2$.

In contrast, the actual FLT does not even seem to be provable in full bounded arithmetic $S_2=T_2$, but this is not related to cryptography. You can find some relevant discussion in my paper Abelian groups and quadratic residues in weak arithmetic.

• Hi Emil: Thankyou for the complete answer. Pardon me for asking again. You write "All known proofs of the Fermat Little Theorem utilize either exponential-size objects, or they rely on exact counting of sizes of bounded sets (which is probably not definable by a bounded formula, i.e., in the polynomial hierarchy, because of Toda’s theorem)." But flt is about $a^{k}$ modulo $p$ and $a^{k}$ is itself an exponential object? – T.... Mar 27 '13 at 14:08
• That’s right, but you don’t really need $a^k$ to formulate Fermat’s little theorem. Given $a$, $k$, and $p$ in binary, you can compute $a^k\bmod p$ in polynomial time by repeated squaring, and the results I mentioned concern a formulation of FLT using this polynomial-time function. – Emil Jeřábek Mar 27 '13 at 14:17
• The factorial conjecture says that similar products shouldn’t be efficiently computable, specifically computing $m!\bmod n$ is as hard as factoring $n$, so this is unlikely to help. Note that even if the product were computable by a polynomial-time algorithm and you could formalize it in $S^1_2$, it is still rather non-obvious how to prove that such exponentially long products are invariant under permutation of the multiplicands (which is the main property used in the wiki proof). – Emil Jeřábek Mar 27 '13 at 21:21
• No, it wouldn’t suffice. Commutativity only tells you that the product of two terms can be permuted. For longer products, you’d have to set up some kind of an argument by induction, which would need to involve products of a more complicated structure than just the modular arithmetic sequences used in the original product (such as $$\prod_{i=1}^{p-1}\begin{cases}ia&\text{if }(ia\bmod p)<k\\1&\text{otherwise}\end{cases}$$ or something of this sort). If it helps your imagination, while the products look finite, in a nonstandard model of arithmetic the index set $[1,p-1]$ is really infinite, ... – Emil Jeřábek Mar 28 '13 at 12:09
• ... and it’s not even a well-ordered sequence (it contains a copy of $\mathbb Q$). – Emil Jeřábek Mar 28 '13 at 12:12