Logique formelle du premier ordre

On commence cette introduction en posant une question à ChatGPT. Pouvez-vous décrire le langage logique du premier ordre (dit langage de calcul des prédicats) ?

ChatGPT :

Le langage logique du premier ordre, également connu sous le nom de logique des prédicats, est un système formel utilisé pour exprimer des déclarations sur des objets et leurs relations. Ce langage est plus expressif que la logique propositionnelle car il permet de parler des propriétés des objets ainsi que des relations entre ces objets. Voici les éléments clés du langage logique du premier ordre :

1. Symboles

Symboles de variable : `x,y,z`… utilisés pour représenter des objets arbitraires dans le domaine de discours.
Symboles de constante : `a,b,c`… qui représentent des objets spécifiques dans le domaine de discours.
Symboles de fonction : `f,g,h`… qui, pour chaque n-uplet d'entrées d'objets, associent un objet de sortie.
Symboles de prédicat : `P,Q,R`… utilisés pour représenter des propriétés des objets ou des relations entre les objets. Par exemple, `P(x)` peut signifier que l'objet `x` possède la propriété `P`, et `R(x,y)` peut signifier que la relation `R` existe entre `x` et `y`.

2. Connecteurs logiques

Négation : `"¬"`, qui inverse la vérité d'une proposition.
Conjonction : `"∧"`, qui est vraie si et seulement si les deux propositions qu'elle connecte sont vraies.
Disjonction : `"∨"`, qui est vraie si au moins une des propositions qu'elle connecte est vraie.
Implication : `"→"`, qui est vraie sauf si la première proposition est vraie et la deuxième est fausse.
Équivalence :`"↔"`, vraie si les deux propositions qu'elle connecte ont la même vérité.

3. Quantificateurs

Quantificateur universel : `∀` (pour tout), utilisé pour exprimer que quelque chose est vrai pour tous les éléments d'un domaine. Par exemple, `∀x,P(x)` signifie que la propriété `P` est vraie pour chaque objet `x`.
Quantificateur existentiel : `∃` (il existe), utilisé pour dire qu'il existe au moins un élément dans le domaine pour lequel la proposition est vraie. Par exemple, `∃x,P(x)` signifie qu'il y a au moins un objet `x` pour lequel `P(x)` est vrai.

4. Formules

Formules atomiques : ce sont des expressions qui ne contiennent pas de connecteurs logiques ou de quantificateurs, par exemple `P(f(x),y)`.
Formules complexes : construites en utilisant des formules atomiques avec des connecteurs logiques et des quantificateurs.

5. Règles d'inférence

Le langage utilise des règles d'inférence formelles pour déduire des conclusions à partir des hypothèses. Ces règles, telles que le Modus Ponens et le Modus Tollens, sont essentielles pour le raisonnement formel.

La logique du premier ordre est largement utilisée en mathématiques, en informatique (notamment en programmation et en bases de données), en philosophie, en linguistique, et dans d'autres sciences formelles pour formaliser et analyser les théories. Elle permet de modéliser avec précision des situations complexes en exprimant des généralisations et des exceptions de manière claire et structurée.

2) Les fondements de la logique du premier ordre

En se limitant à la logique du premier ordre, appelé calcul des prédicats, on se fixe un cadre permettant de définir les règles de déduction formelle, telle une syntaxe qui se fondent sur les formules et sur les termes et non sur les objets qu'ils désignent. C'est pourquoi malgré l'exactitude du raisonnement, le domaine regroupant tous les objets tant définissables qu'indéfinissables garde toujours quelque chose d'indéfinissable. Le raisonnement a beau être exacte, le domaine comprend un mystère insondable dans son infini potentiel, dans son absence de limite. Le domaine n'est pas un objet.

La logique est dite du premier ordre car elle n'utilise qu'un seul type de variable qui peut pacourir une infinité de valeurs distincts possibles appelées ici objects.

ChatGPT ne parle pas des arités. Effectivement, on peut l'intégrer dans le nom des prédicats et des fonctions que nous désignons comme opérateurs. Ainsi `P(".")` et `P(".,.")` désignent deux prédicats distincts, l'un d'arité 1, l'autre d'arité 2. De même `f(".")` et `f(".,.")` désignent deux opérateurs distincts, l'un d'arité 1, l'autre d'arité 2. Quand l'arité du prédicat est nulle alors le prédicat est une constante booléenne inconnue. Il désigne vrai ou faux. Quand l'arité de l'opérateur est nulle alors l'opérateur est une constante objet inconnue. Il désigne un objet inconnu. C'est pourquoi ont regroupe les constantes objets et les fonctions évoquées par ChatGPT en les opérateurs.

3) Grammaire du langage logique du premier ordre :

Une façon précise de définir un langage est d'en donner une grammaire qui l'engendre :

On ajoute la règle de masquage des variables pour pouvoir interpréter les formules où des mêmes variables sont déclarées plusieurs fois. Et on ajoute l'inteprétation fonctionnelle de la formule lorsque certaines de ses variables n'ont pas été déclarées. Les arités ne sont pas mentionnées car on considère qu'elle complète le nom de l'opérateur ou du terme.

Puis, afin d'éviter un usage trop intensif des parenthèses, on définit un ordre de priorité syntaxique des opérations et de la portée des déclarations de variable, de la priorité la plus forte à la plus faible :

`"¬"X"→"Y` signifie `("¬"X)"→"Y` et non `"¬"(X"→"Y)`
`x"∧"y"→"z` signifie `(x"∧"y)"→"z` et non `x"∧("y"→"z")`
`x"→"y"∨"z` signifie `x"→"(y"∨"z)` et non `(x"→"y)"∨"z)`
`AAxP(x)"→"AAyQ(y)` signifie `AAx(P(x)"→"AAyQ(y))` et non `(AAxP(x))"→"(AAyQ(y))`

4) Logique propositionnelle

Le langage logique d'ordre zéro, c'est à dire n'utilisant pas de variable pouvant parcourir une infinité de valeurs distincts possibles, s'appelle la logique propositionnelle. Son langage est décrit par la grammaire suivante :

Les connecteurs logiques sont des opérations booélennes définies par leur table de vérité où le zéro désigne la valeur logique faux et le un désigne la valeur logique vrai :

Pour des raisons de symétrie liées aux corps symétriques des booléens, ont ajoute au langage le connecteur logique « ou exculsif » noté `"⊕"`.

5) Méthodologie

Nous voulons programmer une machine qui génère des déductions. Le raisonnement pour être complet doit être hypothético-déductif. La machine devra donc tester des hypothèses qu'elle devra créer elle-même.

Nous voulons assurez le caractère démocratique de nos recherches. Pour cela, il faut que nos travaux puissent être apréhendés et testés par le plus grand nombre. Cela peut se faire grâce à des logiciels écrits en javascript et mis à disposition via l'Internet, permettant à tout internaute de pouvoir tester la théorie directement dans son navigateur Internet. Une copie de la théorie est ainsi transmise en même temps que le programme qui peut la tester, laissant à l'utilisateur final le soin de vérifier l'intégrité de la copie.

Une première démarche va d'abord consister à explorer la logique propositionnelle, en révélant des analogies avec des structures mathématiques fondamentales. Puis nous exposerons différents algorithmes de résolution pour la logique d'ordre zéro. Puis nous proposerons une approche empirique du raisonnement en logique du premier ordre.

6) Générateur de formules aléatoires

On perfectionne notre grammaire en indiquant des poids entre crochet pour chaque alternative, et aussi pour donner une proirité syntaxique à chaque connecteur. L'entête précise le symbole d'entrée, la liste des symboles non-terminaux, la liste des connecteurs avec leur priorité affichée entre crochet. Les connecteurs et les variables sont représentés par des caractères autres que { , } [ ] car ils sont utilisées pour rédiger la grammaire.

La programmation doit pouvoir se faire la plus naturellement possible. On utilise un automate, voir le détail de la programmation.

6) Analogie et structuration

Dés que la structure booléenne de la logique est posée, on peut déjà y percevoir les embryons des grandes structures simples et fondamentales révélées par les mathématiques que sont les relations d'équivalence, les relations d'ordre, les treillis et les structures de corps.

6.1) Connecteurs s'appliquant à des ensembles

Les connecteurs `"∧","∨","↔","⊕"`, sont associatifs et commutatifs, autrement dit, ils peuvent s'appliquer à un ensemble de propositions. On définit donc des connecteurs s'appliquant à un ensemble fini quelconque de variables booléennes :

La conjonction est considérée comme un ensemble de conditions restrictives, donc l'absence de condition restrictive vaut le vrai. La disjonction est considérée à l'inverse comme un ensemble de solutions, donc l'absence de solution vaut le faux. Cette définition satisfait la loi de Morgan.

Puis il existe deux analogies fondamentales, l'une se rapportant aux classes d'équivalence, définissant l'opérateur d'égalité appliqué à un ensemble de variables booléennes, l'autre se rapportant aux relations d'ordre totale que forme les suites causales ou ordonnées d'implications successives, définissant l'opérateur d'implication appliqué à une suite de variables booléennes :

Un ensemble de variable égale, est faux seulement s'il existe deux variables distincts dans cet ensemble. Donc appliqué à une seule ou aucune variable booléenne c'est toujours vrai.

Une suite causale est vrai lorsque la suite de booléens est croissante, et elle est fausse s'il existe une variable fausse qui arrive après une variable vrai. Donc appliqué à une seule ou aucune variable booléenne elle vaut toujours vrai.

La notion de suite croissante qui désigne un ensemble totalement ordonnée de variables booléennes, se généralise en la notion d'ordre partiel sur un ensemble de variables booléennes.

6.2) Les deux corps symétriques des booléens

Puis il existe deux corps symétrtiques des booléens que l'on présente sous forme de quintuplet avec comme argument dans l'ordre ; le nom de la structure qui porte sur le même ensemble sous-jacent qui est l'ensemble des booléens `{0,1}`, l'addition, l'élément neutre de l'addition, la multiplication, l'élément neutre de la multiplication :

La structure de corps résoud les équations en logique propositionnelle. Considérons 4 variables booléennes `x,y,z,t`. Chaque polynôme correspond à une propositions logiquement différentiable pour au moins une valeur booléenne de `x,y,z,t`. Donc pour savoir si deux propositions sont équivalentes, on les développe en polynôme sous forme normale pour savoir s'il s'agit du même polynôme. Cela donne l'algorithme de résolution par développement de polynômes.

6.3) Le treillis des booléens

Puis il existe un treillis des booléens caractérisé par la distributivité de `"∧"` sur `"∨"` et de `"∧"` sur `"∨"`.

Chaque proposition peut se décomposer en une conjonction de clauses ou symétriquement en une disjonction d'état :

Un littéral est une variable booléenne ou sa négation. Grace à la loi de Morgan, il est possible de supprimer la négation dans le corps des formules et de la garder que au niveau de la variable booléenne.

Cela donne l'algorithme de résolution par développement en une conjonction de clauses, ou en une disjonction d'états.

7) Algorithmes de résolution du calcul proportionnel

Voici 4 méthodes pour déterminer si une proposition est une tautologie, une antilogie, ou est indécidable :

7.1) La table de vérité

Cette méthode consiste à procéder à tous les testes possibles en attribuant aux variables booléennes `x_1,x_2,x_3,..., x_n ` à tour de rôle leur valeur possibles `0` ou `1`, soit `2^n` différentes valeurs booléennes possibles. S'il y a au moins un résultat égal à `1` alors la proposition est satisfaisable. S'il y a au moins un résultat égal à `0` alors la proposition est de négation satisfaisable. Et s'il a au moins un résultat égal à `0` et au moins un résultat égal à `1` alors la proposition est indécidable. Si les résultats sont toujours égaux à `0` alors la proposition est une antilogie. Si les résultats sont toujours égaux à `1` alors la proposition est une tautologie.

7.2) Algorithme de résolution par développement de polynômes.

On transcrit la proposition sous forme d'un polynôme dans un des corps booléens symétriques `sf"Corps"(B, "⊕",0,"∧",1)` ou bien `sf"Corps"(barB, "↔",1,"∨",0)`, qui sont des corps de caractéristique 2 que l'on renomme en `sf"Corps"(K,"+",0,"×",1)`.

La proposition se transcrit en un unique polynôme, une forme normale développée en enlevant les puissances doubles `x^2 = x` et en enlevant les monômes doubles `2x = x"+"x = 0`, puisque nous sommes dans un corps de caractèristique 2. La proposition est tautologique si elle est égale au polynôme `1`, elle est antilogique si elle est égale au polynôme `0`, et elle est indécidable si elle est égale à un polynôme autre que `0` ou `1`.

7.3) Le système axiomatique de Hilbert

Cette théorie utilise les connecteurs logiques `{¬, "⇒"}` qui sont suffisants pour engendrer tous les connecteurs logiques. Et elle utilise des inconnnus que l'on note `a,b,c,...` et qui jouent ici non pas le rôle de variable booléenne mais un rôle uniquement symbolique puisque la résolution s'opère uniquement de façon syntaxique. Les connecteurs n'opèrent pas de calcul booléen, ils ne sont que symboliques.

Puis on utilise des variables supplémentaires dites libres `A,B,C,...` et le connecteur de déduction `⊢` pour écrire les règles de déduction.

On accumule dans un sac toutes les propositions que l'on démontre. Les règles de déduction prennent des propositions présentes dans le sac et opère un calcul pour produire le cas échéant une nouvelle proposition que l'on rajoute dans le sac. Et il y a 4 règles de déductions :

La première règle s'appelle le modus ponens. Elle prend en entrée deux propositions présentes dans le sac, et si l'unification avec l'entête réussit, elle produit une nouvelle proposition que l'on rajoute dans le sac. Les 3 autres règles ont une liste vide comme entête et engendrent des propositions où `A,B,C` parcourent toutes les propositions du langage.

Ce moteur produit exactement l'ensemble de toutes les propositions tautologiques. Pour détecter les propositions indécidables, il faut un autre algorithme.

Si on commence l'algorithme avec un sac contenant une proposition initiale `P`, on produit alors exactement l'ensemble de toutes les déductions possibles de `P`.

7.4) Algorithme de résolution par développement en une conjonction de clauses, ou en une disjonction d'états.

On appelle littéral, une variable booléenne préfixé ou non par le connecteur de négation. Les littéraux sont `x`,`"¬"x`,`y`,`"¬"y`,`z`,`"¬"z`.... On appelle proposition une composition de connecteurs et de variables booléennes. On appel clause une disjonction de littéraux. On appel état une conjonction de littéraux.

On transcrit la proposition en utilisant que les connecteurs `"et"`, `"ou"` et des littéraux. Puis on développe en une disjonction d'états pour prouver la satisfaisabilité, ou en une conjonction de clauses pour prouver la satisfaisabilité de la négation.

7.4.1) Pour prouver l'antilogie d'une conjonction de clauses

Uns fois la proposition développée en une conjonction de clauses ce qui assure au moins la satisfaisabilité de sa négation, on applique l'algorithme suivant. Les règles de déduction du calcul propositionnel sont plus simples dans un langage logique n'utilisant qu'une conjonctions de clauses de littéraux. Une clause est un couple d'ensembles finis de variables booléennes `(A,B)`, le premier ensemble regroupe les variables affirmées dans la clause, et le second ensemble regroupe les variables négativées dans la clause. Par exemple :

On choisit une proposition `P` de départ que l'on décompose en une conjonction de clauses. On regroupe ces clauses de départ dans un sac. Chaque clause contenue dans le sac apporte une contrainte. Le sac correspond à une conjonction. Puis on accumule dans le sac, toutes les clauses que l'on démontre, et on supprime celles qui sont redondantes, jusqu'à déduire le "faux" (la clause vide) auquel cas la proposition est une antilogie, (ou jusqu'à obtenir un sac vide si toutes les clauses sont tautologiques à la suite d'une hypothèse extérieure, auquel cas la proposition est une tautologie). L'algorithme est défini en 5 règles :

Le moteur s'arrête si la conjonction contient la clause vide et auquel cas la proposition `P` est une antilogie, (ou si la conjonction devient vide et auquel cas la proposition `P` est une tautologie).

7.4.2) Pour prouver la tautologie

Par négation nous obtenons le mécanisme symétrique. Une fois la proposition développée en une disjonction d'états ce qui assure au moins sa satisfaisabilité, on applique l'algorithme suivant. Les règles de déduction du calcul propositionnel sont plus simples dans un langage logique n'utilisant qu'une disjonction d'états de littéraux. Un état est un couple d'ensembles finis de variables booléennes `(A,B)`, le premier ensemble regroupe les variables affirmées dans l'état, et le second ensemble regroupe les variables négativées dans l'état. Par exemple :

On choisit une proposition `P` de départ que l'on décompose en une disjonction d'états. On regroupe ces états de départ dans un sac. Chaque état contenu dans le sac apporte une solution. Le sac correspond à une grande disjonction. Il ne fait que réduire une solution plus générale.

Puis on accumule dans le sac, toutes les états possibles que l'on démontre avec ce jeu de règles symétriques, et on supprime ceux qui sont redondants, jusqu'à déduire le "vrai" (l'état vide) auquel cas la proposition est une tautologie, (ou jusqu'à obtenir un sac vide si tous les états sont antilogiques à la suite d'une hypothèse extérieur, auquel cas la proposition est une antilogie). L'algorithme est défini en 5 règles :

Le moteur s'arrête si la disjonction contient l'état vide et auquel cas la proposition `P` est une tautologie, (ou si la disjonction devient vide et auquel cas la proposition `P` est une antilogie).

7.5) Le système de déduction naturelle

Pour pouvoir étendre ce système de déduction à des langages logiques plus riches tel le langage logique du premier ordre, on va opter pour une cinquième méthode dite "naturelle" qui introduit et élimine chaque connecteur logique par une règle de déduction spécifique.

Mais celle-ci se définit dans le cadre d'une conjonction de propositions formant un ensemble de propositions sur lequel on applique des règles de transformations. Pour ne pas être tributaire de cet arbitraire, il faut considérer les autres ensembles de propositions évoqués au chapitre 6, à savoir, les conjonctions, les disjonctions, les parités, les imparités, les classes, et les suites croissantes et peut-être même d'une façon plus générale, les ensembles de variables booléennes munie d'un ordre partiel. Sans avancer davantage dans cette voie de travail, on peut parallèlement à cela proposer une approche beaucoup plus pragmatique et empirique, susceptible de produire immédiatement des applications, et qui stimulera davantage nos lecteurs car moins ingrate.

8) Résolution de la satisfaisabilité par la méthode de Newton

Pour rechercher la satisfaisabilité d'une proposition à l'aide de réseaux de neurones, on définie une logique continue où les valeurs logiques appartiennent à un intervalle réel `]0,1[` et où les connecteurs logique sont des fonctions analytiques. L'exigence de continuité nous oblige à prendre un domaine ouvert, ce qui peut paraître surprenant. Dans cette optique, le vrai absolu noté `1` et le faux absolu noté `0` sont hors domaine et n'apparaissent donc jamais. Les propositions peuvent être quasiment vrais ou quasiment fausses mais jamais complétement. Cela ne gène pas la recherche car la méthode de Newton procède par approximation en suivant les plus grandes pentes. (Et de même dans un réseau de neurone où l'apprentissage procède par approximation en suivant les plus grandes pentes dans la rétropropagation des erreurs.)

Le calcul que fait un neurone est une sigmoïde générique de `]0,1[` vers `]0,1[` et qui possède une raideur initialement fixée à `4pi`. (On peut aussi la fixer à `3pi` ou moins encore s'il y a beaucoup de niveaux de profondeur).

Si on répète cette transormation, on obtient une quasi-sigmoïde 2 à 3 fois plus raide. Le connecteur de négation correspond à une telle sigmoïde mais envoyant `0` sur `1` et envoyant `1` sur `0`, ce que l'on obtient en remplaçant dans la sigmoïde `f` la variable `x` par `1"-"x`.

Le connecteur de conjonction `x "et" y` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `xy`.

Le connecteur de disjonction `x "ou" y` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `x"+"y"-"xy`.

Le connecteur d'implication `x"⇒"y` qui est égal à `"¬"x "ou" y` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `1"-"x"+"y"-"(1"-"x)y` `=` `1"-"x"+"xy`

Le connecteur d'équivalence `x"⇔"y` qui est égal à `(x"⇒"y) "et" (y"⇒"x)` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `(1"-"x"+"xy)(1"-"y"+"xy)` `=` `1"-"x"-"y"+"xy"+"xy"-"x^2y"-"xy^2"+"x^2y^2`. On remplace `x^2` par `x` et `y^2` par `y`. Cela ne change pas la valeur résultat dans les cas `0` ou `1`. On obtient alors la formule `1"-"x"-"y"+"2xy` qui est du même degrés que celle des autres connecteurs binaires.

Le connecteur ou exclusif `x"⊕"y` qui est égal à `"¬"(x"⇔"y)` s'obtient en remplaçant dans la sigmoïde `f` la variable `x` par `1"-"(1"-"x"-"y"+"2xy)` `=` `x"+"y"-"2xy`

Etant donnée une formule `P(x_1,x_2,x_3...,x_n) = P(vec x)` celle-ci peut ainsi se traduire en une fonction continue de `"]"0,1"["^n` vers `]0,1[` comme composée des sigmoïdes qui la composent. Et il est alors possible de rechercher les extremums de cette fonction analytique par la méthode de Newton vectorielle. C'est une recherche des racines de la dérivée. Avec l'itération suivante :

9) La topologie de la logique du premier ordre

Si vous avez fait un peu de topologie vous aurez remarqué que des notions de topologies apparaissent dés qu'il est nécessaire de réunir ou de procéder à une intersection d'une infinités d'ensembles. Et c'est précisément le cas dans la logique du premier ordre pour interpréter les premières formules `AAxP(x)` et `EExP(x)`.

`x`	`y`	`x"∧"y`	`x"∨"y`	`x"→"y`	`x"↔"y`	`x"⊕"y`
0	0	0	0	1	1	0
0	1	0	1	0	0	1
1	0	0	1	1	0	1
1	1	1	1	1	1	0

Cardinal 3	Cardinal 2	Singleton	Ensemble vide
`{x,y,z}^"∧" ↔ (x"∧"y)"∧"z`	`{x,y}^"∧" ↔(x"∧"y)`	`{x}^"∧" ↔x`	`{}^"∧" ↔`1
`{x,y,z}^"∨" ↔ (x"∨"y)"∨"z`	`{x,y}^"∨" ↔(x"∨"y)`	`{x}^"∨" ↔x`	`{}^"∨" ↔`0
`{x,y,z}^"↔" ↔ (x"↔"y)"↔"z`	`{x,y}^"↔" ↔(x"↔"y)`	`{x}^"↔" ↔x`	`{}^"↔"↔`1
`{x,y,z}^"⊕" ↔ (x"⊕"y)"⊕"z`	`{x,y}^"⊕" ↔(x"⊕"y)`	`{x}^"⊕" ↔"¬"x`	`{}^"⊕" ↔`0

Cardinal 3	Cardinal 2	Singleton	Ensemble vide
`{x,y,z}^"=" ↔ (x"↔"y")∧("y"↔"z")`	`{x,y}^"=" ↔(x"↔"y)`	`{x}^"=" ↔`1	`{}^"=" ↔`1
`(x,y,z)^"→" ↔ (x"→"y")∧("y"→"z")`	`(x,y)^"→" ↔(x"→"y)`	`(x)^"→" ↔`1	`()^"→" ↔`1