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. 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 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é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 ℕ 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)

  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 [1].
  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 l'on peut démontrer que tout terme sans variable est égal à un terme de la forme sn0 (un successeur itéré de 0).

la relation « ≤ » peut se définir par l'addition

  • x ≤ y ≡ ∃ z z + x = y.

Les axiomes de l'arithmétique de Peano permettent de démontrer que cette relation définit une relation d'ordre, mais pas l'arithmétique de Robinson[2]. La relation définit cependant une relation d'ordre sur les sn0 (la partie standard d'un modèle de la théorie).

Il existe des variantes de l'arithmétique de Robinson, par exemple énoncées en ajoutant une symbole de relation « ≤ » (pour la relation d'ordre) à la signature, et les axiomes afférents. Les propriétés essentielles demeurent, à savoir qu'elles sont finiment axiomatisables, et Σ10-complétes (voir le paragraphe suivant).

Modèles[modifier | modifier le code]

Les entiers naturels, ℕ muni des opérations usuelles d'addition et de multplication, fournissent un modèle de l'arithmétique de Robinson, le modèle standard.

Plus généralement tout modèle de l'arithmétique de Peano est modèle de l'arithmétique de Robinson, puisque tous les axiomes de cette dernière sont conséquences de l'arithmétique de Peano. cependant l'arithmétique de Robinson a des modèles non standards nettement plus simples[3].

Tout modèle ℳ de l'arithmétique non standard contient une partie standard, qui est l'ensemble des interprétations des sn0 (tous les termes clos du langage, à égalité démontrable près). On montre à l'aide des axiomes, et par des récurrences assez immédiates dans la meta-théorie, que la partie standard est stable par addition et multiplication, qu'elle est isomorphe à ℕ (muni de l'addition et de la multiplication), c'est-à-dire que

  • la partie standard de ℳ est un sous-modèle de ℳ, isomorphe à ℕ.

On a de plus que pour tout élément a de ℳ,

  • si an, avec n un élément standard alors a est standard,
  • si a est non standard et n standard alors na.

On dit que la partie standard de ℳ (c'est-à-dire ℕ à isomorphisme près) est un segment initial de ℳ[4].

propriétés[modifier | modifier le code]

Toutes les formules closes (soit sans variable libre) que l'on obtient à partir des égalités polynomiales par négation, conjonction, disjonction et quantification bornée (∀xn P, qui sont vraies dans le modèle standard de l'arithmétique ℕ sont démontrables dans l'arithmétique de Robinson. Ceci se démontre par induction sur la construction de telles formules. La propriété est étroitement liée aux propriétés des modèles de l'arithmétique de Robinson ci-dessus (que l'on peut d'ailleurs utiliser pour la démonstration).

La propriété reste vraie quand on ajoute des quantificateurs existentiels en tête d'une formule obtenue par de telles constructions, c'est-à-dire la propriété pour les formules de Σ10-complétude,

toute formule close Σ10 est démontrable dans l'arithmétique de Robinson.

Intuitivement ces formules sont celles qui ne mettent en jeu, même de façon cachée, aucun quantificateur universel sur l'ensemble des entiers, mais seulement sur des entiers inférieurs à un entier donné. Dit autrement, les propriétés vraies pour tous les entiers, et qui ne sont pas entièrement triviales (en dehors par exemple des axiomes dont la plupart ont cette forme, ou de x = x), celles qui seraient justement susceptibles de se démontrer par récurrence, ne sont pas exprimables par une formule Σ10.

Une analyse de la démonstration par Gödel de son premier théorème d'incomplétude, due à Robinson, permet de montrer que

pour toute théorie arithmétique cohérente, récursive, et Σ10-complète, il existe un énoncé10) vrai dans le modèle standard mais qui n'est pas démontrable dans la théorie,

soit le premier théorème d'incomplétude.

Article détaillé : théorème d'incomplétude.

Notes et références[modifier | modifier le code]

  1. Soit l'axiome 8, ici
  2. Cori-Lascar 2003 p 73.
  3. Voir par exemple Cori-Lascar 2003 p 103, ex 1.
  4. Cori-Lascar 2003 p 74.

Bibliographie[modifier | modifier le code]

  • René Cori et Daniel Lascar, Logique mathématique II. Fonctions récursives, théorème de Gödel, théorie des ensembles, théorie des modèles [détail des éditions] (chapitre 6, l'arithmétique notée 𝒫0 est l'arithmétique de Robinson).
  • (en) Craig Smorynski, Logical Number Theory I -- An Introduction,‎ (ISBN 3-540-52236-0 et 0-387-52236-0)