Sommaire
Suivant

I) Structures finies, langage et théorie

 

1) Introduction

La théorie des ensembles à pour principal objet d'explorer l'infini, et donc peut parraître à bien des égards comme une question byzantine. En effet, certaines opinions estiment qu'il n'existe pas d'infini physiquement possible ni même conceptuellement. D'autres estiment qu'il n'existe qu'une sorte d'infini, dit potentiel, et dont un exemple est l'ensemble `NN`. D'autres encore estiment que l'on peut concevoir des mondes infinis mais qu'ils doivent nécessairement posséder une quantité d'information finie. Et d'autres encore estiment qu'il existe une multitude d'infinis non équipotents...

Cette controverse découle du fait que tout ce qui peut être dit est nécessairement énumérable, c'est à dire ne constitue qu'au plus un ensemble énumérable d'énoncés, c'est à dire produits par un programme informatique.

Le théorème de Löwenheim-Skolem affirme que, si une théorie du premier ordre écrite dans un langage mathématique dénombrable est réalisable dans un monde infini, alors elle est réalisable dans un monde dénombrable. C'est pourquoi, en logique du premier ordre, on choisira la solution la plus simple qui consiste à récuser les infinis autres que ceux équipotents à `NN`.

Une première approche de l'infini consiste à ne considérer que les mondes finis. L'étape suivante qui révèle les subtilités du calcul intuitionniste consiste à considérer les mondes infinies possédant une quantité d'information finie. Cela est équivalent à récuser l'axiome du choix qui nécessite une quantité d'information infinie pour pouvoir faire une infinité de choix arbitraires.

Le théorème de Godel démontre que toute théorie `T` cohérente, suffisamment complexe pour contenir l'arithmétique, est incomplète. C'est à dire qu'il existe au moins une proposition `P` écrite dans le langage de `T` qui ne pourra pas être tranchée par `T`, autrement dit, telle que `T"⊬"P"` et `T"⊬¬"P`. Et ce théorème est valable non seulement pour les théories du premier ordre, mais aussi pour les théories du second ordre.

À partir d'une théorie, on peut construire un programme informatique qui énumère toutes ses déductions. Cela est dû au fait qu'un langage d'opérateurs de présentation énumérable est encore énumérable. Et en passant en revue tout ce qui peut être dit, en ne retenant que ce qui constitue syntaxiquement une démonstration, et pour chaque telle démonstration en n'en retenant que la conclusion, on énumère ainsi toutes les déductions possibles. Parcontre, si le langage est suffisament riche pour pouvoir exprimer l'arithmétique alors le complémentaire, l'ensemble des énoncées non démontrables, n'est pas énumérable, c'est à dire qu'il n'existe aucun programme informatique capable de les énumérer.

Nous allons décrire dans le cas fini, le langage logique du `n`-ième ordre. Cette logique restreinte au cas fini fait partie de l'analyse combinatoire. Elle constitue un pilier de la théorie des ensembles, sans pourtant vraiment en faire partie puisqu'elle ne s'intéresse pas à l'infini.

Les théories mathématiques dans le cas fini, sont toujours complétables ne fussent qu'en énumérant tous les cas. Et davantage encore, la sémantique y est définie de façon exacte sans déclencher de controverse. Tant que l'on reste dans le cadre de la mécanique non-quantique, il n'y a pas plusieurs opinions distinctes sur la question. La sémantique d'une théorie est l'ensemble des mondes finis et complets la satisfaisant.

Nous ne souhaitons pas utiliser le terme de « modèle » tel qu'il est utilisé dans la théorie des modèles, car sa signification en français est ambigüe, désignant tantôt un patron ou un shéma, tantôt un prototype, tantôt un article achevé qu'on exhibe à titre d'exemple. On utilisera à la place le terme de « monde », mais pris, non pas comme quelque chose d'extérieur à la théorie, mais plutôt comme une instantiation de la théorie, entendue comme une instantiation d'un ensemble sous-jacent fini et d'une complétion complète de la théorie. Ainsi on propose un paradigme quelque peu différent dans lequel la sémantique se définit formellement, et on l'appellera la théorie des mondes finis.

Puis nous nous intéresserons au concept d'ensemble infini, mais avec la rigueur des intuitionnistes, c'est à dire que nous nous intéresserons aux mondes infinis ne contenant qu'une quantité finie d'information. Mais qu'est-ce que la quantité d'information d'un monde ? Un monde peut se définir comme un sous-ensemble d'un ensemble mère énumérable qui représente le langage. La quantité d'information d'un sous-ensembles correspond à la taille du plus petit programme l'énumérant. Ainsi seuls les mondes énumérables sont à considérer dans la sémantique. On rejète ainsi d'une certaine façon l'immanence des infinis, en optant pour l'option de l'engendrement. Toute structure infinie du premier ordre possède trois théories ; sa théorie d'engendrement qui prouve son existence, sa théorie du premier ordre qui révèle ses propriétés du premier ordre, et la conjonction des deux qui constitue ce qu'elle est. Cette approche à l'avantage d'apporter des arguments de poids pour assurer la cohérence qui, sans cela, s'avère d'un fondement inextricable dans les logiques d'ordres supérieurs.

2) La genèse

Au départ, il y a le raisonnement, puisque c'est par le raisonnement que nous voulons faire cette genèse. On fait le choix de la logique constructive qui consiste à poser les règles de déductions dans un langage logique.

2.1) Langage logique

Apparait la variable propositionnelle `x` qui est déclarée de façon universelle, puis le connecteur de démontrabilité `"⊢(.,.)"`. Le language peut alors écrire la proposition suivante. C'est l'axiome d'identité, qui affirme la permanence des propositions :

`AAx, x"⊢"x`

La logique constructive comprend la négation totale, notée `¬"(.)"`. Comme elle est totale, si on prend deux fois la négation d'une proposition on retrouve la proposition initiale. C'est l'axiome de la négation totale :

`AAx, "¬¬"x"⊢"x`
`AAx, x "⊢""¬¬"x`

2.2) La tautologie `"⊤"` et l'antilogie `"⊥"`

On ajoute au langage propositionnelle, la proposition `⊤` qui représente la tautologie, et on ajoute l'axiome suivant :

`AAx, x "⊢⊤"`

On ajoute au langage propositionnelle, la proposition `⊥` qui représente l'antilogie, et on ajoute l'axiome suivant :

`AAx, "⊥⊢"x`

L'équivalence (qui se différencie de l'équivalence sémantique) se définie comme suit. `x` est équivalent à `y` si et seulement si `x"⊢"y` et `y"⊢"x`.

Le langage de dimension zéro n'utilise aucune variable, donc il ne comprend que deux propositions qui sont `⊤` et `⊥`.

On dira qu'une proposition `x` est vrai si et seulement si `"⊤⊢"x`. On dira qu'elle est fausse si et seulement si `x"⊢⊥"`. Et on dira qu'elle est indécidée dans les autres cas.

2.3) Langage de dimension 1

Si nous n'utilisons qu'une seule variable,

---- 22 août 2021 ----

`AAx` signifie quelque soit une proposition `x` écrite dans notre langage logique (de dimension quelconque). Le terme `x"⊢"x` s'apparente à une fonction propositionnelle `p` appliquée à `x`. Le même processus qui a défini la variable désignant une proposition s'applique ici pour concevoir un second type de variable désignant une fonction propositionnelle unaire et que l'on note en mettant le suffixe `"(.)"` sur au moins une de ces apparitions à titre de déclaration. L'expression `AAp"(.)"` signifie quelque soit une fonction propositionelle unaire `p` écrite dans notre langage logique.

La négation d'une proposition de la forme : `AAx, p(x)` est `EEx, ¬p(x)`. L'expression `EEx` signifie qu'il existe une proposition `x` écrite dans notre langage logique. L' introduction du quantificateur `EE` se fait en ajoutant l'axiome suivant qui le définit :

`AA p"(.)",("¬"AA x, p(x)) |-- EEx,"¬"p(x)`

Afin de réduire l'usage des parenthèses, une priorité syntaxique est posée comme suit de la plus forte à la plus faible : Appel de fonction propositionelle `P"(.)"`, négation `"¬(.)"`, déduction `"⊢(.,.)"`, déclaration de variable `AAX, "(_)"` et `EEX, "(_)"`. Le symbole `"(.)"` indique qu'un paramètre est nécessaire et que ce paramètre doit être une proposition. Le symbole `"(_)"` indique qu'un paramètre est nécessaire et que ce paramètre doit être un terme appartenant à "<⊤","⊥",x, "⊢(.,.)>".

La proposition `EEX, X` est tautologique puisque elle se satisfait elle-même, et donc la proposition

`AAX, X`

est antilogique. Ce sont des tautologies et antilogies sémantiques, car nous n'avons pas ajouté les règles formelles de raisonnement pour conclure cela, nous avons construit un modèle satisfaisant la proposition qui s'avère être la proposition elle-même.

---- 22 août 2021 ----

 

 

2.3) Langage de dimension 1

 

Notre langage logique est contextuel, c'est à dire qu'une même sous-formule n'a pas la même signification globale selon où elle se situe dans la formule. Car les variables utilisées auront une signification différente selon le lieu et la façon dont elles ont été déclaré.

Mais une proposition peut déclarer plusieurs variables, aussi devrons nous considérer les fonctions propositionnelles d'arité `n`.

On est amené à considérer une forme plus générale que la proposition qui est la fonction propositionnelle `n`-aire. Les propositions sont les fonctions propositionnelle nullaire. Cette première unification nous amène à utiliser une forme plus générale que la proposition qu'est la fonction propositionnelle .

On note `vec w` une liste de `n` variable propositionnelle. On note `p"(...)"`, une fonction propositionnelle `n`-aire. Et on note `p(vec w)` l'application de de la fonction `p` aux paramètres `vec w`.

L' introduction du quantificateur `EE` se fait en ajoutant l'axiome suivant qui le définit :

`AA p"(...)",("¬"AA vec w, p(vec w)) |-- EEx,"¬"p(vec w)`

L'inférence de type fait que la taille de `vec w` doit correspondre à l'arité de `p`. Aussi cet axiome correspond à une série d'axiome, un pour chaque valeur de `n`.

Afin de réduire l'usage des parenthèses, une priorité syntaxique est posée comme suit de la plus forte à la plus faible : Appel de fonction propositionelle `P"(...)"`, négation `"¬(.)"`, déduction `"⊢(.,.)"`, déclaration de variable `AAX, "(.)"` et `EEX, "(.)"`.

 

 

Les mots sont essentiels pour exprimer toutes pensés, et davantage encore, ils permettent de penser. Appliqué à notre génèse, les mots en questions appelés lexèmes sont des fonctions. Le langage permet de construire des éléments et des littéraux à partir d'autres éléments d'une façon la plus générale, par appel de fonction multi-aire mais limité à un nombre fini d'arguments, à l'aide de deux lexèmes que sont la fonction `n`-aire et la fonction caractéristique `n`-aire

Etant donné un élément `a`, une fonction unaire `f"(.)"` s'applique à l'élément `a` pour former l'éventuel élément `f(a)`. Mais il reste à prouver son existence. La construction est hypothétique, et si l'élément existe alors il sera bien désigné par le terme `f(a)`. De même, une fonction caractéristique unaire `F"(.)"` s'applique à l'élément `a` pour éventuellement retourner un booléen, désignant ainsi une valeur logique. Mais il reste à prouver que cette valeur logique est définie. La valeur booléenne en question est de définition hypothétique, et si la fonction caractéristique `F` est définie en `a` alors la valeur logique évoquée sera bien désignée par le littéral `F(a)`.

Si une fonction `f"(.)"` est définie pour tout élément, alors on l'appellera foncteur unaire. Et si la fonction caractéristique unaire `F"(.)"` est définie pour tout élément, alors on l'appellera relateur unaire.

Le meme processus qui a défini la variable désignant un élément s'applique pour concevoir la variable désignant une fonction unaire. Se pose alors une question : "Pouvons-nous unifier une variable de type élément avec une variable de type fonction unaire ?", ou autrement dit, un élément peut-il être une fonction unaire et vis-versa, ce qui permet entre autre qu'une fonction unaire puisse s'appliquer à elle même. Pourquoi s'interdire cette possibilité qui n'oblige rien, et qui est donc la plus générale ? Chaque élément peut être identifié à une fonction unaire, ou plus exactement chaque élément peut être rendu égale à une fonction unaire, une liberté qui n'entraine pas de contrainte. Et nous touchons là à deux propriétés propres à la nature des éléménts, qu'une fonction unaire est un élément, et qu'un élément peut-être une fonction unaire. Délors, éléments et fonction unaire ne sont désignés que par un seul type de variable.

Néanmoins une distinction persiste entre les éléments qui ne sont pas des fonctions unaires et ceux qui le sont. Cette distinction se concrétise par un relateur unaire `cc(F1)"(.)"` qui appliqué à un élément retourne `1` si c'est une fonction unaire et `0` si ce n'est pas une fonction unaire.

Puis la définition d'une fonction unaire se concrétise par un relateur ternaire `"∈(.,.)"` désignant le lien d'appartenance entre un élément et un ensemble, avec donc comme contrainte, que des éléments distincts qui sont des ensembles doivent nécessairement constituer des ensembles distincts.

`AAxAAy, ccE(x) "et" ccE(y) "et" x "≠" y => ¬(AAz, z"∈"x <=> z"∈"y)`

La valeur du relateur `"∈(.,.)"` entre un élément et un élément qui n'est pas un ensemble n'a pas de signification, et peut être canoniquement fixée à `0`, prolongant par analogie les éléments qui ne sont pas des ensembles en des ensembles vides singularisés en s'accaparant un nom (le nom de l'élément) qui permet ainsi de les différencier.

La question qui se pose est : "Pouvons-nous unifier une variable fonction unaire avec une variable de type élément ?", ou autrement dit, un élément peut-il être une fonction unaire et vis-versa, ce qui permet entre autre qu'une fonction unaire puisse s'appliquer à elle-même. L'unification entre fonctions unaires et éléments est possible. Pourquoi s'interdire cette possibilité qui n'oblige rien, et qui est donc la plus générale ? Chaque élément peut être identifié à une fonction unaire, ou plus exactement chaque élément peut être rendu égale à une fonction unaire, une liberté qui n'entraine pas de contrainte si nous avons toujours la possibilité de créer de nouveaux éléments pour ne pas être à court d'éléments.

---- 20 aout 2021 ----

Néanmoins il existe bien deux sortes d'ensembles qui ne sont pas unifiables, que sont les catégories et les ensembles. Et il en est de même pour les fonctions. Une fonction est définie par son graphe qui est un esnsemble d'arcs (élément, image). Il y a donc deux sortes de fonction, celles qui ont comme graphe une catégorie et celles qui ont comme graphe un ensemble.

 

 

 

L'élément n'est pas suffisant pour évoquer l'infini. C'est pourquoi on conçoit un second type d'objet regroupant des éléments. Et il y a 4 premières façons de regrouper des éléments que sont : la liste, l'arrangement, le sac et l'ensemble. Si nous choisissons la liste, on reste au stade de l'informatique. Et si nous choisissons l'ensemble, on passe à un stade supérieur que sont les mathématiques. Ces 4 façons de regrouper des éléments sont arbitraires. Si nous voulons nous affranchire de cet arbitraire, il nous faudrait dévoiler les briques élémentaires qui ont permis la définition de ces 4 formes d'assemblages, ce qui nous ramène alors à une approche informatique.

La question qui se pose est : "Pouvons-nous unifier une variable de type ensemble avec une variable de type élément ?", ou autrement dit, un élément peut-il être un ensemble et vis-versa, ce qui permet entre autre qu'un ensemble puisse se contenir lui-même. Pourquoi s'interdire cette possibilité qui n'oblige rien, et qui est donc la plus générale ? Chaque élément peut être identifié à un ensemble, ou plus exactement chaque élément peut être rendu égale à un ensemble, une liberté qui n'entraine pas de contrainte. Et nous touchons là à deux propriétés propres à notre logique, nous dirons des propriétés cosmogoniques, qui touchent non pas à un objet créé mais au cadre dans lequel sont créés les objets ou à leur nature, qu'un ensemble est un élément, et qu'un élément peut-être un ensemble. Délors, éléments et ensembles ne sont désignés que par un seul type de variable.

Néanmoins une distinction persiste entre les éléments qui ne sont pas des ensembles et ceux qui le sont. Cette distinction se concrétise par un relateur unaire `ccE"(.)"` qui appliqué à un élément retourne `1` si c'est un ensemble et `0` si ce n'est pas un ensemble. Puis la définition des ensembles se concrétise par un relateur binaire `"∈(.,.)"` désignant le lien d'appartenance entre un élément et un ensemble, avec donc comme contrainte, que des éléments distincts qui sont des ensembles doivent nécessairement constituer des ensembles distincts.

`AAxAAy, ccE(x) "et" ccE(y) "et" x "≠" y => ¬(AAz, z"∈"x <=> z"∈"y)`

La valeur du relateur `"∈(.,.)"` entre un élément et un élément qui n'est pas un ensemble n'a pas de signification, et peut être canoniquement fixée à `0`, prolongant par analogie les éléments qui ne sont pas des ensembles en des ensembles vides singularisés en s'accaparant un nom (le nom de l'élément) qui permet ainsi de les différencier.

2.1) Langage propositionnel

Les variables représentent des éléments qui peuvent etre des ensembles. Elles doivent être quantifiés universellement ou existentiellement sur la catégorie des éléments. Leur domaine au quel elles appartiennent n'est pas limité par un ensemble mais par une catégorie. La catégorie des éléments qui est aussi la catégorie des ensembles.

Une proposition qui comprend de telles variables est dite cosmogonique, propre au cosmos logique. Elle révèle une connaissance globale sur notre logique, sur son cadre. Si on restreint la quantification à un ensemble `E`, la proposition devient une proposition logique relative à `E`. Par exemple, considérons le relateur binaire `P"(.,.)"`  :

Proposition cosmogonique `AAxEEy, P(x,y)`
Proposition relative à `E` `AAxEEy, (x "∈" E) "et" (y "∈" E) => P(x,y)`
`AAx "∈" E, EEy "∈" E, P(x,y)`

Les mots sont essentiels pour exprimer toutes pensés, et davantage encore, ils permettent de penser. Appliqué à notre génèse, les mots en questions appelés lexèmes sont des fonctions.

Le langage permet de construire des éléments et des littéraux d'une façon multi-aire non-infini la plus générale à l'aide de deux lexèmes que sont la fonction `n`-aire et la fonction caractéristique `n`-aire.

 

 

 

 

 

 

Les fonctions non-limitées à un ensemble de départ, les foncteurs et les relateurs sont des objets cosmogoniques, contrairement aux fonctions limitées à un ensemble de départ, aux opérateurs et aux prédicats.

L'ensemble de tous les éléments n'est pas un ensemble. On l'appelle la catégorie des éléments. Et, à la différence d'un ensemble, la catégorie n'évoque pas ses éléments, faisant qu'il est toujours possible de créer un nouvel élément non encore évoqué, bien que celui-ci appartiendra nécessairement à la catégorie des éléments.

L'ensemble des prédicats unaires définis sur `E` se note `E"→"{0,1}`.
L'ensemble des fonctions unaires définis sur `E` se note `E^n"→"{0,1}`.
L'ensemble des prédicats `n`-aires définis sur `E` se note `E^n"→"{0,1}`.
L'ensemble des opérateurs `n`-aires internes à `E` se note `E^n"→"E`.

On remarque qu'il existe une bijection canonique entre les pédicats unaire `P"(.)"` définie sur `E` et les sous-ensembles de `E` :

`(((E"→"{0,1})     →          {A "/" A"⊆"E}), (P"(.)"         |->     {x "/" (x "∈" E) "et" P(x)}))`

Parcontre, si `P` est un relateur unaire, la formule `{x "/" P(x)}` produit une catégorie, une sorte d'ensemble mais qui n'évoque pas nécessairement ses éléments.

À partir de l'ensemble, nous définissons une notion de type qui va faire le lien avec le langage formel que nous construisons. Un ensemble est la première caractéristique d'un tel type, son extension. Puis le type s'enrichie de facultés qui dépassent sa seule compréhension, il munie les éléments d'une syntaxe, ils munie l'ensemble de tous ses éléments d'opérateurs et de prédicats qui sont des connaissances introspectives, des moyens de calcul et de construction. Le type s'accapare les attributs d'une structure mathématique, et l'ensemble auquel il correspond est l'ensemble sous-jacent de la structure. Si un élément possède un type déclaré, il bénéficie de la syntaxe définie dans ce type, et il bénéficie d'un pouvoir d'inférence de type. Par exemple considérons l'expression suivante :

`A = {x "/" EEx, P(x)}`

Le type de `A` dépend du type de `P`. Si `P` est un foncteur alors `A` est une catégorie. Et si `P` est un prédicats alors `A` est un sous-ensemble de `tt(Dép)(P)` l'ensemble de départ de `P`.

La quantification de `x` ne peut s'opérer que sur l'ensemble de départ de `P`. C'est le type de `P` qui oblige cela. L'éxecution de cette contrainte s'appelle le typage par inférence. L'expression `P(x)` sous-entend que `x` appartient à `tt"Dép"(P)` puisqu'il s'applique à `x`. L'inférence de type fait que `x` est de type `tt"Dép"(P)` et qu'il n'est pas nécessaire d'apporter d'autres précisions à sa quantification `EEx` qui signifie `EEx"∈"tt"Type"(x)` c'est à dire `EEx"∈"tt"Dép"(P)`.

La troisième question qui se pose est : "Pouvons-nous unifier une variable fonction unaire avec une variable de type élément ?", ou autrement dit, un élément peut-il être une fonction unaire et vis-versa, ce qui permet entre autre qu'une fonction unaire puisse s'appliquer à elle-même. L'unification entre fonctions unaires et éléments est possible. Pourquoi s'interdire cette possibilité qui n'oblige rien, et qui est donc la plus générale ? Chaque élément peut être identifié à une fonction unaire, ou plus exactement chaque élément peut être rendu égale à une fonction unaire, une liberté qui n'entraine pas de contrainte si nous avons toujours la possibilité de créer de nouveaux éléments pour ne pas être à court d'éléments.

Néanmoins il existe bien deux sortes d'ensembles qui ne sont pas unifiables, que sont les catégories et les ensembles. Et il en est de même pour les fonctions. Une fonction est définie par son graphe qui est un esnsemble d'arcs (élément, image). Il y a donc deux sortes de fonction, celles qui ont comme graphe une catégorie et celles qui ont comme graphe un ensemble.

 

 

 

---- 20 aout 2021 ----

 

Et qu'il est toujours possible d'ajouter un nouvel élément.

Notre approche constructive est à ce stade incapable de reconnaitre l'infini. Il lui faut un axiome supplémentaire pour pouvoir concrétiser l'infini potentiel. C'est la première abstraction. Celle-ci s'opppose aux infinis innés pour ne considérer que les infinis engendrés. Mais pour engendrer un infini potentiel, pour l'engendrer concrètement, il est nécessaire de concevoir au moins un infini inné, celui du temps, celui du nombre d'opérations déterminées à exécutées qui doit être un infini dénombrable. Remarquez que cela n'entraine nullement une quantité information infinie. Ainsi la première abstraction consiste à concrétiser les infinis potentiels grace à un infini particulier qui est aleph, noté `aleph`, le cardinal de `NN`.

Dans cette première abstraction qui s'appelle `aleph`, l'ensemble `NN` existe et représente une quantité d'information ridiculement faible.

Cette abstraction à l'inconvénient d'être monothéiste, n'invoquant qu'un seul dieu, qu'un seul infini. Aussi, devrons-nous explorer d'autres alternatives, des abstractions où il y aurait plusieurs infinis de natures différentes, et incomparables entre eux.

Une propriété fondamentale propre à notre logique est qu'il est toujours possible de créer un nouvel élément, distinct de tous les autres éléments évoqués. C'est le premier axiome, l'axiome de création. Cela explique pourquoi il n'existe pas d'ensemble de tous les éléments. Et cet axiome de création ne peut pas se réduire à un axiome d'existence d'un premier élément, en ajoutant des axiomes telles les briques élémentaires précédement évoquées permettant de définir ; les listes, les arrangements, les sacs, les ensembles, etc.., et permettant ainsi de construire une infinité d'autres éléments à partir de ce premier élément. Car la première abstraction `aleph` permet de construire tous ces éléments, et nous serions alors en présence d'un ensemble de tous les éléments, et donc, dans l'incapacité de satisfaire le premier axiome.

Deux ensembles sont égaux si tout élément de l'un est dans l'autre et que tout élément de l'autre est dans l'un. Aussi il n'y a au plus qu'un seul ensemble vide noté `Ø`. Et il n'y a au plus qu'un seul ensemble singleton contenant `a`, noté `{a}`. Parcontre rien n'indique pour l'instant qu'il n'y a, qu'au plus, un seul ensemble singleton se contenant lui-même, une autre propriété propre à notre logique que nous développerons plus tard.

`AAx, x "∉"Ø`

`AAx, x "∈" {a} <=> x"="a`

Remarquer que l'on nomme l'élément `Ø` avant de savoir s'il existe. C'est une variable avancée par une hypothèse, qui, si cela aboutie à une contradiction, permet de démontrer sa non-existence. Pour prouver son existence, il faut un axiome supplémentaire qui s'inclut naturellement dans un axiome plus vaste définissant le foncteur binaire de différence symétrique `Delta`. L'axiome dit que l'on peut toujours retirer dans un ensemble tous les éléments qui appartiennent à un autre ensemble pour former un autre ensemble. Délors on construit l'ensemble vide à partir de n'importe quel ensemble `a` en exécutant `a Delta a`. On démontre ainsi son existence.

De meme, remarquer que l'on nomme l'ensemble `{a}` avant de savoir s'il existe, et qu'il est composé d'une fonction unaire `{"."}` et d'un argument `a` qui est un élément déjà évoqué, ou bien un nouvel élément, ou bien encore le singleton lui-même que nous définissons. L'existence de `{a}` est avancée par une hypothèse, qui, si cela aboutie à une contradiction, permet de démontrer sa non-existence. Pour prouver son existence, il faut un axiome supplémentaire qui nous permette de le construire, tel le foncteur unaire `{"."}` de construction d'ensemble singleton. Délors on construit l'ensemble singleton contenant `a` en exécutant `{a}`. On démontre ainsi son existence.

Remarquez néanmoins qu'il y a une opération fondamentale faite avant la construction du singleton, qui est soit la création d'un nouvel élément `a` nécessitant l'axiome de création ou soit une référence récurcive afin que l'ensemble contienne comme élément lui-même, ce qui nécessite l'axiome de création récursive, ou soit le choix d'un élément déjà créé appartenant à un ensemble, ce qui nécessite l'axiome du choix fini.

La première étape non-cosmogonique consiste donc à choisir un élément arbitraire `a` dans un ensemble non vide (pour pouvoir choisir un élément) et non réduit à un singleton (pour pouvoir choisir un élément arbitraire). C'est l'axiome du choix fini, qui affirme qu'il est possible de faire un nombre fini de choix arbitraires. Voyez la différence, s'il est possible de créer une infinités de nouveaux éléments indéfinis, il est parcontre impossible de faire une infinité de choix arbitraires, tel le choix arbitraire d'un élément dans chaque ensemble d'une collection infini d'ensembles non vides et non réduits à des singletons. Le premier acte n'apporte pas de quantitié d'information infini alors que le second, si. La deuxième étape est d'en faire un ensemble `{a}`.

2.1) Langage propositionnel

Les variables représentent des éléments qui sont des ensembles. Elles doivent être quantifiés universellement ou existentiellement sur la catégorie des éléments. Leur domaine au quel elles appartiennent n'est pas limité par un ensemble mais par une catégorie. La catégorie des éléments qui est aussi la catégorie des ensembles.

Une proposition qui comprend de telles variables est dite cosmogonique, propre au cosmos logique. Elle révèle une connaissance globale sur notre logique, sur son cadre. Si on restreint la quantification à un ensemble `E`, la proposition devient une proposition logique relative à `E`. Par exemple, considérons le relateur binaire `P"(.,.)"`  :

Proposition cosmogonique `AAxEEy, P(x,y)`
Proposition relative à `E` `AAxEEy, (x "∈" E) "et" (y "∈" E) => P(x,y)`
`AAx "∈" E, EEy "∈" E, P(x,y)`

Les mots sont essentiels pour exprimer toutes pensés, et davantage encore, ils permettent de penser. Appliqué à notre génèse, les mots en questions appelés lexèmes sont des fonctions.

Le langage permet de construire des éléments et des littéraux d'une façon multi-aire non-infini la plus générale à l'aide de deux lexèmes que sont la fonction `n`-aire et la fonction caractéristique `n`-aire.

Etant donné un élément `a`, une fonction unaire `f"(.)"` s'applique à l'élément `a` pour former l'éventuel élément `f(a)`. Mais il reste à prouver son existence. La construction est hypothétique, et si l'élément existe alors il sera bien désigné par le terme `f(a)`.

De même, une fonction caractéristique unaire `F"(.)"` s'applique à l'élément `a` pour éventuellement retourner un booléen, désignant ainsi une valeur logique. Mais il reste à prouver que cette valeur logique est définie. La valeur booléenne en question est de définition hypothétique, et si la fonction caractéristique `F` est définie en `a` alors la valeur logique évoquée sera bien désignée par le littéral `F(a)`.

Si une fonction unaire `f"(.)"` est définie pour tout élément de `E`, alors on l'appellera application unaire sous-entendu de `E` vers `f(E)`. Si de plus `f(E)"⊆"E`, on dira que c'est un opérateur unaire sous-entendu interne à `E`.

De même, si une fonction caractéristique unaire `F"(.)"` est définie pour tout élément de `E`, alors c'est une application unaire de `E` vers `{0,1}` et on dira que c'est un prédicat unaire sous-entendu définie sur `E`.

Si une fonction `f"(.)"` est définie pour tous les éléments de la catégorie des éléments, alors on l'appellera foncteur unaire. Et si la fonction caractéristique unaire `F"(.)"` est définie pour tous les éléments de la catégorie des éléments, on dira que c'est un relateur unaire.

Les fonctions non-limitées à un ensemble de départ, les foncteurs et les relateurs sont des objets cosmogoniques, contrairement aux fonctions limitées à un ensemble de départ, aux opérateurs et aux prédicats.

L'ensemble de tous les éléments n'est pas un ensemble. On l'appelle la catégorie des éléments. Et, à la différence d'un ensemble, la catégorie n'évoque pas ses éléments, faisant qu'il est toujours possible de créer un nouvel élément non encore évoqué, bien que celui-ci appartiendra nécessairement à la catégorie des éléments.

L'ensemble des prédicats unaires définis sur `E` se note `E"→"{0,1}`.
L'ensemble des fonctions unaires définis sur `E` se note `E^n"→"{0,1}`.
L'ensemble des prédicats `n`-aires définis sur `E` se note `E^n"→"{0,1}`.
L'ensemble des opérateurs `n`-aires internes à `E` se note `E^n"→"E`.

On remarque qu'il existe une bijection canonique entre les pédicats unaire `P"(.)"` définie sur `E` et les sous-ensembles de `E` :

`(((E"→"{0,1})     →          {A "/" A"⊆"E}), (P"(.)"         |->     {x "/" (x "∈" E) "et" P(x)}))`

Parcontre, si `P` est un relateur unaire, la formule `{x "/" P(x)}` produit une catégorie, une sorte d'ensemble mais qui n'évoque pas nécessairement ses éléments.

À partir de l'ensemble, nous définissons une notion de type qui va faire le lien avec le langage formel que nous construisons. Un ensemble est la première caractéristique d'un tel type, son extension. Puis le type s'enrichie de facultés qui dépassent sa seule compréhension, il munie les éléments d'une syntaxe, ils munie l'ensemble de tous ses éléments d'opérateurs et de prédicats qui sont des connaissances introspectives, des moyens de calcul et de construction. Le type s'accapare les attributs d'une structure mathématique, et l'ensemble auquel il correspond est l'ensemble sous-jacent de la structure. Si un élément possède un type déclaré, il bénéficie de la syntaxe définie dans ce type, et il bénéficie d'un pouvoir d'inférence de type. Par exemple considérons l'expression suivante :

`A = {x "/" EEx, P(x)}`

Le type de `A` dépend du type de `P`. Si `P` est un foncteur alors `A` est une catégorie. Et si `P` est un prédicats alors `A` est un sous-ensemble de `tt(Dép)(P)` l'ensemble de départ de `P`.

La quantification de `x` ne peut s'opérer que sur l'ensemble de départ de `P`. C'est le type de `P` qui oblige cela. L'éxecution de cette contrainte s'appelle le typage par inférence. L'expression `P(x)` sous-entend que `x` appartient à `tt"Dép"(P)` puisqu'il s'applique à `x`. L'inférence de type fait que `x` est de type `tt"Dép"(P)` et qu'il n'est pas nécessaire d'apporter d'autres précisions à sa quantification `EEx` qui signifie `EEx"∈"tt"Type"(x)` c'est à dire `EEx"∈"tt"Dép"(P)`.

La troisième question qui se pose est : "Pouvons-nous unifier une variable fonction unaire avec une variable de type élément ?", ou autrement dit, un élément peut-il être une fonction unaire et vis-versa, ce qui permet entre autre qu'une fonction unaire puisse s'appliquer à elle-même. L'unification entre fonctions unaires et éléments est possible. Pourquoi s'interdire cette possibilité qui n'oblige rien, et qui est donc la plus générale ? Chaque élément peut être identifié à une fonction unaire, ou plus exactement chaque élément peut être rendu égale à une fonction unaire, une liberté qui n'entraine pas de contrainte si nous avons toujours la possibilité de créer de nouveaux éléments pour ne pas être à court d'éléments.

Néanmoins il existe bien deux sortes d'ensembles qui ne sont pas unifiables, que sont les catégories et les ensembles. Et il en est de même pour les fonctions. Une fonction est définie par son graphe qui est un esnsemble d'arcs (élément, image). Il y a donc deux sortes de fonction, celles qui ont comme graphe une catégorie et celles qui ont comme graphe un ensemble.

---- 19 Août 2021 ----

 

 

 

fonctions dont nous parlons ici doivent être définies sur un ensemble.

 

Ces différentes unifications nous amène aux langages alpha, un langage muni d'une loi interne multi-aire qui identifie ainsi chaque élément à une fonction multi-aire de domaine ensembliste, et que l'on muni d'un relateur binaire d'appartenance identifiant ainsi chaque élément à un ensemble. Mais l'identification doit transporter l'égalité dans les deux sens, c'est à dire que deux ensembles possèdant les même éléments doivent être égaux, et deux fonctions unaires possèdant le meme graphe (ensemble de couples élément-image) doivent être égales.

Tout ensemble peut-etre rendu égale à un autre ensemble. Toutes fonctions milti-aire

La troisième question qui se pose est : "Pouvons-nous unifier une variable fonction avec une variable de type élément ?", ou autrement dit, un élément peut-il être une fonction et vis-versa, ce qui permet entre autre qu'une fonction puisse s'appliquer à elle-même. On ne peut pas unifier une fonction unaire et une fonction binaire car leur comportement diffèrent. Néanmoins si nous considérons des fonctions à la fois binaires et unaires, on peut les unifier. L'unification des fonctions est possibles pour les fonctions multi-aires qui ont toutes le même comportement. Pourquoi s'interdire cette possibilité qui n'oblige rien, et qui est donc la plus générale ? Chaque élément peut être identifié à une fonction multi-aire, ou plus exactement chaque élément peut être rendu égale à une fonction multi-aire, une liberté qui n'entraine pas de contrainte si nous avons toujours la possibilité de créer de nouveaux éléments pour ne pas être à court d'éléments. Néanmoins il existe bien deux sortes d'ensembles qui ne sont pas unifiables, que sont les catégories et les ensembles. Et donc les fonctions dont nous parlons ici doivent être définies sur un ensemble.

Ces différentes unifications nous amène aux langages alpha, un langage muni d'une loi interne multi-aire qui identifie ainsi chaque élément à une fonction multi-aire de domaine ensembliste, et que l'on muni d'un relateur binaire d'appartenance identifiant ainsi chaque élément à un ensemble. Mais l'identification doit transporter l'égalité dans les deux sens, c'est à dire que deux ensembles possèdant les même éléments doivent être égaux, et deux fonctions unaires possèdant le meme graphe (ensemble de couples élément-image) doivent être égales.

Tout ensemble peut-etre rendu égale à un autre ensemble. Toutes fonctions milti-aire

 

---- 18 Août 2021 ----

 

a=b ssi AAx in a, x in b et AAx in b, x in a

a=b ssi AAx a(x)=b(x)

une fonction `a`ppliquée à `x` retourne un élément `a(x)` s'il existe, retourne `oo` s'il n'existe pas, et retourne `?` si, ni son existence, ni son inexistence ne peut être démontrée. Une fonction caractéristque appliquée à `x` retourne `0` ou `1` ou `oo` ou `?`.

 

 

3) Les types dérivés

Un type désigne un ensemble `E` qui est son extension. Une variable de type `E` est une variable dont la valeur est un élément appartenant à `E`. Il est alors possible de construire un ensemble plus vaste `E"+"E` qui constitue un type dérivé de `E`. Et on constate qu'il existe un isomorphisme canonique entre `E"+"E` et `E"×"{0,1}`, l'ensemble des couples composés d'un élément de `E` et d'un booléen. C'est d'ailleurs par ce moyen qu'on le représente concrètement. Et on constate qu'il y a deux plongements canoniques de `E` dans `E"+"E`.

Délors, on constate qu'une duplication d'un ensemble `E` peut facilement être faite en fasant le produit avec `{0,1}`.

Le type comprend des opérateurs, tel que l'opérateur identité `(x|->x)` qui appliqué à un élément de `E` retourne le même élément. Il peut avoir toutes sortes d'autres opérateurs. Et plusieurs types peuvent avoir la même extension, de la même façon que deux structures peuvent avoir le même ensemble sous-jacent. L'isomorphisme et les plongements canoniques évoqués au paragraphe précédent se déclinent pour chaque type de `E` et définissent les types correspondants de `E"+"E`.

Le type est souvent désigné par la même lettre que son ensemble. Et c'est le typage par inférence ou le contexte qui permet de savoir si c'est un type ou un ensemble qui est évoqué dans une formule. On définie en parallèle l'addition des types. Le type `A"+"B` à pour ensemble `A"+"B` représenté par :

`A"+"B = {(a,0) "/" EE a "∈" A} uu {(b,1) "/" EE b "∈" B}`

Puis on souhaite que l'addition des types soit commutative, c'est à dire que `A"+"B` soit identique à `B"+"A`. Pour assurer cela, il faut pouvoir définir une forme normale, un ordre canonique. Or, si tous les éléments sont créés en une quantité infini dénombrable, ils sont néanmoins créés dans un ordre total. La forme normale choisit le sens tel que `A"<"_"def"B``A` a été créé ou construit avant `B`.

Puis on souhaite que l'addition des types soit associative c'est à dire que `(A"+"B)"+"C"` soit identique à `A"+("B"+"C")`. La forme normale correspond à l'aplanissement de la liste d'addition et à sa mise en ordre. Et comme à ce stade tous les ensembles qui ne sont ni des ensemble vides ni des singletons sont créer par addition, la forme normale consiste alors à proposer une liste d'éléments `(a_1,a_2,_3,...,a_n,...)` qui représente l'ensemble `{(a_1,1), (a_2,2), (a_3,3), ..., (a_n,n), ...}` et où `{a_i,1} "<"_"def" {a_2,2}`. Mais n'allons pas plus loin dans ce raisonnement étrange.

---- 31 juillet 2021 ----

 

 

 

 

Puis on souhaite que l'addition d'ensembles soit associative, c'est à dire que `(E"+"E)"+"E"` soit identique à `E"+("E"+"E")` et se note `E"+"E"+"E"`. Cela correspond à l'aplanissement d'une liste mais mise en oeuvre seulement au dernier niveau évoqué.

---- 29 juillet 2021 ----

 

Dans un ensemble `E`, l'ensemble des applications, défini au sens le plus générale, sera donc `E"→"E`, et l'ensemble les prédicats, défini au sens le plus générale, sera `E"→"{0,1}`. C'est comme cela que l'on construit les types dérivés de `E`. Parcontre `E` et `E"→"E` ne peuvent pas être unifiés, tout au plus peut-on plonger `E` dans `E"→"E`. Il existe en effet un moyen canonique pour le faire qui fonctionne en toute circonstance, qui associe à tout élement `y` l'application constante produisant `y`.

`varphi(y) = (x"↦"y)`

 

Qu'est-ce qui est plus général, une application de `A` vers `B`, ou bien une application de `E` vers `E` ? S'il fallait répondre vite à cette question, on répondrait la première, et on ferait une erreur, car chacune contient potentiellement l'autre. En effet les applications de `A` vers `B` couvrent toutes les applications de `E` vers `E` lorsque `A"="B"="E`, et réciproquement lorsque `E"="A"∪"B`, les applications de `E` vers `E` restreintes à `A` couvrent toutes les applications de `A` vers `B`. Et donc la plus générale des deux est la plus simple des deux, c'est à dire l'application de `E` vers `E`. Rappelez-vous cet adage, car il s'appliquera à d'autres situations : « Etant donné deux formes, si chacune est incluse dans l'autre alors la plus générale des deux est la plus simple des deux. »

Dans un ensemble `E`, l'ensemble des applications, défini au sens le plus générale, sera donc `E"→"E`, et l'ensemble les prédicats, défini au sens le plus générale, sera `E"→"{0,1}`. C'est comme cela que l'on construit les types dérivés de `E`. Parcontre `E` et `E"→"E` ne peuvent pas être unifiés, tout au plus peut-on plonger `E` dans `E"→"E`. Il existe en effet un moyen canonique pour le faire qui fonctionne en toute circonstance, qui associe à tout élement `y` l'application constante produisant `y`.

`varphi(y) = (x"↦"y)`

Sans information sur l'ensemble `E`, l'application `varphi` est l'unique plongement constructible de `E` dans `E"→"E`. A partir d'un ensemble `E` qui n'est pas réduit à un singleton ou à l'ensemble vide, on définit donc deux types différents, `E` et `E"→"E`. Il découle de ce constat l'existence de nouveaux types dérivés `(E"→"E)"→"E`, `E"→"(E"→"E)` et `(E"→"E)"→"(E"→"E)`, et une infinité d'autres encore.

Puis on considère les produits `A"×"B` `A,B` sont des types dérivés de `E`. C'est l'ensemble des couples d'éléments où la première composante appartient à `A` et la seconde composante appartient à `B`.

En logique du premier ordre, ces deux opérations `"×"` et `"→"` vont suffire pour couvrir tous les types dérivés pertinent. Il y en a une profusions. Le langage de types est le langage d'opérateurs `"<"E, {0,1}, "×(.,.)","→(.,.)>"` où les opérateurs en question opérent non pas sur des éléments mais sur des types.

Lorque l'on explore les logiques d'ordres supérieurs, qui incorpore dans le langage la programmation, d'autres opérateurs de création de type apparaîtront, dont l'un des plus simples est l'opérateur de Kleen sans mot vide qui appliqué à un ensemble `A` se note `A^"+"` et constitue l'ensemble des listes finies non vides d'éléments de `A`.

3) Langage de types

À partir du langage des types `"<"E, {0,1}, "×(.,.)","→(.,.)>"` qui met en oeuvre un paradigme de programmation qu'est la programmation orienté objet, nous allons définir des types plus généraux regroupant les types qui sont liées entre-eux par des isomorphismes canoniques.

3.1) Le produit `"×"`

La première règle considérée va dévoilé une associativité de l'opérateur `"×"`. En effet, pour tout type `A,B,C` dérivés de `E`, Le type `A"×"(B"×"C)` est canoniquement isomorphe au type (A"×"B)"×"C` et également au type `A"×"B"×"C`

nous posons `A"×"(B"×"C) = (A"×"B)"×"C`. Une succession de produit `A"×"B"×"C` que l'on peut notée ainsi puisque le produit est associatifs, s'appelle une liste. L'associativité va aplanir les arguments en une liste d'arguments qui ne sont pas des listes, pour former une liste dont la taille correspondra à une arité.

 

en changeant leurs méthodes. On mettra pour cela en oeuvre un autre paradigme de programmation qu'est la programmation orienté aspect, qui va modifier le comportement des applications selon les types des arguments qu'on lui propose, et qui va nous permettre de regrouper des types analogues en un seul type plus général. Nous allons établir des règles d'égalités entre types, pour les regrouper dans des classes d'équivalence et les rendre égaux par la programmation d'aspects. L'ensemble de ces règles d'égalité formera une théorie des types. Et la contrepartie de ces règles constitura un ensemble d'aspects qui définira un mécanisme d'application des applications.

Les types appartenant au sous-ensemble `"<"{0,1}, "×(.,.)","→(.,.)>"` sont dit numérique.

 

La seconde règle considérée est la commutativité de l'opérateur `"×"`. C'est à dire pour tout type `A,B` dérivés de `E`, nous posons `A"×"B = B"×"A`. Cela signifie qu'une application qui prend comme premier argument un élément de type `A` et comme second argument un élément de type `B`, est de même type qu'une application qui prend comme premier argument un élément de type `B` et comme second argument un élément de type `A`. Ce choix peut surprendre. Remarquez que lorsque `A"="B` cela est une évidence. Parcontre lorsqu'ils sont distincts, on se doit alors de définir la façon dont une application `f` de type `A"×"B"→"C` va s'appliquer à un couples d'éléments de type `B"×"A`. Cela se fait naturellement en replaçant les arguments d'appel de gauche à droite, dans les premières cases de gauche à droite ayant le type correspondant.

La troisième règle est l'unicité du type infini. C'est à dire qu'il n'y a qu'un seul type infini `E`, ou autrement dit, que pour tout type `A,B` dérivés de `E`, nous posons `A"="B`. Cela suppose que les ensembles infinis `A` en question soient tous énumérables et davantage encore qu'ils soient définis avec leur énumérateur nommé pareillement `A`, qui est une bijection de `NN"→"A`. Cela suppose que chaque type comprend un énumérateur, et que cet énumérateur doit se transporter à travers l'opération `"×"` de façon associative et symétrique. Pour cela on choisie une fois pour toute une bijection `varphi` de `NN"→"NN^2`. Et on peut alors définir l'énumérateur de `A"×"B` qui devra être le même que celui de `B"×"A`, et l'énumérateur de `A"×"(B"×"C)` qui devra être le même que celui de `(A"×"B)"×"C`. On se doit de définir la façon dont une application `f` de type `A"→"C` va s'appliquer à un élément de `B`, et comment une application `f` de type `B"→"C` va s'appliquer à un éléments de `A`. Dans le premier cas on calculera `f"∘"A"∘"B^-1`, et dans le second cas on calculera `f"∘"B"∘"A^-1`, et c'est le type des arguments qui décidera du comportement de l'application.

Pour l'instant nous ne retiendrons que la première règle.

3.2) L'exposant `"→"`

Par convention l'opération `"×"` est syntaxiquement prioritaire sur l'opération `"→"`, faisant que le type `A"×"B"→"C` signifie `(A"×"B)"→"C`, et que le type `A"→"B"×"C` signifie `A"→"(B"×"C")`.

Considérons l'ensemble des applications binaires `A"×"B"→"C``A,B,C` sont des types dérivés de `E` ? Quelle différence y-a-t-il entre une application binaire `f in A"×"B"→"C` et l'application unaire `g in A"→"(B"→"C)` telle que `g(x)(y)"="f(x,y)` ? On peut identifier ces deux applications c'est à dire les considérer comme étant égales. Car `g` définit `f` et réciproquement `f` définit `g`. La transformation d'une fonction à plusieurs arguments en une fonction à un argument qui retourne une fonction sur le reste des arguments, s'appelle la curryfication. L'opération inverse s'appelle la décurryfication. On se doit de définir la façon dont une application `f` de type `A"×"B"→"C` va s'appliquer à un élément de `A`, et comment une application `g` de type `A"→"(B"→"C)` va s'appliquer à un élément de `A"×"B`. Dans le premier cas on procédera d'abord à la curryfication de `f`, et dans le second cas on procédera d'abord à la décurryfication de `g`, et c'est le type des arguments qui décidera du comportement de l'application.

Par convention l'opération `"→"` s'évalue dans le sens inverse de lecture c'est à dire de droite à gauche, faisant que le type `A"→"B"→"C"→"D` correspond au type `A"→"(B"→"(C"→"D))` et donc par décurryfication correspond au type `A"×"B"×"C"→"D`.

Considérons l'ensemble des applications binaires `A"→"B"×"C``A,B,C` sont des types dérivés de `G` ? Quelle différence y-a-t-il entre une application unaire `f in A"→"B"×"C` et le couple d'applications unaires `(g,h) in (A"→"B)"×"(A"→"C)` telle que `(g(x),h(x))"="f(x)` ? On peut identifier ces deux objets c'est à dire les considérer comme étant égaux. Car `(g,h)` définit `f` et réciproquement `f` définit `(g,h)`. La transformation d'une fonction à `n` résultats en `n` fonctions à un résultat, transformant le type `A"→"B"×"C` en le type `(A"→"B)"×"(A"→"C)` s'appelle la distribution. L'opération inverse s'appelle la factorisation. On définit comment un couple d'applications `(g,h)` appartenant à `(A"→"B)"×"(A"→"C)` s'applique à un élément de `A`. L'application opère une duplication de l'argument pour produire le couple `(g(A),h(A))`.

Notez qu'en appliquant la distribution `f"="(g,h)`, l'opérateur `"→"` devient distributif sur l'opérateur `"×"`.

On remarque que le type `{0,1}"→"A` `A` est un type dérivé de `E`, est identique au type `A"×"A`, chaque telle application correspondant à un couple d'éléments de `A`. Et on remarque que le type `A"→"{0,1}` est identique au type `ccP(A)`, chaque telle application correspondant à un sous-ensemble de `A`.

3.3) La non-distinction entre prédicat et opérateur

La distinction entre prédicat et opérateur ne doit pas s'opèrer immédiatement. Dans la métaphore du Big-Bang, au départ, tout est indifférencié. Il en est de même dans notre raisonnement. On définit la valeur logique comme un élément. Le prédicat est alors un opérateur de `A"→"E`, où `A` est un type dérivé de `E`

On définit un langage de types plus général obtenu modulo l'associativité de l'opération `"×"`, modulo la curryfication-décurryfication, et modulo la distribution-factorisation, et dans lequel on exclut les types numériques

3.4) La forme série

Une forme normale est obtenue en appliquant à chaque fois que cela est possible la curryfication et la distribution. On élimine ainsi l'opérateur `"×"` ailleurs qu'à la racine. Ainsi aparait deux sortes de type, un type unaire qui n'utilise que l'opérateur binaire de type `"→"`, et un type `n`-aire qui est une liste de `n` types unaires. La forme normale unaire correspond au langage de types `"<"E, "→(.,.)>"` c'est à dire à l'ensemble des types obtenus par compositions closes de l'opérateur binaire `"→"`, et de `E`.

3.5) La forme liste

Une autre forme normale est obtenue en appliquant à chaque fois que cela est possible la décurryfication et la distribution. L'opérateur `"×"` peut encore se trouver à la racine mais pas seulement, on lui interdit d'être à la racine de l'argument de droite d'un opérateur `"→"`. Ainsi aparait deux sortes de type, un type unaire qui utilise les deux opérateur de type `"×", "→"` mais en ne plaçant jamais un `"×"` à droite d'un `"→"`, et un type `n`-aire qui est une liste de `n` types unaires.

3) Langage de type

Il n'est pas pertinant de démultiplier les types pour la même raison que la forme la plus simple parmis deux formes se contenant potentiellement mutuellement est la plus simple des deux. Ainsi une application de `A"→"B``A` et `B` sont des sous-ensemblee de `E` se ramène à une application de `E"→"E` en la complétant n'importe comment.

Puis, le procédé de currification fait qu'une application de `A"→"(B"→"C)` est équivalente à une application de `A"×"B"→"C`.

L'entier `n` désigne le cardinale de `E`, et le nombre `Q` désigne la quantité d'information du type `E` c'est à dire la quantité d'information nécessaire pour choisir un élément dans `E`.

`n=|E|`

`Q"="ln(n)/ln(2)`

La liste des types considérés commence alors comme suit. Dans l'avant dernière colonne se trouve l'ordre de la logique qui quantifie ces types. Dans la dernière colonne se trouve la quantité d'information que représente la détermination d'un élément du type en question, c'est le logarithme en base `2` du cardinale du type pour obtenir une quantité d'information en nombre de bits :

Type
Forme série
Type
Forme liste
Ordre logique
Quantité
d'information
d'un opérateur
1
`E`
`E`
1
`Q`
1
`E"→"E`
`E"→"E`
2
`nQ`
2
`(E"→"E)"→"E`
`(E"→"E)"→"E`
3
`n^nQ`
`E"→"(E"→"E)`
`E"×"E"→"E`
2
`n^2Q`
5
`((E"→"E)"→"E)"→"E`
`((E"→"E)"→"E)"→"E`
4
`n^(n^n)Q`
`(E"→"(E"→"E))"→"E`
`(E"×"E"→"E)"→"E`
3
`n^(n^2)Q`
`(E"→"E)"→"(E"→"E)`
`(E"→"E)"×"E"→"E`
3
`n^(n"+"1)Q`
`E"→"((E"→"E)"→"E)`
`E"×"(E"→"E)"→"E`
3
`n^(n"+"1)Q`
`E"→"(E"→"(E"→"E))`
`E"×"E"×"E"→"E`
2
`n^3Q`
14
`(((E"→"E)"→"E)"→"E)"→"E`
`(((E"→"E)"→"E)"→"E)"→"E`
5
`n^(n^(n^n))Q`
`((E"→"(E"→"E))"→"E)"→"E`
`(E"×"E"→"E)"×"E"→"E`
3
`n^(n^2+1)Q`
`((E"→"E)"→"(E"→"E))"→"E`
`((E"→"E)"×"E"→"E)"→"E`
4
`n^(n^n n)Q`
`(E"→"((E"→"E)"→"E))"→"E`
`E"×"((E"→"E)"→"E)"→"E`
4
`n^(n^n)nQ`
`(E"→"(E"→"(E"→"E)))"→"E`
`(E"×"E"×"E"→"E)"→"E`
3
`n^(n^3)Q`
`((E"→"E)"→"E)"→"(E"→"E)`
`((E"→"E)"→"E)"×"E"→"E`
4
`n^(n^n)nQ`
`(E"→"(E"→"E))"→"(E"→"E)`
`(E"×"E"→"E)"×"E"→"E`
3
`n^(n^2)nQ`
`(E"→"E)"→"((E"→"E)"→"E)`
`(E"→"E)"×"(E"→"E)"→"E`
3
`(n^n)^2Q`
`(E"→"E)"→"(E"→"(E"→"E))`
`(E"→"E)"×"E"×"E"→"E`
3
`(n^n)n^2Q`
`E"→"(((E"→"E)"→"E)"→"E)`
`E"×"((E"→"E)"→"E)"→"E`
4
`n^(n^n)nQ`
`E"→"((E"→"(E"→"E))"→"E)`
`E"×"(E"×"E"→"E)"→"E`
3
`n^(n^2)nQ`
`E"→"((E"→"E)"→"(E"→"E))`
`E"×"(E"→"E)"×"E"→"E`
3
`(n^n)n^2Q`
`E"→"(E"→"((E"→"E)"→"E))`
`E"×"E"×"(E"→"E)"→"E`
3
`(n^n)n^2Q`
`E"→"(E"→"(E"→"(E"→"E)))`
`E"×"E"×"E"×"E"→"E`
2
`n^4Q`
...
...
...
...

`c_0"="1,c_1"="1,c_2"="2,c_3"="5,c_4"="14,c_5"="42,c_6"="132,...` sont les nombres de Catalan. `c_n` est le nombre d'arbres binaires nus à `n"+"1` feuilles.

4) Langage logique

Le langage logique peut désigner des variables de tous les types dérivés de l'ensemble sous-jacent tels que décrits précédement, mais sous seulement trois forment possibles :

  1. Soit génératrice c'est à dire faisant partie de la présentation de la structure,
  2. Soit quantifié existentiellement,
  3. Soit quantifié universellement.

Dés lors, il n'y a pas de distinction entre prédicats et opérateurs. On parlera indistinctement de variable ou d'expression typées, celles-ci pouvant posséder une valeur élémentaire, fonctionnelle, ou logique selon sont type.

Le langage logique se décrit en 3 niveaux de complexité :

  1. Au premier niveau, les expressions sont les compositions closes des variables génératrices ou quantifiés existanciellement ou universellement auxquelles on ajoute les connecteurs logiques.
  2. Au second niveau, les expressions incluent les programmes informatique d'arrêt sûr.
  3. Au troisième niveau, les expressions incluent les programmes informatique dont l'arrêt n'est pas sûr.

4.1) Langage logique du premier ordre

Si on se restreint à n'utiliser que des variables de type élémentaire et des opérateurs générateurs de type `E^n"→"E` et des prédicats générateurs de type `E^n"→"{0,1}`, alors on constate que le langage restreint au deux premier niveau, c'est à dire sans utiliser l'expression de programmes informatiques, mais seulement la composition close de variables, suffit pour définir une sémantique où vérité sémantique coïncide avec vérité syntaxique.

La coïncidence entre vérité sémantique et vérité syntaxique, signifie que pour toutes propositions `P` exprimables dans le langage en question, le fait que `P` soit vrai dans tous les mondes de l'univers sémantique est équivalente au fait qu'il existe une démonstration de `P` dans le langage en question.

5) Groupe

Un groupe `G` est un ensemble muni d'une loi de composition notée par simple juxtaposition, d'un élément neutre noté `1`, d'un opérateur d'inversion noté par l'exposant `"-"1`, satisfaisant les règles suivantes :

`AA (x,y,z) "∈" G^3, `

`(xy)z= x(yz)`
`x1=1x=x`
`x x^("-"1)=x^("-"1)x=1`

C'est ainsi que l'on décrit la théorie du groupe en notation multiplicative.

Mais pour rendre cette définition incontestable et afin qu'elle soit perçue de la même façon par tous, il convient de formaliser davantage, en procédant à une construction rigoureuse du langage logique utilisé et en y décrivant sa sémantique sous forme d'ensemble de mondes possibles.

Afin de pouvoir désigner facilement la loi de composition qui est un opérateur binaire, et l'opérateur d'inversion qui est un opérateur unaire, on leur donne un nom. Le symbole `"∗"` désignera la loi de composition, et le symbole `frI` désignera l'opérateur d'inversion, faisant que `x"∗"y"="xy` et `frI(x)"="x^("-"1)`, de même pour l'élément neutre, on lui a donné un nom, `1`.

6) Structure et langage

Une structure `G` possède un ensemble sous-jacent de même nom `G` et des opérateurs et prédicats définis dans l'ensemble sous-jacent `G`. Cela signifie que les opérateurs zéro-aires appelés éléments appartiennent à `G`, que les opérateurs unaires appartiennent à `G"→"G`, que les prédicats unaires appartiennent à `G"→"{0,1}`, que les opérateurs binaires appatiennent à `(G"×"G)"→"G`, etc... Et les différents types possibles que peuvent prendrent les opérateurs et prédicats de la présentation de la structure sont les types dérivés de `G`.

Remarquez que les prédicats zéro-aires sont de type `{0,1}` et correspondent à des paramètres booléens.

Ces opérateurs et prédicats sont nommés pour former un langage, et sont regroupés dans la présentation de la structure. Par défaut, les opérateurs seront notés en minuscule et les prédicats seront notés en majuscule. La présentation de la structure va engendrer son langage. Puis la structure possède une théorie écrite dans ce langage.

Cette dichotomie entre le langage et la théorie de la structure est essentielle pour comprendre la subjectivité de la structure. Elle précise ce que connait la structure et ce qu'elle ne connait pas tout en y étant soumis. Ainsi, la structure `"<>/"{EEa}` de langage vide et de théorie précisant l'existance d'un élément, se distingue de la structure `"<"a">/"{}` de langage désignant l'élément `a` et de théorie vide. La première sait qu'elle n'est pas vide mais ne connait aucun élément, la seconde connait un élément.

Dans la structure, l'interprétation du langage est posée comme étant interne à la structure, c'est à dire que les quantifications universelles et existentielles sont interprétées comme ayant une portée limitée à l'ensemble sous-jacent `G` ou à un de ses types dérivés.

La structure est vue de l'intérieur. Aucun élément en dehors de la structure n'est exprimable dans le langage de la structure, et en particulier son ensemble sous-jacent qui peut s'apparenter à un prédicat unaire, ne fait pas partie du langage de la structure.

On se place donc dans la structure `G`. Délors :

Ces prédispositions par défauts sont importantes. Elle donne au contexte un rôle majeur permettant de ne pas noyer l'important dans les détails, incarne une intuition qu'est le concept de structure en définissant un langage logique restreint à son ensemble sous-jacent.

On recourt à la prosopopée. On se place dans la structure `G`, ou plus exactement à la place de la structure `G`, et on adopte son point de vue sur elle-même, le point de vue qu'elle peut avoir d'elle-même.

Dans la structure `G` :

Le langage peut désigner ainsi tous les types dérivés de l'ensemble sous-jacent, mais en quantifiant existentiellement ou universellement chaque nouvelle variable ainsi créée.

Lorsque l'ensemble sous-jacent `G` est fini, la quantification se définit de façon exacte comme suit :

`( AAx"∈"G, P(x) )   <=>  ^^^_(x in G) P(x)`

`( EEx"∈"G, P(x) )  <=>  vvv_(x in G) P(x)`

Le symbole `^^^` est un itérateur de conjonction, il déclare une variable locale et il effectue une conjonction de ce qui suit en faisant varier la variable locale sur tout son domaine de définition. Ainsi par exemple si `G"="{1,2,3}`, nous avons :

`^^^_(x in G) P(x)   <=>   P(1) "et" P(2) "et" P(3)`

Et de même avec le symbole `vvv` qui est un itérateur de disjonction :

`vvv_(x in G) P(x)   <=>   P(1) "ou" P(2) "ou" P(3)`

Puis, lorsque l'ensemble sous-jacent `G` est un infini énumérable, la quantification se définit de façon exacte comme suit :

`AAx"∈"G, P(x) `
`<=>`
 La procédure qui énumère `G` et qui s'arrète lorsqu'elle rencontre un élément satisfaisant `P`, ne s'arrète jamais.
`EEx"∈"G, P(x)`
`<=>`
 La procédure qui énumère `G` et qui s'arrète lorsqu'elle rencontre un élément satisfaisant `P`, est d'arrêt sûr.

Ainsi on définit un langage logique propre à la structure, restreint à son ensemble sous-jacent, utilisant les opérateurs et prédicats de sa présentation, et utilisant de nouveaux opérateurs et prédicats quantifiés universellement ou existentiellement, de type égale à l'ensemble sous-jacent ou à un de ses types dérivés.

Toute proposition écrite dans ce langage aura une signification spécifique dans chaque structure possédant ce même langage. Et d'une manière plus générale, sous le patronage d'un traducteur qui est une application envoyant les opérateurs et prédicats d'un langage vers ceux de même type d'un autre langage pouvant être plus ou moins vaste, toute proposition écrite dans le premier langage aura une signification spécifique dans le second langage.

Le langage d'une structure peut se noter en présentant une liste d'opérateurs et de prédicats non instanciés. Par exemple le langage de la structure de groupe est posé être `("∗",1,frI)`. Par défaut les opérateurs sont notés en minuscule et les prédicats en majuscule, mais il peut y avoir des exceptions par exemple ici avec `frI` qui est un opérateur unaire, et on précise parfois leur type de deux façons, soit par un suffixe indiquant l'arité pour les types simples ; absence de suffixe pour l'arité nulle, suffixe `"(.)"` pour unaires, suffixe `"(.,.)"` pour binaires, suffixe `"(.,.,.)"` pour ternaire, etc.., ou soit par un exposant indiquant explicitement le type.

Puis on adopte une convention d'écriture : Les variables génératrices, que sont les opérateurs et prédicats de la présentation de la structure, sont placés entre chevrons `"<...>"` définissant un langage, et le tout est divisé par la théorie que l'on met parfois entre accolade `{...}` représentant une conjonction. Ainsi la théorie du groupe précédente se note comme suit :

`G =("<∗",1,frI">")/(AAxAAyAAz, (x"∗"y)"∗"z"="x"∗"(y"∗"z), x"∗"1"="1"∗"x"="x, x"∗" frI(x)"="frI(x)"∗"x"="1)`

Et avec les conventions d'écriture du produit `"∗"` par absence de symbole, et de l'inverse `frI` par l'exposant `"-"1`, cela se note :

`G =("<∗",1,frI">")/(AAxAAyAAz, (xy)z"="x(yz), x1"="1x"="x, x x^("-"1)"="x^("-"1)x"="1)`

Vous aurez remarqué que la structure `G` ne mentionne aucun prédicat générateur. Par défaut il y en a au moins un, c'est le prédicat spéciale d'égalité. Le prédicat d'égalité `"="` joue en effet un rôle tout à fait particulier, c'est pourquoi on ne le mentionne pas et on laisse le soin au contexte le cas échant de préciser si le langage considéré est dépourvu du prédicat d'égalité.

6.1) Structure vue de l'extérieur

Sans changer la nature du langage et des structures, il s'avère trés simple de compléter le langage d'une structure afin que celle-ci soit vue de l'exterieur. Pour cela on ajoute à son langage, le prédicats unaire correspondant à son ensemble sous-jacent, et on modifie sa théorie en conséquence. Considérons par exemple la structure `S` :

`S = ("<"a,f"(.)",g"(.,.)", U, V"(.)>")/{AAxEEyAAz, P(x,y,z)}`

où la fonction propositionnelle `P"(.,.,.)"` est écrite dans le langage `"<"a,f"(.)",g"(.,.)", U, V"(.)>"`. Il existe une autre convention d'écriture pour les structures du premier ordre, que l'on justifiera plus-tard, où les opérateurs générateurs sont placés entre chevrons `"<...>"` et les prédicats générateurs sont placés juste après entre accolade `{...}`, et le tout est divisé par la théorie entre accolade `{...}`. Ainsi la structure `S` se note :

`S = ("<"a,f"(.)",g"(.,.)>"{U,V"(.)"})/{AAxEEyAAz, P(x,y,z)}`

La structure `S` peut être étendue en la structure `S_"ext"` en lui adjoingnant un prédicat unaire `S"(.)"` représentant l'ensemble sous-jacent de la structure `S`, et en restreignant sa théorie aux seuls éléments de `S`, ceci afin d'être vue de l'extérieur :

`S_"ext" = ("<"a,f"(.)",g"(.,.)>"{S"(.)",U,V"(.)"})/{AAxEEyAAz, S(x) "et" S(y) "et" S(z) "⇒" P(x,y,z)}`

Remarquez les priorités syntaxiques : Les quantificateurs `AA, EE` ont une portée syntaxique maximale, faisant que `AAx, A(x)"⇒"B(x)` signfifie `AAx, (A(x)"⇒"B(x))` et non `(AAx, A(x))"⇒"B(x)`. Et l'implication (comme l'égalité) a une priorité syntaxique plus faible que les autres connecteurs, faisant que `R "et" S "⇒" T` signfifie `(R "et" S) "⇒" T` et non `R "et" (S "⇒" T)`.

L'ensemble sous-jacent de `S_"ext"` est alors plus vaste et contient `S`, mais comme aucune information n'est donnés sur les éventuels éléments extérieurs à `S`, Il n'y a pas vraiment de différence entre les structures `S` et `S_"ext"`. La seul différence tient dans le langage plus riche que propose `S_"ext"` et qui permet de conjecturer sur l'existence d'élément extérieur à `S`.

6.2) Fonction propositionnelle définissant une structure

La structure stricto sensu ne nomme pas les opérateurs et prédicats de son langage ni son ensemble sous-jacent en vue de dialoguer avec autrui, elle les différencie seulement pour elle-même. En effet, le nommage extérieur a pour but de dialoguer avec l'extérieur. La structure se résume en une théorie, définie à l'aide d'un patron sous forme d'une fonction propositionnelle. Et c'est l'appel de cette fonction propositionnelle qui va nommer pour l'extérieur tous ces opérateurs et prédicats dits générateurs.

Par exemple le patron de la structure de groupe, noté `"Groupe"`, est une fonction propositionnelle définie comme suit :

`"Groupe"(G,"∗",1,frI) <=> ( ( AA(x,y,z)"∈"G^3"," (x"∗"y)"∗"z"="x"∗"(y"∗"z) ),( AAx"∈"G"," x"∗"1"="x ),( AAx"∈"G"," 1"∗"x"="x ),( AAx"∈"G"," x"∗"frI(x)"="1 ),( AAx"∈"G"," frI(x)"∗"x"="1 ) )`

Le patron `"Groupe"` a 4 arguments qui sont listés dans cet ordre :

  1. L'ensemble sous-jacent `G` et que l'on place conventionelement en premier argument .
  2. L'opérateur de produit `"∗"` défini sur cet ensemble.
  3. L'élément neutre `1` appartenant à cet ensemble.
  4. L'opérateur d'inversion `frI` défini sur cet ensemble.

L'expression « Etant donné un groupe `(G,"∗",1,frI)` » aura la même signification que la proposition formelle `"Groupe"(G,"∗",1,frI)`. Lorsque les opérateurs et prédicats ou ensemble sous-jacent sont instanciés, la théorie évoquée s'enrichit alors des définitions des pièces rapportées.

Cette définition du groupe sous forme de fonction propositionnelle, définit un langage logique, le langage de la structure, sans donner de nom à l'ensemble sous-jacent et aux opérateurs et prédicats puisque identifiés par leur place occupée dans la liste des arguments. Vous comprendrez que ce n'est pas trés pratique, aussi nous demanderons au contexte de les nommer, et cela se fait en appliquant le patron sur des symboles non instanciés une première fois mais à titre de modèle. Cela mentionne explicitement l'ensemble sous-jacent `G` et le langage de la structure de groupe qui servira de modèle `("∗",1,frI)` commun à toutes les groupes. Voyez ici que l'on utilise le terme de modèle pour autre chose que celui de monde. Le symbole `G` désigne l'ensemble sous-jacent, c'est ce sur quoi porte les quantificateurs `AA` et `EE` du langage de la structure.

On adopte une nouvelle notation, `E¦` pour désigner une restriction à un ensemble sous-jacent désigné par un prédicat unaire `E`. Ainsi par exemples les deux expressions suivantes sont équivalentes :

`A¦AAxEEy B¦AAzEEt, P(x,y,z,t)`

`AAx"∈"A, EEy"∈"A, AAz"∈"A"⋂"B, EEt"∈"A"⋂"B, P(x,y,z,t)`

Une proposition écrite dans un langage signifie qu'il appartient à ce langage, et donc on pourra préciser le langage en le mettant en exposant, tel un type. L'ensemble sous-jacent est ce sur quoi porte les quantifications par défaut, on pourra le préciser grace au symbole `"¦"`. La définition du groupe devient :

`"Groupe"(G,"∗",1,frI)<=>G"¦" ( ( AAxAAyAAz"," (x"∗"y)"∗"z"="x"∗"(y"∗"z) ),( AAx"," x"∗"1"="x ),( AAx"," 1"∗"x"="x ),( AAx"," x"∗"frI(x)"="1 ),( AAx"," frI(x)"∗"x"="1 ) )^("(∗",1,frI")")`

Ainsi nous avons défini un langage logique spécifique `("∗(.,.)",1,frI"(.)")` propre à tous les groupes, et une restriction à un ensemble sous-jacent `G` mentionné par le préfixe propositionnelle `G¦`.

On remarque que le langage peut être plus grand que celui utilisé par la proposition mais pas l'inverse. On remarque que l'expression d'une proposition logique avec son type qui est un langage constitue une structure qui nomme son langage.

Si nous définissons plusieurs structures de même langage, c'est à dire utilisant les mêmes symboles d'opérateur et de prédicat, telles que les groupes `(G,"∗",1,frI)` et `(H,"∗",1,frI)` où seul change le nom du groupe qui est identique au nom de son ensemble sous-jacent, alors on pourra spécifier les opérateurs à l'aide d'un indice pour savoir à quelle groupe ils font référence : `"∗"_G`, `1_G`, `frI_G`, `"∗"_H`, `1_H`, `frI_H`.

Notez que la variable `G` peut-être vu comme un ensemble, ou plus que cela, comme une structure que le contexte lui attribue, ici, une structure de groupe. Le groupe `G` détermine son ensemble sous-jacent, sa loi de composition interne `"∗"_G` son élément neutre `1_G` et sa loi d'inversion `frI_G`, mais l'ensemble `G` ne détermine aucune loi ni élément, il ne détermine que lui-même c'est à dire l'ensemble sous-jacent. L'égalité `G"="H` peut désigner une égalité d'ensemble ou bien une égalité de groupe, et c'est au contexte de le préciser. Il se peut que `G"="H` en tant qu'ensemble, et que `G"≠"H` en tant que groupe.

6.3) Le domaine de Herbrand

Toute structure du premier ordre comprend une partie calculable, qui est l'ensemble des éléments correspondant à des compositions closes d'opérateurs appartenant à la présentation de son langage. C'est le domaine de Herbrand. Puis la structure comprend une partie définissable plus vaste. La partie calculable représente ce que connait la structure, ce qu'elle est capable de construire. Tandis que la partie seulement définissable, qui apparaît lorsqu'il y a des quantificateurs existentiels dans la théorie sous forme prénexe, est plus difficile à circonscrire.

La structure est dite universelle si sa théorie sous forme prénexe ne comprend pas de quantificateur existentiel.

Le concept d'élément constructible ou calculable par la structure se définit facilement pour les structures du premier ordre c'est à dire ne comprennant que des opérateurs de type dérivé de la forme `E` ou `E^n"→"E` avec `n "∈" NN` et ne quantifiant que des variables élémentaires appartenant à `E`. C'est l'ensembles des éléments désignés par les termes clos du langage. C'est le domaine de Herbrand.

La partie calculable est susceptibles de constituer une infinité énumérable d'éléments distincts. Le procédé de construction de cette partie met en oeuvre la récursivité générale, qui, en retours, en donne une définiton complète. D'où l'adage « La récurcivité est consubstantielle à la notion de structure ».

Néanmoins il manque la partie définissable non calculable qui peut ne pas être vide, lorsque la théorie sous forme prénexe contient des quantificateurs existentiels. Par exemple considérons la structure de langage `"<∗(.,.)>"` et de théorie `{EEa, a"∗"a"="a}`. Cet structure ne contient aucun élément calculable puisque son langage d'opérateur est `"<∗>"`. Néanmoins il existe un élément `a` qui est évoqué par sa théorie. Dans ce cas `a` est un élément non calculable mais définissable. On verra dans quelle mesure par le procédé de skolémization et le nommages de nouveaux opérateurs et prédicats, on peut étendre le langage de la structure afin que tous les éléments définissables y soient calculables.

On généralise l'opérateur de Kleene (sans le mot vide) `""^"+"` en l'opérateur de clôture `"°"` qui calcule l'ensemble des compositions closes d'opérateurs, appelé le domaine de Herbrand. Et on le note aussi en regroupant entre crochet `"<"...">"` les opérateurs ou ensembles d'opérateurs que l'on veut clôturer. Ainsi par exemple :

`L = {a,b, f"(.)",g"(.,.)"}`

`L"°"= "<"L">" = "<"a,b, f,g">" = {a, b, f(a), f(b), g(a,a),g(a,b), f(f(a)), g(a,f(a)),....}`

Considérons à titre d'exemple la structure de groupe, présentée comme une structure universelle de langage `("∗",1,frI)`, auquel on ajoute par exemple deux symboles d'éléments `a, b`. Le groupe va engendrer tous les éléments calculables de la structure libre du langage grace à sa théorie d'engendrement, qui est une mise en pratique de la récurcivité générale, et qui n'est pas une théorie du premier ordre. Puis la théorie du premier ordre du groupe va quotienter la structure libre ainsi construite, pour produire les éléments calculables du groupe. La théorie du groupe `("∗",1,frI,a,b)` étant universelle c'est à dire ne contenant pas de quantificateur existentiel dans sa forme prénexe, le groupe restreint à ses seuls éléments calculables constitue encore un groupe qui est appelé le groupe engendré, ou dit minimal.

Ainsi une structure universelle possède deux théories, et donc trois théories :

  1. La théorie d'engendrement de la structure universelle, qui n'est pas du premier ordre, et qui affirme que l'ensemble des éléments calculables est engendré par les opérateurs générateurs, et que la structure universelle considérée se restreint à ces seuls éléments.
  2. La théorie du premier ordre de la structure universelle
  3. La conjonction des deux théories et qui constitue la structure universelle engendrée (ou dite minimale).

Considérons par exemple le groupe bigène libre :

`G="Groupe"("∗",1,frI,a,b)`

Le premier argument du patron `"Groupe"` est sa loi de composition interne `"∗"`, le second argument est l'élément neutre `1`, le troisième argument est l'opérateur d'inversion `frI`, et les arguments suivants sont des éléments générateurs `a,b`. Dans cet exemple il y a que deux éléments générateurs. Les éléments de la structure sont construits à partir des opérateurs de la présentation. Puis, à charge de ces affectations effectuées par l'appel, le patron `"Groupe"` transporte la théorie du groupe suivante :

`AAxAAyAAz, (x"∗"y"∗")z"="x"∗"(y"∗"z)`
`AAx, x"∗"1"="x`
`AAx, 1"∗"x"="x`
`AAx, xfrI(x)"="1`
`AAx, frI(x)x"="1`

Les éléments du groupe sont les classes d'équivalences de la relation d'équivalence définie comme suit : `x` et `y` étant deux termes quelconques appartenant à la structure libre `"<∗",1,frI,a,b">"`, ils sont équivalents si et seulement si la théorie du groupe le démontre, ce qui se note, `G|--x"="y`.

De même que précédement, il existe un langage du groupe, commun à tous les groupes. Une distinction doit donc s'opérer entre le langage du groupe `"<∗", 1, frI">"` qui est le même pour tous les groupes et qui est celui du modèle, et la définition du groupe qui instancie les opérateurs et prédicats du modèle. C'est pourquoi si nous définissons plusieurs groupes, en utilisant les même symboles d'opérateurs que ceux du modèle, `G"=Groupe"("∗",1,frI,a,b)` et `H"=Groupe"("∗",1,frI,a,b)`, on enrichit la notation en spécifiant ces opérateurs à l'aide d'un indice pour savoir à quelle groupe ils font référence : `"∗"_G`, `1_G`, `frI_G`, `a_G`, `b_G`, `"∗"_H`, `1_H`, `frI_H`, `a_H`, `b_H`.

La notion de structure engendrée peut s'appliquer à des structures non universelles, c'est à dire contenant des quantificateurs existentiels dans leur théorie sous forme prénexe, mais cela ajoute alors une propriété dans la théorie d'engendrement qui n'est pas du premier ordre et qui affirme que tous les éléments sont calculables, c'est à dire appartiennent au domaine de Herbrand, c'est à dire sont désignés par des termes clos du langage de la structure. Autrement dit, la structure sera dite engendrée s'il est ajouté dans sa théorie d'engendrement cette propriété du second ordre qui affirme que l'ensemble sous-jacent se limite au domaine de Herbrand.

7) Calculabilité et définissabilité

Le langage d'une structure désigne tout ce que peut dire une structure, et limite donc tout ce qu'elle peut démontrer par elle-même, c'est à dire ce qu'elle peut savoir par elle-même, ou dit autrement, ce qu'elle peut calculer ou définir par elle-même. Cela introduit les notions de calculabilité et de définissabilité, deux notions relatives au langage de la structure et à sa théorie.

Un élément est dit calculable par la structure si et seulement si il est désigné par un terme clos du langage de la structure c'est à dire, au premier ordre, une composition close d'opérateurs appartenant à la présentation de la structure, autrement dit s'il appartient au domaine de Herbrand.

Un élément est dit définissable par la structure si et seulement si il existe une démonstration, faite à partir de la théorie de la structure et avec le langage de la structure, de l'existence de cet élément, et il est dit définissable de façon unique, si de plus, la théorie peut démontrer son unicité. Notez qu'un tel élément peut appartenir au domaine de Herbrand tant que la théorie n'a pas démontré le contraire, et de même deux éléments `x` et `y` d'expression distincte peuvent être égaux tant que la théorie n'a pas démontré le contraire.

Dans l'exemple d'un groupe `G`, ne possèdant que la théorie du groupe et aucune autre information, on remarquera qu'aucun élément autre que l'élément neutre (c'est à dire assurement distinct de lui) n'est calculable ni définissable par le groupe `G` lui-même. Cela est facile à démontrer puisque le groupe trivial `{1}` est un exemple de groupe constituant un monde et qui ne contient que cet élément.

8) Monde

Un monde fini est une structure dont l'ensemble sous-jacent est de cardinalité fini, où tous les éléments sont calculables et où la théorie est complète.

Un monde `G` est un groupe s'il possède le langage `("∗(.,.)",1,frI"(.)")` et s'il vérifie la théorie du groupe. Et toutes les propositions écrites dans le langage `("∗(.,.)",1,frI"(.)")` qui est le langage commun à tous les groupes, auront une signification spécifique dans `G`. Par exemple considérons la proposition `P` suivante :

`P = ( AAxEEy, x"="y"∗"y )^("("E, "∗(.,.)",1,frI"(.))")`

Cette proposition signifie que tous les éléments sont des carrés.

Lorsque la proposition `P` est vrai dans la structure `G`, nous dirons que `P` se réalise dans `G` ou que `G` satisfait `P`, et nous noterons :

`G"⊨"P`

Ce symbole `"⊨"` désigne une implication sémantique. Et on l'étend aux propositions écrites dans un même langage logique. Il signifie que tous les mondes qui satisfont `G` satisfont `P`. Et on l'étend également aux ensembles de mondes. Il correspond alors simplement à une inclusion entre ensembles de mondes. (Dans le cas fini, la sémantique d'une proposition correspond à l'ensemble des mondes finis la satisfaisant.)

L'implication syntaxique, quant-à elle, est plus compliqué à définir. C'est le lien de démontrabilité par les règles du système de déduction choisie et qui se note :

`G"⊢"P`

Les symboles `"⊨"` et `"⊢"` ne font pas partie du langage logique. C'est en cela qu'ils diffèrent du symbole d'implication `"⇒"` qui, lui, fait partie du langage logique.

Si le premier terme est omis, alors il est remplaçé par la tautologie, ou bien sur le plan sémantique par l'ensemble de tous les mondes. Ainsi l'expression `"⊨"P` signifie que `P` est valide, c'est à dire vrai dans tous les mondes. L'expression `"⊭"P` signifie que que `"¬"P` est saisfaisable, c'est à dire qu'il existe au moins un monde où `P` est faux. L'expression `"⊭¬"P` signifie que `P` est saisfaisable, c'est à dire qu'il existe au moins un monde où `P` est vrai. Tandis que l'expression `"⊢"P` signifie que `P` est une tautologie, c'est à dire démontrable sans hypothèse. L'expression `"⊢¬"P` signifie que `P` est une antilogie. L'expression `("⊬"P) "et" ("⊬¬"P)` signifie que `P` sans autre hypothèse est indécidable. L'expression `("⊭"P) "et" ("⊭¬"P)` signifie que `P` est satisfaisable et que `"¬"P` est satisfaisable, c'est à dire qu'il existe au moins un monde où `P` est vrai et qu'il existe au moins un monde où `P` est faux.

9) Langage du n-ième ordre

Au premier ordre, seuls les éléments peuvent être quantifiés `EE` ou `AA`. Au second ordre, les opérateurs et prédicats s'appliquant à des éléments peuvent à leur tour être quantifiés. Au troisième ordre, les opérateurs et prédicats s'appliquant à des opérateurs et prédicats s'appliquant à des éléments, peuvent à leur tour être quantifiés, etc.. La notion d'ordre correspond à l'ordre des cardinalités des types dérivés : en `n` au premier ordre, en `n^n` au second ordre, en `n^(n^n)` au troisième ordre, etc..

Chaque opérateur et prédicat possède un type dérivé de l'ensemble sous-jacent. Conventionnellement on ajoute parfois en exposant leur type explicite comme suit :

Dans une proposition, tous les opérateurs et prédicats y apparaissant doivent être quantifiés, soit préalablement en faisant parti d'un langage d'une structure, soit implicitement selon le contexte, ou soit explicitement dans la proposition. Sinon nous obtenons une fonction propositionnelle, et qui doit alors être déclarée comme telle par un prototype.

Conventionnellement, l'introduction de nouveaux opérateurs ou prédicats dans une proposition, sans qu'ils n'aient été préalablement déclarés, sont par défaut quantifiés universellement sur l'ensemble auquel se restreint le langage logique, et possède un type dérivé déterminé par la forme syntaxique utilisée, selon un mécanisme d'inférence de type. Cela s'applique aussi aux propositions décrites littéralement. Ainsi par exemples, après avoir défini l'opérateur d'inversion `x"↦"x^("-"1)`, si nous disons :

« Étant donné la fonction `f`, nous avons `f(f(x))"="x^("-"1)` »

Cela signifie : `AAx,f(f(x))"="x^("-"1)`. Et de même, si nous disons :

« Étant donné un élément `a` nous avons `f(A)"⊆"A => (a"∈"A "ou" a^("-"1)"∈"A)` »

Cela signifie : `AA A "(.)", f(A)"⊆"A => (a"∈"A "ou" a^("-"1)"∈"A)`. Et par ailleurs, si nous disons :

« On définit la proposition `P(f)"="( AAxEEy,x"="f(f(y)) )` »

Le type de `f` est déterminé comme s'appliquant à un élément et retournant un élément. L'inférence de type dans cette expression assigne donc à `f` le type `E"→"E`. La proposition `P(f)` définie alors un prototype de fonction propositionnelle de type `(E"→"E)"→"{0,1}` autrement dit `P` est une application qui prend en entrée une application dans `E` et retourne un booléen.

Dans le cas infini, la sémantique des opérateurs et prédicats s'avèrent incomplète. Mais dans le cas fini qui nous intéresse ici, la sémantique est bien définie. Elle est fini et fait partie de la combinatoire, le nombre d'applications de `A"→"B` étant égale à :

`|A"→"B|=|B|^|A|`

Nous pouvons calculer le cardinal de tous ces types d'opérateurs et prédicats. Par exemple, le nombre d'opérateurs de type `((E"→"E)"→"E)->(E"→"E)` est :

`|((E"→"E)"→"E)->(E"→"E)| = (|E|^|E|)^(|E|^(|E|^|E|))`

10) La négation

Le langage logique permet facilement d'exprimer la négation d'une proposition, par un procédé récurcif, en inversant les quantificateurs `AA`, `EE` dans l'entête puis en négativant la fonction propositionnelle sur laquelle ils portent, ou bien en inversant les deux symboles `"et"`, `"ou"` et en négativant leurs arguments, ou bien en inversant les deux symboles `"⇔"`, `"⊕"` et en laissant inchangés leurs arguments, ou bien en remplaçant l'expressions de la forme `A"⇒"B` directement par `A "et" "¬"B`. Cela se définit formellement dans le langage logique utilisant les connecteurs booléens `¬`, `"et"`, `"ou"`, `"⇒"`, `"⇔"`, `"⊕"`, à l'aide de ces 8 règles de substitutions :

`"¬"(AA alpha, beta(alpha))`
=
`EE alpha, "¬"beta(alpha)`
`"¬"(EE alpha, beta(alpha))`
=
`AA alpha, "¬"beta(alpha)`
`"¬"(A "et" B)`
=
`"¬"A "ou" "¬"B`
`"¬"(A "ou" B)`
=
`"¬"A "et" "¬"B`
`"¬"(A"⇔"B)`
=
`A"⊕"B`
`"¬"(A"⊕"B)`
=
`A"⇔"B`
`"¬"(A"⇒"B)`
=
`A "et" "¬"B`
`"¬¬"A`
=
`A`

Par exemple, considérons la proposition suivante :

`P(R) = ( EEh"(.)"AAx, R(x,h(x)) => x"≠"h(x) )`

Cette proposition signifie littéralement qu'il existe une application `h` telle qu'à chaque fois que `x` est en `R`-relation avec son image `h(x)`, alors il est différent de son image `x"≠"h(x)`. La négation s'obtient ainsi :

`"¬"P(R) = "¬"( EEh"(.)" AAx, R(x,h(x)) => x"≠"h(x) )`
`"¬"P(R) =     AAh"(.)" EEx, R(x,h(x)) "et" x"="h(x) `

Un monde fini est représenté par une structure, d'ensemble sous-jacent fini, où tous les éléments sont calculables, et dont la théorie est complète. Néanmoins il est possible de concevoir des mondes finis où les éléments ne sont pas calculables, en les enlevant du langage de la structure et en ajoutant l'affirmation de leur existence en nombre limité dans la théorie. La structure finie peut toujours être rendu calculable en augmentant son langage et en particulier en ajoutant tous ses éléments dans son langage. Ainsi, l'implication sémantique appliqué à des structures finies n'est pas influencée par l'état de connaissance des structures sur elle-même. Donc pour toute proposition `P` écrite dans le langage d'un monde fini `M`, nous avons toujours `M"⊨"P` ou bien `M"⊨¬"P`. C'est à dire que la négation de l'expression `M"⊨"P` que l'on note `M"⊭"P` signifie exactement `M"⊨¬"P`.

11) Equivalence de Skolem et de Herbrand

Pour interpréter correctement ce que signifie une succession de quantifications telle que `AAxEEyAAzEEt`, il convient d'étudier l'équivalence de Skolem ainsi que sa contraposée, l'équivalence de Herbrand.

Lorsque l'ensemble sous-jacent est fini, ces équivalences sont valides. Par exemple, étant donné une fonction propositionnelle `P"(.,.)"`, nous avons l'équivalence de Skolem :

   `AAx EEy, P(x,y)`  
`<=>`
  `EEy"(.)"AAx, P(x,(y(x))`   

Et sa contraposé qui est l'équivalence de Herbrand :

   `EEx AAy, P(x,y)`  
`<=>`
  `AAy"(.)"EEx, P(x,y(x))`   

Cela est valable pour tout type d'opérateur ou prédicat. Considérons un élément `x` de type `X`, un élément `y` de type `Y`, et une fonction propositionnelle `P"(.,.)"` de type `X"→"Y"→"{0,1}`. L'équivalence de Skolem s'écrit comme suit :

   `AAx^X EEy^Y, P(x,y)`  
`<=>`
  `EEy^(E"→"Y)AAx^X, P(x,y(x))`   

Et sa contraposé est l'équivalence de Herbrand :

   `EEx^X AAy^Y, P(x,y)`  
`<=>`
  `AAy^(E"→"Y)EEx^X, P(x,y(x))`   

10.1) Skolémization

Lorsque l'ensemble sous-jacent est fini, toute théorie admet une expression skolémizée où tous les qantificateurs existentiels sont placée en premier. Cette expression explicite toutes les dépendances qu'ils peut y avoir entre les variables évoquées dans la théorie.

12) Différentes théories de groupe

Nous devons revenir sur la définition du groupe car il y a plusieurs façons de définir la théorie du groupe, soit par une théorie du premier ordre, soit par une théorie du second ordre, ou soit par une théorie universelle du premier ordre dans un langage augmenté, et nous verrons plus tard encore d'autre façons de définir un groupe. Toutes ces façons sont équivalentes dans le cas fini, mais plus dans le cas infini.

12.1) Définition du premier ordre

On définit une structure de groupe, en notation multiplicative, comme suit. On présente un ensemble-sous jacent `G`. On le muni d'une loi de composition interne `"∗(.,.)"`, qui admet un élément neutre et qui admet pour chaque élément un inverse. Autrement dit on munit `G` d'une application de `G"×"G"→"G`, que l'on nomme `"∗"`, et qui doit satisfaire la théorie du groupe suivante :

`AAxAAyAAz, (x"∗"y"∗")z"="x"∗"(y"∗"z)`
`EE1AAx, x"∗"1"="x" et "1"∗"x"="x" et "EEy, yx"="1" et "xy"="1`

Tout cela se fait implicitement en énonçant simplement :

`(G,"∗")` est un groupe

ou encore :

`"Groupe"(G,"∗")`

Puis une distinction doit s'opérer entre le modèle et le groupe en tant que monde fini. Le modèle est la structure comprenant le langage `("∗")` et comprenant la théorie précédente. Tandis qu'un groupe est une réalisation du modèle. Un groupe d'au plus `n` éléments est un groupe engendré dont le langage est `(e_1,e_2,e_2,...,e_n,"∗")`, et dont on a ajouté dans sa théorie la propriété suivante :

`AAx, x"="e_1 "ou" x"="e_2 "ou" ... "ou" x"="e_n`

et dont la théorie est ensuite rendu complète. Ainsi l'ensemble sous-jacent est nécessairement inclus dans le sac des éléments générateus `⟅ e_1,e_2,e_2,...,e_n ⟆` et le monde ainsi défini a une connaissance complète de lui-même, ce qui n'est pas le cas du modèle. Le monde fini peut calculer tous ses éléments, et déterminer la valeur de vérité de toutes les propositions qu'elle peut exprimer dans son langage.

Dans le cas générale, la théorie `"Groupe"(G,"∗")` enrichie le langage de la structure `G` avec l'opérateur `1` rendu ainsi définissable par la structure. Mais celui-ci ne fait pas partie du langage de la structure. Il est définissable, et s'avère même définissable de façon unique par la structure, mais il n'est pas calculable par la structure. D'une certaine façon la structure sait qu'il existe mais ne le connait pas. Par contre, si le groupe `G` est fini, alors dans une extension du langage permettant de calculer tous les élémnts, le groupe connaît tous ses éléments et donc connaît l'élément neutre qui en fait partie.

12.2) Définition du second ordre

Cette définition se distingue de la précédente en ce qu'elle affirme l'existence d'un opérateur d'inversion `frI"(.)"`. La théorie précedente est remplacée par :

`AAxAAyAAz, (x"∗"y"∗")z"="x"∗"(y"∗"z)`
`EE1EE frI"(.)"AAx, x"∗"1"="x" et "1"∗"x"="x" et "xfrI(x)"="1" et "frI(x)x"="1`

lorsque l'ensemble sous-jacent est fini, l'équivalence de Skolem devient assurement valide, et donc cette deuxième définition du groupe devient exactement équivalente à la première. Aussi dans le cas fini, elle est noté pareillement :

`(G,"∗")` est un groupe

ou encore :

`"Groupe"(G,"∗")`

La théorie `"Groupe"(G,"∗")` enrichie le langage de la structure `G` avec des opérateurs `1` et `frI"(.)"` rendus ainsi définissables par la structure. Mais ceux-ci ne sont pas dans le langage de la structure et s'avèrent non calculables par la structure. D'une certaine façon la structure ne les connait pas, bien qu'il s'avère qu'ils soient définissables de façon unique.

12.3) Définition du premier ordre dans un langage augmenté :

Dans le langage augmenté des opérateurs `1,frI"(.)"`, la définition du second ordre précédente s'exprime au premier ordre :

`AAxAAyAAz, (x"∗"y"∗")z"="x"∗"(y"∗"z)`
`AAx, x"∗"1"="x`
`AAx, 1"∗"x"="x`
`AAx, xfrI(x)"="1`
`AAx, frI(x)x"="1`

On désigne ainsi l'élément neutre de la loi par `1` et l'opérateur d'inversion par `frI"(.)"`. Le langage du groupe est ainsi augmenté en `(G, "∗", 1, frI)`. Tout cela se fait implicitement en énonçant simplement :

`(G,"∗",1,frI)` est un groupe

ou encore :

`"Groupe"(G,"∗",1,frI)`

La distinction avec la définition précédente tient dans la calculabilité de `1` et de l'opérateur `frI"(.)"`. L'élément `1` est calculable, alors que dans la définition précédente l'élément `1` n'était que définissable et non calculable. De même, l'opérateur `frI"(.)"` est calculable, alors que dans la définition précédente l'opérateur `frI"(.)"` n'était que définissable et non calculable.

Puis une distinction doit s'opérer entre le modèle et le groupe en tant que monde : Le modèle est la structure comprenant le langage `(G, "∗", 1, frI)` et comprenant la théorie précédente, et il s'applique à tous les groupes. Tandis qu'un monde est une réalisation du modèle. Un groupe d'au plus `n` élément est une théorie complète de langage `(e_1,e_2,e_2,...,e_n,1,frI)`, et l'ensemble sous-jacent est inclus dans le sac `⟅ e_1,e_2,e_2,...,e_n ⟆`. Pour le monde fini, tout les objets finis sont calculables, parcontre pour le modèle, sa théorie et son langage sont insuffisant pour tout définir et tout calculer.

 


Dominique Mabboux-Stromberg
5 avril 2020
 
Sommaire
Suivant