|
Le théorème de l’incomplétude ontologique interdit d’espérer une théorie complète mais on peut quand même vouloir une théorie de la plupart des ensembles bien définis par des méthodes élémentaires.
La production des vérités arithmétiques à partir d’une formule initiale avec un nombre fini de règles est un cas particulier d’une méthode générale. On dira qu’un ensemble de vérités atomiques est énumérable s’il peut être produit à partir d’un nombre fini de formules initiales avec un nombre fini de règles de production. Cette définition de l’énumérabilité est équivalente à celle de TüringTuring. Nous présenterons une approche formelle qui le montrera plus précisément et qui prouvera les théorèmes fondamentaux de l’énumérabilité et de l’indécidabilité. L’ensemble de toutes les vérités atomiques d’appartenance à tous les ensembles énumérables est énumérable. Il suffit d’un nombre fini de formules initiales et de règles pour produire toutes ces vérités. Ces formules et ces règles seront données dans la section suivante.
L’ensemble de tous les ensembles énumérables peut être choisi comme base de la théorie des ensembles finitaires, au même sens où les nombres entiers ont été choisis comme base des mathématiques classiques. L’avantage de ce choix est qu’il permet d’énoncer des règles de production de vérités et des principes élémentaires de raisonnement avec beaucoup de généralité. Il suffit d’adapter les méthodes, classiques et éprouvées, de calcul sur les nombres entiers au calcul sur les ensembles énumérables. On obtient une théorie aussi fiable que la théorie des nombres entiers, c’est à dire absolument fiable.
==L’énumérabilité selon Smullyan==
Le chapitre précédent a rappelé l’équivalence entre l’existence d’une machine universelle et l’énumérabilité de toutes les vérités atomiques d’appartenance aux ensembles énumérables. Dans cetteCette section, nous commençons par exposerexpose une autre définition de l’énumérabilité, issue des travaux de Post et Smullyan, qui repose sur la notion de règle de production.
[[Fondements des mathématiques : l'énumérabilité selon Smullyan|Texte de cette section]]
L’exemple de l’ensemble VAF0 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.
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 <. 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 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.
Commençons par donner la définition des ensembles génériques, celle des ensembles énumérables en résultera immédiatement. VAF0 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+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 équivaut à 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 au 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 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 Türing, il faut prouver (i) et (ii).
(i) Un ensemble Smullyan-énumérable est Türing-énumérable.
(ii) Un ensemble Türing-é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 Türing-é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. A partir d’une définition rigoureuse du concept de machine de Türing 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 Türing 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.
==Les vérités atomiques sur les ensembles énumérables==
Les logiciens sont en général des minimalistes. On ne veut pas plus de principes qu’il n’est nécessaire. On veut un nombre minimal d’objets de base, d’opérateurs et de prédicats fondamentaux, d’axiomes et de règles de déduction. Un petit nombre est en général considéré comme suffisant.
Enum est défini avec une douzaine d’opérateurs (14), deux douzaines de prédicats (25) et plus d’une centaine de règles (122). Mais je suis aussi un minimaliste. Un petit nombre de notions fondamentales veut souvent dire un gros travail d’interprétation des principes. Les livres les plus courts ne sont pas toujours les plus faciles à lire, parce que tout ce qui n’est pas dans le livre est laissé en exercice pour le lecteur. On pourrait définir Enum avec moins d’opérateurs, de prédicats et de règles, mais ses principes seraient alors plus difficiles à comprendre et exigeraient davantage de travail d’interprétation.
Les 15 opérateurs fondamentaux de Finitaire1 sont les 14 de Enum plus Non.
Les deux notions premières, ou prédicats fondamentaux, les plus importantes, de Finitaire1 sont “être dans”, ou “être élément de”, et “être égal à”“=”. Les autres prédicats fondamentaux servent à définir les constructions auxiliaires.
Les 27 prédicats fondamentaux sont ceux de Enum plus “est prouvablement faux” et “est un prédicat sans variables liées”.
===Les axiomes de Finitaire1===
====Les axiomes d’existence des ensembles====
Parmi les 27 prédicats fondamentaux de Finitaire2Finitaire1, tous sauf quatre (“=”, “être dans”, “être prouvable”vrai” et “être prouvablement faux”) conduisent à des ensembles énumérables de vérités atomiques qui interviennent dans les raisonnements seulement pour justifier les constructions auxiliaires. Nous verrons qu’on peut s’en passer en les remplaçant par deux, ou même un, schéma d’axiomes, mais celui-ci requiert la compréhension de la notion de prédicat finitaire, qui doit être définie séparément. La plupart des règles de Enum et de la négation dans les prédicats finitaires servent justement à définir avec précision cette notion.
Les ensembles sont définis et remplis avec les règles de de production de Enum, les règles ou pseudo-règles associées à l’opérateur Non, et les trois formules initiales de Enum.
Toutes les règles de production de Enum ainsi que les pseudo-règles associées à l’opérateur Non, peuvent être traduites par des formules closes du calcul des prédicats du premier ordre. Il suffit de les compléter avec des quantificateurs universels pour toutes leurs variables libres. Par exemple, la règle Eform2 est traduite par la formule suivante.
Pour tout x, si x est une expression formelle alors sx est une expression formelle
====Le principe d’induction complète====
Le schéma d'axiomes du principe d'induction complète a déjà été énoncé. Tous les axiomes, en nombre infini, obtenus à partir de ce schéma sont des axiomes de Finitiare1Finitaire1.
La théorie Finitaire1 est l’ensemble de tous les axiomes qui viennent d'être cités et de toutes les formules que l’on peut déduire par les règles de déduction dude calculla logique du despremier prédicatsordre.
===Autres formulations des axiomes de Finitaire1===
| 