Fondements des mathématiques : Les ensembles finitaires

Les ensembles finitaires sont définis avec des moyens élémentaires mais ils sont souvent infinis.

Les mathématiques finitaires consistent à mettre en pratique un principe de progression ontologique, commencer par ce qui est simple, évident, élémentaire, pour poursuivre sur des bases solides.

L’esprit des mathématiques finitaires : commencer par ce qui est simple et évident

L’ensemble des nombres entiers est le plus illustre de tous les ensembles finitaires. Il est à raison considéré comme la base de toute ontologie mathématique. Pour donner une idée de l’importance des nombres entiers, on peut rappeler ces propos, de Kronecker, que Dieu a créé les nombres entiers et qu’à partir de là les mathématiciens ont créé tout le reste de l’univers mathématique.

Les vérités sur les nombres entiers sont évidentes. Tous les axiomes sont vrais par définition au sens où l’on sait qu’ils sont vrais dès qu’on a compris ce que c’est qu’un nombre entier.

Les méthodes de calcul élémentaire de calcul sur les nombres entiers sont complètement connues. On connaît suffisamment de règles pour savoir si une équation, n’importe laquelle, entre combinaisons élémentaires (addition, multiplication, exponentiation et beaucoup d’autres) de nombres entiers, est vraie ou fausse. Les calculs ont toujours une fin. Les vérités atomiques forment un ensemble décidable. Cette complétude des règles de calcul numérique est un cas particulier d’un phénomène très remarquable. Il suffit d’un nombre fini de règles pour connaître des vérités en nombre infini. Les simples mortels, les esprits finis que nous sommes, connaissent l’infini. C’est pourquoi les mathématiques finitaires traitent essentiellement des ensembles infinis.

Les vérités atomiques sur les nombres entiers positifs peuvent toutes être produites à partir d’une unique formule, 0 = 1, et un nombre réduit, une douzaine, de règles de production de vérités. On peut ainsi voir 0 = 0 comme la source de toutes les vérités arithmétiques et les règles de calcul comme les premières indications de chemins que l’on peut suivre à partir de là.

La théorie des nombres entiers peut être considérée comme une source des vérités mais par certains aspects on peut la trouve trop réduite pour la choisir comme base. On voudrait plutôt une théorie des ensembles qui permette de définir davantage d’ensembles bien définis, au sens suivant.

Tous leurs éléments d’un ensemble bien défini sont nommés et toutes les questions sur les vérités atomiques, c’est à dire les appartenances d’un élément à un ensemble et les égalités entre éléments, sont définies sans équivoque. On ne sait pas forcément comment trouver la réponse à la question mais on sait que la question est sensée.

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 Turing. 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.

Le principe de Saint Thomas, je crois ce que je vois, peut être appliqué aux ensembles de base que sont les ensembles énumérables. Comme les éléments de ces ensembles sont toujours des formules on peut les montrer. Dire la vérité sur une formule n’est alors pas très difficile. La formule aba commence par la lettre a, elle contient b mais pas c, elle est symétrique, ... Ces évidences semblent peut être peu intéressantes mais elles méritent cependant un peu d’attention parce qu’elles suffisent comme source de beaucoup de vérités mathématiques. A partir de vérités aussi simples et évidentes que les précédentes on peut déduire des théorèmes très remarquables, pas du tout évidents, et qui nous apprennent beaucoup sur la nature de la raison.

Même lorsque les règles sont très élémentaires, les ensembles finitaires peuvent être très compliqués et les vérités à leur sujet ne sont parfois pas du tout évidentes, même si elles sont atomiques. On sait qu’elles sont des vérités parce que les axiomes sont vrais. Mais comment sait-on que les axiomes sont vrais ? Comment le prouve-t-on ?

La théorie des modèles de la vérité mathématique ne répond pas complètement à ces questions. On ne veut pas seulement une théorie T des ensembles qui soit cohérente, parce que cela veut seulement dire que T dit la vérité sur un univers possible, sur des objets concevables. On veut que T dise la vérité sur des ensembles et pas sur n’importe quels objets. Comment connaît-on des vérités sur les ensembles ?

La vérité sur un ensemble résulte de sa définition. Si E est l’ensemble qui contient aba comme unique élément alors aba est dans E mais abc n’est pas dans E,...

Nous verrons que de telles évidences suffisent pour trouver presque tous les axiomes des théories des ensembles finitaires. Un nombre relativement petit d’axiomes évidents permet de prouver toutes les évidences intuitives, et à partir d’elles on peut prouver presque toutes les vérités mathématiques .Cela montre que la raison est capable de se connaître elle-même, au moins en partie, et qu’il n’est même pas très difficile de la dire puisqu’il suffit d’énoncer des évidences. Celles-ci sont simples, claires et acceptables pour tout être rationnel.

Qu’est-ce qu’un ensemble finitaire ?

Le principe des principes des mathématiques finitaires, c’est de s’en tenir à des ensembles bien définis, c’est-à-dire qu’ils peuvent être déterminés complètement à l’intérieur d’une théorie.

Les ensembles finitaires sont d’abord des systèmes, ou ensembles, formels, c’est à dire des ensembles de formules, et ensuite d’autres ensembles que l’on peut construire progressivement en partant des systèmes formels. Ils peuvent être des ensembles d’ensembles formels, des ensembles d’ensembles d’ensembles formels, ...

Un ensemble est finitaire s’il peut être défini en un nombre fini d’étapes finitaires à partir des objets de base de la théorie. Une étape est finitaire si elle respecte une règle finitaire. Une définition du concept “finitaire” requiert donc une liste des règles finitaires. On exige de ces règles qu’elles ne permettent de construire que des ensembles bien définis.

Définir ou construire un ensemble c’est la même chose. Comme les prédicats, auxquels ils sont étroitement apparentés, un ensemble est construit par sa définition.

A partir de deux ensembles E et F, construire E Union F, E Inter F et E moins F, sont trois règles finitaires. Ces règles sont très nombreuses. Chacun peut faire usage de son imagination pour inventer des règles finitaires.

La liste des règles finitaires ne peut jamais être complète, pour les raisons suivantes. La règle d’après laquelle on peut construire à partir d’une liste L bien définie de règles finitaires et d’un ensemble E0 d’objets de base, l’ensemble U de tous les ensembles constructibles en un nombre fini d’étapes à partir des éléments de E0 et des règles de L, est une règle finitaire. Si L était la liste de toutes les règles finitaires, U serait l’ensemble de tous les ensembles finitaires et il serait lui-même finitaire. Il serait donc élément de lui-même. La règle d’après laquelle à partir de tout prédicat finitaire, on peut construire son extension conceptuelle, est aussi une règle finitaire, sachant qu’un prédicat est finitaire lorsque toutes ses variables, libres ou liées, sont restreintes à des ensembles finitaires déjà construits. On pourrait alors définir à partir de U l’ensemble BR de tous les ensembles finitaires qui ne sont pas éléments d’eux-mêmes. BR serait finitaire, il serait et ne serait pas élément de lui-même. Cette contradiction oblige à renoncer à l’hypothèse de l’existence d’une liste de toutes les règles finitaires. Une liste des règles finitaires est donc nécessairement incomplète même si elle est très élargie. L’ensemble de tous les ensembles finitaires s’il existe, est indicible.

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. Cette section expose 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.

Texte de cette section

Les vérités atomiques sur les ensembles énumérables

Les vérités atomiques sur les ensembles énumérables sont les vérités d’appartenance d’un élément à un ensemble énumérable et les égalités entre ensembles énumérables. Les secondes peuvent être définies à partir des premières avec l’axiome d’extensionnalité et elles sont beaucoup moins élémentaires. On peut prouver qu’elles ne forment pas un ensemble énumérable

Nous allons définir une théorie Enum qui contient toutes les vérités atomiques d'appartenance aux ensembles énumérables.

Enum va être définie par des formules initiales, que l’on peut considérer comme des axiomes, et des règles de production, que l’on peut aussi considérer comme des axiomes, ou comme des règles de déduction. Comme c’est l’usage dans ce cahier, la théorie formelle est développée dans un langage semi-naturel. Les mots de la langue courante peuvent être considérés comme des symboles formels et on peut leur appliquer les règles de grammaire du calcul des prédicats. Il est de toutes façons très facile de traduire les énoncés semi-naturels ainsi obtenus en énoncés purement formels.

Cette méthode du langage semi-naturel présente un grand avantage dans le cas présent, parce que Enum est défini avec un grand nombre d’opérateurs et de prédicats fondamentaux. Pour faire une théorie purement formelle, il faudrait un glossaire assez volumineux pour donner aux symboles formels leur signification dans une langue naturelle.

Les prédicats fondamentaux de la théorie des ensembles sont “est élément de”, ou “est dans” et “=”. Mais on introduit dans Enum d’autres prédicats fondamentaux pour les constructions auxiliaires, les fonctions et les prédicats, principalement.

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.

Lorsque les logiciens définissent toutes les notions à partir d’un petit nombre d’entre elles, ils se servent en général de techniques qui font disparaître l’énumérabilité des vérités atomiques. L’introduction de la négation et de la généralisation dans les expressions définissantes pose ce genre de problème. Enum ne se sert pas de ces opérateurs justement pour que l’énumérabilité de ses formules atomiques vraies soit manifeste.

Nous verrons plus loin comment développer une théorie élémentaire des ensembles finitaires, Finitaire1, en introduisant la négation et du même coup, la généralisation.

En tant que théorie Enum est évidemment cohérente. Puisqu’elle ne contient pas de négations, elle ne peut pas contenir de contradictions. Puisqu’elle est un ensemble de formules atomiques, on peut la considérer comme un modèle d’elle-même. Mais cela ne suffit pas pour prouver que Enum est vraie en tant que théorie des ensembles. Si ses formules initiales ou ses règles étaient mal choisies, elle ne cesserait pas d’être cohérente, mais ses formules ne pourraient plus être interprétées comme des vérités sur les ensembles. Comment être sûr que ses formules initiales et ses règles ont été bien choisies ? Comment le prouver ?

Tous les objets, les opérateurs et les prédicats de Enum ont une signification universelle, c’est à dire compréhensible par tout être rationnel. Compréhensible ne veut pas dire ici immédiatement compréhensible mais seulement qu’un peu de travail suffit pour se familiariser avec ces notions et reconnaître que leurs significations ne sont pas équivoques.

Dès qu’on a compris ces notions, la vérité des formules initiales de Enum est évidente. Il en va de même pour la vérité des règles de production. Il suffit de s’assurer que dans tous les cas, si les prémisses sont vraies, la conclusion l’est aussi. Cela suffit pour prouver que Enum est valide, qu’elle ne contient que des vérités. La section suivante prouvera qu’il y a un sens à dire qu’elle est complète, qu’elle contient toutes les règles, en nombre fini, dont on a besoin pour dire des vérités sur les ensembles infinis.

Enum peut être considérée comme une théorie des nombres généralisée. Les méthodes habituellement employées pour définir des ensembles de nombres sont utilisées dans Enum pour définir des ensembles d’expressions formelles. L’existence de Enum peut être considérée comme une des preuves que la raison est au moins partiellement connaissable. On sait dire des lois qui permettent de produire des vérités rationnelles de base.

La plupart des axiomes des théories des ensembles sont traduits dans Enum par quelques règles de production. Les axiomes de la somme, de l’infini, de compréhension et de remplacement en font partie. Certaines règles de production de Enum sont donc des versions élémentaires des axiomes ensemblistes. La cohérence et la vérité de Enum prouvent qu’il est possible de donner une formalisation fiable de la théorie des ensembles. Mais Enum est trop élémentaire pour aller loin en mathématiques.

Formules initiales et règles de production pour les vérités atomiques d’appartenance aux ensembles énumérables

Cette section définit une théorie complète des ensembles énumérables, au sens où elle contient toutes les vérités atomiques d’appartenance à tous les ensembles énumérables. La preuve de sa complétude est donnée dans la section suivante.

Texte de cette section

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

Texte de cette section

Les négations des faussetés atomiques et le principe d’induction complète

Les prédicats à partir desquels les ensembles de Enum sont définis ne contiennent pas la négation. Cela permet à Enum d’être une théorie complète, au sens où elle peut prouver toutes ses vérités, mais ce n’est pas suffisant pour une théorie générale des ensembles finitaires parce qu’on veut pouvoir y définir des ensembles à partir de prédicats qui contiennent des négations.

Pour remplir les ensembles définis avec la négation dans leurs prédicats, il faut pouvoir prouver des négations de faussetés atomiques. Explicitons le processus de production de ces négations.

Quelques négations de faussetés atomiques de base

Quelques formules sont évidemment des négations de faussetés atomiques.

Les premières d’entre elles nient l’égalité entre des objets de base différents, s’il y a au moins deux objets de base. Avec les trois objets de base o , X , Z , on obtient trois négations de faussetés atomiques initiales, non(o=X) , non(o=Z), non(X=Z)

Quelques règles de production pour les non-équations, ou négations d’équations, suffisent pour engendrer toutes les non-équations vraies entre expressions formelles, parce que par définition, deux expressions formelles ne sont égales que si elles sont toutes les deux des combinaisons des mêmes objets de base, avec les mêmes opérateurs appliqués dans le même ordre.

A partir des non-équations vraies on peut engendrer des non-appartenances vraies. Par exemple on a la règle suivante, si non(x=y) alors non(x est dans Singleton de y).

De telles non-appartenances vraies sont les négations de faussetés atomiques les plus élémentaires pour une théorie des ensembles parce qu’on peut les produire sans faire usage du principe d’induction complète. Celui-ci est le principe finitaire le plus important. Il nous donne la capacité de prouver presque tout ce qu’on veut prouver sur les ensembles infinis, pourvu qu’ils soient finitaires. On peut l’énoncer de la façon suivante.

Le schéma d’axiomes du principe d’induction complète

Soit E un ensemble défini par induction à partir d’un élément initial i et d’une fonction génératrice g. Cela veut dire que E contient i et toutes ses images, g(i), g(g(i)), g(g(g(i))), ...obtenues par un nombre fini d’applications de g . E est l’ensemble induit par g à partir de i.

Soit P(x, y1,...,yn) un prédicat d’une théorie des ensembles finitaires, avec n+1 variables libres. La formule suivante est un axiome.

Pour tous y1,...,yn, tout i et toute fonction g

si P(i, y1,...,yn)

et si pour tout x si P(x, y1,...,yn) alors P(g(x), y1,...,yn)

alors pour tout x, si x est dans Ensemble induit par g à partir de i alors P(x, y1,...,yn)

Cet axiome peut servir à prouver la négation d’une fausseté atomique. Si on sait déjà que P(c, y1,...,yn) est faux, on peut déduire que c n’est pas dans E.

Tel qu’il a été explicité, c’est un schéma d’axiomes qui montre comment formuler un nombre infini d’axiomes en remplaçant P(x, y1,...,yn) par les prédicats d’une théorie.

On peut considérer le principe d’induction complète comme une définition de la notion d’ensemble induit, au sens où il fixe la signification de cette notion.

Les vérités atomiques, ou singulières, de l’arithmétique élémentaire, peuvent toutes être connues, ainsi que les négations des faussetés atomiques, sans faire usage de la puissance déductive de la logique du premier ordre. Des règles de production suffisent, parce que l’ensemble des vérités singulières est décidable. On l’apprend tout simplement en apprenant à compter, à faire des additions et des multiplications. En revanche la connaissance des vérités atomiques ensemblistes ne peut pas se passer des lois générales et de la logique du premier ordre. Des raisonnements fondés sur des lois générales permettent parfois de prouver des vérités singulières.

La négation dans les prédicats finitaires

Cette section montre comment élargir l’ontologie de Enum pour introduire la négation dans les prédicats finitaires. Elle expose aussi des règles, et des pseudo-règles, de production pour les négations des faussetés atomiques.

Texte de cette section

Les axiomes d’une théorie élémentaire des ensembles finitaires

Cette section expose les axiomes de Finitaire1, qui est une théorie élémentaire des ensembles finitaires. Finitaire1 est ainsi nommée parce qu’elle peut servir de base pour développer des théories plus puissantes.

L’ontologie de Finitaire1

L’ontologie de Finitaire1, c’est à dire l’ensemble de tous les êtres nommés dans la théorie, contient principalement des expressions formelles et des ensembles. Les autres êtres, les fonctions les prédicats, les X-termes, les Z-termes, sont des objets auxiliaires qui servent à construire des ensembles. Finitaire1 emprunte donc à Enum son ontologie en la complétant avec les négation dans les prédicats.

Les trois objets de base de Finitaire1 sont ceux de Enum, o, X et Z.

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 “=”. Les autres prédicats fondamentaux servent à définir les constructions auxiliaires.

Les 27 prédicats fondamentaux sont ceux de Enum plus “est faux” et “est un prédicat sans variables liées”.

Les axiomes de Finitaire1

Les axiomes sont des formules de la logique du premier ordre, définies avec les objets de base, les opérateurs et les prédicats fondamentaux. Nous verrons plus loin comment le nombre d’opérateurs et de prédicats fondamentaux de Finitaire1 peut être réduit sans modifier véritablement la théorie.

L’axiome d’extensionnalité

L’axiome d’extensionnalité est un axiome nécessaire pour toutes les théories des ensembles. Il dit que deux ensembles sont égaux s’ils ont les mêmes éléments. Si un être n’obéit pas à cet axiome alors il ne peut pas être un ensemble.

Sous la forme suivante, c’est un axiome de Finitaire1.

Pour tout x et tout y, si (x et y sont des ensembles et si pour tout z, (z est dans x équivaut à z est dans y) ) alors x = y

L’inclusion entre ensembles est définie de la façon suivante. x est inclus dans y =def (x et y sont des ensembles et pour tout z, si z est dans x alors z est dans y)

On peut alors énoncer l’axiome d’extensionnalité d’une façon plus brève.

Pour tout x et tout y, si (x est inclus dans y et y est inclus dans x) alors x = y

Les axiomes d’existence des ensembles

Parmi les 27 prédicats fondamentaux de Finitaire1, tous sauf quatre (“=”, “être dans”, “être vrai” et “être 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 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

Il s’agit bien d’une loi générale.

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 Finitaire1.

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 de la logique du premier ordre.