En la teoría de modelos , el problema de la función exponencial de Tarski pregunta si la teoría de los números reales junto con la función exponencial es decidible . Alfred Tarski había demostrado previamente que la teoría de los números reales (sin la función exponencial) es decidible .
El problema
El campo real ordenado R es una estructura sobre el lenguaje de anillos ordenados L o = (+, ·, -, <, 0,1), con la interpretación habitual dada a cada símbolo. Tarski demostró que la teoría del campo real , Th ( R ), es decidible. Es decir, dada cualquier L o -sentencia φ existe un procedimiento efectivo para determinar si
Luego preguntó si este era todavía el caso si se agregaba una función unaria exp al lenguaje que se interpretó como la función exponencial en R , para obtener la estructura R exp .
Resultados condicionales y equivalentes
El problema puede reducirse a encontrar un procedimiento eficaz para determinar si cualquier polinomio exponencial dado en n variables y con coeficientes en Z tiene una solución en R n . Macintyre y Wilkie (1995) demostraron que la conjetura de Schanuel implica que tal procedimiento existe y, por lo tanto, dio una solución condicional al problema de Tarski. La conjetura de Schanuel trata con todos los números complejos, por lo que se esperaría que fuera un resultado más fuerte que la decidibilidad de R exp , y de hecho, Macintyre y Wilkie demostraron que solo se requiere una versión real de la conjetura de Schanuel para implicar la decidibilidad de esta teoría.
Incluso la versión real de la conjetura de Schanuel no es una condición necesaria para la decidibilidad de la teoría. En su artículo, Macintyre y Wilkie demostraron que un resultado equivalente a la decidibilidad de Th ( R exp ) es lo que denominaron la Conjetura débil de Schanuel. Esta conjetura establece que existe un procedimiento efectivo que, dado n ≥ 1 y polinomios exponenciales en n variables con coeficientes enteros f 1 , ..., f n , g , produce un entero η ≥ 1 que depende de n , f 1 , ..., f n , g , y tal que si α ∈ R n es una solución no singular del sistema
entonces g ( α ) = 0 o | g ( α ) | > η −1 .
Solución alterna
Recientemente, se han realizado intentos de manejar la teoría de los números reales con funciones como la función exponencial o seno al relajar la decidibilidad a la noción más débil de cuasi-decidibilidad. Una teoría es cuasi-decidible si hay un procedimiento que decide la satisfacibilidad, pero que puede funcionar para siempre para entradas que no son robustas en un cierto sentido bien definido. Tal procedimiento existe para sistemas de n ecuaciones en n variables ( Franek, Ratschan & Zgliczynski 2011 ).
Referencias
- Kuhlmann, S. (2001) [1994], "Teoría de modelos de la función exponencial real" , Enciclopedia de Matemáticas , EMS Press
- Macintyre, AJ; Wilkie, AJ (1995), "Sobre la decidibilidad del campo exponencial real", en Odifreddi, PG (ed.), Kreisel 70th Birthday Volume , CLSI
- Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr (2011), "La satisfacción de los sistemas de ecuaciones de funciones analíticas reales es cuasi-decidible", Fundamentos matemáticos de la informática 2011 , LNCS, 6907 , Springer, doi : 10.1007 / 978-3-642-22993-0_30