Problema da função exponencial de Tarski

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 editar

O campo real ordenado R é uma estrutura sobre a linguagem dos anéis ordenados Lor = (+,·,−,<,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 Lor-sentença φ não é um procedimento eficaz para determinar se

         

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 Rexp.

Resultados condicionais e equivalentes editar

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 . 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úmeros complexos assim seria esperado para ser um resultado mais forte do que a decidibilidade de Rexp 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(Rexp) é 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 f1, ..., fn, g, produz um inteiro η ≥ 1 que depende de n, f1, ... , fn, g, e de tal modo que se α ∈ R  é uma solução não singular do sistema

  

então ou g(a)=0 ou |g(a)|>η .

Solução alternativa editar

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 editar

  • 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)