<p>This example is a bit lower in the hierarchy than what Kaveh asks for, but it is an open problem whether the soundness of the uniform $\mathrm{TC}^0$ algorithms for integer division and iterated multiplication by <a href="http://dx.doi.org/10.1016/S0022-0000%2802%2900025-9" rel="noreferrer">Hesse, Allender, and Barrington</a> can be proved in the corresponding theory $\mathit{VTC}^0$.</p>

<p>The argument is pretty elementary, and there should be no problem formalizing it in $\mathit{TV}^0$, but with respect to $\mathit{VTC}^0$ it suffers from a chicken-and-egg problem: it makes heavy use of the very functions whose $\mathrm{TC}^0$-computability is furnished by the algorithm.</p>

<p>For another example, the Jacobi symbol $\left(\frac an\right)$ is polynomial-time computable, but its soundness in the form</p>

<blockquote>
  <p>if $p$ is an odd prime and $\left(\frac ap\right)=1$, then $a$ is a quadratic residue modulo $p$</p>
</blockquote>

<p>is not provable in $S^1_2$ unless factoring can be done in probabilistic polynomial time, by the arguments <a href="http://www.math.cas.cz/~jerabek/papers/factor.pdf" rel="noreferrer">here</a>.</p>

<p>Another class of examples is given by irreducibility testing and factorization algorithms for polynomials (primarily over finite fields and over the rationals). These invariably rely on Fermat’s little theorem or its generalizations (among others), and as such are not known to be formalizable in an appropriate theory of bounded arithmetic. Typically, these algorithms are randomized, but for deterministic polynomial-time examples, one can take <a href="http://en.wikipedia.org/wiki/Factorization_of_polynomials_over_a_finite_field_and_irreducibility_tests#Rabin.27s_test_of_irreducibility" rel="noreferrer">Rabin’s irreducibility test</a> or the <a href="http://en.wikipedia.org/wiki/Tonelli%E2%80%93Shanks_algorithm" rel="noreferrer">Tonelli–Shanks square-root algorithm</a> (formulated so that a quadratic nonresidue is required as a part of the input).</p>

CC BY-SA 3.0
2013-04-05T18:24:57.387Z
2013-04-08T14:11:00.377Z
2013-04-08T14:11:00.377Z
Emil Jeřábek
<p>The <a href="http://en.wikipedia.org/wiki/AKS_primality_test">AKS primality test</a> seems like a good candidate if Wikipedia is to be believed.</p>

<p>However, I would expect such an example to be hard to find. Existing proofs are going to be phrased so that they are obviously not done in bounded arithmetic, but they will likely be "adaptable" to bounded arithmetic with more or less effort (usually more).</p>

CC BY-SA 3.0
2013-04-05T08:09:04.050Z
I haven't looked at the proof in the AKS papers but AKS seems to be a good candidate.
Kaveh
CC BY-SA 3.0
2013-04-05T11:59:45.890Z
Indeed, Emil Jerabek has shown that even the correctness of the Miller-Rabin test is not provable in $S^1_2$ under standard non-collapsing assumptions. [*Dual weak pigeonhole principle, Boolean complexity, and derandomization*, APAL 129 (2004), 1-37]
François G. Dorais
CC BY-SA 3.0
2013-04-05T12:10:47.477Z
Actually, Emil's argument relies the fact that every prime satisfies Fermat's Little Theorem is not provable in $S^1_2$. The same reasoning applies here, under standard assumptions, it is not provable in $S^1_2$ that every prime passes the AKS test.
François G. Dorais
CC BY-SA 3.0
2013-04-05T13:05:38.357Z
There is a wonderful paper by Krajicek and Pudlak that gives a bunch more examples: http://www.karlin.mff.cuni.cz/~krajicek/j-crypto.ps
François G. Dorais
CC BY-SA 3.0
2013-04-05T14:14:02.593Z
@François, why not posting an answer? :)
Kaveh
CC BY-SA 3.0
2013-04-05T19:33:29.047Z
So, I get the highest upvote count for making an early lucky guess, while others actually know what is going on. Math is just like MTV.
Andrej Bauer
CC BY-SA 3.0
2013-04-05T06:26:39.433Z
2013-04-05T06:32:17.583Z
2013-04-05T06:32:17.583Z
Andrej Bauer
<p>This is the same idea as Andrej's answer but with more details.</p>

<p>Krajicek and Pudlak [<a href="http://karlin.mff.cuni.cz/~krajicek/j-crypto.ps">LNCS 960, 1995, pp. 210-220</a>] have shown that if $P(x)$ is a $\Sigma^b_1$-property that defines primes in the standard model and $$S^1_2 \vdash \lnot P(x) \to (\exists y_1,y_2)(1 &lt; y_1, y_2 &lt; x \land x = y_1y_2)$$ then there is a polynomial time factoring algorithm. This gives a bunch of examples since any NP algorithm for primality testing basically yields such a $\Sigma^b_1$ formula. In particular, the AKS primality test gives such a formula (when appropriately recast in the language of $S^1_2$). The paper by Krajicek and Pudlak gives more cryptography related examples of this kind but predates AKS and related advances by a few years.</p>

CC BY-SA 3.0
2013-04-05T17:33:36.593Z
2013-04-05T17:33:36.593Z
François G. Dorais
<p>I am looking for natural examples of <em>efficient algorithms</em> (i.e. in polynomial time) s.t.</p>

<ol>
<li>their correctness and efficiency can be proven constructively (e.g. in <a href="http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic">$PRA$</a> or <a href="http://en.wikipedia.org/wiki/Heyting_arithmetic">$HA$</a>), but</li>
<li>no proof using only efficient concepts is known (i.e. we don't know how to prove their correctness and efficiency in $TV^0$ or $S^1_2$).</li>
</ol>

<p>I can make artificial examples myself. However I want interesting natural examples, i.e. algorithms studied for their own sake, not created just to answer this type of questions.</p>

CC BY-SA 3.0
2013-04-05T06:23:05.543Z
Perhaps something from automata theory, where an algorithm is easy, but to show it works one needs to consider all subsets of something or other?
Andrej Bauer
CC BY-SA 3.0
2013-04-05T06:23:58.000Z
How about polynomial-time primality checking? That proof is likely to be complicated enough to be hard to stick inside $S^1_2$?
Andrej Bauer
CC BY-SA 3.0
2013-04-05T07:37:18.087Z
Would probabilistic algorithms work for you? Formalizing probability seems to require the reals, and analysis generally takes you into the territory of second-order arithmetic. This is just a guess -- I don't know very much about how much probability can be done in HA though.
Neel Krishnaswami
CC BY-SA 3.0
2013-04-05T07:59:56.460Z
@Neel, actually Emil's thesis "[Weak pigeonhole principle, and randomized computation](http://www.math.cas.cz/~jerabek/papers/phd.pdf)" is about formalizing probabilistic algorithms. A main axiom needed for formalizing some of these seems to be approximate counting which is not part of $TV^0$ or $S^1_2$. I think it might be simpler to stick to the deterministic polytime case with $TV^0$ and $S^1_2$.
Kaveh
CC BY-SA 3.0
2013-04-05T08:11:36.390Z
ps: It would be more interesting if we can prove that the correctness/efficiency of the algorithms are not provable in these theories, or at least are equivalent to statements which are believed to be unprovable in them. However asking for that is probably too much with what we know currently.
Kaveh
CC BY-SA 3.0
2013-04-05T12:56:58.667Z
@Neel, most of the relevant probability can be done in first-order systems since you never really need to know the exact probability of an event, you usually only need to compare that probability with certain rational numbers.
François G. Dorais
<cc.complexity-theory><reference-request><lo.logic><proof-complexity><constructive-mathematics>
Constructively efficient algorithms without efficient correctness and efficiency proof
Kaveh
# Constructively efficient algorithms without efficient correctness and efficiency proof

(Asked by: username_0 on 2013-04-05)

I am looking for natural examples of *efficient algorithms* (i.e. in polynomial time) s.t.

1. their correctness and efficiency can be proven constructively (e.g. in [$PRA$](http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic) or [$HA$](http://en.wikipedia.org/wiki/Heyting_arithmetic)), but
2. no proof using only efficient concepts is known (i.e. we don't know how to prove their correctness and efficiency in $TV^0$ or $S^1\_2$).

I can make artificial examples myself. However I want interesting natural examples, i.e. algorithms studied for their own sake, not created just to answer this type of questions.

**Tags:** cc.complexity-theory, reference-request, lo.logic, proof-complexity, constructive-mathematics
> **Comments:**
> **username_1**: Perhaps something from automata theory, where an algorithm is easy, but to show it works one needs to consider all subsets of something or other?  
> **username_1**: How about polynomial-time primality checking? That proof is likely to be complicated enough to be hard to stick inside $S^1_2$?  
> **username_2**: Would probabilistic algorithms work for you? Formalizing probability seems to require the reals, and analysis generally takes you into the territory of second-order arithmetic. This is just a guess -- I don't know very much about how much probability can be done in HA though.  
> **username_0**: @Neel, actually Emil's thesis "[Weak pigeonhole principle, and randomized computation](http://www.math.cas.cz/~jerabek/papers/phd.pdf)" is about formalizing probabilistic algorithms. A main axiom needed for formalizing some of these seems to be approximate counting which is not part of $TV^0$ or $S^1_2$. I think it might be simpler to stick to the deterministic polytime case with $TV^0$ and $S^1_2$.  
> **username_0**: ps: It would be more interesting if we can prove that the correctness/efficiency of the algorithms are not provable in these theories, or at least are equivalent to statements which are believed to be unprovable in them. However asking for that is probably too much with what we know currently.  
> **username_3**: @Neel, most of the relevant probability can be done in first-order systems since you never really need to know the exact probability of an event, you usually only need to compare that probability with certain rational numbers.  

---

## 3 answers

### Answer by username_3 on 2013-04-05. Score: 15 | Accepted answer

This is the same idea as Andrej's answer but with more details.

Krajicek and Pudlak [[LNCS 960, 1995, pp. 210-220](http://karlin.mff.cuni.cz/~krajicek/j-crypto.ps)] have shown that if $P(x)$ is a $\Sigma^b\_1$-property that defines primes in the standard model and $$S^1\_2 \vdash \lnot P(x) \to (\exists y\_1,y\_2)(1 < y\_1, y\_2 < x \land x = y\_1y\_2)$$ then there is a polynomial time factoring algorithm. This gives a bunch of examples since any NP algorithm for primality testing basically yields such a $\Sigma^b\_1$ formula. In particular, the AKS primality test gives such a formula (when appropriately recast in the language of $S^1\_2$). The paper by Krajicek and Pudlak gives more cryptography related examples of this kind but predates AKS and related advances by a few years.


---

### Answer by username_4 on 2013-04-05. Score: 11

This example is a bit lower in the hierarchy than what Kaveh asks for, but it is an open problem whether the soundness of the uniform $\mathrm{TC}^0$ algorithms for integer division and iterated multiplication by [Hesse, Allender, and Barrington](http://dx.doi.org/10.1016/S0022-0000%2802%2900025-9) can be proved in the corresponding theory $\mathit{VTC}^0$.

The argument is pretty elementary, and there should be no problem formalizing it in $\mathit{TV}^0$, but with respect to $\mathit{VTC}^0$ it suffers from a chicken-and-egg problem: it makes heavy use of the very functions whose $\mathrm{TC}^0$-computability is furnished by the algorithm.

For another example, the Jacobi symbol $\left(\frac an\right)$ is polynomial-time computable, but its soundness in the form

> if $p$ is an odd prime and $\left(\frac ap\right)=1$, then $a$ is a quadratic residue modulo $p$

is not provable in $S^1\_2$ unless factoring can be done in probabilistic polynomial time, by the arguments [here](http://www.math.cas.cz/~jerabek/papers/factor.pdf).

Another class of examples is given by irreducibility testing and factorization algorithms for polynomials (primarily over finite fields and over the rationals). These invariably rely on Fermat’s little theorem or its generalizations (among others), and as such are not known to be formalizable in an appropriate theory of bounded arithmetic. Typically, these algorithms are randomized, but for deterministic polynomial-time examples, one can take [Rabin’s irreducibility test](http://en.wikipedia.org/wiki/Factorization_of_polynomials_over_a_finite_field_and_irreducibility_tests#Rabin.27s_test_of_irreducibility) or the [Tonelli–Shanks square-root algorithm](http://en.wikipedia.org/wiki/Tonelli%E2%80%93Shanks_algorithm) (formulated so that a quadratic nonresidue is required as a part of the input).


---

### Answer by username_1 on 2013-04-05. Score: 10

The [AKS primality test](http://en.wikipedia.org/wiki/AKS_primality_test) seems like a good candidate if Wikipedia is to be believed.

However, I would expect such an example to be hard to find. Existing proofs are going to be phrased so that they are obviously not done in bounded arithmetic, but they will likely be "adaptable" to bounded arithmetic with more or less effort (usually more).

> **Comments:**
> **username_0**: I haven't looked at the proof in the AKS papers but AKS seems to be a good candidate.  
> **username_3**: Indeed, Emil Jerabek has shown that even the correctness of the Miller-Rabin test is not provable in $S^1_2$ under standard non-collapsing assumptions. [*Dual weak pigeonhole principle, Boolean complexity, and derandomization*, APAL 129 (2004), 1-37]  
> **username_3**: Actually, Emil's argument relies the fact that every prime satisfies Fermat's Little Theorem is not provable in $S^1_2$. The same reasoning applies here, under standard assumptions, it is not provable in $S^1_2$ that every prime passes the AKS test.  
> **username_3**: There is a wonderful paper by Krajicek and Pudlak that gives a bunch more examples: http://www.karlin.mff.cuni.cz/~krajicek/j-crypto.ps  
> **username_0**: @François, why not posting an answer? :)  
> **username_1**: So, I get the highest upvote count for making an early lucky guess, while others actually know what is going on. Math is just like MTV.  

---

