# Constructively efficient algorithms without efficient correctness and efficiency proof

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$ or $HA$), 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.

• 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 Apr 5 '13 at 6:23
• 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 Apr 5 '13 at 6:23
• @Neel, actually Emil's thesis "Weak pigeonhole principle, and randomized computation" 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 Apr 5 '13 at 7:59
• 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 Apr 5 '13 at 8:11
• @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 Apr 5 '13 at 12:56

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

Krajicek and Pudlak [LNCS 960, 1995, pp. 210-220] 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.

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 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.

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 or the Tonelli–Shanks square-root algorithm (formulated so that a quadratic nonresidue is required as a part of the input).

The 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).

• 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 Apr 5 '13 at 11:59
• 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 Apr 5 '13 at 12:10
• There is a wonderful paper by Krajicek and Pudlak that gives a bunch more examples: karlin.mff.cuni.cz/~krajicek/j-crypto.ps – François G. Dorais Apr 5 '13 at 13:05
• @François, why not posting an answer? :) – Kaveh Apr 5 '13 at 14:14
• 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 Apr 5 '13 at 19:33