Arithmétique de Robinson

L'arithmétique de Robinson introduite en 1950 par Raphael Robinson est une théorie du premier ordre pour l'arithmétique des entiers naturels, qui est finiment axiomatisable. Ses axiomes sont essentiellement ceux de l'arithmétique de Peano sans le schéma d'axiomes de récurrence. L'arithmétique de Robinson suffit pour le théorème d'incomplétude de Gödel-Rosser et pour le théorème de Church (indécidabilité du problème de la décision), au sens où l'arithmétique de Robinson, et même toute théorie axiomatique dans le langage de l'arithmétique qui est récursive et cohérente et qui a pour conséquence les axiomes de l'arithmétique de Robinson, est nécessairement incomplète et indécidable. L'arithmétique de Robinson étant finiment axiomatisable, l'indécidabilité du calcul des prédicats du premier ordre dans le langage de l'arithmétique se déduit immédiatement de ce dernier résultat. On peut également en déduire par codage cette indécidabilité pour d'autres langages. La théorie de Robinson est une théorie du calcul des prédicats du premier ordre égalitaire, dont les axiomes sont vrais dans l'ensemble N des entiers naturels muni de ses opérations usuelles. Le langage de la théorie a pour signature (éléments primitifs du langage) un symbole de constante « 0 », pour le nombre zéro un symbole de fonction unaire « s » pour la fonction successeur, celle qui à n associe n + 1 deux symboles de fonction binaire (ou opération) « + » et « • », pour l'addition et la multiplication Les axiomes sont donnés ci-dessous (les variables libres sont implicitement universellement quantifiées) sx ≠ 0 c'est-à-dire que 0 n'est pas un successeur (sx = sy) → x = y c'est-à-dire que la fonction successeur est injective y = 0 ∨ ∃x (sx = y) cet axiome permet de raisonner par cas, suivant qu'un entier (un objet de la structure en toute généralité) est nul ou un successeur x + 0 = x x + sy = s(x + y) x•0 = 0 x•sy = (x•y) + x On retrouve avec ces 4 derniers axiomes les définitions par récurrence de l'addition et de la multiplication de l'arithmétique de Peano, qui, en particulier, assurent que tout terme sans variable peut être démontré égal à un terme de la forme sn0 (un successeur itéré de 0).