Arithmétique de Robinson

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 ℕ 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[1]

4. x + 0 = x
5. x + sy = s(x + y)
6. x•0 = 0
7. 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 sⁿ0 (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 sⁿ0 (la partie standard d'un modèle de la théorie, voir section suivante).

Il existe des variantes de l'arithmétique de Robinson, par exemple énoncées en ajoutant un 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 Σ₁⁰-complètes (voir la section Propriétés).

L'ensemble des entiers naturels ℕ munis des opérations usuelles d'addition et de multiplication est un modèle de l'arithmétique de Robinson : c'est le modèle dit 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 sⁿ0 (ceux-ci représentent tous les termes clos du langage, à égalité démontrable dans la théorie 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 a ≤ n, avec n un élément standard alors a est standard,
• si a est non standard et n standard alors n ≤ a.

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

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 (∀x ≤ n P), et qui sont vraies dans le modèle standard de l'arithmétique ℕ, sont démontrables dans l'arithmétique de Robinson. Ceci se prouve par induction sur la construction de telles formules. Ce résultat est étroitement lié aux propriétés des modèles de l'arithmétique de Robinson ci-dessus, et celles-ci peuvent d'ailleurs être utilisées pour la démonstration.

Le résultat reste vrai pour des formules closes obtenues en ajoutant des quantificateurs existentiels en tête d'une formule obtenue par de telles constructions : c'est la propriété de Σ₁⁰-complétude,

toute formule close Σ₁⁰ vraie 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é, c'est-à-dire que les propriétés vraies pour tous les entiers, en particulier celles susceptibles de se démontrer par récurrence, ne sont pas exprimables par une formule Σ₁⁰.

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

pour toute théorie arithmétique cohérente, récursive, et Σ₁⁰-complète, il existe un énoncé (Π₁⁰) 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.

• 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 𝒫₀ est l'arithmétique de Robinson).
• (en) Craig Smorynski, Logical Number Theory I -- An Introduction, Berlin, Springer Verlag, 1991, 405 p. (ISBN 978-3-540-52236-2 et 0-387-52236-0, BNF 37385798)