Converting Mathematical Statements to SAT Formulas

Question

Is it possible to write a mathematical statement (like Goldbach's conjecture, for example) as a nontrivial 3-SAT formula that is satisfiable iff that statement is true? iff it is false? iff it is independent of the axioms of ZFC? So, for any statement, you would have (at most) 3 formulas, for which only one can be satisfiable. Is there any work in this field (you can use the Pythagorean Theorem as a more simpler example)?

Answer 1

If you want to know whether there exists a general method/algorithm which can convert any given mathematical statement (by which you mean statements written in logic (say first-order logic, second-order logic ... etc)) to a SAT formula which is True iff that statement is True, then the answer is No.

The reason being that evaluating whether an SAT formula is true or false is decidable (in exponential time if not faster), whereas these logics are usually undecidable. So, no such algorithm can exist.

Of course, there are logics which are decidable, and the statement of those logic can be converted to SAT formula (maybe trivial ones like True or False as mentioned by @D.W) by a specific algorithm. See: http://www.lsv.fr/~haase/documents/h18.pdf

Answer 2

It depends on the mathematical statement. If it has the form

$$\exists x_1 \in S_1 \cdots \exists x_n \in S_n . \varphi(x_1,\dots,x_n)$$

where $\varphi(x_1,\dots,x_n)$ is some condition on $x_1,\dots,x_n$ and $S_1,\dots,S_n$ are finite sets, then yes, it can be expressed as a 3CNF formula in a straightforward way.

However, statements like $\exists x \in S_1 \forall y \in S_2 . \varphi(x,y)$ or $\exists x_1 \in \mathbb{R} \cdots \exists x_n \in \mathbb{R} . \varphi(x_1,\dots,x_n)$ are harder.

There is a trivial sense in which the answer is yes: every mathematical statement is either true or false, so it corresponds to either the 3CNF formula $\text{True}$ (i.e., $(x_1 \lor \neg x_1)$) or the 3CNF formula $\text{False}$ (i.e., $(x_1) \land (\neg x_1)$). This reduction is nonconstructive and might not be computable, though.

You might be interested in https://en.wikipedia.org/wiki/Existential_theory_of_the_reals.

Undecidable is a property of languages, not of mathematical statements. Perhaps you mean "independent of the axioms of ZFC".