<p>$S^1_2$ is a theory of bounded arithmetic, that is, a weak axiomatic theory obtained by severely restricting the schema of induction of <a href="http://en.wikipedia.org/wiki/Peano_arithmetic#First-order_theory_of_arithmetic">Peano arithmetic</a>. It is one of the theories defined by Sam Buss in his <a href="http://www.math.ucsd.edu/~sbuss/ResearchWeb/BAthesis/">thesis</a>, other general references include Chapter V of Hájek and Pudlák’s <a href="http://projecteuclid.org/euclid.pl/1235421926">Metamathematics of first-order arithmetic</a>, Krajíček’s “Bounded arithmetic, propositional logic, and complexity theory”, Buss’s Chapter II of the <a href="http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookII/">Handbook of proof theory</a>, and Cook and Nguyen’s <a href="http://www.cs.toronto.edu/~sacook/homepage/book/">Logical foundations of proof complexity</a>.</p>

<p>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).</p>

<p>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).</p>

<p>The result on FLT, $S^1_2$, and factoring stems from Krajíček and Pudlák’s paper <a href="http://www.karlin.mff.cuni.cz/~krajicek/j-crypto.ps">Some consequences of cryptographical conjectures for $S^1_2$ and EF</a>, 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$.</p>

<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$.</p>

<p>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 <a href="http://www.math.cas.cz/~jerabek/papers/flt.pdf">Abelian groups and quadratic residues in weak arithmetic</a>.</p>

CC BY-SA 3.0
2013-03-27T14:08:24.187Z
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?
Turbo
CC BY-SA 3.0
2013-03-27T14:17:48.973Z
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
CC BY-SA 3.0
2013-03-27T15:08:14.520Z
There is a proof using modular arithmetic (http://en.wikipedia.org/wiki/Proofs_of_Fermat%27s_little_theorem#Proofs_using_modular_arithmetic). If I understand correctly, if one can show that the product of $a,2a,3a,\dots,(p-1)a$  modulo $p$ in $O(log^{c}(p))$ arithmetic steps (something like the factorial conjecture in BSS model), then we have one way of proving flt in $S_{2}^{1}$. Correct?
Turbo
CC BY-SA 3.0
2013-03-27T21:21:43.487Z
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
CC BY-SA 3.0
2013-03-28T04:42:42.307Z
"it is still rather non-obvious how to prove that such exponentially long products are invariant under permutation of the multiplicands" Wouldn't commutativity of products of integers suffice in showing such long products are invariant ubnder permutation of multiplicands? Or is commutativity of modular products of integers is assumed unknown or cannot be proven in $S_{2}^{1}$?
Turbo
CC BY-SA 3.0
2013-03-28T04:51:33.847Z
commutativity of products or of modular products of integers
Turbo
CC BY-SA 3.0
2013-03-28T12:09:35.747Z
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
CC BY-SA 3.0
2013-03-28T12:12:19.850Z
... and it’s not even a well-ordered sequence (it contains a copy of $\mathbb Q$).
Emil Jeřábek
CC BY-SA 3.0
2013-03-28T13:34:16.860Z
Hi Emil: Great response. But what role does $k$ have to play here? I could pick $k = p$. Perhaps I am missing the point or am illiterate in this topic.

 I tried to read the articles you mentioned including Buss' work. Unfortunately since I am illiterate in this language I find the articles including Buss' work non-penetrable due to not just the language but also due to the framework/methods used? Though elementary they seem to escape intuition. Would you recommend some basic articles/books that will provide ideas/intuition to why we need the new framework before I touch the articles?
Turbo
CC BY-SA 3.0
2013-03-28T13:35:03.583Z
Also where would I find notes on the nonstandard model of arithmetic you are quoting? I feel there are more issues at hand here as well. Is there any survey that provides links to computational complexity? Why is it necessary to study these topics w.r.t comp complexity? What major advantage do these tools provide?
Turbo
CC BY-SA 3.0
2013-04-03T11:16:17.963Z
I’m sorry, but this is a bit too many questions at the same time. An overview of the basic connections between computational complexity and proof complexity is given e.g. in the Preface of Krajíček’s book. The books I mentioned in the first paragraph (Krajíček’s and Cook and Nguyen’s in particular) are as introductory as it gets; if you still find them impenetrable, and if you never heard of nonstandard models of arithmetic before, this indicates that you’d need to learn some logic first, such as from Mendelson’s “Introduction to Mathematical Logic”.
Emil Jeřábek
CC BY-SA 3.0
2015-11-02T11:08:42.770Z
To which result? Can you be more specific?
Emil Jeřábek
CC BY-SA 3.0
2015-12-24T16:03:11.273Z
No, there is no such converse. Generally, you cannot get provability in a weak theory out of a purely computational assumption.
Emil Jeřábek
CC BY-SA 3.0
2013-03-26T15:39:52.947Z
2013-03-26T15:56:20.607Z
2013-03-26T15:56:20.607Z
Emil Jeřábek
<p>In a <a href="http://www.gwu.edu/~asl2010/img/razborov.pptx">talk</a> by Razborov, a curious little statement is posted.</p>

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

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

<cc.complexity-theory><lo.logic><proof-complexity>
Proofs in $S_{2}^{1}$
Turbo
# Proofs in $S_{2}^{1}$

(Asked by: username_0 on 2013-03-26)

In a [talk](http://www.gwu.edu/~asl2010/img/razborov.pptx) 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}$?

**Tags:** cc.complexity-theory, lo.logic, proof-complexity

---

## 1 answers

### Answer by username_1 on 2013-03-26. Score: 21 | Accepted answer

$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](http://en.wikipedia.org/wiki/Peano_arithmetic#First-order_theory_of_arithmetic). It is one of the theories defined by Sam Buss in his [thesis](http://www.math.ucsd.edu/~sbuss/ResearchWeb/BAthesis/), other general references include Chapter V of Hájek and Pudlák’s [Metamathematics of first-order arithmetic](http://projecteuclid.org/euclid.pl/1235421926), Krajíček’s “Bounded arithmetic, propositional logic, and complexity theory”, Buss’s Chapter II of the [Handbook of proof theory](http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookII/), and Cook and Nguyen’s [Logical foundations of proof complexity](http://www.cs.toronto.edu/~sacook/homepage/book/).

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](http://www.karlin.mff.cuni.cz/~krajicek/j-crypto.ps), 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](http://www.math.cas.cz/~jerabek/papers/flt.pdf).

> **Comments:**
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: There is a proof using modular arithmetic (http://en.wikipedia.org/wiki/Proofs_of_Fermat%27s_little_theorem#Proofs_using_modular_arithmetic). If I understand correctly, if one can show that the product of $a,2a,3a,\dots,(p-1)a$  modulo $p$ in $O(log^{c}(p))$ arithmetic steps (something like the factorial conjecture in BSS model), then we have one way of proving flt in $S_{2}^{1}$. Correct?  
> **username_1**: 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).  
> **username_0**: "it is still rather non-obvious how to prove that such exponentially long products are invariant under permutation of the multiplicands" Wouldn't commutativity of products of integers suffice in showing such long products are invariant ubnder permutation of multiplicands? Or is commutativity of modular products of integers is assumed unknown or cannot be proven in $S_{2}^{1}$?  
> **username_0**: commutativity of products or of modular products of integers  
> **username_1**: 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, ...  
> **username_1**: ... and it’s not even a well-ordered sequence (it contains a copy of $\mathbb Q$).  
> **username_0**: Hi Emil: Great response. But what role does $k$ have to play here? I could pick $k = p$. Perhaps I am missing the point or am illiterate in this topic.   I tried to read the articles you mentioned including Buss' work. Unfortunately since I am illiterate in this language I find the articles including Buss' work non-penetrable due to not just the language but also due to the framework/methods used? Though elementary they seem to escape intuition. Would you recommend some basic articles/books that will provide ideas/intuition to why we need the new framework before I touch the articles?  
> **username_0**: Also where would I find notes on the nonstandard model of arithmetic you are quoting? I feel there are more issues at hand here as well. Is there any survey that provides links to computational complexity? Why is it necessary to study these topics w.r.t comp complexity? What major advantage do these tools provide?  
> **username_1**: I’m sorry, but this is a bit too many questions at the same time. An overview of the basic connections between computational complexity and proof complexity is given e.g. in the Preface of Krajíček’s book. The books I mentioned in the first paragraph (Krajíček’s and Cook and Nguyen’s in particular) are as introductory as it gets; if you still find them impenetrable, and if you never heard of nonstandard models of arithmetic before, this indicates that you’d need to learn some logic first, such as from Mendelson’s “Introduction to Mathematical Logic”.  
> **username_1**: To which result? Can you be more specific?  
> **username_1**: No, there is no such converse. Generally, you cannot get provability in a weak theory out of a purely computational assumption.  

---

