Can any 1st-order proof be expressed with an SMT?

Question

Is it possible to rephrase every proof which uses first-order logic into a proof which uses satisfiability modulo theories? In other words, can a program which automatically solves SMT questions solve every first-order proof based on decidable theories as well?

Answer 1

It's slightly unclear to me what you're asking here, but I believe it's the following:

Question: Let $Sat$ be the problem of telling whether a sentence $p$ is satisfiable relative to a c.e. theory $T$, and Prove be the problem of telling whether a sentence $p$ is provable from a c.e. theory $T$. Is $Prove$ "reducible" to $Sat$?

Note that by Craig's trick, the c.e. axiomatizable theories are exactly the computably axiomatizable theories.

The answer depends on exactly what "reducible" means in this case. There are two natural notions here: many-one and Turing. The first says "no" and the second says "yes."

Specifically, the key fact is this:

Completeness theorem (special case): A sentence $p$ is satisfiable relative to a c.e. theory $T$ iff $\neg p$ is not provable relative to $T$.

The transformation $p\mapsto \neg p$ is clearly computable, so the only potential issue is whether the switch from "is in" to "is not in" - that is, whether we're allowed to exchange positive $Sat$-information for negative $Prove$-information. Turing reductions do allow this, while many-one reductions don't.

(Strictly speaking, the statement above just shows that the map $p\mapsto\neg p$ doesn't yield a many-one reduction, and doesn't rule out the possibility of a non-obvious many-one reduction between $Sat$ and $Prove$. But we can indeed prove that none exists - this follows e.g. from the fact that $Prove$ is c.e. but not computable.)