Fondements des mathématiques/Les axiomes des théories des ensembles/Formules initiales et règles de production pour les vérités atomiques d’appartenance aux ensembles énumérables

Les ensembles sont ici des systèmes formels, ou ensembles d'expressions formelles, des ensembles de ces ensembles et ainsi de suite.

Les expressions formelles

Les expressions formelles pourraient être définies comme des suites finies de symboles mais il est plus commode de leur donner la structure formelle de combinaisons d’opérateurs avec des objets de base.

Les nombres entiers positifs peuvent être considérés comme des expressions formelles définies à partir d’un unique objet de base, 0, et d’un opérateur unaire (à une place), s, la fonction de succession. s0=1, ss0=2 et ainsi de suite.

Un nombre fini d’objets de base et d’opérateurs peuvent être choisis pour définir l’ensemble des expressions formelles.Pour la preuve du théorème fondamental de l’énumérabilité, il est commode de choisir un objet de base, appelons-le o, un opérateur unaire, s, et deux opérateurs binaires, a et b.

“est une expression formelle” est un prédicat unaire fondamental de Enum.

Eform1 o est une expression formelle

Eform2 Si x est une expression formelle alors sx est une expression formelle

Eform3 Si x et y sont des expressions formelles alors axy et bxy sont des expressions formelles

(x et y sont des expressions formelles) est une abréviation pour (x est une expression formelle et y est une expression formelle).

Les fonctions

Les termes

De nombreuses fonctions peuvent être définies à partir d’opérateurs fondamentaux quand on introduit des variables et des termes comme objets auxiliaires.

Par exemple, x fois x, ou x au carré, est un terme, dont la seule variable est x. Il définit la fonction qui à x associe son carré.

Quand on introduit les variables et les termes comme des objets, des “quelque chose”, dans la théorie, il faut distinguer entre les constantes et les variables. Les expressions formelles, les ensembles, les fonctions et les prédicats (qui seront introduits plus loin) sont des constantes. Les variables et les termes qui contiennent des variables ne sont pas des constantes. Ce sont des objets auxiliaires, intermédiaires dans les calculs sur les constantes et qui servent à définir des fonctions et des prédicats.

On peut considérer les termes comme des formes, ou des cadres, destinées à être remplies avec des constantes pour former d’autres constantes.

Remplir un terme avec une constante c, consiste à substituer c à toutes les occurrences d’une variable.

Les listes de constantes

Les fonctions peuvent avoir n’importe quel nombre fini de variables, ou arguments. Une façon commode de formaliser cela consiste à introduire un opérateur binaire fondamental C. Cxy est le couple de x et y.

CxCyz est le triplet de x, y et z. et ainsi de suite pour toutes les listes finies. On pourrait aussi définir un triplet par CCxyz. Le choix fait ici est arbitraire, mais une fois qu’il est fait, il vaut mieux s’y tenir, pour simplifier le traitement formel des fonctions. Il en va de même pour les quadruplets, qui sont définis par CwCxCyz, et pour tous les n-uplets, ou listes de n éléments. Dans le traitement formel des fonctions, une distinction des objets simples, ou listes de un élément, parmi les listes est alors requise.

“est simple” et “est une constante” sont des prédicats unaires fondamentaux.

Simp1 Si x est une expression formelle alors x est simple

Simp2 Si x est un ensemble alors x est simple

Const1 Si x est simple alors x est une constante

Const2 Si x et y sont des constantes alors Cxy est une constante

“est un ensemble” est un prédicat unaire fondamental qui sera introduit plus loin. Les expressions formelles, les ensembles, et leurs listes finies, sont les constantes de Enum. Pour simplifier l’ontologie on n’inclut pas les fonctions parmi les constantes. Cela veut dire qu’on ne peut pas construire d’ensembles de fonctions et de fonctions de fonctions. Ces constructions ne sont pas nécessaires ni pour définir les ensembles énumérables.

Les X-variables

Dans Enum, nous introduisons deux ensembles infinis de variables, les X-variables, X, X’, X’’, ... et les Z-variables, Z, Z’, Z’’, ... Les X-variables servent à définir des fonctions, par l’intermédiaire des X-termes. Les Z-variables servent à définir des prédicats, par l’intermédiaire des Z-termes.

“est une X-variable” est un prédicat unaire fondamental, X est un objet de base. Un opérateur unaire ‘ (prime) est introduit pour produire d’autres X-variables, en nombre infini.

Xvar1 X est une X-variable

Xvar2 Si x est une X-variable alors x’ est une X-variable

Ici X est un objet de la theorie de même que X’, X’’, X’’’ et les autres X-variables.

Les X-termes

Les X-termes serviront à définir des fonctions. Les règles suivantes initient l’ontologie des X-termes et donc celle des fonctions. Cette ontologie est déterminante pour la puissance des théories.

Nous définirons deux types de fonctions, celles qui produisent des expressions formelles et celles qui produisent des ensembles. Les premières sont ici appelées fonctions numériques, parce que les expressions formelles sont une sorte de nombres généralisés. Les secondes sont les fonctions ensemblistes. Elles seront introduites plus loin.

“est un X-terme numérique ” est un prédicat unaire fondamental.

Xterme1 Si x est une expression formelle alors x est un X-terme numérique

Xterme2 Si x est une X-variable alors x est un X-terme numérique

Xterme3 Si x et y sont des X-termes numériques alors Cxy est un X-terme numérique

Xt-Num1 Si x est un X-terme numérique alors sx est un X-terme numérique

Xt-Num2 Si x et y sont des X-termes numériques alors axy et bxy sont des X-termes numériques

Chaque X-terme définit une fonction

“est une fonction” est un prédicat unaire fondamental. “Image par...de” est un opérateur binaire fondamental. Il sera souvent abrégé avec “Im par...de”. Ils seront introduits plus loin.

Si f est une fonction et si x est dans le domaine de f alors Image par f de x existe, ou est une constante. Si x n’est pas dans le domaine de f ou si f n'est pas une fonction alors Image par f de x ne peut pas être considéré comme le nom de quelque chose, ou comme une constante.

“Fonction”.est un opérateur unaire fondamental. Il sera souvent abrégé par Fonc.

“est une fonction numérique” et “est un X-terme” sont des prédicats unaires fondamentaux

FoncNum1 Si t est un X-terme numérique alors Fonction t est une fonction numérique

FoncNum2 Si t est un X-terme numérique alors t est un X-terme

FoncNum3 Si f est une fonction numérique alors f est une fonction

= est le prédicat binaire fondamental de l’égalité. Les règles pour l’égalité sont données plus loin.

“est obtenue par une suite correcte de substitutions de la liste... dans” est un prédicat ternaire fondamental qui sera introduit plus loin avec des règles auxiliaires.

On peut alors énoncer la règle fondamentale des fonctions.

Fonc Si t est un X-terme et c est une constante et d est obtenu par une suite correcte de substitutions de la liste c dans t et d est une constante alors d = Image par Fonction t de c

Les parenthèses sont souvent omises dans l’énoncé de ces règles parce qu’elles ne contiennent qu’un seul opérateur “Si...alors”. Il est implicite que les prémisses sont rassemblées entre le si et le alors, de même pour les conclusions qui suivent le alors.

La règle FoncNum1 est la seule qui introduit des fonctions numériques dans l’ontologie de Enum. Toutes les fonctions numériques y sont donc définies par des X-termes numériques. Nous verrons plus loin que l’ontologie des fonctions ensemblistes est également déterminée par l’ontologie des X-termes ensemblistes.

Nous voudrions que s, a et b soient des fonctions pour cette théorie. Mais on ne peut pas simplement dire que s, a et b sont des fonctions parce qu’ils ne sont pas des objets de la théorie et ne peuvent pas l’être, si l’on veut que les règles ordinaires de la grammaire des opérateurs soient respectées. Une formule telle que ass est grammaticalement incorrecte, parce que s n’est pas un nom d’objet mais un nom d’opérateur qui sert à nommer les objets de la théorie.

Mais Fonction sX est un nom pour la fonction s, de même que Fonction aXX’ et Fonction bXX’ pour les fonctions a et b de deux variables.

Règles de base pour les égalités

“=” est un prédicat binaire fondamental.

Les ensembles énumérables peuvent toujours être définis comme des ensembles d’expressions formelles. Pour produire les vérités atomiques sur les ensembles énumérables, on a besoin des équations entre noms d’expressions formelles et entre listes d’expressions formelles. Les équations entre expressions formelles peuvent toutes être engendrées avec l’unique règle Eq1 parce que deux expressions formelles sont égales si et seulement si elles sont composées avec la même combinaison des opérateurs s, a et b, dans le même ordre.

Les égalités entre fonctions ne sont pas nécessaires dans Enum. On n’en a pas besoin pour produire les vérités atomiques d’appartenance aux ensembles énumérables. Comme on va définir des fonctions ensemblistes, on n’aura cependant besoin d’équations entre ensembles. Cela pose a priori un problème, parce que l’égalité des ensembles est fixée par l’axiome d’extensionalité et que l’ensemble de toutes les égalités entre ensembles n’est pas énumérable. Mais pour produire les vérités atomiques d’appartenance aux ensembles énumérables, on n’a pas besoin de toutes les égalités entre ensembles. Les règles Eq1, Fonc et les suivantes suffiront.

Eq1 Si x est une constante alors x = x

La règle suivante suffit alors pour produire toutes les équations entre listes d’expressions formelles.

EqC Si x = y et v = w alors Cxv = Cyw

Les noms d’expressions formelles peuvent contenir des fonctions. La règle Fonc2 produit des égalités qui contiennent de tels noms. Pour produire les autres, on a besoin des règles suivantes.

Eq1 Si x = y alors y = x

Eq2 Si x = y et y = z alors x = z

EqIm Si x = y et Image de x par f est une constante alors Image de x par f = Image de y par f

Eq2 est la règle fondamentale qui permet d’enchainer des calculs.

Ces règles doivent être complétées par les deux suivantes pour pouvoir enchainer les productions.

EqEform Si x = y et x est une expression formelle alors y est une expression formelle

EqEns Si x = y et x est un ensemble alors y est un ensemble EqDans Si x = y et x est dans z alors y est dans z

La construction finitaire des ensembles infinis

“est dans” est un prédicat binaire fondamental.

“est un ensemble” est un prédicat unaire fondamental.

“Ensemble induit par...à partir de” est un opérateur binaire fondamental. Il sera souvent abrégé par “Ind par...de”.

Ensemble induit par g à partir de i est l’ensemble qui contient i et toutes ses images, g(i), g(g(i)), g(g(g(i))), ...obtenues par un nombre fini d’applications de g.

Infini1 Si i est une constante et g est une fonction alors Ensemble induit par g à partir de i est un ensemble

Infini2 Si i est une constante et g est une fonction alors i est dans Ensemble induit par g à partir de i

Infini3 Si x est dans Ensemble induit par g à partir de i alors Image par g de x est dans Ensemble induit par g à partir de i

Ensemble induit par g à partir de i est souvent infini, pour de nombreuses fonctions g.

Ces règles permettent de prouver une version finitaire de l’axiome de l’infini.

Les extensions des prédicats finitaires

L’axiome de compréhension de Frege dit que pour tout prédicat, ou concept, il existe l’ensemble de tous les êtres pour lesquels ce concept est vrai. Autrement dit, tout concept a une extension conceptuelle. Russell a prouvé que cet axiome est trop général pour être cohérent. Nous avons donc besoin d’une forme plus faible de l’axiome de compréhension si nous voulons une théorie fiable.

Dans les mathématiques finitaires, il semble assez naturel de se limiter aux constructions prédicatives des ensembles. Cela veut dire que le prédicat par lequel on définit un ensemble ne mentionne que des ensembles déjà définis. Même le domaine d’existence, associé aux opérateurs d’existentiation et de généralisation doit être un ensemble déjà défini.

L’axiome de séparation de Zermelo va au delà des définitions prédicatives parce qu’il autorise comme domaine d’existence la classe de tous les ensembles. Ces définitions non-prédicatives posent des difficultés quand on cherche des preuves de cohérence. Elles semblent cependant assez indispensables à certaines parties avancées des mathématiques.

Ici nous allons d’abord définir les prédicats comme des objets de la théorie. (Etre un objet de la théorie, c’est faire partie de son domaine d’existence, ou de son univers.) Parmi les prédicats, on distinguera les prédicats finitaires. Dans Enum, les prédicats finitaires sont toujours obtenues avec des conjonctions, des disjonctions et des existentiations à partir de prédicats atomiques.

Des règles finitaires plus générales, qui introduisent la négation dans les prédicats, et permettent d’y définir des généralisations prédicatives peuvent être énoncées pour obtenir des théories plus puissantes que Enum. Elles ne sont pas nécessaires pour définir les ensembles énumérables.

Les prédicats finitaires ne contiennent que des variables prédicatives. Les premières variables prédicatives sont celles qui varient seulement sur un ensemble nommé dans le prédicat, une constante. Les autres variables prédicatives ne doivent varier qu’à l’intérieur d’un ensemble désigné par une variable dont on sait déjà qu’elle est prédicative.

“est un prédicat finitaire” est un prédicat unaire fondamental et sera introduit plus loin.

“Extension de” est un opérateur unaire fondamental, il sera souvent abrégé par Ext.

Frege1 Si x est un prédicat finitaire alors Extension de x est un ensemble

Frege2 Si p est un prédicat finitaire et q est obtenu par une suite correcte de substitutions de la liste c dans p et q est vrai alors c est dans Extension de p

“est vrai” est un prédicat unaire fondamental et est introduit plus loin.

Les Z-variables et les Z-termes

Les X-variables ne sont pas introduites dans les prédicats, parce que pour le traitement à venir des fonctions ensemblistes, on a besoin d’une nette séparation entre la substitution à des X-variables et la substitution à des Z-variables.

“est une Z-variable” et “est un Z-terme” sont des prédicats unaires fondamentaux.

Zvar1 Z est une Z-variable

Zvar2 Si x est une Z-variable alors x’ est une Z-variable

Zterm1 Si x est une Z-variable alors x est un Z-terme

Zterm2 Si x est une constante alors x est un Z-terme

Zterm3 Si x est un Z-terme et f est une fonction alors Im par f de x est un Z-terme

Zterm4 Si x et y sont des Z-termes alors Cxy est un Z-terme

Des prédicats

“Dans” et “Egale” sont des opérateurs binaires fondamentaux.

Ils ne sont pas des prédicats fondamentaux de Enum mais seulement des opérateurs qui servent à nommer des prédicats formels. On emploie ici prédicat en deux sens, d’une part les prédicats fondamentaux de Enum, qui ne sont pas des objets de Enum, d’autre part, les prédicats formels, ou tout simplement prédicats, qui sont des objets de Enum. Le contexte doit suffire pour comprendre à chaque fois de quels prédicats l’on parle.

“est un prédicat” est un prédicat unaire fondamental. On pourrait dire aussi, “est un prédicat formel”, pour éviter l’équivoque, mais je n’adopterai pas cet usage, pour éviter des formulations trop lourdes.

PredDans Si x est un Z-terme et (y est un ensemble ou y est une Z-variable) alors (x Dans y) est un prédicat

PredEgale Si x et y sont des Z-termes alors (x Egale y) est un prédicat

“...Et....”, “...Ou...” et “il existe un...tel que” sont des opérateurs binaires fondamentaux qui servent à nommer des prédicats. Ils sont distincts des opérateurs logiques de conjonction, de disjonction et d’existentiation utilisés dans toutes les théories.

PredEt Si p et q sont des prédicats alors (p Et q) est un prédicat

PredOu Si p et q sont des prédicats alors (p Ou q) est un prédicat

PredExist Si x est une Z-variable et p est est un prédicat alors (il existe un x tel que p) est un prédicat

Des prédicats finitaires

PredFinDans Si x est un Z-terme et y est un ensemble alors (x Dans y) est un prédicat finitaire

PredFinEgale Si c est une constante et x est une Z-variable alors (x Egale c) et (c Egale x) sont des prédicats finitaires

PredFinEt1 Si p et q sont des prédicats finitaires alors (p Et q) est un prédicat finitaire

PredFinEt2 Si x est un Z-terme et y est une Z-variable et p est un prédicat finitaire et y a au moins une occurrence dans p alors ((x Dans y) Et p) et (p Et (x Dans y)) sont des prédicats finitaires

PredFinEt3 Si x et y sont des Z-termes et ont toutes leurs variables dans p et p est un prédicat finitaire alors ((x Egale y) Et p) et (p Et (x Egale y)) sont des prédicats finitaires

La règle suivante est ainsi nommée parce qu’elle permet de prouver une version finitaire de l’axiome de remplacement.

Fraenkel Si x est une Z-variable et y est un Z-terme et p est un prédicat finitaire et y a toutes ses variables dans p alors ((x Egale y) Et p) et (p Et (x Egale y)) sont des prédicats finitaires

PredFinOu Si p et q sont des prédicats finitaires et p a toutes ses variables dans q et q a toutes ses variables dans p alors (p Ou q) est un prédicat finitaire

“a au moins une occurrence dans” et “a toutes ses variables dans” sont des prédicats binaires fondamentaux introduits avec les règles auxiliaires sur les variables.

PredFinExist Si p est un prédicat finitaire et x est une Z-variable alors (il existe un x tel que p) est un prédicat finitaire

Un prédicat de vérité

“est vrai” est un prédicat unaire fondamental.

Pvrai1 Si x est dans y alors (x Dans y) est vrai

Pvrai2 Si x = y alors (x Egale y) est vrai

PvraiEt Si p et q sont vrais alors (p Et q) est vrai

“est une assertion” est une prédicat unaire fondamental.

Asser1 Si x est une constante et y est un ensemble alors (x Dans y) est une assertion

Asser2 Si x et y sont des constantes alors (x Egale y) est une assertion

Asser3 Si p et q sont des assertions alors (p Et q) et (p Ou q) sont des assertions

PvraiOu Si p est vrai et q est une assertion alors (p Ou q) et (q Ou p) sont vrais

PvraiExist Si p est vrai et c est une constante et c est simple et z est une Z-variable et p est obtenu à partir de la substitution de c à toutes les occurrences de z dans q alors (il existe un z tel que q) est vrai

Ce prédicat de vérité est partiel. Il ne détermine la vérité que des énoncés formés avec des égalités et des appartenances.

Des opérateurs ensemblistes dérivés

Les opérateurs Singleton de, Paire de, Union, Inter, Ensemble-somme de, Ensemble-image par...de, et Produit cartésien de...et, peuvent être définis avec la présente ontologie des prédicats finitaires.

Singleton de x est l’ensemble qui contient x comme unique élément.

Singleton de x =def Extension de Z Egale x

Paire de x et y =def Extension de (Z Egale x Ou Z Egale y)

x Union y =def Extension de (Z Dans x Ou Z Dans y)

x Inter y =def Extension de (Z Dans x Et Z Dans y)

Ensemble-somme de x =def Extension de (il existe un Z' tel que (Z' Dans x Et Z Dans Z'))

Ensemble-image par f de x =def Extension de (il existe un Z' tel que(Z' Dans x Et Z Egale Image par f de Z'))

Produit cartésien de x et y =def Extension de (Z Dans x Et Z’ Dans y)

Singleton de et Union permettent de construire tous les ensembles finis.

Les règles suivantes ne sont pas des règles de production de Enum. Ce sont des règles dérivées à partir des règles déjà énoncées (et des règles auxiliaires, exposées plus loin) et de la définition des opérateurs ensemblistes.

Sing1 Si x est une constante alors Singleton de x est un ensemble

Sing2 Si x est une constante alors x est dans Singleton de x

Union1 Si x et y sont des ensembles alors x Union y est un ensemble

Union2 Si z est dans x ou z est dans y alors z est dans x Union y

Inter1 Si x et y sont des ensembles alors x Inter y est un ensemble

Inter2 Si z est dans x et z est dans y alors z est dans x Inter y

L’opérateur Union permet de faire la réunion d’un nombre fini d’ensembles.

Comme abréviation dans les preuves à venir, on introduira Union(E, F,...G) où E, F, ..., G est une liste finie d’ensembles pour abréger ((E Union F) Union ... Union G).

“Ensemble-somme de...” permet de faire la réunion d’un ensemble fini ou infini d’ensembles.

Esom1 Si x est un ensemble alors Ensemble-somme de x est un ensemble

Esom2 Si y est dans z et z est dans x alors y est dans Ensemble-somme de x

Eim1 Si x est un ensemble et f est une fonction alors Ensemble-image de x par f est un ensemble

Eim2 Si x est dans y et Image de x par f est une constante alors Image de x par f est dans Ensemble-image de y par f

Pcart1 Si x et y sont des ensembles alors Produit cartésien de x et y est un ensemble

Pcart2 Si u est dans x et v est dans y alors Cuv est dans Produit cartésien de x et y

Produit cartésien de x et y peut être abrégé par (x Pcart y).

Les fonctions ensemblistes

Pour définir des fonctions ensemblistes, c’est à dire des fonctions qui associent des ensembles à des ensembles, on définit des X-termes ensemblistes qui déterminent des extensions. Pour cela on a besoin de la règle suivante.

XtZt Si x est un Z-terme alors x est un X-terme

Dans les X-termes, les Z-variables sont considérées comme des constantes. Cela veut dire que seules les X-variables donnent lieu à des substitutions. Les Z-termes servent seulement à construire des prédicats dont on prend ensuite l’extension.

XtDans Si x et y sont des X-termes alors x Dans y est un X-terme

XtEgale Si x et y sont des X-termes alors x Egale y est un X-terme

XtEt Si x et y sont des X-termes alors x Et y est un X-terme

XtOu Si x et y sont des X-termes alors x Ou y est un X-terme

XtExist Si x est un X-terme et z est une Z-variable alors (il existe un z tel que x) est un X-terme

XtExt Si t est un X-terme alors Extension de t est un X-terme

La règle suivante permet alors de définir toutes les fonctions ensemblistes dont on a besoin dans Enum.

FoncEns1 Si t est un X-terme alors Fonction Extension de t est un fonction ensembliste

FoncEns2 Si f est une fonction ensembliste alors f est une fonction

On n’ a pas donné la règle pour l’introduction de “Ensemble induit par...à partir de” dans les X-termes parce qu’elle n’est pas nécessaire pour définir les ensembles énumérables.

Règles auxiliaires pour les variables

L’égalité, l'ordre et la différence des variables

“est avant” et “≠” sont des prédicats binaires fondamentaux. x ≠ y veut dire que x n’est pas égal à y, mais il n’est pas défini ainsi à l’intérieur de Enum, parce qu’on n’y veut pas de négations.

EqXvar Si x est une X-variable alors x = x

EqZvar Si x est une Z-variable alors x = x

OrVar1 Si x est une X-variable alors X est avant x’

OrVar2 Si x est une Z-variable alors Z est avant x’

OrVar3 Si x est avant y alors x’ est avant y’

DiffVar1 Si x est avant y alors x ≠ y et y ≠ x

DiffVar2 Si x est une X-variable et y est une Z-variable alors x ≠ y et y ≠ x

La substitution à toutes les occurrences d’une variable

“est obtenu par la substitution de...à toutes les occurrences de...dans” est un prédicat fondamental quaternaire. subst vyxu est une abréviation pour v est obtenu par la substitution de y à toutes les occurrences de x dans u.

x est une variable =def (x est une X-variable ou x est une Z-variable)

SubVar1 Si c est une constante et x est une variable alors c est obtenu par la substitution de c à toutes les occurrences de x dans x

SubVar2 Si c est une constante et x et y sont des variables et x ≠ y alors x est obtenu par la substitution de c à toutes les occurrences de y dans x

SubConst Si c et d sont des constantes et x est une variable alors c est obtenu par la substitution de d à toutes les occurrences de x dans c

SubC Si subst vyxu et subst qyxp alors subst (Cvq)yx(Cup)

SubIm Si subst vyxu et f est une fonction alors subst (Image par f de v)yx(Image par f de u)

SubExt1 Si subst vyxu et x est une X-variable alors subst (Extension de v)yx(Extension de u)

SubExt2 Si subst vyxu et x est une Z-variable alors subst (Extension de u)yx(Extension de u)

Les règles SubstIm , SubExt1 et SubExt2 sont subtiles. Lorsque f est défini par un terme t, f = Fonction t, son nom contient en général des X-variables , celles qui ont des occurrences dans t. Mais ces variables ne sont pas libres. On ne doit pas y faire de substitutions parce que cela changerait la constante f. On dit que ces variables sont liées par l’opérateur Fonction. La règle SubIm respecte le principe que les variables liées ne sont pas concernées par les substitutions, de même que la règle SubstExt2, parce que les Z-variables sont liées par l’opérateur Extension. En revanche les X-variables ne sont pas liées par cet opérateur. Parmi les fonctions de Enum définies par des X-termes qui contiennent des Z-variables, les seules qui sont vraiment intéressantes sont celles pour lesquelles ces variables sont liées et il n’est pas nécessaire de faire des substitutions aux occurrences des Z-variables dans Fonction t. Pour élargir l’ontologie avec des fonctions de fonctions, on peut introduire des Y-variables.

Il faut introduire des règles semblables à SubC pour tous les opérateurs qui servent à construire des X-termes et des prédicats.

Subs Si subst vyxu alors subst (sv)yx(su)

Suba Si subst vyxu et subst qyxp alors subst (avq)yx(aup)

Subb Si subst vyxu et subst qyxp alors subst (bvq)yx(bup)

SubDans Si subst vyxu et subst qyxp alors subst (v Dans q)yx(u Dans p)

SubEgale Si subst vyxu et subst qyxp alors subst (v Egale q)yx(u Egale p)

SubEt Si subst vyxu et subst qyxp alors subst (v Et q)yx(u Et p)

SubOu Si subst vyxu et subst qyxp alors subst (v Ou q)yx(u Ou p)

SubExist1 Si subst vyxu et x ≠ z alors subst (il existe un z tel v)yx(il existe un z tel que u)

SubExist2 Si z est une Z-variable et y est une constante et u est un prédicat alors subst (il existe un z tel que u)yz(il existe un z tel que u)

“est premier dans” est un prédicat binaire fondamental.

VarPrem1 Si x est une variable alors x est premier dans x

VarPrem2 Si x est premier dans t et z est une constante alors x est premier dans Ctz et x est premier dans Czt

VarPremC Si x est premier dans t et y est premier dans u et (x est avant y ou x = y) alors x est premier dans Ctu et dans Cut

VarPremIm Si x est premier dans t et f est une fonction alors x est premier dans Image par f de t

VarPremExt Si x est une X-variable et est premier dans t alors x est premier dans Extension de t

Il faut introduire des règles semblables pour tous les opérateurs qui servent à construire des X-termes et des prédicats.

VarPrems Si x est premier dans t alors x est premier dans st

VarPrema Si x est premier dans t et y est premier dans u et (x est avant y ou x = y) alors x est premier dans atu et dans aut

VarPremb Si x est premier dans t et y est premier dans u et (x est avant y ou x = y) alors x est premier dans btu et dans but

VarPremDans Si x est premier dans t et y est premier dans u et (x est avant y ou x = y) alors x est premier dans (t Dans u) et dans (u Dans t)

VarPremEgale Si x est premier dans t et y est premier dans u et (x est avant y ou x = y) alors x est premier dans (t Egale u) et dans (u Egale t)

VarPremEt Si x est premier dans t et y est premier dans u et (x est avant y ou x = y) alors x est premier dans (t Et u) et dans (u Et t)

VarPremOu Si x est premier dans t et y est premier dans u et (x est avant y ou x = y) alors x est premier dans (t Ou u) et dans (u Ou t)

VarPremExist Si x est premier dans t et x ≠ z alors x est premier dans (il existe un z tel que t)

Les suites correctes de substitutions de variables

“est obtenu par une substitution correcte de ... dans” et “est obtenu par une suite correcte de substitutions de la liste ... dans” sont des prédicats ternaires fondamentaux.

SubCor1 Si t est un X-terme et x est une X-variable et x est premier dans t et subst uwxt et w est simple alors u est obtenu par une substitution correcte de w dans t

SubCor2 Si p est un prédicat et x est une Z-variable et x est premier dans p et subst qwxt et w est simple alors q est obtenu par une substitution correcte de w dans p

SubCor3 Si v est obtenu par une substitution correcte de w dans u alors v est obtenu par une suite correcte de substitutions de la liste w dans u

SubCor4 Si v est obtenu par une suite correcte de substitutions de la liste w dans u et x est obtenu par une substitution correcte de y dans v alors x est obtenu par une suite correcte de substitutions de la liste Cyw dans u

Ces règles prescrivent l’ordre des substitutions des éléments d’une liste aux variables d’un X-terme ou d’un prédicat. Par exemple a(sso)a(so)o est obtenu par une suite correcte de substitutions de la liste CoCso(sso) dans aXaX’X’’.

Pour ne pas compliquer le formalisme, on n’a pas donné assez de règles pour produire toutes les vérités lorsque les premières variables libres dans un prédicat sont quantifiées. Cela oblige alors à quantifier uniquement sur les dernières variables libres d’un prédicat pour que les suites correctes de substitutions soient produites.

Les occurrences des Z-variables

“a au moins une occurrence dans” est un prédicat binaire fondamental.

OcZvar1 Si x est une Z-variable alors x a au moins une occurrence dans x

OcZvar2 Si t et z sont des Z-termes et x a au moins une occurrence dans t alors x a au moins une occurrence dans Ctz et dans Czt

OcZvar3 Si t est un Z-terme et x a au moins une occurrence dans t et f est une fonction alors x a au moins une occurrence dans Image par f de t

OcZvar4 Si x a au moins une occurrence dans t et y est un Z-terme alors x a au moins une occurrence dans (t Dans y), dans (y Dans t), dans (y Egale t) et dans (t Egale y)

OcZvar5 Si p et q sont des prédicats et x a au moins une occurrence dans p alors x a au moins une occurrence dans (p Et q) et x a au moins une occurrence dans (p Ou q)

OcZvar6 Si p est un prédicat et x a au moins une occurrence dans p et x ≠ z alors x a au moins une occurrence dans (il existe un z tel que p)

L’inclusion des variables dans les Z-termes

“a toutes ses variables dans” est un prédicat binaire fondamental.

IncVarTerm1 Si x est un Z-terme alors x a toutes ses variables dans x

IncVarTerm2 Si x est une constante et y est un Z-terme alors x a toutes ses variables dans y

IncVarTerm3 Si x a toutes ses variables dans y et z est un Z-terme alors x a toutes ses variables dans Cyz et dans Czy

IncVarTerm4 Si x et y ont toutes leurs variables dans z alors Cxy a toutes ses variables dans z

IncVarTerm5 Si x a toutes ses variables dans y et u a toutes ses variables dans v alors Cxu a toutes ses variables dans Cyv et dans Cvy

IncVarTerm6 Si x a toutes ses variables dans y et y est un Z-terme et f est une fonction alors x a toutes ses variables dans Image par f de y et Image par f de x a toutes ses variables dans y

L’inclusion des variables dans les prédicats

IncVarPred1 Si x , y et z sont des Z-termes et x a toutes ses variables dans Cyz alors x a toutes ses variables dans (y Dans z)

IncVarPred2 Si z est un prédicat et x et y sont des Z-termes et ont toutes leurs variables dans z alors (x Dans y) et (x Egale y) ont toutes leurs variables dans z

IncVarPred3 Si p, q et r sont des prédicats et p a toutes ses variables dans q alors p a toutes ses variables dans (q Et r), dans (r Et q), dans (q Ou r) et dans (r Ou q)

IncVarPred4 Si p, q et r sont des prédicats et p et q ont toutes leurs variables dans r alors (p Et q) et (p Ou q) ont toutes leurs variables dans r

IncVarPred5 Si p et q sont des prédicats et z est une Z-variable et p a toutes ses variables dans Cqz alors (il existe un z tel que p) a toutes ses variables dans q

IncVarPred6 Si p et q sont des prédicats et z est une Z-variable et Cpz a toutes ses variables dans q alors p a toutes ses variables dans (il existe un z tel que q)

Conclusion : la définition du système Enum de toutes les vérités atomiques d’appartenance à tous les ensembles énumérables

Les 3 objets de base de Enum

o * X * Z

Les 14 opérateurs fondamentaux de Enum

s * a * b * C * ‘ (prime) * Image par...de * Fonction * Ensemble induit par...à partir de * Extension de * Dans * Egale * Et * Ou * il existe un...tel que

Les 25 prédicats fondamentaux de Enum

est une expression formelle * est un ensemble * est dans * = * est simple * est une fonction numérique * est une fonction * est une constante * est une X-variable * est un X-terme * est une Z-variable * est un Z-terme * est un prédicat * est un prédicat finitaire * est vrai * est une assertion * est une fonction ensembliste * est avant * ≠ * est obtenu par la substitution de...à toutes les occurrences de...dans * est premier dans * est une substitution correcte de...dans * est une suite correcte de substitutions de la liste...dans * a au moins une occurrence dans * a toutes ses variables dans

Les 3 formules initiales de Enum

o est une expression formelle * X est une X-variable * Z est une Z-variable

Les 122 règles de production de Enum

Ce sont toutes celles qui ont été exposées, sauf les règles dérivées.