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 verdaderas de los números reales. Existen varias teorías de este tipo diferentes, con diferente poder expresivo, dependiendo de las operaciones primitivas que se permite usar 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 verdadera en la teoría?
La teoría de los 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 demostró Tarski , esta teoría es decidible; véase el teorema de Tarski-Seidenberg y la eliminación del cuantificador . Las implementaciones actuales de los procedimientos de decisión para la teoría de campos cerrados reales se basan a menudo en la eliminación de cuantificadores por 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 es válida, entonces se seguiría la decidibilidad de esta teoría. [1] [2] En contraste, 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 enteros (ver teorema de Richardson ).
Aún así, uno 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 deben terminar para fórmulas de entrada que son robustas , es decir, fórmulas cuya satisfacibilidad no cambia si la fórmula está ligeramente perturbada. [3] Alternativamente, también es posible utilizar enfoques puramente heurísticos. [4]
Referencias
- ^ Macintyre, AJ ; Wilkie, AJ (1995), "Sobre la decidibilidad del campo exponencial real", en Odifreddi, PG (ed.), Kreisel 70th Birthday Volume , CLSI
- ^ Kuhlmann, S. (2001) [1994], "Teoría de modelos de la función exponencial real" , Enciclopedia de Matemáticas , EMS Press
- ^ Ratschan, Stefan (2006). "Resolución eficiente de restricciones de desigualdad cuantificadas sobre los números reales". Transacciones ACM en lógica computacional . 7 (4).
- ^ Akbarpour, Behzad; Paulson, Lawrence Charles (2010). "MetiTarski: un demostrador de teorema automático para funciones especiales de valor real". Revista de razonamiento automatizado . 44 .