arithmétique de Robinson

L'arithmétique de Robinson est une partie finiment axiomatisable de l'arithmétique de Peano des entiers naturels, c'est-à-dire que le schéma d'axiomes de récurrence n'apparaît pas. Elle a été introduite en 1950 par Raphael Robinson. L'arithmétique de Robinson suffit pour que l'on puisse démontrer les théorèmes d'incomplétude et d'indécidabilité : une théorie axiomatique récursive et cohérente dans le langage de l'arithmétique qui a pour conséquence les axiomes de cette théorie est nécessairement indécidable et incomplète. Le fait qu'elle soit finiment axiomatisable permet d'en déduire immédiatement l'indécidabilité du calcul des prédicats du premier ordre dans le langage de l'arithmétique et, modulo codage, dans d'autres langages.