En la teoría de modelos , el problema de la función exponencial de Tarski plantea la pregunta de 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 . [1]
El cuerpo real ordenado es una estructura sobre el lenguaje de anillos ordenados , con la interpretación usual dada a cada símbolo. Tarski demostró que la teoría del cuerpo real , , es decidible. Es decir, dada cualquier oración - existe un procedimiento efectivo para determinar si
Luego preguntó si esto seguía siendo así si uno añadía una función unaria al lenguaje que se interpretaba como la función exponencial en , para obtener la estructura .
El problema se puede reducir a encontrar un procedimiento eficaz para determinar si cualquier polinomio exponencial dado en variables y con coeficientes en tiene una solución en . Macintyre y Wilkie (1996) demostraron que la conjetura de Schanuel implica que existe tal procedimiento y, por lo tanto, dieron una solución condicional al problema de Tarski. [2] 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 , 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 es lo que denominaron la conjetura débil de Schanuel. Esta conjetura afirma que existe un procedimiento eficaz que, dados y polinomios exponenciales en variables con coeficientes enteros , produce un entero que depende de , y tal que si es una solución no singular del sistema
entonces o bien .