Mostrar código-fonte de Problema da função exponencial de Tarski

{{Wikificação|data=agosto de 2015}}
Na [[teoria dos modelos]], '''o problema da função exponencial''' '''de Tarski''' pergunta se a teoria dos números reais junto com a função exponencial é decidível. [[Alfred Tarski]] tinha mostrado anteriormente que a teoria dos números reais (sem a função exponencial) é decidível.

==O problema==
O campo real ordenado '''R''' é uma estrutura sobre a linguagem dos [[Anel (matemática)|anéis]] ordenados L<sub>or</sub> = (+,·,−,<,0,1), com a interpretação usual dada a cada símbolo. Foi provado por Tarski que a teoria do corpo real, Th('''R'''), é decidível. Isto é, dado qualquer L<sub>or</sub>-sentença φ não é um procedimento eficaz para determinar se
         <math>\operatorname{Th}(\R)\models\varphi.</math>
Ele então perguntou se este era o caso de se acrescentar uma função unária  exp  para a linguagem que foi interpretada como a função exponencial em '''R''', para obter a estrutura '''R'''<sub>exp</sub>.

==Resultados condicionais e equivalentes==
O problema pode ser reduzido para buscar um procedimento eficaz para determinar se um dado polinomial exponencial em n variáveis e com coeficientes em Z possui uma solução em '''R'''<math>^n</math>. [[Angus Macintyre]] & [[Alex Wilkie]] em 1995 mostraram que a conjectura de Schanuel implica num procedimento existente deste tipo, e, portanto, deu uma solução condicional para o problema de Tarski. A conjectura de Schanuel lida com todos os [[Número complexo|números complexos]] assim seria esperado para ser um resultado mais forte do que a decidibilidade de '''R'''<sub>exp</sub> e, de fato, Macintyre e Wilkie provaram que apenas uma versão real da conjectura de Schanuel é necessária para implicar na decidibilidade desta teoria.

Mesmo a versão real da conjectura de Schanuel não é uma condição necessária para a decidibilidade da teoria. Em seu papel, Macintyre e Wilkie mostraram que um resultado equivalente à decidibilidade de Th('''R'''<sub>exp</sub>) é o que eles nomearam de Conjectura Fraca do Schanuel. Esta conjectura afirma que existe um procedimento eficaz que, dado ''n'' ≥ 1 e exponenciais polinômios em ''n'' variáveis com coeficientes inteiros f<sub>1</sub>, ..., f<sub>n</sub>, g, produz um inteiro η ≥ 1 que depende de n, f<sub>1</sub>, ... , f<sub>n</sub>, g, e de tal modo que se α ∈ '''R'''<math>^n</math> é uma solução não singular do sistema
  <math> 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</math>
então ou g(a)=0 ou |g(a)|>η<math>^{-_1}</math>.

==Solução alternativa==
Recentemente, existem tentativas de lidar com a teoria dos números reais com funções como exp, levando a decidibilidade à noção mais fraca de quasi-decidibilidade. Uma teoria é quasi-decidível se, e somente se, existe um procedimento que leva a satisfatibilidade mas que pode correr para sempre para as entradas que não são robustas em certo sentido, bem definido. Existe um procedimento deste tipo para os sistemas de ''n'' equações em ''n'' variáveis (Franek, Ratschan & Zgliczynski (2011)) .

==Referências==
*Kuhlmann, S. (2001), "Model theory of the real exponential function", in Hazewinkel, Michiel, Encyclopedia of Mathematics, Springer, ISBN 978-1-55608-010-4
*Macintyre, A.J.; Wilkie, A.J. (1995), "On the decidability of the real exponential field", in Odifreddi, P.G., Kreisel 70th Birthday Volume, CLSI
*Franek, Peter; Ratschan, Stefan; Zgliczynski, Piotr (2011), "Satisfiability of Systems of Equations of Real Analytic Functions Is Quasi-decidable", LNCS 6907, Springer, doi:10.1007/978-3-642-22993-0_30 Missing or empty |title= (help)

[[Categoria:Funções matemáticas]]