En lógica matemática , un lenguaje de primer orden de los números reales es el conjunto de todas las oraciones bien formadas de lógica de primer orden que involucran cuantificadores universales y existenciales y combinaciones lógicas de igualdades y desigualdades de expresiones sobre variables reales. La teoría de primer orden correspondiente es el conjunto de oraciones que son realmente verdaderas para los números reales. Hay varias teorías diferentes de este tipo, con diferente poder expresivo, dependiendo de las operaciones primitivas que se permite usar en la expresión. Una pregunta fundamental en el estudio de estas teorías es si son decidibles : es decir, si existe un algoritmo que pueda tomar una oración como entrada y producir como salida una respuesta "sí" o "no" a la pregunta de si la oración es verdadera en la teoría.
La teoría de cuerpos reales cerrados es la teoría 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 lo 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 cuerpos reales cerrados a menudo se basan en la eliminación de cuantificadores por 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 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] Por el contrario, la extensión de la teoría de cuerpos reales cerrados con la función seno es indecidible ya que esto permite la codificación de la teoría indecidible de los números enteros (véase el teorema de Richardson ).
Aun así, se puede manejar el caso indecidible con funciones como seno mediante el uso de algoritmos que no necesariamente terminan siempre. En particular, se pueden diseñar algoritmos que solo se requiere que terminen para fórmulas de entrada que sean 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]