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

104 Views Asked by At

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.

1

There are 1 best solutions below

11
On BEST ANSWER

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