Conversión de declaraciones matemáticas a las fórmulas SAT

Question

¿Es posible escribir una declaración matemática (como la conjetura de Goldbach, por ejemplo) como una fórmula no trivial de 3 satélites que es satisfactoria IFF esa declaración es verdadera?iff es falso?¿Si es independiente de los axiomas de ZFC?Entonces, para cualquier declaración, tendrías (a lo sumo) 3 fórmulas, para las cuales solo se puede satisfacer.¿Hay algún trabajo en este campo (puede usar el teorema de Pitágoras como un ejemplo más sencillo)?

Answer 1

Si desea saber si existe un método / algoritmo general que puede convertir cualquier declaración matemática dada (por la cual le refieren las declaraciones escritas en la lógica (indique la lógica de primer orden, la lógica de segundo orden ... etc.)) aUna fórmula SAT que es verdadera IFF Esa declaración es verdadera, entonces la respuesta es no.

La razón que se está evaluando si una fórmula SAT es verdadera o falsa es decidible (en tiempo exponencial si no más rápido), mientras que estas lógicas generalmente son indecidables .Por lo tanto, no puede existir tal algoritmo.

Por supuesto, hay lógicas que son decididas, y la declaración de esas lógicas se puede convertir a la fórmula SAT (quizás triviales como VERDADERA o FALSE, como se mencionó por @ D.W) por un algoritmo específico.Consulte: http://www.lsv.fr/~haase/documents/h18.PDF

Answer 2

Depende de la declaración matemática. Si tiene el formulario

$$ \ existe x_1 \ in s_1 \ cdots \ existe x_n \ in s_n. \ varphi (x_1, \ dots, x_n) $$

donde $ \ varphi (x_1, \ dots, x_n) $ es alguna condición en $ x_1, \ puntos, x_n $ y $ s_1, \ dots, s_n $ son conjuntos finitos, luego sí, se puede expresar como una fórmula de 3CNF de una manera directa. < / p>

Sin embargo, las declaraciones como $ \ existen x \ en S_1 \ forall y \ in s_2. \ varphi (x, y) $ o $ \ existes x_1 \ in \ mathbb {r} \ cdots \ existes x_n \ in \ mathbb {r}. \ Varphi (x_1, \ dots, x_n) $ son más difíciles.

Hay un sentido trivial en el que la respuesta es SÍ: Toda declaración matemática es verdadera o falsa, por lo que corresponde a la fórmula 3CNF $ \ texto {true} $ < / span> (es decir, $ (x_1 \ lor \ neg x_1) $ ) o la fórmula 3CNF $ \ texto {FALSE } $ (es decir, $ (x_1) \ land (\ neg x_1) $ ). Esta reducción no es constatuctiva y podría no ser computable, sin embargo.

Podría estar interesado en https://en.wikipedia.org/wiki/existencial_theory_of_the_reals.

indecidable es una propiedad de idiomas, no de declaraciones matemáticas. Tal vez usted signifique "independiente de los axiomas de ZFC".