Voir la source de Axiomes des théories des ensembles/Énumérabilité selon Smullyan

{{Chapitre
  | idfaculté = mathématiques
  | numéro    = 6
  | précédent = [[../Théorèmes fondamentaux de l’énumérabilité et de l’indécidabilité/]]
  | suivant   = [[../|Sommaire]]
  | niveau    = 17
}}

== Un exemple  ==
L’ensemble ''VAF₀'' des vérités atomiques de l’arithmétique élémentaire va nous servir ici pour donner un contenu concret aux définitions qui vont suivre.
 
''VAF₀'' est défini avec :

* un objet de base, 0 ;
* un opérateur unaire ''s'' ;
* la fonction de succession ;
* deux opérateurs binaires, + et · , l’addition et la multiplication ;
* deux prédicats binaires fondamentaux, = et <.

On pourrait faire un choix plus restreint (0, +, · et = par exemple), mais les axiomes de l’arithmétique formelle sont plus faciles à énoncer avec ce choix-la.

L’unique formule initiale de ''VAF₀'' est 0 = 0. Ses règles de production sont les suivantes.

* '''R1''' Si ''x = y'' alors ''sx'' = ''sy'' ;
* '''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 ''VAF₀'' sont obtenus à partir de 0 = 0 en appliquant un nombre fini de fois les règles de production '''R1''' à '''R13'''.

== Les ensembles génériques  ==
Commençons par donner la définition des ensembles génériques, celle des ensembles énumérables en résultera immédiatement. ''VAF₀'' est un ensemble générique. Les ensembles génériques sont énumérables.

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, composées avec 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 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'' + ''s''0 et ''x'' · (''sy'' + ''s0'') sont des termes. 

Une clause atomique est une formule atomique construite avec des prédicats fondamentaux et des termes, par exemple :

:''x'' + ''y'' = ''z''.

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.

== Les ensembles énumérables  ==
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 :

<math>x \in E \; \Leftrightarrow \ Px \in Eg</math>

== Les ensembles génériques sont énumérables  ==
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 au point de vue d’un autre ensemble générique.

Pour montrer qu'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 qu'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.

== L'équivalence entre les définitions de Turing et Smullyan  ==
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 et est introduite ici seulement par souci d’uniformité. C’est pourquoi cette définition est ici appelée énumérabilité au sens de Smullyan.

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'').

== La définition de Smullyan et les théories axiomatiques des ensembles  ==
Les définitions de Turing et de Smullyan permettent toutes les deux de définir des ensembles énumérables de vérités atomiques. Mais celle de Smullyan est avantageuse au 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.

{{Bas de page
  | idfaculté = mathématiques
  | numéro    = 5
  | précédent = [[../Théorèmes fondamentaux de l’énumérabilité et de l’indécidabilité/]]
  | suivant   = [[../|Sommaire]]
}}