Fondements des mathématiques/Cohérence des théories finitaires
La construction d’un modèle de Finitaire1
[modifier | modifier le wikicode]Pour prouver que Finitaire1 est cohérente il suffit de lui trouver un modèle. La construction de l’ensemble des formules atomiques est la partie un peu difficile de la preuve. Dès que cet ensemble est défini, la preuve que tous les axiomes de Finitaire1 sont vrais pour ce modèle est aussi triviale que la preuve formelle de la vérité des axiomes de l’arithmétique formelle. Il suffit d’écrire les définitions, d’appliquer des règles logiques simples pour déduire formellement des évidences naturelles et on obtient le théorème de cohérence au bout de quelques dizaines de pages.
Nous verrons que pour construire un modèle de Finitaire1 convenable pour formaliser la preuve de cohérence, il faut élargir son ontologie. Un seul axiome d’existence supplémentaire suffit.
Infini4 Si x est un X-terme et f est une fonction alors Ensemble induit par f à partir de x est un X-terme
Plus exactement, la formule généralisée et close obtenue à partir de cette règle est choisie comme axiome. La théorie Finitaire2 est définie avec tous les axiomes de Finitaire1 et cet unique axiome supplémentaire. La définition d’un modèle de Finitaire2 est laissée en exercice. Elle ne pose pas de difficultés de principe. Il en va de même pour d’autres théories finitaires élargies.
L’axiome supplémentaire de Finitaire2 permet de définir des fonctions qui incluent une ou plusieurs inductions infinies dans leur définition. Cela permet de construire des ensembles par des inductions infinies sur des constructions par induction infinie. C’est exactement ce dont nous aurons besoin pour définir un modèle de Finitaire1.
Parmi les 27 prédicats fondamentaux de Finitaire1, tous sauf quatre, « est dans », « = », « est vrai » et « est faux » ne posent aucune difficulté. L’ensemble de toutes les vérités atomiques formulées avec ces 23 prédicats est énumérable. Il est engendré avec les règles de production de Enum et les règles supplémentaires de Finitaire1. Tous les axiomes de Finitaire1 qui traduisent ces règles sont évidemment vrais quand on prend cet ensemble de vérités atomiques comme modèle.
Les vérités atomiques formulées avec « est vrai » et « est faux » peuvent toutes être obtenues à partir des vérités atomiques d’égalité et d’appartenance, par la même technique qui sert à construire l’ensemble des vérités à partir d’un modèle
Les égalités entre expressions formelles, qu’elle soient nommées directement ou par l’intermédiaire d’une fonction numérique, sont également toutes énumérables.
Il nous suffit donc définir l’ensemble des vérités atomiques d’appartenance et d’égalités entre ensembles.
Pour définir un modèle de Finitaire1, on part de Enum et on le complète pour inclure toutes les vérités atomiques sur les ensembles définis par l’extension de prédicats avec négation.
Nous allons raisonner par induction sur la complexité des définitions d’ensembles. Celle-ci est mesurée par deux indices, appelés ici complexités fonctionnelle et formelle.
Si un prédicat finitaire ne contient pas de fonctions ensemblistes dans sa définition, sa complexité fonctionnelle est zéro.
Toutes les fonctions ensemblistes définies par des prédicats de complexité fonctionnelle n sont également de complexité fonctionnelle n.
Si un prédicat finitaire contient des fonctions ensemblistes de complexité fonctionnelle n dans sa définition et si toutes les autres fonctions ensemblistes qu’il contient sont de complexité fonctionnelle inférieure à n alors il est de complexité fonctionnelle n+1.
La complexité formelle d’un prédicat est le nombre maximal d’opérateurs emboîtés, Et, Ou, Non, (il existe un…tel que…), qu’il contient. Les prédicats atomiques sont de complexité formelle zéro.
Définissons une ontologie ensembliste progressive O(n) de la façon suivante. O(0) est l’ontologie ensembliste de Enum, c’est-à-dire l’ensemble de tous les ensembles, de toutes les expressions formelles, et de toutes leurs listes finies, qui ont un nom dans Enum.
O(n+1) est l’ensemble de tous les êtres qui satisfont à l’une des trois conditions suivantes.
(i) être dans O(n)
(ii) être égal à Ensemble induit par g à partir de x, où x est dans O(n) et g est n’importe quelle fonction de Finitaire1 telle que toutes les constantes qui entrent dans sa définition sont dans O(n).
Appelons O1(n+1) l’ensemble de toutes les listes finies d’êtres qui satisfont (i) ou (ii).
(iii) être égal à Image par f de x où x est dans O1(n+1) et f est n’importe quelle fonction de Finitaire1 telle que toutes les constantes qui entrent dans sa définition sont dans O1(n+1)
L’ontologie de Finitaire1 est obtenue en prenant la somme des O(n) pour tous les nombres entiers positifs n.
Comme toutes les définitions de Finitaire1 sont prédicatives, nous pourrons montrer que les éléments d’un ensemble de O(n) sont toujours ou bien des expressions formelles ou bien des ensembles de O(n). On voit ici l’importance des définitions prédicatives dans la définition de notre ontologie progressive. Elles permettent d’associer à la progression ontologique un ordre dans la production des vérités.
At(n) est l’ensemble des assertions atomiques de degré n. At(n) contient toutes les égalités vraies ou fausses entre éléments de O(n) et tous les énoncés d’appartenance d’un élément de O(n) à un élément de O(n).
Vat(n) est l’ensemble des vérités atomiques de degré n (appartenances et égalités) associées à O(n).
Vat(0) =def toutes les vérités atomiques d’appartenance et toutes les égalités entre expressions formelles et entre ensembles définis dans Enum.
Nous allons définir une fonction qui permet de construire Vat(n+1) à partir de Vat(n). La somme Vat des Vat(n) sera le modèle cherché de Finitaire1.
À partir de Vat(n) il est aisé de produire Vat1(n+1), l’ensemble de toutes les vérités atomiques sur les éléments de O1(n+1) pour les raisons suivantes. Comme la complexité d’un X-terme est arbitrairement grande, les images d’un élément de O(n) par une fonction itérée un nombre de fois aussi grand que l’on veut sont toujours dans O(n). On peut donc produire à partir de Vat(n) toutes les vérités atomiques d’appartenance à (Ensemble induit par f à partir de x) pour n’importe quel x dans O(n) et n’importe quel f qui satisfait aux conditions citées en (ii). On peut alors définir l’ensemble de toutes les égalités entre ces ensembles induits et avec les éléments de O(n) et finalement toutes les égalités entre les listes finies d’éléments de O1(n+1).
At1(n+1) est l’ensemble des assertions atomiques (appartenance ou égalité) vraies ou fausses sur les éléments de O1(n+1).
Fat1(n+1) =def At1(n+1) Moins Vat1(n+1) , est l’ensemble des faussetés atomiques.
Nous allons montrer qu’à partir de Vat1(n+1) et Fat1(n+1) on peut définir par une double induction infinie sur la complexité des prédicats l’ensemble Vat(n+1).
Soit Vat(n+1, i, j) l’ensemble des vérités atomiques sur des ensembles définis par des prédicats de complexité fonctionnelle i ou inférieure, de complexité formelle j ou inférieure, et dont les constantes sont toutes dans O1(n+1).
On définit de même At(n+1, i, j) et Fat(n+1, i, j) = At(n+1, i, j) Moins Vat(n+1, i, j).
Vat(n+1, 0, 0) = Vat1(n+1)
Vat(n+1, i, j+1) peut être construit à partir de Vat(n+1, i, j) et Fat(n+1, i, j). La même technique qui sert à définir l’ensemble des vérités à partir d’un modèle sert ici à remplir tous les ensembles définis avec des prédicats de complexité formelle j+1. Les égalités entre ces ensembles et avec les ensembles précédemment définis sont alors déterminées par l’axiome d’extensionalité.
Vat(n+1, i+1, 0) peut être construit lorsque les Vat(n+1, i, j) ont tous été définis, parce que toutes les vérités atomiques sur les images par des fonctions de complexité fonctionnelle i ont été précédemment déterminées.
Vat(n+1) =def Somme des Vat(n+1, i, j) pour i et j entiers positif
Vat =def Somme des Vat(n) pour n entier positif.
Vat est définie avec une induction infinie par la fonction qui produit Vat(n+1) à partir de Vat(n). Mais cette fonction requiert elle-même une induction infinie dans sa définition. Cela montre le rôle de l’axiome supplémentaire de Finitaire2 pour cette construction du modèle Vat de Finitaire1.
