La decidibilità del campo esponenziale reale

L’elaborato tratta la decidibilità della teoria del campo esponenziale reale analizzando analogie e differenze con la teoria dei campi reali chiusi. La teoria dei campi reali chiusi nel linguaggio L:={+,-,*,0,1,<}, che è la teoria del campo dei numeri reali nello stesso linguaggio, ammette eliminazione dei quantificatori e il teorema di Tarski afferma che la teoria è decidibile. In generale se una L-teoria ammette eliminazione dei quantificatori ed esiste una procedura meccanica tale che per ogni L-formula chiusa senza quantificatori dia risposta positiva se essa è un teorema e negativa se non lo è, allora tale teoria è decidibile. La teoria del campo esponenziale reale nel linguaggio L:={+,-,*,0,1,<,exp} non ammette eliminazione dei quantificatori. Per questo motivo per verificare la sua decidibilità è necessario procedere in altro modo. In particolare si dimostra che se vale la congettura di Schanuel allora tale teoria è decidibile. L’idea è quella di dare uno schema di assiomi validi per espansioni opportune della teoria dei numeri reali, dimostrando poi che esiste una teoria ricorsiva che assiomatizza la teoria del campo reale esponenziale. Questo equivale a dire che la teoria è decidibile.