Récursivement énumérable

L’exemple de l’ensemble des vérités atomiques de l’arithmétique formelle (que nous noterons VAF0) va nous servir ici à donner un contenu concret aux définitions qui vont suivre. VAF0 est représenté par un nombre fini de règles permettant la création d'un ensemble dans lequel on peut retrouver et démontrer les théorèmes fondamentaux que l'on trouve dans l'arithmétique classique des nombres entiers.

VAF0 est défini avec :

• un objet de base, noté ici 0 pour faciliter l'analogie avec l'arithmétique classique ;
• un opérateur unaire s, la fonction successeur (dans le cas de l'arithmétique classique sx=x+1, par exemple, s7=8) ;
• deux opérateurs binaires, + et . , l’addition et la multiplication ;
• deux prédicats binaires fondamentaux, = et <.

On pourrait toutefois choisir un nombre plus restreint d'opérateurs ou de prédicats. On peut par exemple définir VAF0 uniquement en utilisant les symboles suivants: 0, +, . , et =, mais les règles de production et les axiomes de l’arithmétique formelle seraient plus difficiles à énoncer.

L’unique formule initiale que l'on considère pour la création de VAF0 est 0=0. On a alors les règles de production suivantes :

R1 Si x=y alors sx=sy (sx : successeur de x)

R2 Si x=y alors x<sy

R3 Si x<y alors x<sy

R4 Si x=y alors x+0=y

R5 Si x+y=z alors y+x=z

R6 Si x+y=z alors x+sy=sz

R7 Si x=x alors x.0=0

R8 Si x.y=z alors y.x=z

R9 Si x.y=z alors x.sy=z+x

R10 Si x=y alors y=x

R11 Si x=y et y=z alors x=z

R12 Si x=y et y<z alors x<z

R13 Si x=y et z<y alors z<x

Les éléments de VAF0 sont alors obtenus à partir de l'assertion "0=0" et à l'application un nombre fini de fois des règles de production R1 à R13.

Commençons par donner la définition des ensembles génériques: celle des ensembles énumérables en résultera immédiatement car les ensembles génériques sont énumérables. On pourra alors remarquer que l'ensemble VAF0 est un ensemble générique.

Un ensemble générique Eg est défini à partir de cinq ensembles finis, l’ensemble des objets de base, l’ensemble des opérateurs fondamentaux, l’ensemble des prédicats fondamentaux, l’ensemble des formules initiales et l’ensemble des règles de production.

Les éléments de Eg sont des formules atomiques, c'est-à-dire des formules créées grâce à des noms d’objet et des prédicats fondamentaux. Les objets sont obtenus à partir des objets de base en leur appliquant les opérateurs fondamentaux. Les formules initiales ou prédicats fondamentaux sont des formules atomiques.

Pour expliciter les règles de production, il faut introduire des noms de variable, distincts de tous les noms d’objets, d’opérateurs et de prédicats déjà introduits. Les variables de R1 à R13 sont x, y et z. Les termes sont obtenus à partir des objets et des variables en leur appliquant les opérateurs fondamentaux. 0, x+s0 et x. (sy+s0) sont des termes. Une clause atomique est une formule atomique construite avec des prédicats fondamentaux et des termes, x+y=z par exemple.

Une règle de production est définie par un nombre n fini de clauses atomiques. Les n-1 premières clauses sont les conditions de production, ou prémisses, la dernière clause est le résultat, ou conclusion. Toutes les règles de R1 à R10 ne contiennent qu’une seule prémisse. R11, R12, et R13 en contiennent deux. On impose en général que toutes les variables mentionnées dans la conclusion aient d’abord été mentionnées dans les prémisses. On interprète une règle de production en disant que si les conditions de production sont satisfaites alors le résultat est produit.

L’ensemble générique Eg est l’ensemble toutes les formules obtenues à partir des formules initiales en appliquant un nombre fini, éventuellement très grand, de fois les règles de production.

Un système formel E est énumérable s’il existe un ensemble générique Eg et un prédicat unaire P fondamental de Eg tels que x est dans E si et seulement si Px est dans Eg.

Un ensemble générique est un ensemble de formules atomiques tandis qu’un ensemble énumérable est un ensemble d’objets. Cette différence n’est pas fondamentale. Les ensembles génériques sont énumérables et leurs formules peuvent être considérées comme des objets. Plus précisément, chaque prédicat fondamental d’un ensemble générique Eg peut être considéré comme un opérateur du point de vue d’un autre ensemble générique.

Pour montrer que Eg est énumérable, définissons l’ensemble générique Eg’ avec les mêmes objets de base et les mêmes opérateurs fondamentaux que Eg. Chaque prédicat fondamental de Eg est considéré comme un opérateur fondamental de Eg’. Eg’ , quant à lui, a un seul prédicat unaire, P. Chaque formule atomique f de Eg est un objet pour Eg’ . Les formules initiales de Eg’ sont les formules Pf où f est une formule initiale de Eg. Les règles de production de Eg’ sont obtenues à partir de celles de Eg en remplaçant leurs formules f par Pf. Eg est énumérable parce qu’il est défini par Eg’ et le prédicat unaire P.

La définition présente de l’énumérabilité est un peu différente de celle de Smullyan (Theory of formal systems) parce qu’ici les expressions formelles sont des formules bien formées, au sens de la grammaire des opérateurs, alors que dans la théorie de Smullyan, les expressions formelles sont toutes les suites finies de symboles. Cette différence est mineure.

• Si A et B sont des ensembles récursivement énumérables alors :
  • A ∩ B est aussi un ensemble récursivement énumérable ;
  • A ∪ B est aussi un ensemble récursivement énumérable ;
  • A × B est aussi un ensemble récursivement énumérable.
• L'image réciproque d'un ensemble récursivement énumérable par une fonction récursive partielle est aussi un ensemble récursivement énumérable.
• Un ensemble est récursivement énumérable si et seulement s'il se trouve au niveau ${\displaystyle \Sigma _{1}^{0}}$de la hiérarchie arithmétique.
• Un ensemble E est décidable si et seulement si E et son complémentaire sont récursivement énumérables.

Pour prouver que l’énumérabilité au sens de Smullyan est équivalente à l’énumérabilité au sens de Turing, il faut prouver (i) et (ii).

(i) Un ensemble Smullyan-énumérable est Turing-énumérable.

(ii) Un ensemble Turing-énumérable est Smullyan-énumérable.

(i) est assez évident pour tous ceux qui savent programmer un ordinateur. On peut définir un ordre sur l’ensemble de toutes les productions, celles-ci étant définies comme des suites finies de règles de production. Le problème de savoir si une formule est obtenue par une production à partir des formules initiales est décidable parce qu’une production ne produit qu’un nombre fini de formules. On programme alors l’ordinateur pour qu’il examine toutes les productions une par une. Si la formule étudiée est obtenue par une de ces productions, alors l’ordinateur s’arrête, sinon il examine la production suivante. Un ordinateur ainsi programmé s’arrête si et seulement si la formule étudiée fait partie de l’ensemble Smullyan-énumérable étudié. Un ensemble Smullyan-énumérable est donc toujours Turing-énumérable.

(ii) On considère les vérités de la forme « x est l’état numéro i d’une machine dont le programme est y et dont l’état initial est z ». L’état numéro zéro est défini par l’état initial de la mémoire et la position initiale de la machine. L’état numéro i+1 est obtenu après l’exécution d’une instruction sur l’état numéro i. À partir d’une définition rigoureuse du concept de machine de Turing universelle, on peut définir un ensemble Smullyan-énumérable qui contient toutes les vérités de la forme ci-dessus, ainsi que toutes celles qui précisent que la machine s’est arrêtée, pour un programme PrU d’une machine universelle. Cela prouve (ii).

Les définitions de Turing et de Smullyan permettent toutes les deux de définir des ensembles énumérables. Mais celle de Smullyan est avantageuse du point de vue de l’axiomatique, parce que les règles de production peuvent être immédiatement traduites en axiomes. Les axiomes ainsi définis sont automatiquement vrais si le modèle est un ensemble générique défini avec ces règles de production. La définition de Smullyan simplifie souvent la tâche quand on veut trouver un modèle, un ensemble de vérités atomiques, pour des axiomes.