# Provability in $S^1_2$

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.

• There aren’t that many natural statements of this form ($\forall\Delta^b_1$ ) in the first place, all I can think of are various consistency statements. Over a weaker base theory, the strongest $\forall\Delta^b_1$ sentence provable in $S^1_2$ is the consistency of the Extended Frege propositional proof system, which is not a very powerful statement. Then, simple examples of $\forall\Delta^b_1$ statements not provable in $S^1_2$ are consistency statements for calculi that we assume not to be p-simulated by EF: ... – Emil Jeřábek supports Monica Sep 4 '17 at 13:26
• ... for instance, the consistency of the first-order theory in the language of pure equality axiomatized by $\exists x\,\exists y\,(x\ne y)$, formulated as a usual Hilbert-style or sequent calculus. – Emil Jeřábek supports Monica Sep 4 '17 at 13:27
• @EmilJeřábek Arbitrary $Π^0_1$ statements can be rephrased in EFA as $∀Δ^b_1$ (though sometimes only by replacing $∀x$ with $∀y \, ∀x<\log(y)$, which gives $S^1_2$ a strong extra assumption). Correctness/optimality of algorithms is usually already $∀Δ^b_1$. I am also interested in examples that can be converted to $∀Δ^b_1$ if $S^1_2$ were to prove P=PSPACE (but only if their unprovability in $S^1_2$ has been shown unconditionally). Consistency statements are a good example, but it would be surprising if they were essentially the only example. – Dmytro Taranovsky Sep 4 '17 at 16:33

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

• Even simpler, $S^1_2$ does not appear to prove that numbers satisfying the AKS test are prime. However, can you actually show that all these are indeed unprovable in $S^1_2$, using “reasonable computational complexity conjectures”, as the question asks? – Emil Jeřábek supports Monica Sep 5 '17 at 11:22
• I missed the sentence about "reasonable computational complexity conjectures" when I first read the question. I have no idea how such a condition unprovability result could be shown. The discussion made it seem plausible that all true $\forall \Delta^b_1$ used in practice are $S^1_2$-provable, so I proposed some possible counterexamples. – Itai Bar-Natan Sep 13 '17 at 23:23