Langage logique général

La logique est dite du premier ordre car elle n'utilise qu'un seul type de variable.

La structure s'énumérant est la clef de voûte qui lie les trois pans du langage : le langage de programmation pour l'énumérateur, le langage de propriétés pour la théorie, et le langage de données pour l'élément.

2) Langage de données

On part de la présentation d'un langage d'opérateurs d'arité fixe tel que par exemple :

Les éléments de `L` sont appelés les opérateurs générateurs du langage. L'arité de ces opérateurs, c'est à dire le nombre d'arguments qu'ils prennnent, est indiqué par le suffixe `"(.)"` qui désigne une arité `1`, ou par le suffixe `"(.,.)"` qui désigne une arité `2`, ou par une absence de suffixe qui désigne une arité zéro. Un opérateur d'arité zéro constitue un élément.

Les opérateurs générateurs `a,f"(.)",g"(.,.)"` engendrent l'univers de Herbrand noté `{a,f"(.)",g"(.,.)}°"`. C'est l'ensemble de tous les emboitements possibles en respectant l'arité des opérateurs que l'on peut faire avec les opérateurs générateurs `a,f"(.)",g"(.,.)"`. Les emboitements doivent être de taille finie et clos c'est à dire sans argument laissé libre. Et les opérateurs générateurs peuvent être utilisés en nombre autant que l'on veut. On résume cela en disant que c'est l'ensemble de toutes les compositions closes d'opérateurs générateurs.

Un terme est une composition close d'opérateurs générateurs. Par exemple :

Dans la façon de parler, le « langage » désigne aussi bien `L` que `L°`. Parler de langage `L` ou de langage `L"°"` est synonyme et signifie indifféremment les deux à la fois. Pour être plus précis, on dira l'ensemble des « termes du langage » ou l' « univers du langage » pour désigner l'univers de Herbrand, l'ensemble `L"°"`. Et on dira l'ensemble des « opérateurs générateurs du langage » ou la présentation du langage » pour désigner la présentation, l'ensemble `L`.

Le nom des opérateurs ne change pas la structure de l'univers de Herbrand. Une traduction changeant de façon biunivoque les noms des opérateurs (nécessairement de même arité) constitue un isomorphisme c'est à dire une bijection respectant les opérations d'emboitement. Fort de cette remarque, on définie la signature d'un langage d'opérateurs, comme étant la suite finie d'entiers `(n_0, n_1, n_2, n_3,...)` définie comme suit : L'entier `n_0` désigne le nombre d'éléments générateurs, l'entier `n_1` désigne le nombre d'opérateurs unaires générateurs, l'entier `n_2` désigne le nombre d'opérateurs binaires générateurs, l'entier `n_3` désigne le nombre d'opérateurs générateurs d'arité `3` figurant dans la présentation du langage, et ainsi de suite. Par exemples :

Cette signature caractérise la structure des univers de Herbrand à isomorphisme près.

3) Langage de programmation

On pose les bases d'un langage de programmation permettant de programmer l'énumération de tous les termes du langage `{a,f"(.)",g"(.,.)"}`.

D'un point de vue informatique, une énumération est un processus qui émet un flux de données. On parlera de flux de sortie. On est donc amené à considérer des processus de calcul pouvant posséder non seulement des entrées et des sorties, qualifiées d'individuelles car ne contenant qu'un seul terme à la fois, mais également des flux d'entrée et des flux de sortie.

Un flux peut se terminer par la méta-donnée `"FIN"`, on dira alors qu'il est fermé. Toute entrée ou sortie peut être considérée comme un flux, ce qui a l'avantage d'unifier les procédés d'entrée-sortie. Ceci est d'autant plus pertinent que les données ne sont pas bornées en taille et donc a priori ne peuvent qu'être transmises qu'à travers un flux en mettant en oeuvre un autre protocole de bas niveau non encore explicité ici.

Le processus s'arrête lorsque tous ses flux de sortie sont fermées c'est à dire ont émit la méta-donnée `"FIN"`.

Les entrées individuelles peuvent être transmises au début d'un flux d'entré. De même, les sorties individuelles peuvent être transmises au début d'un flux de sortie. Ce faisant, les processus les plus courants auront exactement un flux d'entrée et un flux de sortie.

L'hypothèse de créer des flux parallèles n'apportent pas grand chose, en tout cas dans cette première partie où on ne s'interesse pas intensément à l'efficacité ou à la complexité du calcul, sachant que deux flux parallèles peuvent se fusionner parallèlement sans difficulté en un seul flux, alternant les données de l'un à l'autre. C'est pourquoi il est intéressant de modéliser un langage de programmation mettant en oeuvre un seul type de processus possédant un flux d'entrée et un flux de sortie.

On utilise le symbole pipe `¦`, symbole utilisé par le shell Unix, pour signifier que le flux de sortie du processus situé à gauche du symbole est relié au flux d'entrée du processus situé à droite du symble. Exemple : `A¦B¦C` signifie que le processus `A` produit un flux de sortie qui est relié au flux d'entrée de `B` qui possède un flux de sortie relié au flux d'entré de `C`.

Si un processus possède un flux d'entrée qui n'est raccordé à rien, alors le flux est fermé, et cela revient au même à ce qu'il soit raccordé à un flux de sortie n'émettant que la seule méta-donnée `"FIN"`. Si un processus n'utilise pas son flux d'entrée, alors quelque soit le flux de sortie qui y est raccordé, cela ne change pas son flux de sortie.

Puis il faut pouvoir composer ces flux de façon parallèle ou de façon série. Parce que notre langage est focalisé sur les processus qu'il nomme par des lettres majuscules, et que nous ne nommons pas les flux, nous allons concevoir ces deux opérations sur les processus eux-mêmes.

On compose les processus `A, B, C` de façon parallèle par l'expression `(A,B,C)`. Le flux d'entrée est démultiplié et envoyé sur chacun des processus `A, B, C`. Et le flux de sortie correspond à la fusion des flux de sortie de chacun des processus `A, B, C`. Et, la manière par défaut de construire ce flux, consiste à alterner les données provenant de `A` puis de `B` puis de `C` et de recommencer ainsi de suite.

On compose les processus `A, B, C` de façon série par l'expression `[A,B,C]`. Le flux d'entrée est démultiplié et envoyé sur chacun des processus `A, B, C`. Et le flux de sortie correspond au flux de `A` qui s'il se termine, alors la méta-donnée `"FIN"` est retirée et le flux se prolonge avec celui émit par `B`, puis si la méta-donnée `"FIN"` apparait, alors celle-ci est retirée et le flux se prolonge avec celui émit par `C`.

Puis il existe une autre opération moins évidente qui consiste à générer tous les produits possibles sous forme de couples.

Etant donné deux flux de données `tau_1,tau_2,tau_3,tau_4,...` et `sigma_1, sigma_2, sigma_3,sigma_4,...`, le flux produit d'espace est un flux qui énumère tous les couples possibles d'un élément du premier flux et d'un second élément du second flux. Et, la manière par défaut de construire ce flux, consiste à parcourir le plan par des diagonales et cela produit le flux de couples suivant :

On compose les processus `A, B` en produit d'espaces par l'expression `A"×"B`. Le flux d'entrée est démultiplié et envoyé sur chacun des processus `A, B`. Et le flux de sortie correspond au balayage de l'espace à deux dimensions des couples de données `(x,y)` où `x` est émit par `A` indépendamment de l'autre processus, et où `y` est émit par `B` indépendamment de l'autre processus.

Puis il faut pouvoir appliquer un opérateur générateur unaire tel que `f"(.)"` à un flux pour produire le même flux mais dans lequel chaque élément, que nous désignons par `tau`, est remplacé par `f(tau)`. Parce que nous ne nommons pas les flux mais les processus qui les crée, on conçoit cet opération sur les processus. On note `f(A)` le processus qui effectue le même calcul que le processus `A` mais qui va en modifier le flux de sortie en remplaçant chaque élément du flux, que nous désignons par `tau`, par `f(tau)`.

De même, il faut pouvoir appliquer un opérateur générateur binaire tel que `g"(.,.)"` à un flux de couples pour produire le même flux mais dans lequel chaque couple d'éléments, que nous désignons par `(tau,sigma)`, est remplacé par `g(tau,sigma)`. On note `g(A"×"B)` le processus qui effectue le même calcul que le processus `A"×"B` mais qui va en modifier le flux de sortie en remplaçant chaque couple d'éléments du flux, que nous désignons par `(tau,sigma)`, par `g(tau,sigma)`.

De même, il faut pouvoir donner un sens à un opérateur générateur d'arité zéro tel que `a`. Dans le langage de programmation, un élément générateur tel que `a` désigne un processus émettant le flux `a, "FIN"`.

Pour finir, il faut pouvoir programmer récurcivement, c'est à dire construire un programme qui s'appelle lui-même sachant qu'a chaque appel, un nouveau processus est créé dans un nouvel environnement. On note la création d'un programme à l'aide du symbole d'égalité et d'une lettre majuscule désignant son processus relativement à l'environnement en cours. Tout ça pour préciser que si cette lettre est répétée dans le programme, cela correspond à un appel récurcif et donc à la création d'un nouveau processus de même nom mais dans un nouvel environnement empilé dans la pile des appels.

Le programme d'énumération des termes du langage `{a,f"(.)",g"(.,.)"}` s'écrit comme suit :

4) Séparation entre le langage et la structure

Les univers de Herbrand constituent des langages trés généraux, appelés parfois carrières. Ils se définissent à partir d'un ensemble d'opérateurs générateurs `L` caractérisé par une signature. Une fois posé ce mécanisme de construction. Une fois définie ce genre de langage. On sépare le sens, de la symbolique. On sépare le signifié, du signifiant. Ceci afin que le langage serve à exprimer autre chose que lui-même. On appelle élément, le signifié. Et on appelle terme, le signifiant. Les éléments sont regroupés dans la structure, dans son ensemble sous-jacent noté `"<"L">"`. Et les termes sont regroupés dans le langage, dans son univers noté `L"°"`.

`L` étant l'ensemble `{a,f"(.)",g"(.,.)"}`, par convention les deux notations suivantes sont égales :

La présentation d'une structure énumère les différents opérateurs générateurs de son langage et les met entre crochets `"< >"` pour produire l'ensemble sous-jacent de la structure :

Au départ la structure coïncident avec le langage, chaque élément est désigné par un unique terme. Deux termes distincts désignent forcement deux éléments distincts. Il n'y pas de différence entre les termes et les éléments, entre l'ensemble sous-jacent de la structure et l'univers du langage, sauf d'un point de vue sémantique : l'opérateur est emboitant dans le langage alors qu'il est agissant dans la structure. Dans un cas, c'est un légo qui s'emboite avec d'autres légos. Et dans l'autre cas, c'est une application de `E^n->E` où `E` désigne l'ensemble sous-jacent de la structure et où `n` désigne l'arité de l'opérateur générateur en question.

Pour rompre l'identité entre la structure et son langage, sans sortir de la carrière qui représente le pouvoir d'expression du langage, on commence par introduire les égalités entre deux termes. Cela permet de définir les théories d'égalités de dimension zéro, dit de dimension zéro car n'utilisant aucune variable.

Tant qu'il n'y a aucune règle posée, la structure coïncide au langage d'opérateurs, et elle sera dite libre. Autrement dit, une structure libre est identique à un langage d'opérateurs, son ensemble sous-jacent est identique à l'univers de Herbrand.

La signature d'une structure libre est la signature de son langage. Les structures libres, pour chaque signature, sont uniques à isomorphisme près.

5) Langage de propriété

On utilise le prédicat d'égalité `"="`, comme une sorte d'instruction implémentant une base de données. Le prédicat d'égalité s'applique à deux termes quelconques du langage et signifie que ces deux termes désignent le même élément.

Nous avons définie au chapitre 2, un langage de données qu'est l'univers de Herbrand permettant d'exprimer tous les éléments. Maintenant il nous faut définir un langage de propriétés qui permette d'exprimer toutes les théories d'égalités, de dimension zéro pour commencer.

Une clause d'égalité est une disjonction de littéraux d'égalité. La disjonction peut ne contenir qu'un seul littéral. Par convention la disjonction vide (ou clause vide) est toujours fausse. Exemple de clause d'égalité :

Une théorie d'égalité est une conjonction de clauses d'égalité. La conjonction peut ne contenir qu'une seul clause. Par convention la conjonction vide est toujours vrai. Exemple de théorie d'égalité :

Le langage de propriété que nous utilisons comprend le prédicat d'égalité `"="` s'appliquant à deux termes quelconques du langage `L`, et les connecteurs logiques de conjonction `"et"` et de disjonction `"ou"`.

Notez que l'on n'utilise pas le connecteur logique de négation `¬`, ni aucune variable.

L'étude du langage propositionnel montre que les opérations logiques `"et","ou"` sont réciproquement distributives l'une par rapport à l'autre. C'est à dire que pour tout littéraux `x,y,z` nous avons :

On déduit de cette propriété que toute théorie d'égalité se décompose de façon unique en une conjonction de clauses à l'ordre près des clauses et à l'ordre près des littéraux dans chaque clause. C'est pourquoi cette décomposition est choisie comme étant l'expression de la théorie d'égalité.

L'expression d'une théorie d'égalité est un ensemble de clauses d'égalité, à l'ordre près des littéraux dans chaque clause. L'ensemble correspond ici à une conjonction, on parlera d'ensemble conjonctif. Exemple :

L'expression d'une théorie d'égalité est parfois exprimée sous forme d'un ensemble d'ensembles de littéraux. Le premier niveau d'ensemble correspondant à une conjonction, et les seconds niveaux d'ensembles correspondent à des disjonctions. Exemple :

Notez que conventionellement une conjonction vide est toujours vrai, et une disjonction vide est toujours fausse.

6) Structure

Une structure comprend un langage et une théorie d'égalité exprimée dans ce langage. L'univers du langage constitue la carrière, une matrice où son mémorisées les données, c'est une structure libre.

On commene par ne considérer que des théories d'égalité de dimension zéro, c'est à dire sans variable. Un littéral d'égalité constitue un raccourcis dans la matrice (ou carrière). Ces raccourcis rendent la structure liée.

On note la structure sous forme d'un quotient, le quotient d'un langage `L` par une théorie d'égalité `T`. On la note aussi par le quotient de la structure libre `"<"L">"` par une théorie d'égalité `T`. Les deux écritures sont valables, mais la seconde écriture désigne à la fois la structure et son ensemble sous-jacent :

`L` est un langage d'opérateurs, c'est à dire un ensemble fini d'opérateurs d'arité fixe.

`T` est une théorie d'égalité de dimension zéro, c'est à dire un ensemble fini de clauses d'égalité entre termes que l'on présente entre braquette `{ }`. Chaque clause n'utilise que des opérateurs de `L`, le prédicat `=`, et le connecteur logique `"ou"`.

`S` désigne à la fois la structure et son ensemble sous-jacent, et on laisse le soin au contexte de décider si c'est la structure ou l'ensemble sous-jacent dont il est question.

Une fois posé la structure `S`, tout opérateur de `S` obéït implicitement à la théorie de la structure et de même pour tout ensembles engendré par compositions closes d'opérateurs de `S`. Ainsi l'expression `"<"L">"` désigne l'ensemble sous-jacent de la structure engendrés par `L` en respectant `T`.

Par exemple, considérons le langage `{a, f"(.)"}`. Une structure cyclique de 3 éléments peut se présenter comme suit :

Le langage de la structure `S` est : `{a, f"(.)"}`.
La théorie de la struture `S` est : `{f^3(a)"="a}`.
L'ensemble sous-jacent est : `S = "<"a,f"(.)>" = {a, f(a),f^2(a)}`.

7) La règle de raisonnement

Pour procéder au raisonnement, on utilise des variables `A, B, C...`, désigant un terme quelconque du langage `L`.

Les variables sont de valeurs identiques si et seulement si elle représente le même terme dans le langage libre `L`, et on note cela à l'aide du symbole identité `-=`.

Les variables sont de valeurs égales si et seulement si elle désigne le même élément de la structure, et on note cela à l'aide du symbole d'égalité `=`. L'égalité est une relation d'équivalence sur l'ensemble des termes du langage `L`.

Un terme `A` est inclus dans un terme `B` si et seulement si il constitue un sous-terme de `B` et on note `A sube B`. Notez que `A` est un sous-terme de `A`. Par exemple nous avons :

La substitution par `C` de tous les termes identiques à `A` qui sont inclus dans `B`, se note `B_(A|->C)`. Par exemple nous avons :

8) Hierarchie de chomsky

6) Extension et quotientage

L'ajout d'un opérateur générateur au langage, s'appelle une extension du langage. Cela consiste à ajouter un nouvel opérateur générateur `b` au langage. Et cela augmente considérablement l'univers de Herbrand associé, plus encore que si nous ajoutions une dimension supplémentaire. Dans l'exemple précédent nous avons définie une structure `S`. Si on ajoute un nouvel élément générateur `b` au langage de la structure, on obtient une nouvelle structure notée `S[b]` et nous avons :

L'ajout à la théorie d'une clause d'égalité qui doit être exprimé dans le langage de la théorie, s'appelle un quotientage. Cela augmente les possibilités d'égalité entre termes. Par exemple, si on ajoute la clause `f(a)"="f(b)` à la structure `S[b]` on obtient une nouvelle structure notée `S[b]"/"{f(a)"="f(b)}` et nous avons :

7) Les démonstrations constructives

La théorie `T` d'une structure énumère tout ce qu'elle démontre constructivement. C'est à dire qu'il existe un énumérateur, appelé l'énumérateur de `"<"T">"`, qui énumère toutes les propositions exprimables dans le langage de la structure et démontrables constructivement par `T`.

Une structure comprend un langage `L` et une théorie `T`. On engendre, en prenant la clôture par composition close, l'ensemble sous-jacent de la structure `"<"L">"`, et on engendre, en prenant la clôture par démonstration constructives, l'ensemble des clauses d'égalité démontrables constructivements `"<"T">"`. Notez que la même notation est utilisée pour exprimer deux sortes de clôture, et on laisse au contexte le soin de lever l'ambiguité.

Les théories d'égalité ne peuvent démontrer constructivement que des égalités. Y-a-t-il un moyen de déterminer si une théorie d'égalité d'une structure entraine constructivement l'égalité de tous les éléments de la structure ? oui, par exemple pour le langage `{a,f"(.)",g"(.,.)"}`, il suffit de démontrer copnstructivement les égalités `f(a)=a` et `g(a,a)=a` ce que l'énumérateur de `"<"T">"` fera en un temps finie. Par contre la négation ne peu pas être prouvée par ce moyen. La négation ne fait pas partie du langage logique des théories d'égalité.

4) Logique d'égalité du premier ordre

2) Les structures du premier ordre

On munie l'univers de Herbrand d'une théorie d'égalité du premer ordre pour former une structure du premier ordre

C'est une structure libre, car il n'existe aucune relation d'égalité. Deux compositions closes, d'expression différente, representent deux éléments distincts de la structure libre que constitue l'univers de Herbrand.

2) Les extensions du langage

L'utilisation d'une variable `x` correspond à une extension du langage quotienté par une théorie :

possible engendrant un espace de Herbrand infini. C'est le langage composé d'un élément et d'une fonction unaire `L ={a, s"(.)"}` et qui représente d'une certaine façon les entiers naturel.

Puis on posera petit à petit les règles de déduction et leurs axiomes lorsque leur apparition sera nécessaire comme par évidence intuitive.

On définie le langage logique par des règles de construction tel une grammaire. Et on commence par choisir les opérateurs qui nous sont indispenssables. Un terme est une composition close du langage d'opérateurs `{a, s"(.)"}`. Ce langage peut être augmenté de variables élémentaires telles que par exemple `x, y` ou fonctionnelles tel que par exemple `f"(.)"` pour former le langage d'opérateurs `{a, s"(.)", x, y, f"(.)"}`. Voici des exemples de termes :

Puis on choisit les prédicats qui nous sont indispenssables, et le seul qui nous soit indispenssable à ce stade est l'égalité `=`. Un littéral affirmatif est la composition close d'un prédicats parmis `{"=(.,.)"}` avec des termes du langage d'opérateurs `{a, s"(.)"}`. Le langage des prédicats peut aussi être augmenté de variables prédicatives telles que par exemple `X, P"(.)", Q"(.,.)"` pour former le langage de prédicats `{"=(.,.)", X, P"(.)", Q"(.,.)"}`. Le prédicat `X` d'arité nulle est simplement une valeur booléenne inconnue. Voici des exemples de littéraux affirmatifs :

Un littéral peut en plus être négativé par l'opérateur logique `¬` tel que par exemples `x!=y, ¬P(x)`

Une expression logique est une combinaison de littéraux à l'aide d'opérateurs logiques.

Toute expression logique se ramène à une conjonction de clauses. En effet, prenez par exemples l'expression logique `(X =>Y) => Z` où `X, Y, Z` sont trois valeurs logiques, cette expression logique est équivalente à `(X "ou" Z) "et" (¬Y "ou" Z)`.

2) Quantification

Une proposition unidimensionnelle quantifie une variable. Elle possède une tête et un corps séparé par une virgule. La tête quantifie la variable à l'aide d'un opérateur `AA` ou `EE` et le corps est une expression logique dans le langage augmenté de cette variable. Voici un exemple de proposition avec une variable élémentaire :

La variable quantifiée peut être fonctionnelle. Voici un exemple de proposition avec une variable fonctionnelle unaire :

Par symétrie, on conçoit qu'il est posssible de quantifier des variables prédicatives. Voici un exemple d'une proposition avec une variable prédicative unaire :

Le corps d'une telle proposition peut également être constitué par une autre proposition unidimensionnelle, auquel cas le résultat est une proposition bidimensionnelle. Et cela peut se répéter, formant ainsi des propositions de dimension `n`, c'est à dire utilisant `n` variables qui sont soient élémentaires, fonctionelles ou prédicatives. Voici un exemple de proposition de dimension 3 utilisant une variable prédicative unaire et deux variables élémentaires, et qui correspond à un axiome de l'égalité :

3) Aspect calculatoire

Sémantiquement, et selon l'approche intuitionniste, une variable élémentaire interne représente un élément calculable du modèle, un terme de l'espace de Herbrand, ou autrement dit un élément de la structure libre `"<"a,s"(.)>"`. De même une variable fonctionnelle représente une fonction calculable du modèle, et une variable prédicative représente une fonction logique calculable dans le modèle.

Selon le principe élémentarien, les éléments du modèle sont énumérables comme tout ce qui est calculable. Les fonctions et prédicats calculable sont énumérables.

Et il n'y a pas de différence essentielle entre une fonction et un prédicat, juste une question accessoire sur la forme du résultat. C'est pourquoi on n'adopte pas d'écriture spécifique pour différentier une variable fonctionnelle d'une variable prédicative, sachant que l'usage qui en est fait après, tranche nécessairement la question.

Le modèle dans lequel les propositions sont réalisées ou non est l'espace de Herbrand munie des fonctions et prédicats calculable.

4) Négation

Considérons une variable élémentaire `x` et un prédicat unaire `P"(.)"`. Considérons la proposition `AA x, P(x)`. Le quantificateur `AA` appliqué à la variable `x` correspond à un `"et"` intégré sur l'ensemble des valeurs calculables de `x`. L'opérateur `"et"` est représenté par le symbole `^^` (tel que l'intersection) . L'ensemble des éléments de l'espace de Herbrand est représenté par `Omega`. Nous avons :

L'ensemble des valeurs possible de `x`, noté `Omega`, est par principe énumérable. Cela entraine que la proposition `AA x, P(x)` est réfutable en un temps fini dans le cas où celle-ci serait fausse. Et il s'agit là d'une périssologie car on définie justement la valeur logique fausse de cette proposition par le fait qu'elle doit être réfutée en un temps fini. Parcontre elle n'est pas assurement affirmable en un temps fini dans le cas où elle ne serait pas fausse. C'est pourquoi l'affirmation d'une telle proposition est parfois appellée un oracle.

En tant qu'idée mathématique sans contrainte matériel d'aucune sorte, on peut se placer à l'infini et ainsi connaître l'oracle. Mais il faut en quelque sorte, être immortel dans un monde immortel et de surcroit régit par la mécanique classique, somme-toute, des présupposés assurement faux, mais qui à notre échelle sont approximativement vrai..

Si on adopte ce principe qui correspond au présuposé des mathématiques, à savoir que le monde dans le quel est développé cette mathématique perdure éternellement et est régis par la mécanique classique, et que nous pouvons nous placer abstraitement à l'infini et ainsi connaitre la valeur logique de la proposition, alors toutes les propositions exprimables dans notre langage ont une valeur logique bien définie.

La négation d'une propostion unidimensionnelle s'obtient alors simplement en inversant le quantificateur de la tête et en négativant le corps.

Le quantificateur `EE` appliqué à la variable `x` correspond à un `"ou"` intégré sur l'ensemble des valeurs calculables de `x`. L'opérateur `"ou"` est représenté par le symbole `vv` (tel que l'union). L'ensemble des éléments de l'espace de Herbrand est représenté par `Omega`. Nous avons :

On convient que cette règle de calcul de la négation s'applique quelque soit le type de variable, élémentaire, fonctionnelle ou prédicative d'arité quelconque.

Il est alors nécessaire, pour respecter la sémantique, pour respecter notre vision intuitive des fonctions et des prédicats, d'introduire dans le langage d'opérateurs l'ensemble des moyens nécessaires pour calculer toutes les fonctions et tous les prédicats considérés comme possibles.

Dans les cas dégénérés où nous n'avons pas cette propriété, la signification de la proposition `AA P(.), P(a)` change du sens habituel. Car elle signifie : « Quelque soit la fonction logique `P(.)` que nous pouvons construire avec les moyens qui nous sont données, nous avons la propriété `P(a)` ».

5) Élémentarisation

Puis on opère une élémentarisation des fonctions et des prédicats. Deux fonctions `f"(.)", g"(.)"` sont dites égales ssi `AA x, f(x)=g(x)`. Deux prédicats `R"(.)", S"(.)"` sont dits égaux ssi `AAx, R(x)<=>S(x)`. Et de même pour des fonctions et prédicats d'arité supérieur. Il est alors possible de créer pour chaque fonction et pour chaque prédicat modulo l'égalité ainsi définie, un élément qui le désigne. On obtient ainsi une deuxième catégorie d'éléments.

Il est alors possible de définir des variables (élémentaires, fonctionnelles ou prédicative) typées. Le type booléen se note `0`. Le type élément se note `1`. Le type élément de deuxième catégorie se note `2`. Le type `1->0` désigne celui d'un prédicat unaire, le type `(1,1)->1` désigne celui d'une fonction binaire, le type `(2,2)->0` désigne celui d'un prédicats opérant sur deux éléments de deuxième catégorie, le type `(1,2)->1` désigne celui d'une fonction opérant sur un élément de première catégorie et un élément de deuxième catégorie pour produire un élément de première catégorie, etc...

Les fonction et prédicats créés par ce procédé peuvent à leur tour être élémentarisés de la même façon et former les éléments de troisième catégorie, et ainsi de suite.

On cherche à étendre la capacité d'expression du langage, et on veut choisir une voie dans laquelle le langage obtenu permettra d'exprimer de façon simple une opération de raisonnement jugée fondamentale qu'est la récurrence générale.

6) Fonctionnisation et prédicarisation

Puis on opère une fonctionnisation des termes avec varibiable. Un terme avec une variable `x` libre, tel que par exemple `g(g(x,v),x)`, permet de créer une nouvelle fonction `h"(.)"` définie par `h(x) = g(g(x,v),x)` et qui peut alors être ajoutée au langage d'opérateurs. On notera :

Puis on opère une prédicarisation des propositions avec varibiable. Une proposition avec une variable `x` libre, tel que par exemple `AA v, g(x,v)=g(v,x)`, permet de créer un nouveau prédicat `N"(.)"` définie par `N(x) <=> AA v, g(x,v)=g(v,x)` et qui peut alors être ajouté au langage de prédicats. On notera :

3) Logique respectueuse de l'indépendance

On enrichie le langage logique à l'aide de la notion d'indépendance entre quantificateur `AA` et `EE`, et plus finement encore, entre quantificateur `AA` et opération logique `"ou"`, et symétriquement aussi entre quantificateur `EE` et opération logique `"et"`.

Considérons deux variables élémentaires `x, y` et deux prédicats binaires `A"(.,.)", B"(.,.)"`. Considérons la proposition suivante :

Cela signifie que quelque soit `x` et `y`, il y a toujours une des deux propositions `A(x,y)` ou `B(x,y)` qui est vrai. Maintenant, considérons qu'il existe un prédicat unaire `D"(.)"` tel que nous ayons :

Le modèle est alors plus simple, puisque l'alternative se fait indépendament de la valeur de `"y"`. On notera ce `"ou"` indépendant de `AAy` avec la notation de Hintikka et Sandu. Les deux propositions suivantes sont équivalentes :

Le `EEz` se ramenant à une opération logique `"ou"`, la même qualité d'indépendance à l'égard de `AAy` peut se produire. Auquel cas les 4 propositions suivantes sont équivalentes :

`AAx, AAy, (EEz"/"AAy) W(x,y,z)`
`AAx, AAy, W(x,y,z_1) ("ou/"AAy) W(x,y,z_2) ("ou/"AAy) W(x,y,z_3) ("ou/"AAy) ...`
`EE D_1"(.)",EE D_2"(.)",EE D_3"(.)", AAx, AAy,`
        `(W(x,y,z_1) "et" D_1(x) "et" ¬D_2(x) "et" ¬D_3(x) "et" ...)`
      `"ou"(W(x,y,z_2) "et" ¬D_1(x) "et" D_2(x) "et" ¬D_3(x) "et" ...)`
     `"ou"(W(x,y,z_3) "et" ¬D_1(x) "et" ¬D_2(x) "et" D_3(x) "et" ...)`
      `"ou" ...`
`EEf(.), AAx, AAy, W(x,y,f(x))`

On utilise parfois, après la quantification d'une variable, le symboles ` / ` qui signifie "tel que" pour préciser le domaine où s'étend la quantification. Ainsi l'expression suivante :

signifie quelque soit `x` tel que `x` appartenant à `A` et que `x` appartient à `B`, nous avons `x` appartient à `C`. Cette formule est équivalente à chacune des expressions suivantes :

sur un ensemble au sens large c'est à dire sur un terme du langage non augmenté de cette variable,

Axiome d'extensionnalité : Si deux ensembles ont les mêmes éléments, alors ils sont égaux. ( entraine Axiome de l'ensemble vide : Il existe un ensemble sans élément. (<=schéma d'axiomes de compréhension))

La négation d'une formule s'obtient en remplaçant les quantificateurs `AA` par `EE` et reciproquement, en laissant intacte les expressions sous les symboles ` / ` et en négativant l'expression logique.

Remarquez que l'expression logique `AA x in Ø, P(x)` est identiquement vrai quelque soit `P` tandis que l'expression logique `EE x in Ø, P(x)` est identiquement faut quelque soit `P`.

Puis on opère une unification des objets. Deux fonctions `f"(.)", g"(.)"` sont dites égales ssi `AA x, f(x)=g(x)`. Deux prédicats `R"(.)", S"(.)"` sont dits égaux ssi `AAx R(x)<=>S(x)`. Il est alors possible de définir pour chaque fonction et pour chaque prédicat modulo l'égalité ainsi définie, un élément qui le désigne. On obtient ainsi une deuxième catégorie d'éléments.

Il est alors possible d'étendre les opérateurs et prédicats à ses nouveaux éléments, faisant que le terme `f(f)` est un sens.

Cela n'engendre pas le paradoxe de Russel "l'ensemble des ensembles qui ne se contiennent pas se contient-il ?" car l'existence de l'ensemble n'est pas obligé. Ainsi la proposition suivante est simplement contraditoire :

---- 26 mai 2017 -----

Une liste telle que `O = (a,f"(.)",g"(.,.)")` peut retourner ces éléments en fonction d'un index. Nous avons :

`O[1] = a`
`O[2] = f"(.)"`
`O[3] = g"(.,.)"`
`O[4] = "FAIL"`

A partir d'une liste, on fabrique un énumérateur en mémorisant un index. Le créateur d'énumérateur se note `"Enumérateur"`

`E = "Enumérateur"(O)`

L'énumérateur `E` possède un index initialisé à `0`. L'instruction d'incrémentation `"++"` appliqué à l'énumérateur `E` se note `E"++"`. Cette instruction incrémente l'index de l'énumérateur et retourne `a`. Puis si nous répétons l'instruction `E"++"`, son index est encore incrémenté et l'instruction retourne `f"(.)"`. Et ainsi de suite.

Etant donné une liste d'énumérateurs tel que par exemple `(E_1, E_2, E_3)`. Nous définissons l'opérateur `"Parallèle"` et l'opérateur `"Produit"` comme suit :

L'opérateur `"Parallèle"` appliqué à cette liste crée un énumérateur qui exécute de façon parallèle chacun des énumérateurs de la liste de la façon suivante : Il incrémente un énumérateur et si cet énumérateur retourne `"FAIL"` alors il le retire de la liste et passe au suivant, sinon il produit le résultat et passe au suivant quant il arrive au bout de la liste, il repasse au premier énumérateur de la liste.

L'opérateur `"Produit"` appliqué à cette liste crée un énumérateur de triplets de la façon suivante il incrémente un énumérateur et passe au suivant et quant il arrive au bout de la liste, il repasse au premier énumérateur de la liste.

On programme un énumérateur H des termes du langage L de façon récurcive. On pose d'abord un énumérateur des opérateurs générateurs de `L` que l'on présente sous forme d'une liste `O = (a,f"(.)",g"(.,.)")`. Cela revient à munir l'ensemble `L` d'un ordre totale.

Puis l'énumérateur H lance une énumération en parallèle d'une suite finie d'énumérations énumérés par L

Logique du premier ordre

1) Introduction