On procède à une classification des théories d'égalité du premier ordre, à équivalence près, pour chaque langage rudimentaire décrit par une présentation de structure. Et on commence par la structure de présentation vide et d'ensemble sous-jacent `S`.
Les variables `bbx,bby,bbz...` sont notées en gras et sont quantifiées universellement sur `S`, le `"ou"` est noté à l'aide du symbole `|` et les théories sont représentées sous forme d'ensemble de clauses. Par commodité on notera la clause `bbx"="e_1"|"bbx"="e_2` par l'expression `bbx"∈"{e_1,e_2}`.
Dans une structure de présentation vide, c'est à dire composée uniquement d'un ensemble sous-jacent `S` sur lequel nous n'avons pas de connaissance, on a vite fait le tour des propriétés possibles d'égalité du premier ordre. Il existe exactement 2 théories possibles que sont :
Structure `(S)`
La théorie vide, S0, n'apporte aucune information d'égalité sur l'ensemble `S`.
La théorie S1 unifie tous les éléments de `S` entre eux. Et comme, rappellons le, la formule `(AA x in Ø, "faux")` est vrai, il peut ne pas y avoir d'élément du tout. Il y a soit aucun élément ou bien soit un seul élément. Elle désigne la structure vide `S = Ø` ou bien la structure à un seul élément `S = {x}`.
Si on munie la structure à l'aide d'un élément singulier `e`, alors il existe exactement 3 théories possibles que sont :
Structure `(S,e)`
Notez que le cas où il n'y a aucun élément n'est plus possible, car la présentation de `S` a ajouté l'existence de l'élément `e`. C'est une propriété existentielle que la théorie d'égalité ne peut pas formuler, et qui ne peut être formulé que par la présentation de la structure. Seul la présentation de la structure avance des propriétés existencielles.
La théorie S1 unifie tous les éléments à `e`. Elle désigne la structure à un seul élément `S={e}`.
La théorie S2 unifie tous les éléments entre eux qui ne sont pas `e` s'ils existent. Elle désigne soit la structure à un seul élément `S={e}` soit la structure à deux éléments `S = {e,x}`.
Si on munie la structure à l'aide de deux éléments singuliers `e_1, e_2` alors il existe exactement 7 théories possibles que sont :
Structure `(S,e_1,e_2)`
La théorie vide, S0, est la mère de toutes les théories. Elle représente la structure libre `(S,e_1,e_2)` en notation élémentarienne.
La théorie S1 décide que `e_1"="e_2`. Elle désigne les structures d'au moins un élément avec `e_1"="e_2`.
La théorie S2 désigne la structures ne comprenant qu'un élément `e_1`, et donc avec `e_1"="e_2`. Notez que la théorie `{bbx"="e_2}` est une théorie équivalente car elle désigne la structure ne comprenant qu'un élément `e_2`, avec donc `e_2"="e_1`.
La théorie S3 affirme qu'il n'existe pas d'éléments autre que `e_1` et `e_2`. Mais ne décide pas si `e_1` et `e_2` sont distinct.
La théorie S4 unifie les éléments entre eux autre que `e_1` mais ne décide pas si `e_1"="e_2`. Il peut ne pas y avoir d'éléments autre que `e_1` auquel cas nous aurons `e_2=e_1`. Elle désigne les structures de 1 ou 2 éléments avec pour les structures à 2 éléments deux cas distincts, soit `e_1=e_2` et le deuxième élément n'est pas mentionné dans la présentation et est désigné par la variable `x`, ou soit `e_1"≠"e_2` et il n'y a pas d' élément autre que `e_1` et `e_2`.
La théorie S5 unifie les éléments entre eux autre que `e_1` et décide que `e_1"="e_2`.
La théorie S6 unifie les éléments entre eux qui ne sont ni `e_1` ni `e_2` et ne décide pas si `e_1"="e_2`.
Ces théories d'égalité s'emboitent comme des poupées russes et forme un treillis. Chaque arête du treillis correspond à une clause qu'il faut ajouter pour passer d'une théorie à l'autre. Pour passer de la théorie S2 à la théorie S4 on ajoute la clause `bbx"="e_1|bby"="e_1|bbx"="bby`. Pour passer de la théorie S4 à la théorie S5 on ajoute la clause `e_1"="e_2`.
On notera au passage que l'ordre des éléments de la présentation `e_1` et `e_2` paradoxalement n'intervient pas dans la décomposition en ces 7 théories d'égalité. Si on munie la structure à l'aide de 3 éléments singuliers présentés dans un ordre précis, alors il existe un plus grand nombre de théories et l'ordre des éléments de la présentation intervient.
La description sémantique de ces théories ouvre les portes vers un nouveau langage qui reste à formaliser. Pour démontre l'équivalence entre deux théories sans l'avènement de ce langage, on est contraint de revenir aux sources du raisonnement et d'utiliser des règles formelles de déduction. L'ensemble de ces règles forme un corpus logique. A titre d'exemple on verra comment démontrer l'équivalence entre la théorie `{bbx"="e_1|bby"="e_1|bbx"="bby}` et la théorie `{bbx"="e_2|bby"="e_2|bbx"="bby}` à l'aide de ces seuls règles formelles de déduction.
Un semi-prédicat `A"(.)"` n'est utilisable qu'affirmativement. Sa négation n'est pas autorisé dans le langage des théories d'égalité.
Le semi-prédicat `A"(.)"` définie un sous-ensemble `A` de `S` comme suit :
`A(x) <=> x"∈"A`
Dans une approche constructive, le semi-prédicat `A"(.)"` est dit calculable mais sa négation ne l'est pas nécessairement. Autrement dit, si `x"∈"A` alors le calcul de `A(x)` donnera toujours une réponse affirmative en un temps fini, tandis que si `x"∉"A`, le calcul de `A(x)` peut ne jamais donner de réponse.
On s'interdit le droit d'invoquer la négation du semi-prédicat, `¬A"(.)"`, comme si celui-ci n'était pas calculable. Cela définit une limitation du langage logique des théories d'égalités du premier ordre. Dans une présentation de structure, la présence d'un prédicat sera interprété comme un semi-prédicat à défaut de précision contraire. La présentation de la structure délimite ainsi étroitement le langage des théories d'égalité sur cette structure.
Dans la logique élémentarienne, l'ensemble sous-jacent `S` est par principe énumérable. C'est à dire qu'il existe un énumérateur, un programme énumérant tous les éléments de `S`. Le semi-prédicat `A"(.)"` constitue aussi un programme donnant une réponse affirmative en un temps fini si on lui met en entré un élément de `A`. On peut alors programmer un énumérateur des éléments de `A`. Pour cela, on prend chaque élément `x` énuméré par `S` et on calcule `A(x)`, et sans attendre la réponse, on réitère pour les éléments énumérés suivant par `S`. Ainsi on lance plusieurs processus parallèles dont le nombre grossie indéfiniment. Et dès qu'un `A(x)` produit une réponse affirmative, on produit l'élément `x` en question. Le langage de programmation pour écrire formellement ce programme sort du sujet de notre exposé. Noter que l'aspect constructif reste basé sur la notion physique d'une machine idéale se développant indéfiniment mais toujours selon les principes de la physique classique.
Autrement dit le semi-prédicat `A"(.)"` définie l'ensemble `A` inclus dans `S` d'une façon constructive mais uniquement pour son intérieur. Le complémentaire de `A` dans `S` n'est pas définie de façon constructive. Autrement dit, `A` peut toujours énumèrer tous ses éléments, mais ne peut pas toujours énumèrer tous les éléments de son complémentaire dans `S`.
Dans une structure ne possédant qu'un semi-prédicat unaire, c'est à dire composée uniquement d'un ensemble sous-jacent `S` sur lequel nous n'avons pas de connaissance, et d'un prédicat unaire `A"(.)"` définie sur cet ensemble, mais de tel sorte que l'on n'a pas le droit d'évoquer sa négation, comme si le prédicat inverse `¬A"(.)"` n'était pas calculable, définissant ainsi une limitation du langage logique des théories d'égalité, on a vite fait le tour des propriétés possibles d'égalité du premier ordre sur une telle structure. Il existe exactement 5 théories possibles que sont :
Structure `(S, A"(.)")`
de littéraux
La théorie S1 affirme que tous les éléments sont dans `A`.
La théorie S2 unifie tous les éléments entre eux sans préciser où il se trouve.
La théorie S2 unifie tous les éléments qui sont en dehors de `A`, c'est à dire affirme que s'il existe un élément en dehors de `A` alors il est nécessairement unique. La théorie S3 unifie tous les éléments sans préciser où il se trouve. La théorie S4 unifie tous les éléments entre eux et le place dans `A` s'il en existe.
Si on ajoute à la structure un élément singulier `e`, alors il existe exactement ... théories possibles que sont :
Structure `(S, A(.), e)`
`e` est dans `A`. Tous les éléments sont dans `A`. Tous les éléments sont égaux à `e`. Soit `e` est dans `A`
Soit tous les éléments sont égaux à `e`.Tous les éléments autre que `e` sont dans `A`. Tous les éléments autre que `e` sont unifiés entre eux. Tous les éléments en dehors de `A` sont unifiés entre eux. Tous les éléments autre que `e` sont unifiés entre eux.
`{bbx"="e|bby"="e|A(bbx)|A(bby)|bbx"="bby}`
`{A(e), bbx"="e|bby"="e|bbx"="bby}`
`{bbx"="e|A(bbx), bbx"="e|bby"="e|bbx"="bby}`
`{A(bbx), bbx"="e|bby"="e|bbx"="bby}`
Le nombre minimum de variables universelles nécessaire pour exprimer une théorie d'égalité s'appelle sa dimension logique. Cette dimension va nous servir pour limiter la puissance de démonstration et explorer les démonstrations dans un ordre de leur complexitées.
Nous allons décrire un mécanisme de démonstration formelle en vue de l'automatiser. Nous aurons besoin des axiomes de l'égalité.
1) L'égalité est une relation symétrique. Il faudrait ajouter cet axiome `bbx"="bby"|"bby"≠"bbx`. Mais de façon plus astucieuse, on convient de l'intégrer dans la règle même de déduction ce qui évite de le poser comme axiome, faisant que pour unifier A=B avec C≠D on tente d'unifier A=B avec C≠D et on tente également d'unifier A=B avec D≠C.
2) L'égalité est une relation transitive. On ajoute l'axiome `bbx"="bbz|bbx"≠"bby|bby"≠"bbz` qui est de dimension logique 3, et qui n'est donc pas utilisé dans les deux premières dimensions.
3) L'égalité permet la substitution, à savoir si une proposition quelconque `P(a)` est vrai et que `a=b` alors la proposition `P(b)` est vrai. Nous intégrerons cet axiome dans la règle même de déduction ce qui évite de le poser comme axiome.
L'expression d'une théorie est une liste de clauses. On s'implifie cette liste en supprimant les clauses qui peuvent être déduite d'une seul clause déjà présente. On obtient une liste de clauses redondantes logiquement car comprenant de multiples déductions possibles.
Nous prenons à titre d'exemple la démonstration de l'équivalence entre les deux théories d'égalités suivantes :
`{bbx"="e_1|bby"="e_1|bbx"="bby}`
`{bbx"="e_2|bby"="e_2|bbx"="bby}`
On commence par démontrer l'implication de la première sur la seconde. On raisonne par l'absurde. On part d'une théorie composée de la négation de la seconde théorie et de l'affirmation de la première théorie que voici :
`EE u, EEv, AAbbx, AAbby, u"≠"e_2, v"≠"e_2, u"≠"v, bbx"="e_1|bby"="e_1|bbx"="bby`
Et on tente de démontrer une clause fausse ou vide, la clause vide étant une clause fausse. Tout se passe comme si on avait ajouté au langage deux éléments singuliers `u` et `v`. La théorie peut se noter alors plus simplement par :
`{u"≠"e_2,v"≠"e_2,u"≠"v,bbx"="e_1|bby"="e_1|bbx"="bby}`
Hypothèse : On met la théorie sous forme d'une liste de clauses numérotées :
`bbx"="bbz | bbx"≠"bby | bby"≠"bbz` `u"≠"e_2` `v"≠"e_2` `u"≠"v` `bbx"="e_1 | bby"="e_1 | bbx"="bby`
Déduction : La règle de déduction sur les clauses consiste à unifier un littérale affirmatif d'une clause avec un littérale négatif d'une autre clause et à produire la clause résultante réunissant ces deux clauses unifiées en enlevant les deux littéraux unifiées. Voici tout ce que l'on peut déduire de dimension 0 avec ce procédé :
`u"="e_1 | e_2"="e_1` `v"="e_1 | e_2"="e_1` `u"="e_1 | v"="e_1`
Ce seul procédé de déduction ne suffit pas à résoudre le problème.
Choix d'une alternative : On considère la première alternative rencontrée de dimension nulle `u"="e_1 | e_2"="e_1`. On considère alors 2 cas, et il faut montrer que chacun de ces deux cas est absurde, c'est à dire produire une clause fausse ou vide pour chacun des deux cas.
1er cas : On considére le cas, `u"="e_1`.
Substitution : Alors on remplace dans les formules e_1 par u :
Simplification des clauses : Les clauses triviales (5) et (7) sont toujours vrai et donc sont marquées ainsi :
`bbx"="bbz | bbx"≠"bby | bby"≠"bbz` `u"≠"e_2` `v"≠"e_2` `u"≠"v` `bbx"="u | bby"="u | bbx"="bby` Vrai `v"="u | e_2"="u` Vrai
Déduction de dimension au plus 1 :
`bbx"="u | e_2 "="bbx` `bbx"="v | e_2 "="bbx` `bbx"="u | v "="bbx` `e_2"="u`
Substitution : Alors on remplace dans les formules `e_2` par `u` et on obtient une clause fausse (1) `u"≠"u`
2ième cas : On considére le cas, `e_2"="e_1`.
Substitution : Alors on remplace dans les formules `e_2` par `e_1` :
`bbx"="bbz | bbx"≠"bby | bby"≠"bbz` `u"≠"e_1` `v"≠"e_1` `u"≠"v` `bbx"="e_1 | bby"="e_1 | bbx"="bby` `u"="e_1 | e_2"="e_1` `v"="e_1 | e_2"="e_1` `u"="e_1 | v"="e_1`
Déduction de dimension 0 :
---- 10 janvier 2016 ----