Problema de la función exponencial de Tarski

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 ${\displaystyle \mathbb {R}}$ ${\displaystyle L_{\text{o}}=(+,-,<,0,1)}$${\displaystyle \nombreoperador {Th} (\mathbb {R} )}$${\displaystyle L_{\text{o}}}$${\estilo de visualización \varphi}$

${\displaystyle \mathbb {R} \modelos \varphi .}$

Luego preguntó si esto seguía siendo así si se añadía al lenguaje una función unaria que se interpretaba como la función exponencial en , para obtener la estructura . ${\estilo de visualización \exp}$${\displaystyle \mathbb {R}}$${\displaystyle \mathbb {R} _ {\exp}}$

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. ${\estilo de visualización n}$${\displaystyle \mathbb {Z}}$${\displaystyle \mathbb {R} ^{n}}$${\displaystyle \mathbb {R} _ {\exp}}$

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 polinomios exponenciales y en variables con coeficientes enteros , produce un entero que depende de , y tal que si es una solución no singular del sistema ${\displaystyle \operatorname {Th} (\mathbb {R} _{\exp })}$${\displaystyle n\geq 1}$${\estilo de visualización n}$${\displaystyle f_{1},\puntos ,f_{n},g}$${\displaystyle \eta \geq 1}$${\displaystyle n,f_{1},\puntos ,f_{n},g}$${\displaystyle \alpha \in \mathbb {R} ^{n}}$

${\displaystyle f_{1}(x_{1},\ldots ,x_{n},e^{x_{1}},\ldots ,e^{x_{n}})=\ldots =f_{n}(x_{1},\ldots ,x_{n},e^{x_{1}},\ldots ,e^{x_{n}})=0}$

entonces o bien . ${\displaystyle g(\alpha )=0}$${\displaystyle |g(\alpha )|>{\tfrac {1}{\eta }}}$