Les corps commutatifs

1) Introduction

La structure de corps constitue le fondement permettant de formaliser et de résoudre les équations courantes. Il découle de ce constat que de nombreuses propriétés sur les équations réelles ou complexes se déclinent en des propriétés similaires valables pour les autres corps.

On s'intéresse aux corps finis ou infinis de type fini, c'est à dire engendrés par un nombre fini d'éléments, où on entend par engendré, le fait que tout élément est obtenu par une composition close d'opérateurs générateurs de la structure. On fait ce choix d'une approche constructive car celle-ci nous assure la cohérence dans les logiques d'ordre supérieure, et nous maintient en sympathie avec l'informatique.

On commence par décrire la structure de corps commutatif telle qu'elle est présentée de façon académique à partir de ses deux seuls opérateurs binaires appelés addition et multiplication. Et on en décrit sa théorie. C'est la présentation académique de la structures, qui joue le rôle d'interface, et qui engendre un langage de composition d'opérateurs et un langage logique du premier ordre. On aborde ainsi la théorie de la démonstration et la théorie des modèles. On décrit le langage de composition d'opérateurs, le langage de la logique du premier ordre, et leur grammaires formelles. Puis on décrit les règles de déductions, ce qu'est une démonstration.

On décrit ce qu'est une théorie d'égalité. On décrit la calculabilité des opérateurs. On décrit la définissabilité des opérateurs. On décrit les structures de demi-corps commutatif, demi-anneau commutatif, anneau commutatif, qui ont même langage et qui mettent en oeuvre une propriété fondamentale qu'est l'associativité des opérateurs et la distributivité de la multiplication par rapport à l'addition. Puis on décrit ce qu'est la structure en tant que modèle, et ce que peut être un modèle (ou monde). On décrit ce qu'est un morphisme et un isomorphisme.

Puis on décrit l'extension d'une structure selon le point de vue constructif par l'ajout d'un élément connue ou inconnue. Puis on définie l'extension libre, puis on la décrit de façon contrainte par une théorie d'égalité. Puis on décrit l'extension de demi-anneau commutatif, de demi-corps commutatif, et de corps commutatif. Cette extension diffère de l'extension classique basée sur un plongement, car elle englobe tous les plongement possible, elle produit non pas une structure mais une superposition de structures, qui par analogie à la mécanique quantique, correspond à une superposition d'états.

2) Corps commutatif

Bien qu'elle peut paraître compliquée, il est judicieux de commencer par étudier la structure de corps commutatif, parcequ'elle est utilisée concrètement dans la vie de tous les jours. Et c'est en étudiant ses différentes parties que l'on étudiera les structures plus rudimentaires. On sépare la description des opérateurs de celle de leur syntaxe. La syntaxe est là pour définir un langage formel simplifié, plus pratique. Mais il ne s'agit pas toujours que d'une apparence, car la nature de la structure entretient parfois des liens étroits avec son langage, et donc révèle une partie de son être dans la forme de son apparence.

2.1) Opérateurs

Le corps commutatif se définit de façon académique en énumérant juste trois objets `(K,"+","∗")`. Il comprend un ensemble sous-jacent `K` regroupant l'ensemble des éléments du corps, que l'on muni de deux lois internes que sont l'addition notée `"+(.,.)"` et la multiplication notée `"∗(.,.)"`. L'addition est associative, commutative, admet un élément neutre noté `0`, appelé élément nul ou le zéro, et pour chaque élément `x` il existe un opposé noté `-x` qui ajouté à `x` redonne `0`. La multiplication est associative, commutative, admet un élément neutre noté `1`, et pour chaque éléments non nuls, `x"≠"0`, il existe un inverse noté `sf"inv"(x)` qui multiplié par `x` redonne `1`. Le zéro `0` est absorbant. Et la multiplication est distributive par rapport à l'addition.

2.2) Syntaxe

Une composition d'opérateurs est un arbre dans lequel chaque noeud est un opérateur et les fils de chaques noeud sont les arguments des opérateurs et constituent des sous-arbres. La représentation sous forme d'une formule linéaire (une suite de caractères) utilise l'emboitement des parenthèses pour créer la dimension supplémentaire qu'est la profondeur de l'arbre.

Pour réduire l'usage des parenthèses ainsi que d'autres symboles, on fait le choix d'une syntaxe : Les opérateurs d'addition et de multiplication possèdent une syntaxe centrée, `"+"(x,y) = x"+"y` et `"∗"(x,y) = x"∗"y`. La priorité syntaxique de la multiplication est plus forte que celle de l'addition, faisant que `x"+"y"∗"z = x"+"(y"∗"z)`.

On définit l'opérateur binaire de soustraction `-"(.,.)"` de syntaxe centrée comme suit : `x-y` `"="` `x+(-y)`. La priorité syntaxique de la soustraction est égale à celle de l'addition, et ces deux opérations ont un sens syntaxique d'évaluation qui est le sens de lecture, de gauche à droite, et qui signifie que l'on évalue l'argument de gauche avant l'argument de droite, faisant que `a-c+b-d+e` `"="` `(((a-c)+b)-d)+e`. Ce sens syntaxique est celui par défaut.

On notera souvent la multiplication `"∗"` par absence de symbole de telle sorte que par exemple : `x"∗"y"∗"z` `"="` `xyz`. On note l'inverse de `x` également par `x^-1 = sf"inv"(x)`. On définit l'opérateur binaire de division `/"(.,.)"` de syntaxe centrée comme suit : `x"/"y` `"="` `xy^-1`. La priorité syntaxique de la division est égale à celle de la multiplication.

On se place dans le corps `K`. Les quantificateurs `AA` et `EE` ont un domaine par défaut qui est l'ensemble `K`, c'est à dire que pour un symbole de variable quelconque, tel que par exemple `x`, l'expression`AA x` signifie `AA x "∈" K` et l'expression `EE x` signifie `EE x "∈" K`.

2.3) Théorie du corps commutatif

La structure est définie par un triplet d'opérateurs `(K,"+","∗")`. Le premier opérateur est un prédicat unaire qui sert pour déterminer l'ensemble sous-jacent. Les deux autres opérateurs sont binaires et vont par leur symbole engendrer un langage de composition d'opérateurs, et un langage de la logique du premier ordre dans lequel pourra s'exprimer la théorie du corps commutatif.

Le langage proprement dit de la structure `(K,"+","∗")` ne contient pas le nom de la structure `K`, car implicitement, le langage qui est du premier ordre c'est à dire qui n'utilise qu'un seul type d'élément, ne désigne que des éléments appartenant à la structure. Autrement dit, le type d'élément utilisé est celui des éléments appartenant à la structure. C'est pourquoi la présentation du langage ommet le premier symbole `("+","∗")` .

On décompose la théorie du corps commutatif en une conjonction de clauses prénexes, et on otient ainsi `9` axiomes :

On manipule un deuxième type de variable que sont les opérateurs unaires ou binaires, internes à la structure. Un opérateur binaire sera souvent désigné par la variable `"∗"` que l'on note parfois `"∗(.,.)"` pour préciser son arité, et qui se note aussi par absence de symbole en juxtaposant les arguments. Un opérateur binaire commutatif sera plus souvent désigné par la variable `"+"` que l'on note parfois `+"(.,.)"` pour rappeler son arité. Mais cela n'est nullement une obligation.

La théorie du corps, dans le langage de la logique engendré par les seuls opérateurs `"+(.,.)"` et `"∗(.,.)"`, est découpée en `9` clauses prénexes appelées axiomes. Cette décomposition entraine une complexification de certaines clauses, car les éléments neutres et l'élément absorbant ne font pas partie du langage de la structure telle que présentée de façon académique. Ils ne figurent pas dans la présentation du corps. Il ne figurent que sont forme de proposition existentiel dans la théorie du corps. La différence en est la calculabilité : On sait qu'ils existent mais on ne donne pas de moyen de les désigner par des termes du langage.

Les fonctions propositionnelles évoquées ci-dessus se définissent ainsi  :

`sf"Corps_commutatif"("+","∗") = {sf"Anneau_commutatif"("+","∗"), sf"Reversible_ou_absorbant"("∗")}`
`sf"Anneau_commutatif"("+","∗") = {sf"Distributif"("∗","+"), sf"Groupe_abelien"("+"), sf"Monoïde_commutatif"("∗")}`
`sf"Groupe_abelien"("+") = {sf"Monoïde_commutatif"("+") , sf"Reversible"("+")}`
`sf"Monoïde_commutatif"("+") = {sf"Semi_groupe"("+"), sf"Commutatif"("+"), sf"Avec_neutre"("+")}`
`sf"Demi-groupe_commutatif"("+")={AAxAAyAAz, x"+"(y"+"z) = (x"+"y)"+"z}`
`sf"Demi-groupe"("∗")={AAxAAyAAz, x(yz) = (xy)z}`
`sf"Distributif"("∗","+")={AAxAAyAAz, x(y"+"z) = xy"+"xz}`
`sf"Commutatif"("+")={AAxAAy, x"+"y = y"+"x}`
`sf"Avec_neutre"("∗") = {EEeAAx, xe = x}`
`sf"Reversible"("∗") = {AAxEEeAAy, xey = y}`
`sf"Reversible_ou_absorbant"("∗")={AAx, (EEeAAy, xey"="y)"∨"(AAy, xy"="x)}`

Le corps étant commutatif, la définition de l'élément neutre à droite fait office de définition de l'élément neutre, la définiton de la réversibité à droite fait office de la réversibilité, la réversibilité ou absorption à droite fait office de réversibilité ou absorption, et la distributivité à droite fait office de distributivité. Ainsi pour les puristes, ou dans le cadre des corps non-commutatifs, la définition complète est :

`sf"Avec_neutre"("∗") = {EEeAAx, xe "=" x, ex"="x}`
`sf"Reversible"("∗") = {AAxEEeAAy, xey "=" y, yxe"=" y}`
`sf"Reversible_ou_absorbant"("∗") = {AAx, (EEeAAy, xey "=" y, yxe "=" y)"∨"(AAy, xy"="x, yx"="x)}`
`sf"Distributif"("∗","+")={AAxAAyAAz, x(y"+"z) = xy"+"xz, (y"+"z)x = yx"+"zx}`

L'énumération des théories entre crochet `{...}` correspond à la conjonction des théories. La virgule sépare les déclarations de variables quantifiés du reste de la formule ou bien correspond au connecteur logique `"et"`. Le symbole `"∨"` désigne le connecteur logique `"ou"`. On remarque que la théorie du corps ainsi exposé est écrite en utilisant les seuls connecteurs logiques `"ou"`, `"et"` et le seul prédicat `"="`. Et donc en particulier, elle n'utilise pas le connecteur logique de négation. C'est une théorie dite d'égalité.

3) Modèle

Afin que le langage signifie autre chose que lui-même, on sépare le signifiant, du signifié. On sépare la théorie `T`, du modèle `M`. Le modèle, par principe de construction, constitue l'épreuve ultime. Et dans la conception classique où l'on suppose que tout peut être tranchée, le modèle tranche toutes les propositions écrites dans le langage du premier ordre, en deux valeurs de vérité possibles, vrai ou faux. Lorsque le modèle `M` tranche la proposition `T` en répondant vrai, on dit que `M` satisfait `T` et on note :

`M ⊨ T`

Une structure se présente en énumérant ses opérateurs générateurs, et constitue un modèle. Considérons par exemple la structure `(K,"+","∗")`. Elle constitue un modèle qui comprend un ensemble `K` composé d'éléments tous bien identifiés dans le modèle, même si le langage et la théorie connue de la structure ne permettent pas de les identifier. Et il comprend deux lois internes complètement définies `"+"`, `"∗"` sur cet ensemble `K` dans le modèle, même si le langage et la théorie connue de la structure ne permettent pas de les définir. Et leurs symboles `"+(.,.)"`, `"∗(.,.)"` engendrent le langage de la structure c'est à dire, un langage de composition d'opérateurs, et un langage de la logique du premier ordre.

La structure `(K,"+","∗")` constitue un corps commutatif si et seulement si elle satisfait la théorie `sf"Corps_commutatif"("+","∗")` ce qui se note :

`(K,"+","∗") ⊨ sf"Corps_commutatif"("+","∗")`

Le méta-opérateur `"⊨"` teste si le modèle satisfait la théorie. Le modèle étant complètement déterminé, constituant l'épreuve ultime, il tranche toutes les propositions du langage logique du premier ordre, et le fait de façon classique par la réponse vrai ou faux.

En admettant la mécanique classique, ces modèles existent bien dans les cas finis et aussi dans les cas infinis rudimentaires où le langage est trop faible pour pouvoir exprimer l'arithmétique. Parcontre dans les cas infinis contenant l'arithmétique, l'existence de tel modèle est tout à fait hypothétique car nous ne connaissons pas le moyen mécanique utilisé par le monde pour qu'il puisse répondre à la question à laquelle on le soumet.... Et la prudence aurait dû consisté à dire qu'il n'en existât point.

Notez que le langage de la structure `("+","∗")` doit contenir le langage de la théorie qu'elle teste, ou autrement dit, la théorie doit être écrite dans le langage de la structure. Et c'est la présentation de la structure qui définit son langage. Les structures que nous étudions, le corps, le demi-corps, l'anneau, le demi-anneau, ont toutes une définition académique contenant les symboles d'opérateurs `"+"`, `"∗"` dans cet ordre. Elles ont donc toutes le même langage.

4) Monde

Il existe une seconde conception du modèle appelé monde, qui ne tranche pas les propositions `P` directement mais qui tranche la question de leur démontrabilité notée `⊢ P`. Autrement dit, le monde qui constitue l'épreuve ultime, tranche toutes les propositions du langage logique du premier ordre de façon plus générale, en trois valeurs de vérité possibles :

1- Vrai, c'est à dire que `P` est démontrable, ce qui se note `|--P`.

2- Faux, c'est à dire que `"¬"P` est démontrable, ce qui se note `|-- ¬P`.

3- Indécidé, c'est à dire que `P` n'est pas démontrable, et que `¬P` n'est pas démontrable, ce qui se note `(⊬ P) "et" (⊬¬P)`.

Et donc pour bien comprendre ce qu'est un monde, il faut répondre à la question "qu'est ce qu'une preuve ?". Une preuve, appelée aussi une démonstration, est un objet de taille finie, vérifiable par des moyens mécaniques rudimentaires, qui comporte une conclusion et des hypothèses. Autrement dit la preuve repose sur l'usage de règles de déduction simples appliquées en chaines à des hypothèses pour aboutir à une conclusion. On présentera trois systèmes de preuve appelé aussi système de démonstrations ; le système axiomatique d'Hilbert, la déduction naturelle, et le calcul des séquents. Bien entendu ces trois systèmes sont équivalents.

Le système de démonstration constitue un procédé mécanique idéalisé, rendu parfait en enlevant les jeux et imperfections qui pourrait y avoir dans les rouages ainsi que toutes les perturbations exogènes au principe. Et donc son déterminisme est bien fondé du moment que l'on admet la mécanique classique.

En cela le monde redevient une évidence de la mécanique classique. Et il est définie par le système de démonstration que l'on aura choisi et auquel on aura adjoint un ensemble de propositions appelés axiome du monde et qui joue le rôle des hypothèses. Le monde est alors un programme qui, appliqué à n'importe quel proposition, va explorer toutes les démonstrations qu'il est possible d'écrire, et va donner une réponse vrai ou faux, ou ne jamais donner de réponse. Et comme nous ne faisons pas parti de ce monde, nous pouvons nous y placer à la fin des temps pour récolter cette troisième réponse qu'est la non réponse.

Il convient de distinguer ce qu'est une proposition, de ce qu'est un ensemble de propositions vu comme une conjonction. La proposition fait partie d'un langage du premier ordre, et elle est de taille finie. Tandis que l'ensemble de propositions peut être de taille infinie, et dans ce cas, même mis sous forme de conjonction, elle ne fait pas partie du langage. C'est ce qui distingue un monde d'une théorie. Néanmoins si on ne s'intéresse qu'au monde finiment axiomatisé alors il n'y a pas de différence entre un tel monde et une théorie.

La mécanique quantique constate que le comportement d'un ensemble d'éléments diffère selon que les éléments en questions sont indiscernables entre-eux ou non. La structure devient dépendante des connaissances que nous avons sur elle. Elle perd une partie de son objectivité. Dans cette nouvelle conception, une structure `(K,"+","∗")`, en tant que monde, n'est pas définie indépendament de sa théorie connue `T`. On la note sous forme d'un quotient `(K,"+","∗")"/"T`. Elle constitue un monde qui comprend un ensemble `K` composé d'éléments plus ou moins bien identifiés par le langage engendré par `("+","∗")` et la théorie `T` écrite dans ce langage. Deux éléments sont distinguables s'il existe une proposition unaire vrai pour l'un et fausse pour l'autre. Un élément est identifié s'il existe une proposition unaire vrai pour l'élément en question et fausse pour tous les autres éléments. L'introduction de cette subjectivité, qui introduit dans la définition de la structure les connaissances que nous avons sur elle, ne change pas le sens des formules, car les quantificateurs usuels `AA, EE` ne font pas la différence entre éléments indiscernables et éléments identifiés. La structure `(K,"+","∗")"/"T` constitue un corps commutatif si et seulement si elle satisfait la théorie `sf"Corps_commutatif"("+","∗")`. Et cela se note comme suit :

`(K,"+","∗")"/"T ⊨ sf"Corps_commutatif"("+","∗")`

Le méta-opérateur `"⊨"` teste si le monde satisfait la théorie. Le méta-opérateur peut répondre vrai ou faux ou non décidé. S'il répond vrai, alors, soit `T=> sf"Corps_commutatif"("+","∗")` auquel cas ce teste ne complète pas la théorie et ne fait que confirmer une connaissance déjà acquise, soit `¬(T=> sf"Corps_commutatif"("+","∗"))` auquel cas la théorie connue de la structure est augmentée et devient `T "et" sf"Corps_commutatif"("+","∗")`. Le test va modifier la structure, de la même façon que l'observation va perturber l'objet sujet de l'observation. S'il répond faux, c'est le même cas de figure en inversant les valeurs logiques. Par contre, s'il répond que ce n'est pas décidé, cela signifie que certaines connaisances supplémentaires sur la structure peuvent en faire un corps commutatif, et que certaines connaisances supplémentaires sur la structure peuvent en faire un non corps commutatif. Mais comment cela peut-il être possible ? C'est la superposition d'états quantiques.

Dans ce dernier cas l'observation n'aura pas perturbé l'objet observé, tout se passe comme si l'observation n'avait pas eu lieu, comme si l'objet observé s'était dérobé à nos investigations. Cette troisième réponse traduit donc l'échec de notre tentative d'observation. On peut penser que en répétant indéfiniment l'opération on finira par avoir une réponse vrai ou faux qui complétera le cas échéant la théorie du monde.

5) Langage de calcul du premier ordre

Pour définir la calculabilité des éléments, il nous faut définir le langage permettant le calcul des éléments. C'est le langage des compositions d'opérateurs générateurs. Par exemple considérons une structure de présentation `(a,b,f"(.)",g"(.,.)")`. Les compositions d'opérateurs générateurs sont appelés des termes et forme un ensemble noté `"<"a,b,f"(.)",g"(.,.)>"`. Chaque terme tel que par exemple `g(f(b),g(a,b))` désigne un élément de la structure. Et cet élément est calculable justement par cette formule, en évaluant chaque opérateur générateur.

Pour définir la calculabilité des opérateurs, il nous faut définir un langage permettant à partir des arguments d'entrés de calculer l'élément de sortie. Pour simplifier notre description, nous prendrons le cas particulier d'une arité égale à `3` et les trois variables d'entrée `x,y,z` dans cet ordre. Il existe plusieurs niveaux de calcul des opérateurs ternaires. Les opérateurs ternaires calculables de niveau `0` sont ceux générateurs, c'est dire présents dans la présentation. Les opérateurs ternaires calculables de premier niveau sont les compositions d'opérateurs générateurs et des variables muettes `x,y,z` qui servent d'entrée. Par exemple la composition `g(f(x),g(z,x))` définit un opérateur ternaire `s(x,y,z) = g(f(x),g(z,x))`. Les compositions d'opérateurs générateurs et de variables d'entrées `x,y,z`, sont ainsi identifiés aux opérateurs ternaires calculables de premier niveau, et forment un ensemble noté :

`"<"a,b,f"(.)",g"(.,.)>"[x,y,z]`

On explicite les grammaires formelles qui engendrent ces langages. La grammaire formelle des éléments calculables est la suivante :

`sfC -> a"|"b`
`sfX -> sfC|f(sfX)|g(sfX,sfX)`

`sfC` et `sfX` sont des symboles non-terminaux de la grammaire. La première ligne signifie que le symbole `sfC` doit être remplacé par un des éléments générateurs `a` ou `b`, le signe `"|"` indiquant une alternative. Ainsi la première ligne définit `sfC` comme représentant une constante génératrice, c'est à dire un élément quelconque parmi `a,b`. La seconde ligne signifie que le symbole `sfX` doit être remplacé, soit par `sfC`, soit par `f(sfX)` ou soit par `g(sfX,sfX)`. Ainsi la seconde ligne définit `sfX` récursivement, comme représentant une composition d'opérateurs quelconque parmi `a,b,f"(.)",g"(.,.)"`. Puis, parce qu'on ne cherche pas à distinguer les éléments générateurs des opérateurs générateurs, on intègre la définition de `sfC` directement dans `sfX`. La grammaire devient :

`sfX -> a"|"b"|"f(sfX)"|"g(sfX,sfX)`

On adopte une nouvelle notation pour désigner l'ensemble engendré par une grammaire. On le note par un symbole non terminal suivi d'un slash et de la grammaire formelle. Les caractères non-terminaux sont en lettre majuscule droite. Ainsi l'ensembles des éléments calculables se note de deux façons :

`"<"a,b,f"(.)",g"(.,.)>"   =   sfX"/"(sfX -> a"|"b"|"f(sfX)"|"g(sfX","sfX))`

La grammaire formelle des opérateurs ternaires calculables de premier niveau est la suivante :

`sfV -> x|y|z`
`sfO -> sfV|a|b|f(sfO)|g(sfO,sfO)`

La première ligne définit `sfV` comme représentant une variable parmi l'entête d'appel `(x,y,z)`. La seconde ligne définie `sfO` comme représentant un opérateur ternaire calculable par le langage de la structure.

`"<"a,b,f"(.)",g"(.,.)>"[x,y,z]   =   sfO"/"({:(sfV -> x|y|z),(sfO -> sfV"|"a"|"b"|"f(sfO)"|"g(sfO","sfO)):}) `

6) Langage de la logique du premier ordre

Pour définir la définissabilité des éléments et des ensembles, il nous faut définir le langage permettant la définition d'éléments et d'ensembles. C'est le langage de la logique du premier ordre utilisant le langage de la structure et des variables muettes `x,y,z,...`, qui pour partie sont quantifiées, et pour partie sont utilisées comme `n` arguments d'entrée. Cela permet de définir les prédicats définissables `n`-aire, c'est à dire les ensembles définissables de `n`-uplets d'éléments de la structure. Puis on définit ce qu'est un élément définissable. C'est un élément qui appartient à un ensemble définissable dont on prouve qu'il est un singleton.

6.1) Langage de la logique du premier ordre sans quantificateur

On commence par construire les propositions sans quantificateur. Et on commence par décrire les littéraux positifs. Considérons par exemple une structure de présentation `(A, B, F"(.)",G"(.,.)",a,b,f"(.)",g"(.,.)")` où les prédicats générateurs sont notés en majuscule, et où les opérateurs générateurs sont noté en minuscule. Noter que le nom de la structure est omis puisqu'il n'intervient pas dans la définition de son langage. Le prédicat générateur `F"(.)"` désigne un sous-ensemble d'éléments de la structure. Les prédicats générateurs nullaire `A` et `B` désignent deux valeur booléennes. Le prédicat générateur `G"(.,.)"` désigne une relation, c'est à dire un ensemble de couples d'éléments de la structure. On ajoute le prédicat spéciale d'égalité entre éléments noté `"=(.,.)"`.

Un littérale positif est soit le booléen faux noté `"⊥"`, soit le booléen vrai noté `"⊤"`, soit un inconnu booléen parmi `A,B`, soit un prédicat générateur parmi `F"(.)",G"(.,.)"` appliqué à des termes de `"<"a,b,f"(.)",g"(.,.)>"`, soit une égalité entre deux termes de `"<"a,b,f"(.)",g"(.,.)>"`. L'ensemble des littéraux positifs se note donc :

`{ "⊥","⊤",A,B, F"(.)",G"(.,.)","=(.,.)" } @ "<"a,b,f"(.)",g"(.,.)>"   =   sfL"/"({:(sfX -> a"|"b"|"f(sfX)"|"g(sfX","sfX)),(sfL ->"⊤|⊥|"A"|"B"|"F(sfX)"|"G(sfX,sfX)) :})`

Où l'opérateur `@` appliqué à deux ensembles est défini comme suit. L'ensemble `F@G`, regroupe toutes les compositions possibles d'un élément `n`-aire de l'ensemble `F` avec `n` éléments de l'ensemble `G`, et comprend donc les éléments nullaires de l'ensemble `F`. Les propositions sans quantificateur sont les combinaisons booléennes de littéraux positif. L'ensemble des propositions sans quantificateur se note donc :

`sfP"/"({: (sfX -> a"|"b"|"f(sfX)"|"g(sfX","sfX)) , (sfL ->"⊤|⊥|"A"|"B"|"F(sfX)"|"G(sfX,sfX)) , (sfP ->sfL|¬sfP|(sfPvvsfP)|(sfP^^sfP)|(sfP"⇒"sfP)) :})`

L'ensemble des propositions ternaires sans quantificateur se note donc :

`sfP"/"({: (sfV -> x"|"y"|"z) ,(sfX -> sfV"|"a"|"b"|"f(sfX)"|"g(sfX","sfX)) , (sfL ->"⊤|⊥|"A"|"B"|"F(sfX)"|"G(sfX,sfX)) , (sfP ->sfL|¬sfP|(sfPvvsfP)|(sfP^^sfP)|(sfP"⇒"sfP)) :})`

 

 

 

---- 8 juin 2021 ----

 

Le langage logique du premier ordre est un langage contextuel, comme le sont les langages de programmation évolués. ils introduisent des déclarations de variable qui enrichit le langage, et une sous-formule n'a pas la même signification selon l'endroit où elle se trouve, car il faut tenir compte d'un contexte qui indique les variables déclarées en cours (et qui joue ainsi le rôle de nouveaux éléments générateurs). Les variables sont déclarées à l'aide des quantificateurs `AA, EE`. Lorsque une variable est déclaré une deuxième fois, elle masque la variable de même nom pendant toute sa portée. Lorsque une variable est utilisée sans être déclarée, elle constitue un argument de la formule, et les arguments de la formule sont placées dans l'ordre de leur première apparition. Le nombre d'argument d'une formule constitue son arité. Lorsque l'arité est nulle, la formule est dite clause et elle constitue une théorie. Lorsque l'arité est `n`, la formule définit un prédicat `n`-aire.

L'ensemble des formules d'arité fixe quelconque s'obtient en construisant un langage de façon formelle selon la grammaire suivante :

`T->P"|"(EE V, P)"|"(AA V, P)`

En conclusion, l'ensemble des théories utilisant au plus `n` variables élémentaires et `m` variables booléennes se définit formellement comme un langage, grâce à la grammaire suivante :

Arguments :	`V -> x_1|x_2|x_3|...|x_n`
Variable lié :	`V -> y_1|y_2|y_3|...|y_m`
Variable booléenne :	`B -> b_1|b_2|b_3|...|b_m`
Elément :	`X -> V|(X "+"X)|(X"∗"X)`
Littéraux positif :	`L ->"⊤|⊥|"B"|"X"="X`
Proposition sans quantificateur :	`P ->L|¬P|(PvvP)|(P^^P)|(P"⇒"P)`
Théorie :	`T->P"|"(EE V, P)"|"(AA V, P)`

 

 

`"<"x,y,z,"+","∗>" = {x, x"+"x, x"∗"y, x"+"y, (x"+"x)"∗"z, (y"+"x)"∗"(z"+"y),...}`

C'est l'ensemble des éléments engendrés par les opérateurs `x,y,z,"+","∗"`, ou autrement dit, calculable à partir de ces opérateurs. Cet ensemble se définit formellement comme un langage, grâce à la grammaire suivante :

 

---- 6 juin 2021 ----

 

 

 

 

 

4) Qu'est ce qu'une preuve ?

Une preuve est un objet de taille finie, vérifiable par des moyens mécaniques rudimentaires, qui comporte une conclusion et des hypothèses. Autrement dit la preuve repose sur l'usage de règles de déduction simples appliquées en chaines à des hypothèses pour aboutir à une conclusion.

On présente trois systèmes de preuve, le système axiomatique d'Hilbert, la déduction naturelle, et le calcul des séquents. Bien entendu ces trois systèmes sont équivalents.

4.1) Système axiomatique d'Hilbert

Lorsque une formule du premier ordre est désignée sous forme d'une variable, elle admet alors une seconde notation sous forme fonctionnelle en contenant ses variables non déclarées placées dans l'ordre de leur première apparition . Par exemple :

`h(y,z)    =     AAx, P(x,y) => P(z,x)`

Une preuve est une suite de formules du premier ordre `(h_0,h_1,h_2,...,h_n)` où chaque `h_i` vérifie l'une des trois conditions suivantes :

1) `h_i` est l'un des axiomes :

(Calcul propositionelle)

`A=>(B=>A)`

`(A=>(B=>A) ) =>((A=>B)=>(A=>A))`

`(¬A =>¬B) =>((¬A=>B)=>A)`

(Quantification)

`AAx, A(x) =>A(t)`

`AAx, (A=> B(x)) => (A=>AAx, B(x))`

(Egalite)

`x=x`

`x=y =>(A(x) =>A(y))`

2) `h_i` est une hypothèse

3) `h_i` est obtenue par modus ponens à partir de deux formules `h_j, h_k` telque `j<i` et `k<i`. C'est à dire qu'il existe `j<i ,k<i` tel que `h_k = (h_i=>A)`

--- 4 juin 2021 ---

On présente le système de la déduction naturelle. C'est un ensemble de règles qui introduit et élimine chaque connecteur logique. Les règles de déduction sont construites à l'aide d'un nouveau connecteur multi-aire, qui est celui de la déduction `"⊢"`, et à l'aide de variables libres `A,B,C,...` désignant des théories quelconques. Cela forme un nouveau langage plus riche appelé langage étendu, qui permet d'écrire des règles de déduction.

Les règles de déduction naturelle sont au nombre de 12 :

Règle d'introduction du `"et"`	`(A, B)⊢ A "et" B`		Règles d'élimination du `"et"`	`(A "et" B) ⊢ A` `(A "et" B)⊢ B`
Règles d'introduction du `"ou"`	`A⊢(A "ou" B)` `B⊢(A "ou" B)`		Règles d'élimination du `"ou"`	`(A "ou" B,A"⇒"C,B"⇒"C)⊢C`
Règle d'introduction du `"⇒"`	`(A"⊢"B)⊢(A"⇒"B)`		Règle d'élimination du `"⇒"` dite règle du modus ponens	`(A, A"⇒"B)⊢B`
Règle d'introduction du `"¬"`	`(A"⊢⊥")⊢ "¬"A`		Règle d'élimination du `"¬"`	`(A, "¬"A)⊢ ⊥`
Règle "Ex falso"	`"⊥" ⊢ A`		Règle "Ex falso"	`"⊥" ⊢ A`
Règle "Ab absurdo"	`("¬"A"⇒⊥")⊢ A`		Règle "Ab absurdo"	`("¬"A"⇒⊥")⊢ A`

Puis on considère le procéder d'unification qui permet d'unifier une variable libre à n'importe quelle théorie et pouvant contenir de telles variables libres. Remarquez que ce procédé d'unification permet de définir des théories récurcives que l'on exclut dans un premier temps.

La règle de déduction possèdent une entête qui est une liste de théorie (du langage étendu) et un corps qui est une théorie (du langage étendu). Par exemple, considérons la règle suivante :

`(A"⇒"B, A" et "C) |-- B" et "C`

Cette règle s'applique par exemple au couple de propositions suivantes `(a"⇒"b, a" et "¬b)`. Elle procéde une unification entre son entête et le couple de propositions en question. Si l'unification réussie ce qui est le cas ici, les variables libres étant affectées comme suit : `A"="a,B"="b,C"=¬"b`, la règle produit alors son corps dans lequel les variables libres affectées sont remplacées par ce qu'elles contiennent `b" et ¬"b`, et les eventuelles variables libres non affectées c'est à dire qui n'apparaissent que dans le corps de la règle, peuvent prendre comme valeurs toutes les théories du langage.

Ce type de règle de déduction est pertinent pour plusieurs raisons. D'abord il s'inspire d'un principe trés général d'apprentissage par similitude. Et surtout, il s'appuit sur un mécanisme d'unification qui, lorsqu'il est bien programmé, s'avère de complexité linéaire.

Notez bien que ces régles de déduction ne font pas partie du langage mais du langage étendu.

La définition du connecteur de déduction `"⊢"` différe de celle de l'implication `"⇒"`. La proposition `A"⊢"B` signifie que l'on peut déduire `B` de `A` par un procédé mécanique qui est celui de la démonstration tel que défini par la règle elle-même, alors que la proposition `A"⇒"B`, sans la règle de déduction dite du modus ponens `(A, A"⇒"B)⊢B`, ne permet pas de déduire `B` de `A`. Cette distinction est inutile en logique propositionnelle, mais elle devient nécessaire si on enrichie le langage en une logique du premier ordre. Car la théorie devenant incomplète, il se peut qu'une proposition `B` ne soit pas démontrable par `A` et que sa négation `"¬"B` non plus, `"¬"(A"⊢"B) "et" "¬"(A"⊢¬"B)`, et en identifiant le connecteur de déduction et le connecteur d'implication, on aboutirait à la contradiction suivante `"¬"(A"⇒"B) "et" "¬"(A"⇒¬"B)`.

Un moyen simple d'étudier ces théories est la façon empirique en programmant un moteur qui applique ces règles de déduction. Un tel moteur comprend un algorithme d'unification et un générateur de propositions. Voir Implémentation des langages d'opérateurs.

---- 9 avril 2014 ----

Mais une difficulté apparait. Certaines prémisses de ces règles ne sont pas des propositions du langage propositionnel mais sont des propositions du langage propositionnel étendu. La règle d'introduction de l'implication ainsi que la règle d'introduction de la négation ont comme prémisses non pas l'existence d'une proposition dans le sac, mais l'existence d'une démonstration.

---- 9 avril 2019 ----

Puis il faut ajouter les règles relatives au symbole de déduction `"⊢"` ; La règle d'introduction du `"⊢"`, et la règle d'élimination du `"⊢"` qui est déjà présente puisqu'elle correspond à la règle d'introduction du `"⇒"`.

Règle d'introduction du `"⊢"`

`(A"⇒"B)⊢(A"⊢"B)`

 

Règle d'introduction du `"et"`	`(H"⊢"A, G"⊢"B) ⊢ (H,G "⊢" (A "et" B))`
Règles d'élimination du `"et"`	`(A "et" B) ⊢ A` `(A "et" B)⊢ B`
Règles d'introduction du `"ou"`	`A⊢(A "ou" B)` `B⊢(A "ou" B)`
Règles d'élimination du `"ou"`	`(A "ou" B,A"⇒"C,B"⇒"C)⊢C`
Règle d'introduction du `"⇒"`	`(A"⊢"B)⊢(A"⇒"B)`
Règle d'élimination du `"⇒"` dite règle du modus ponens	`(A, A"⇒"B)⊢B`
Règle d'introduction du `"¬"`	`(A"⊢⊥")⊢ "¬"A`
Règle d'élimination du `"¬"`	`(A, "¬"A)⊢ ⊥`
Règle "Ex falso"	`"⊥" ⊢ A`
Règle "Ab absurdo"	`("¬"A"⇒⊥")⊢ A`

---- 27 mai 2021 ----

3) Les deux langages de la structure

La structure

Le langage de programmation des opérateurs se subdivise en plusieurs niveaux. Le langage logique du premier ordre regroupent toutes les propositions logiques du premier ordre n'utilisant que les opérateurs de définition de la structures, et le prédicat d'égalité entre élément.

Notez qu'un prédicat est un opérateur dont l'ensemble d'arrivé est l'ensemble des booléens `{0,1}`, qu'un prédicat nullaire est un booléen, et qu'un opérateur nullaire est un élément.

3) Langage

Les deux opérateurs "+","∗" évoqué dans la définition de la structure engendre un langage selon la grammaire formelle suivante :

X -> +(X,X)

Le dernier niveau regroupe tous les programmes d'arrêt sûr.

3) Calculabilité

La définition du corps commutatif `(K,"+","∗")` précise un ensemble sous-jacent et deux opérateurs binaires internes. Elle constitue ce que l'on appelle en informatique, une interface, un ensemble de 3 commandes de bas niveau. En dehors de la commande `K"(.)"` qui permet d'interagir avec l'exterieur, les autres opérateurs sont internes et dits générateurs, dans le sens qu'ils vont engendrer le langage des opérateurs et un langage des propositions. Le langage des opérateurs définit le domaine des opérateurs calculables. Le langage des propositions définit le domaine des opérateurs définissables.

On se place dans un environnement plus large, un ensemble d'éléments plus vaste. L'interface propose un prédicat unaire `K"(.)"` qui appliqué à un élément quelconque retourne le booléen `1` s'il appartient à la structure, ou retourne le booléen `0` sinon. L'interface propose un opérateur binaire `"+(.,.)"` qui appliqué à deux éléments `x,y` de la structure retourne l'élément désigné par `x"+"y`. L'interface propose un second opérateur binaire `"∗(.,.)"` qui appliqué à deux éléments `x,y` de la structure retourne l'élément désigné par `x"∗"y`.

Les opérateurs et prédicats figurant dans l'interface sont dits générateurs, et sont par principe effectif, c'est à dire qu'ils produisent leurs résultats par un procédé effectif qui nous est donné. Ils constituent les opérateurs calculables de base permettant de définir tous les autres opérateurs calculables, et plus précisement, calculable à partir des opérateurs générateurs de la structure, c'est à dire programmable dans le langage de la structure. Puis dans notre cas, la calculabilité étant ici une notion interne à notre structure, nous n'utilisons donc pas le prédicat `K"(.)"`ni le nom `K` de la structure.

L'approche constructive utilise le concept d'éléments calculables et fait donc la distinction entre l'ensemble des éléments d'une structure et l'ensemble des éléments calculables de la structure. Un élément est calculable si et seulement s'il existe une composition close d'opérateurs générateurs qui lui est égale. Et dans notre cas il n'y en a pas. Un opérateur unaire interne `r"(.)"` est calculable si et seulement s'il existe un programme d'arrêt sûr n'utilisant que les opérateurs générateurs de la structure et qui appliqué à un élément `x` produit l'élément image `r(x)`.

Pour une meilleur compréhension, il convient de bien différentier l'interface et le langage. L'interface sont les commandes, ce qui définit complètement la structure de façon effective. Le langage parcontre ne regroupe que les symboles des commandes qui peuvent être composées pour construire d'autre opérateur. Dans cet esprit, un élément calculable est désigné par une expression du langage qui est une composition close d'opérateurs générateurs, dans laquelle on n'évalue pas les opérateurs générateurs.

On définie deux sortes de quantifications, l'une, `AAx, EEx`, portant sur tous les éléménts x de la structure, l'autre `bar AAx, bar EEx` portant sur les seuls éléments x calculables de la structure. On définie deux sortes de quantifications sur les opérateurs, l'une, `AAr(.), EEr(.)`, portant sur tous les opérateurs unaire r(.) de la structure, l'autre `bar AA r(.), bar EE r(.)` portant sur tous les opérateurs unaire calculables r(.) de la structure.

Remarquez que la structure de corps présenté avec cette interface `(K,"+","∗")` ne contient pas d'élément calculable, et que la soustraction `-"(.,.)"` et la division `/"(.,.)"` ne sont pas des opérateurs calculables. Certes, ils sont définissablent en utilisant la propriété `sf"Reversible"("+")` et `sf"Reversible_ou_absorbant"("∗")` mais pas calculable à partir des seuls opérateurs générateurs `"+(.,.)", "∗(.,.)"`.

4) Définissabilité

L'interface définit le langage des opérateurs qui engendre tous les opérateurs calculables. L'interface définit également le langage des propositions. La théorie de la structure énumère toutes les démonstrations possibles écrites dans le langage des propositions, et donc énumère toutes les propositions démontrables, et donc énumère tous les opérateurs définissables.

On note `L"/"T` la structure de langage `L` et de théorie `T`. Dans notre exemple `L = ("+","∗")` et `T = sf"Corps_commutatif"("+","∗")`.

On peut définir une relation interne à la structure, par son graphe qui est un ensemble d'arcs symbolisés par l'opérateur binaire `"↦"`. Par exemples l'ensemble `{a"↦"b, c"↦"d}` représente si `a!=c`, la fonction qui envoie `a` sur `b` et `c` sur `d`. L'ensemble `{x"↦"h(x), y"↦"g(y) "/" x "∈" A, y "∈" B}` représente si `A` et `B` sont disjoints, la fonction qui envoie les éléments de `A` sur leur image par `f`, et les éléments de `B` sur leur image par `g`. Puis par convention, nous notons : `(x"↦"h(x)) = {x"↦"h(x) "/" x "∈" L}`.

Un élément `e` est dit définissable si et seulement s'il existe une proposition unaire `P"(.)"` écrite dans le langage de la structure, qui définit l'unique élément `e`, c'est à dire telle que `x"="e` et que `EE!x, P(x)`. L'élément `e` peut alors être désigné par la proposition qui le définie. `e="@"P` ou simplement `P(e)` ou encore `e"∈"P`.

La définition se généralise à un ensemble d'éléments. Un ensemble `E` d'éléments est dit définissable si et seulement s'il existe une proposition unaire `P"(.)"` écrite dans le langage de la structure, qui définit l'appartenance à cet ensemble, c'est à dire telle que `AAx, P(x) <=> x "∈" E`. L'ensemble `E` peut alors être désigné par la proposition qui le définie. `E=P`. Aussi, l'élément `e` est définissable si et seulement si le singletion `{e}` est définissable.

Un opérateur unaire interne `f"(.)"` est dit définissable si et seulement s'il existe une proposition, binaire, `P"(.,.)"` écrite dans le langage de la structure, qui définit l'opérateur `f` en définissant pour chaque élément `x` l'unique image `f(x)`, c'est à dire telle que `y"="f(x)`et que `AAxEE!y, P(x,y)`. L'opérateur `f"(.)"` peut alors être désigné par la proposition qui le définie. `f="@"P` ou encore `AAx, P(x,f(x)))` ou encore `f(x) "∈" P(x)`

La définition se généralise à un opérateur de `L` vers `ccP(L)`. Un tel opérateur `Q` est dit définissable si et seulement s'il existe une proposition binaire `P"(.,.)"` écrite dans le langage de la structure, tel que  `AAxAAy, P(x,y) <=> y "∈" Q(x)`. L'opérateur `Q` peut alors être désigné par la proposition qui le définie. `Q=P`

5) Nomination

La nomination consiste à ajouter dans l'inteface un opérateur interne à la structure ou élément appartenant à la structure. Cela ne change pas la structure mais cela peut augmenter le domaine de calculabilité de la structure.

L'alternative nécessite une décision, un choix, qui, suivi d'une nomination, va enrichire le langage de la structure mais en la spécialisant puisqu'un choix a été fait, pouvant occasionner une rupture de symétrie. Par contre, s'il n'y a pas d'alternative, alors il n'y a pas de choix, le candidat est unique, la nomination qui va enrichire le langage de la structure ne spécialise pas la structure. Ainsi, les opérateurs définissables peuvent être ajoutés au langage sans spécialiser la structure ni rompre ses symétries.

La définissabilité d'un élément permet de l'identifier et de le nommer par sa définition, mais ne permet pas de le calculer à partir de l'interface, tant qu'il n'est pas intégré dans l'interface. Néanmoins il sert comme éléments définissable premettant d'engendrer d'autres éléments définissables.

La structure de corps définie avec cette interface `(K,"+","∗")` contient deux éléments définissables que sont l'élément neutre de la multiplication noté `1` et l'élément absorbant de la multipliction noté `0`. En effet, ces éléments sont bien définis de façon unique. Car s'il y avait un deuxième élément neutre pour la multiplication `e` alors nous aurions `e"∗"1"="1` et `e"∗"1"="e` et donc `e"="1`. De même pour l'addition il n'y a qu'un seul élément neutre `0`. Puis on démontre que l'élément neutre de l'addition `0` est absorbant pour la multiplication. Nous avons : `xy = (x"+"0)y = xy"+"0y`. Si `0` n'était pas absorbant alors il aurait un inverse `0^-1`. Posons `y"="0^-1`, nous aurions `x0^-1` `"="` `x0^-1"+"00^-1` `"="` `x0^-1"+"1` et donc `0 = 1`, et donc `0` `"="` `x0` `"="` `x1` `"="` `x` et donc le corps n'aurait qu'un seul élément et il serait absorbant. Puis on démontre qu'il n'y a qu'un seul élément absobant. S'il y avait un deuxième élément absorbant `a` alors nous aurions `a"∗"0"="a` et `a"∗"0"="0` et donc `a"="0`.

L'élément neutre de l'addition noté `0` se définit par la proposition unaire `P(x) = {AAy, y"+"x"="y}` que l'on peut écrire `x|->AAy, y"+"x"="y`

`{0} = (x"↦"AAy, y"+"x"="y)`

 

---- 26 mai 2021 ----

`P(a) = (AAx, ax"="x, xa"="x)`

`P = {a"↦"(AAx, ax"="x, xa"="x) "/" a"∈"G}`

---- 26 mai 2021 ----

5) Demi-corps commutatif

La structure de demi-corps commutatif se présente de façon académique avec le même langage `(D,"+","∗")`. Le demi-corps commutatif reprend la théorie du corps commutatif mais en enlevant la clause `sf"Reversible"("+")`. Autrement dit l'existence des éléments opposés n'est plus garantie. Tout corps est un demi-corps, et nous verrons que tout demi-corps se plonge dans un corps.

6) Demi-anneau commutatif

La structure de demi-anneau commutatif se présente de façon académique avec le même langage `(D,"+","∗")`. Le demi-anneau commutatif reprend la théorie de l'anneau commutatif mais en remplaçant la clause `sf"Reversible_ou_absorbant"("∗")` par la clause `sf"Avec_absorbant"("∗")`. Autrement dit l'existence des éléments opposés n'est plus garantie. Seul l'existence d'un élément absorbant est garanti. Tout anneau est un demi-anneau, et nous verrons que tout demi-anneau se plonge dans un anneau..

`sf"Avec_absorbant"("∗") = {EEaAAx, xa = a}`

Montrons que l'élément absorbant est nécessairement l'élément neutre de l'addition.

---- 25 mai 2021 ----

7) Chaque demi-corps anneau se plonge dans un anneau commutatif

Il y a deux façons courantes de construire un anneau `K` à partir d'un demi-anneau `D` de telle sorte que le demi-anneau se plonge dans l'anneau, `D "↪" K`, généralisant la construcion de `ZZ` à partir de `NN`. La première façon est celle enseignées à l'école qui définie une structure sur les couples gain-perte et qui la quotiente par une théorie d'égalité spécifique traduisant le rôle du couples gain-perte. La seconde façon est celle par collage de deux copie de la structure. Mais ces deux façons peuvent être présentées de manière plus générale et standardisée comme suit :

• La première façon consiste à procéder à une extension élémentaire en ajoutant un élément `i` et à quotienter la structure ainsi obtenue `D[i]` par une théorie d'égalité, qui donnera à `i` le rôle de `-1`.
   
• La seconde façon consiste à procéder à une extension élémentaire en ajoutant un opérateur unaire `-"(.)"` et à quotienter la structure ainsi obtenue `D[``-"(.)"]` par une théorie d'égalité spécifique qui donnera à `-"(.)"` le rôle de la négation unaire.

8) Morphisme

Etant donné deux structures de même langage `(A,u,v,f"(.)","+(.,.)")` et `(B,u,v,f"(.)","+(.,.)")`. Une application varphi de `A` vers `B` est un morphisme si elle respecte les opérateurs du langage, c'est à dire :

`AA(x,y) "∈" A^2,`

`varphi(u) = u`
`varphi(v) = v`
`Avarphi(f(x)) = f(varphi(x))`
`varphi(g(x,y)) = g(varphi(x),varphi(y))`

L'inférence de type permet de savoir à quelle structure, `A` ou `B`, font référence les symboles du langage, u,v,f"(.)","+(.,.)" selon leur position dans la proposition. L'application `varphi` est bijectif si et seulement si :

`AA(x,y) "∈" A^2,` `varphi(x) = varphi(y) =>x=y`

Un isomorphimse est un morphisme bijectif. Deux structures `A` et `B` de même langage sont isomorphes, ce qui se note `A ≅ B`, s'il existe un isomorphisme passant de l'un à l'autre. Etant donné deux structures isomorphes `A` et `B` toute propositions d'ordre quelcconque écritez dans le langage de la structure a la même valeur logique dans les deux structures.

9) L'extension par un élément

L'extension d'une structure `(S ,"+","∗")` consiste à ajouter un élément inconnue `i`, qui peut être dans `S` ou à l'extérieur de `S`.

Si `i` appartient à `S` alors cela ne change pas la structure dans le langage initiale. Mais cela augmente son langage en faisant un choix arbitraire, le choix d'un élément `i` parmi ceux de `S`. L'ajout de l'élément `i` dans l'interface s'appelle une nomination, la nomination de `i`. Et les structures ainsi produites dans le langage enrichie `(S ,"+","∗",i)` peuvent être nombreuses et non-isomorphes entre-elles.

Si la structure admet un élément définissable que nous nommons `i` est définissable, est unique, alors la nomination de `i` n'entraine aucun choix d'élément. Il s'agit alors d'une extension par l'ajout d'un élément définissable. La structures ainsi produites `(S ,"+","∗",i)` est alors unique.

---- 25 mai 2021 ----

Si `i` n'appartient pas à `K` alors la structure s'agrandie en nombre d'éléments d'une façon généralement considérable. Car l'ajout d'un nouvel élément se traduit par l'extension des lois de compositions sur des éléments qui peuvent être en dehors de `D`. Pour chaque élément `x` de `D`, les valeurs `x"+"i`,  `i"+"x`,  `x i`,  `ix` ainsi que les valeurs `i"+"i` et `ii`, constituent de nouveaux éléments inconnus. Et ces éléments inconnues peuvent être en dehors de `D`. Puis ces éléments étant inconnues leurs combinaisons entre-elles et avec des élèments de `D` constituerons encore d'autres éléments inconnues, etc...

Ces éléments inconnues sont les combinaisons closes d'opérateurs parmi `i`,`"+(.,.)"`, `"∗(.,.)"` et les éléments de `D`. Ils sont désignés par ses combinaisons

L'extension est dite libre si ces termes sont distincts deux à deux, et n'appartiennent à `D` que lorsque le degrès du polynome est égale à zéro.

Grâce à la distributivité du produit par rapport à l'addition et grâce à la commutativité, ces valeurs inconnues qui sont obtenues par combinaisons closes d'opérateurs parmi `i`,`"+(.,.)"`, `"∗(.,.)"` et les éléments de `D`, se développent en pôlynome de variable `i` à coefficient dans `D`, c'est à dire qu'ils sont tous de la forme :

`x_0+x_1i+x_2i^2+x_3i^3 + ... + x_ni^n`

On chercher à définir l'extension de corps commutatif la plus libre. L'extension d'anneau commutatif libre

L'extension est dite libre si ces termes sont distincts deux à deux, et n'appartiennent à `D` que lorsque le degrès du polynome est égale à zéro.