Are there any sets of axioms that have an efficient algorithm for all provable statements?

I'm looking for a set of axioms that are reasonably expressive (non-trivial) such that any statement that can be proved as true from the set of axioms can be done so efficiently. By this I mean that an algorithm is known that takes polynomial time to find a proof for any true statement, polynomial in terms of the size of the statement (and thus there is also a guarantee that all proofs have a polynomial sized encoding in terms of the size of the statement).

For example, Presburger arithmetic is decidable in time $$2^{2^{cn}}$$ for some $$c>0$$. I'm looking for something that is decidable in time $$poly(n)$$. There are some trivial options that work (such as everything is true, or a contradiction proves everything), but I'm looking for something non-trivial.

• Someone asked about clarifying "trivial", but then deleted their comment. A rule that throws out most trivial cases is "there are an infinite number of true and false statements, and for all integers $c$ there is a true statement with a proof of size greater than $c$". There may be some edge cases that are still pretty boring that satisfy this condition, but it seems like a good start. – Phylliida Jul 15 '20 at 17:18
• (To clarify for other readers, that person was me. I removed my comment once I noticed the argument in my answer, which in my opinion provided a sufficiently strong negative result to constitute an answer.) – Noah Schweber Jul 15 '20 at 17:31
• BTW I did not downvote or vote to close. – Noah Schweber Jul 15 '20 at 18:15

While the term "nontrivial" is still a bit unclear, there's a good sense in which a positive answer to your question is extremely unlikely:

Suppose $$T$$ does not prove "There is exactly one element in the universe." Then we can in polynomial time reduce the set of unsatisfiable propositional sentences to the set of $$T$$-theorems. In particular, if $$\mathsf{P\not=NP}$$ this gives a strong negative answer to your question.

To do this, we argue as follows. Given a $$\mathsf{SAT}$$ instance $$\theta$$ with propositional atoms $$a_1,...,a_n$$, consider the first-order sentence $$\theta':\equiv\exists x_1,y_1,...,x_n,y_n[\varphi(x_1,y_1,...,x_n,y_n)]$$ where $$\varphi$$ is the first-order formula gotten from $$\theta$$ by replacing each $$a_i$$ with the formula $$x_i=y_i$$. Assuming $$T$$ is consistent with the existence of two distinct elements, we have that $$\theta$$ is satisfiable in the propositional sense iff $$T\cup\{\theta'\}$$ is consistent. And the construction $$\theta\mapsto\theta'$$ is sufficiently simple for this reduction to be efficient.

So basically, unless $$T$$ is extremely silly we can always embed $$\mathsf{coSAT}$$ into the $$T$$-$$\mathsf{THEOREM}$$.

EDIT: And in fact the situation is much worse - as Tom Baker observed, we can in fact get all of $$\mathsf{PSPACE}$$ (the point being that as soon as $$T$$ has a model with more than one element, we can efficiently reduce the theory of the two-element pure set to the set of $$T$$-theorems).

• Nice, this does seem to rule out most things, or at least, makes the boundary very clear. The main exception is if encoding SAT clauses in this way takes exponential space. An analogy would be encoding subset sum in unary (tally marks) to make it solvable in poly time in terms of the size of the input. – Phylliida Jul 15 '20 at 17:31
• @Phylliida True, but the encoding here is linear. The length of $\theta'$ is roughly four times that of $\theta$ at worst (basically, the matrix $\varphi$ has length about twice that of $\theta$, and the block of quantifiers at the front is at worst roughly twice as long as $\theta$). – Noah Schweber Jul 15 '20 at 17:33
• @Phylliida I've now asked a followup question. – Noah Schweber Aug 20 '20 at 17:34
• @Phylliida There's less to that than meets the eye. A "pure set" is just a structure with, well, no structure - pedantically, it's a structure in the empty language. Two pure sets are isomorphic iff they have the same cardinality (there's no additional structure to preserve), so in the same way that we can abuse terminology and say "the two-element cyclic group" we can say "the two-element pure set" - that phrase specifies the structure in question up to isomorphism. Meanwhile, the first-order theory of a structure is the set of all first-order sentences true in that structure. (continued) – Noah Schweber Aug 25 '20 at 15:08
• So, for example, allowing for the usual abbreviations the sentences "$\exists x,y(x\not=y)$" and "$\forall x\exists y\forall z(x=z\vee y=z)$" are in the first-order theory of the two-element pure set. Meanwhile, "$\exists x,y,z(x\not=y\wedge y\not=z\wedge x\not=z)$" and "$\forall x,y(x*y=y*x)$" are not: the former is false in the two-element pure set (it says "there are three distinct elements"), and the latter isn't even grammatically correct in this context since it uses the symbol "$*$" which isn't in the language of pure sets (which, again, has only the logical apparatus). – Noah Schweber Aug 25 '20 at 15:11