# Are there any arithmetic theories in which all provable statements have efficiently computable witnesses?

Let's say a formula $\forall_{x_1,\dots,x_m} \exists_{y_1,\dots,y_n} P(x_1,\dots,x_m,y_1,\dots,y_n)$ in the first-order language of arithmetic is $T(n)$-verifiable if there is an algorithm running in time $T(m + \sum \log_2 (x_i + 1))$ which given any list of numbers $x_1, \dots x_m$ outputs a list $y_1, \dots, y_n$ such that when all the numbers are substituted into $P$ (each written as $SS\dots0$) the resulting formula is also $T(n)$-verifiable. For the base case, we'll say all true unquantified sentences and all true sentences with a single quantifier (either existential or universal) are $T(n)$-verifiable for any function $T$. For logical connectives, $A \land B$ is $T(n)$-verifiable if and only if both $A$ and $B$ are, $A \vee B$ is $T(n)$-verifiable if and only if at least one of them is, etc.

Now consider the set of all $2^{o(n)}$-verifiable sentences (the union over all $T(n) \in 2^{o(n)}$ of all $T(n)$-verifiable sentences). This includes the axioms of Peano arithmetic, since they are stated with a single universal quantifier, but we don't get all the instances of the induction schema. It also won't include statements like the totality of exponentiation expressed with the $\beta$ function, since the existentially quantified values are too big to output in time.

Is this set of formulas logically closed, or alternatively, is it possible to prove any sentences that aren't $2^{o(n)}$-verifiable using only $2^{o(n)}$-verifiable sentences as premises? Also, is Robinson arithmetic $T(n)$-verifiable for some class of functions? I know that Presburger arithmetic is decidable in doubly-exponential time, and presumably we can find witnesses in a similar amount of time, but since Robinson arithmetic has no induction I'm not sure if we can prove anything that has a witness we can't find more quickly than that. On the other hand, I don't yet have a good reason to believe Robinson arithmetic is $O(T(n))$-verifiable for any function $T$.