Fondements des mathématiques/Les axiomes des théories des ensembles/Théorèmes fondamentaux de l’énumérabilité et de l’indécidabilité
Le premier de ces théorèmes montre en quel sens l’ensemble de tous les ensembles énumérables est complètement connu. On pourrait l’appeler le théorème de complétude de l’énumérabilité. Il est équivalent à la preuve d’existence d’une machine universelle, donnée par Turing en 1936, qui est à l’origine de l’invention des ordinateurs.
Le second de ces théorèmes montre en quel sens l’ensemble des ensembles énumérables ne peut pas être complètement connu. On pourrait l’appeler le théorème d’incomplétude de l’énumérabilité. Il est équivalent à l’indécidabilité du problème de l’arrêt, prouvée par Turing dans le même article fondateur (On computable numbers, with an application to the Entscheidungsproblem).
Le théorème fondamental de l’énumérabilité
[modifier | modifier le wikicode]Nous le démontrerons sous la forme suivante.
Tous les ensembles énumérables peuvent être représentés dans Enum
où Enum est l’ensemble de formules atomiques qui a été précédemment défini.
Autrement dit.
L’ensemble de toutes les vérités atomiques d’appartenance à tous les ensembles énumérables est énumérable.
Au lieu d’une preuve générale et abstraite, nous allons étudier la construction d’un ensemble énumérable particulier, un ensemble VAF0 de vérités atomiques de l’arithmétique formelle. Celui-ci a déjà été introduit avec la définition de l’énumérabilité de Smullyan. Rappelons ici comment il a été déterminé.
Un exemple d’ensemble énumérable, les vérités arithmétiques atomiques
[modifier | modifier le wikicode]VAF0 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, et deux prédicats binaires fondamentaux, = et <.
L’unique formule initiale de VAF0 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 VAF0 sont obtenus à partir de 0=0 en appliquant un nombre fini de fois les règles de production R1 à R13.
La représentation des formules
[modifier | modifier le wikicode]Montrons comment représenter VAF0 à l’intérieur de Enum. Le choix suivant n’est qu’une possibilité parmi d’autres.
0 est représenté par o
s est représenté par so
+ est représenté par sso
. est représenté par ssso
= est représenté par sssso (4 s devant le o)
< est représenté par ssssso (5 s devant le o)
Abrégeons “est représenté par” avec erp.
- Si u erp x alors su erp asox
1 erp asoo, 2 erp asoasoo, 3 erp asoasoasoo, ....
- Si u erp x et v erp y alors u+v erp assobxy
0+0 erp assoboo,
1+(2+3) erp assob(asoo)(assob(asoasoo)asoasoasoo),
Les parenthèses ont été introduites pour la lisibilité mais elles ne sont pas nécessaires, parce que la notation de Lukasiewicz a été adoptée. Elle consiste simplement à mettre un opérateur devant ses arguments, écrire +xy au lieu de x+y.
- Si u erp x et v erp y alors u.v erp asssobxy
1.1 erp asssob(asoo)(asoo),
2.2 erp asssob(asoasoo)(asoasoo),
- Si u erp x et v erp y alors u=v erp assssobxy
0=0 erp assssoboo,
0=1 erp assssobo(asoo),
2+2=4 erp assssob(assob(asoasoo)asoasoo)(asoasoasoasoo)
- Si u erp x et v erp y alors u<v erp asssssobxy
0<1 erp asssssobo(asoo),
Cette technique de représentation montre que les noms d’objets et les expressions bien formées de n’importe quel ensemble énumérable peuvent être représentés dans Enum, parce qu’il n’y a pas de limites aux nombres finis d’objets de base, d’opérateurs et de prédicats fondamentaux qui peuvent être ainsi représentés. s, a et b ont été choisis précisément dans ce but. b peut être interprété comme un opérateur de couplage, distinct du C de Enum, mais semblable quant à la façon dont il est utilisé. a peut être interprété comme un opérateur d’application d’une fonction, distinct du “Image par...de” de Enum, mais semblable.
La représentation d’un ensemble générique
[modifier | modifier le wikicode]La méthode
[modifier | modifier le wikicode]Pour construire la représentation d’un ensemble générique Eg dans Enum, on commence par l’ensemble fini Rep-Eg0 des représentations de ses formules initiales.
Rep-VAF00 =def Singleton de assssoboo
puisque l’unique formule initiale de VAF0 est 0=0.
On définit ensuite une fonction de production Prod, telle que ProdX contient toutes les formules de X et toutes leurs conséquences par une seule application d’une des règles de production de Eg.
On peut ainsi définir toute une suite de sous-ensembles de Rep-Eg : Rep-Eg0, Rep-Eg1=Prod(Rep-Eg0), Rep-Eg2 = Prod(Rep-Eg1), ...
Rep-Eg est alors obtenu en prenant la somme de tous les Rep-Eg(n) où n est un nombre entier.
La fonction Prod qui produit ainsi Rep-VAF0 est définie en plusieurs étapes.
La représentation des termes constants
[modifier | modifier le wikicode]L’univers U de VAF0 est l’ensemble de ses noms d’objets. Il délimite l’ontologie de VAF0.
U est obtenu par induction à partir de 0 et de l’opérateurs s, + et . .
La fonction de succession s est représentée dans Enum par Succ. Succ =def Fonction asoX
La fonction d’addition + est représentée dans Enum par Add.
Add =def Fonction assobXX’
La fonction de multiplication est représentée dans Enum par Mult. Mult =def Fonction asssobXX’
U est est représenté dans Enum par Tconst, l’ensemble des termes constants.
On définit Tconst à partir de Singleton de o et de la fonction Tprod.
Pour tout ensemble x de représentants de termes, Tprod(x) est l’ensemble des représentants obtenus à partir de ceux de x en appliquant une fois l’une des fonctions Succ, Add ou Mult.
Tprod =def Fonction Extension de (il existe un Z’ tel que (Z Egale Im par Succ de Z’ Et Z’ Dans X)) Ou (il existe un Z’ tel qu’il existe un Z’’ tel que Z Egale Im par Add de CZ’Z’’ Et Z’ Dans X Et Z’’ Dans X) Ou (il existe un Z’ tel qu’il existe un Z’’ tel que Z Egale Im par Mult de CZ’Z’’ Et Z’ Dans X Et Z’’ Dans X)
Tconst =def Ensemble somme de Ensemble induit par Tprod à partir de Singleton de o
La représentation des règles de production
[modifier | modifier le wikicode]On va définir des ensembles Inst-R1, Inst-R2, ... qui contiennent des représentations de toutes les règles de production de VAF0 lorqu’elles sont singularisées à des objets, c’est à dire les instances de ces règles.
Par exemple, (si 0=ss0 alors s0=sss0) est une instance de la règle R1.
L’ensemble Inst-R1 des instances de R1 est obtenu avec la fonction Rep-R1.
Rep-R1 =def Fonction C(assssobXX’)(assssob(asoX)asoX’)
Inst-R1 =def Ensemble-image par Rep-R1 de Produit cartésien de Tconst et Tconst
On définit de même Inst-R2, Inst-R3,...
La production des conséquences
[modifier | modifier le wikicode]Définissons maintenant des fonctions Prod1, Prod2, ... telles que Prodn(X) est l’ensemble des conséquences de X par une application de la règle Rn.
Soit C1-Rep-VAF00 l’ensemble des conséquences de Rep-VAF00 par la règle R1.
C1-Rep-VAF00 =def Extension de (il existe un Z’ tel que (Z’ Dans Rep-VAF00 Et CZ’Z Dans Inst-R1))
Cela conduit à la définition suivante de Prod1.
Prod1 =def Fonction Extension de (il existe un Z’ tel que (Z’ Dans X Et CZ’Z Dans Inst-R1))
Prod2, Prod3, jusqu’à Prod10 peuvent être définis de la même façon.
Comme R11, R12 et R13 ont deux prémisses, les définitions de Prod11, Prod12 et Prod13 sont un peu plus compliquées.
Prod11 =def Fonction Extension de (il existe un Z’ tel qu’il existe un Z’’ tel que (Z’ Dans X Et Z’’ Dans X Et CZ’CZ’’Z Dans Inst-R11))
Prod =def Fonction Prod1(X) Union (Prod2(X) Union (Prod3(X) Union ... Prod13(X) ))
Rep-VAF0 =def Ensemble-somme de (Ensemble induit par Prod à partir de Rep-VAF00)
Cela termine cette construction, ou définition, de la représentation Rep-VAF0 dans Enum de l’ensemble VAF0 de toutes les vérités atomiques de l’arithmétique formelle.
N’importe quel ensemble générique peut être représenté avec la même technique, parce qu’il n’y a pas de limites quant aux nombres de formules initiales et de règles de production.
Enum lui-même peut être complètement représenté à l’intérieur de Enum. Cela ne contredit pas le théorème de Tarski parce que Enum ne contient pas de négations. Nous montrerons plus loin que cette représentation de Enum à l’intérieur d’elle-même conduit au théorème fondamental de l’indécidabilité.
La représentation d’un ensemble énumérable
[modifier | modifier le wikicode]Définissons maintenant le représentant Rep-E d’un ensemble énumérable E défini à partir d’un ensemble générique Eg et d’un prédicat unaire P de Eg. E est un sous-ensemble de U, l’univers des noms d’objet de Eg.
Eg est représenté dans Enum par Rep-Eg , P par Rep-P.
Rep-E =def Extension de (a(Rep-P)Z Dans Rep-Eg)
Conclusion : tout ensemble énumérable peut être représenté dans Enum. Enum est universel.
Ce théorème a la même portée que celui de Turing sur l’existence d’une machine universelle.
Le principal intérêt de Enum n’est pas de fournir une autre démonstration de ce théorème. L’avantage de Enum par rapport au formalisme de Turing, c’est qu’il se prête naturellement à une formulation axiomatique de la théorie des ensembles.
Le théorème fondamental de l’indécidabilité
[modifier | modifier le wikicode]Nous le démontrerons sous la forme suivante.
Les complémentaires de tous les ensembles énumérables ne peuvent pas être tous représentés dans Enum.
Autrement dit.
L’ensemble de toutes les faussetés atomiques d’appartenance à tous les ensembles énumérables n’est pas énumérable.
Autrement dit.
L’ensemble de toutes les vérités atomiques d’appartenance à tous les ensembles énumérables est indécidable.
Soit Rep-Enum un représentant de Enum et supposons que le complémentaire de Enum (dans l’ensemble des formules atomiques) soit représenté par Rep-Cenum.
Le procédé de représentation que nous avons introduit permet aisément de définir un prédicat binaire “est représenté par” ou “erp” défini pour toutes les expressions formelles. Pour toute expression formelle x, x erp y si et seulement si y est le représentant de x.
On peut également définir une fonction numérique Rep-Dans telle que Rep-Dans(x, y) est dans Rep-Enum si et seulement si l’expression formelle représentée par x est dans l’ensemble représenté par y.
On peut alors définir le prédicat unaire suivant.
il existe un y tel que x est représenté par y et Rep-Dans(y, x) est dans Rep-Cenum.
Ce prédicat unaire est finitaire. Son extension est donc un ensemble représenté par une expression formelle RS.
RS est-elle dans l’ensemble qu’elle représente ?
x est dans l’ensemble représenté par RS équivaut par définition à
il existe un y tel que x est représenté par y et Rep-Dans(y, x) est dans Rep-Cenum.
RS est dans l’ensemble représenté par RS équivaut donc à
il existe un y tel que RS est représenté par y et Rep-Dans(y, RS) est dans Rep-Cenum.
Et donc à :
RS n’est pas dans l’ensemble représenté par RS.
C’est une contradiction.
L’hypothèse de l’existence de Rep-Cenum doit donc être rejetée. Cela termine cette démonstration du théorème fondamental de l’indécidabilité.