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.