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 même conceptuellement ni physiquement possible. 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 au plus qu'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 finies. 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. 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, tantôt 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) Les types dérivés

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` en associant à tout élement `y` l'application constante produisant `y`. 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 en les regroupant et 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.

3.1) Le produit `"×"`

La première règle considérée est l'associativité de l'opérateur `"×"`. C'est à dire que pour tout type `A,B,C` dérivés de `E`, 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é.

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