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 en realidad son verdaderas para los números reales. Existen varias teorías diferentes, con diferente poder expresivo, dependiendo de las operaciones primitivas que se permiten utilizar en la expresión. Una cuestión fundamental en el estudio de estas teorías es si son decidibles : es decir, ¿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 decidible? cierto en la teoría.
La teoría de campos cerrados reales 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 demuestra Tarski , esta teoría es decidible; ver Teorema de Tarski-Seidenberg y Eliminación del cuantificador . Las implementaciones actuales de procedimientos de decisión para la teoría de campos cerrados reales a menudo se basan en la eliminación de cuantificadores mediante descomposición algebraica cilíndrica .
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 se seguiría la decidibilidad de esta teoría. [1] [2] Por el contrario, la extensión de la teoría de campos cerrados reales con la función seno es indecidible ya que esto permite codificar la teoría indecidible de los números enteros (ver el teorema de Richardson ).
Aun así, se puede manejar el caso indecidible con funciones como el seno mediante el uso de algoritmos que no necesariamente terminan siempre. En particular, se pueden diseñar algoritmos que solo deban terminar para fórmulas de entrada que sean robustas , es decir, fórmulas cuya satisfacibilidad no cambie si la fórmula se altera ligeramente. [3] Alternativamente, también es posible utilizar enfoques puramente heurísticos. [4]