Provability in $S^1_2$

Question

What are some examples of natural true statements of the form $∀n φ(n)$ ($φ$ is a polynomial time computation/test) that are unprovable in $S^1_2$?

Examples may be unconditional or dependent on reasonable computational complexity conjectures.

While this class of statements naturally corresponds to correctness of polynomial time algorithms (where correctness of the output is coNP), much of mathematics is reflected in these statements, including, for example, Fermat's Last Theorem if it is stated in a way that does not require exponentiation to be total, as well as various numeric tests of open conjectures in number theory.

$S^1_2$ is in some ways the weakest natural base theory for reverse mathematics. It consists of basic arithmetical axioms, closure of unary numbers under multiplication, and polynomial induction on NP predicates: $φ(0) ∧ ∀n (φ(n)→φ(2n)∧φ(2n+1)) ⇒ ∀n φ(n)$ where $φ$ is an NP formula (i.e. φ is $Σ^b_1$; φ may have other free variables; numbers are binary numbers). It is closely connected to polynomial time computation: An $S^1_2$ proof of $∀x ∃y φ(x,y)$ ($φ$ is an NP formula) can be converted into a polynomial time algorithm for finding an example $y$ given $x$ (however, the conversion uses cut-elimination and is not polynomial in proof length). For this class of formulas, $S^1_2$ is conservative over PV$_1$, which is (modulo choice of language and formalization) $S^1_2$ with the polynomial induction restricted to $φ$ that are polynomial time computations.

It remains open whether $S^1_2$ proves P=PSPACE, but assuming plausible computational complexity conjectures, there are sharp limits on provability in $S^1_2$. For example, if factoring is hard, then $S^1_2$ does not prove that every nonprime number -- as tested, for example, by AKS primality test -- has a nontrivial factor (and conversely, the ordinary definition of prime numbers would not provably satisfy many results in number theory). However, these examples can be conceptually grouped with $Π^0_2$ statements in that unprovability depends on number/set existence axioms beyond the power of the base theory. A recurring conjecture is that while the proofs may be hard, the propositions are usually provable if we have have the required existence axioms and basic properties.

A plausible conjecture is that typical (in current mathematical and computer science literature) true statements of the form $∀n φ(n)$ (polynomial time computable $φ$) are already provable in $S^1_2$. The answers may illuminate how accurately the conjecture holds, or show clear limits to this type of polynomial time reasoning.

Answer 1

(Note: I'm not actually familiar with $S^1_2$ and the related formalism, but I'm going by your description of the theory, and I have been already thinking about related questions in an informal way.)

Here are two true number-theoretical statements of the form $\forall n. \varphi (n)$ that don't have any obvious proofs in $S_2^1$:

• If $p$ is prime according to the AKS test, and $a < p$, then $p$ passes the Fermat test: $a^{p-1} \equiv 1 \pmod {p}$ where $a^{p-1} \pmod {p}$ is calculated according to the standard divide-and-conquer algorithm.

• The Jacobi symbol $\left( \frac {p} {q} \right)$ where $p$ and $q$ are positive integers and $q$ is odd, calculated according to the Euclidean algorithm, satisifies all the expected properties. For example, $\left( \frac {p_0 p_1} {q} \right) = \left( \frac {p_0} {q} \right) \left( \frac {p_1} {q} \right)$ and $\left( \frac {p} {q_0 q_1} \right) = \left( \frac {p} {q_0} \right) \left( \frac {p} {q_1} \right)$.

Hopefully these two example should be enough to inspire you to come up with further examples of the same nature.

However, there isn't any clear way to actually prove that these statements are $S^1_2$-unprovable. This seems to be of comparable difficulty as proving the polynomial-time uncomputability of factoring/discrete logarithms/etc..