Arithmétique de Robinson

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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'apparait pas. Elle a été introduite en 1950 par Raphael Robinson (en). L'arithmétique de Robinson suffit pour que l'on puisse démontrer les théorèmes d'incomplétude et d'indécidablité : une théorie 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écidablité du calcul des prédicats du premier ordre dans le langage de l'arithmétique et, modulo codage, dans d'autres langages.

Axiomes[modifier | modifier le code]

La théorie de Robinson est une théorie du calcul des prédicats du premier ordre égalitaire. Les axiomes sont en particulier valides pour l'ensemble N des entiers naturels muni de ses opérations usuelles. Le langage de la théorie a pour signature (des éléments primitifs du langage)

  • un symbole de constante 0
  • un symbole de fonction unaire « s » pour la fonction successeur ;
  • 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)

  1. sx ≠ 0
    c'est-à-dire que 0 n'est pas un successeur
  2. (sx = sy) → x = y
    c'est-à-dire que la fonction successeur est injective
  3. 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 ; dans l'arithmétique de Peano, il est conséquence du schéma d'axiomes de récurrence.
  4. x + 0 = x
  5. x + sy = s(x + y)
  6. x•0 = 0
  7. x•sy = (xy) + 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. Celles-ci assurent en particulier que tout terme sans variable est égal à un terme de la forme sn0 (un successeur itéré de 0).