Decidibilidad de las teorías de primer orden de los números reales

En lógica matemática , un lenguaje de primer orden de los números reales es el conjunto de todas las proposiciones bien formadas de lógica de primer orden que involucran cuantificadores universales y existenciales, así como combinaciones lógicas de igualdades y desigualdades de expresiones sobre variables reales. La teoría de primer orden correspondiente es el conjunto de proposiciones que son realmente verdaderas para los números reales. Existen varias teorías de este tipo, con diferente poder expresivo, dependiendo de las operaciones primitivas que se permiten en la expresión. Una cuestión fundamental en el estudio de estas teorías es si son decidibles : es decir, si existe un algoritmo que pueda tomar una proposición como entrada y producir como salida una respuesta afirmativa o negativa a la pregunta de si la proposición es verdadera en la teoría.

La teoría de los cuerpos reales cerrados es aquella en la que las operaciones primitivas son la multiplicación y la suma; esto implica que, en esta teoría, los únicos números que se pueden definir son los números algebraicos reales . Como demostró Tarski , esta teoría es decidible; véase el teorema de Tarski-Seidenberg y la eliminación de cuantificadores . Las implementaciones actuales de los procedimientos de decisión para la teoría de los cuerpos reales cerrados suelen basarse en la eliminación de cuantificadores mediante descomposición algebraica cilíndrica .

El algoritmo decidible de Tarski se implementó en computadoras electrónicas en la década de 1950. Su tiempo de ejecución es demasiado lento para que pueda alcanzar resultados interesantes. ^{[ 1 ]}

El problema de la función exponencial de Tarski se refiere a la extensión de esta teoría a otra operación primitiva, la función exponencial . Es un problema abierto si esta teoría es decidible, pero si la conjetura de Schanuel se cumple, entonces la decidibilidad de esta teoría se seguiría. ^{[ 2 ] [ 3 ]} En contraste, la extensión de la teoría de campos reales cerrados con la función seno es indecidible ya que esto permite la codificación de la teoría indecidible de los enteros (véase el teorema de Richardson ).

Sin embargo, es posible abordar el caso indecidible con funciones como el seno mediante algoritmos que no necesariamente terminan siempre. En particular, se pueden diseñar algoritmos que solo deben terminar para fórmulas de entrada robustas , es decir, fórmulas cuya satisfacibilidad no cambia si la fórmula se perturba ligeramente. ^{[ 4 ]} Alternativamente, también es posible utilizar enfoques puramente heurísticos. ^{[ 5 ]}

• Construcción de los números reales
• Axiomatización de Tarski de los números reales : teoría de segundo orden de los números reales.