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.