Arithmétique de Robinson — Wikipédia

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

• Portail de la logique
• Portail des mathématiques