Le calcul propositionnel en logique classique est identique au calcul des équations booléennes. Les propositions élémentaires sont des inconnus booléens `x_1,x_2,x_3,...`, et les propositions sont les équations booléennes. Il y 4 méthodes pour déterminer si une proposition est une tautologie, une antilogie, ou un indécidable :
La méthode la plus structurée semble être par développement de polynômes dans le corps des booléens.
La logique ternaire va ajouter une valeur de vérité supplémentaire, et nous obliger à définir d'autres logiques. On verra dans quelle mesure ces nouvelles logiques peuvent contenir la logique classique initiale.
La logique propositionnelle classique traite des équations booléennes. Elle conçoit deux valeurs logiques, le faux représenté par la valeur `0` et le vrai représenté par la valeur `1`, que l'on regroupe en un ensemble `{0, 1}` appelé l'ensemble des booléens, et que l'on munit de l'addition `"+"` et du produit `"⁎"` pour former le corps des booléens, un corps à deux éléments noté `C_2` et qui est identique au corps `ZZ"/"2ZZ`. L'élément neutre de l'addition est `0`, l'élément absorbant de la multiplication est `0`, l'élément neutre de la multiplication est `1`. Les lois du corps `C_2` sont donc :
La priorié syntaxique de la multiplication est posée plus forte que celle de l'addition, faisant que `x"+"y"⁎"z` signifie `x"+"(y"⁎"z)` et non `(x"+"y)"⁎"z`, puis la multiplication est souvent notée par absence de symbole en juxtaposant simplement les termes, `x"+"yz`. On remarque que l'addition correspond au connecteur logique « ou exculsif », et que la multiplication correspond au connecteur logique « et ». Voici la correspondance pour les autres connecteurs :
Il existe une symétrie parfaite intervertissant les deux valeurs booléennes. Un même corps est définissable en permuttant le `0` avec le `1`, que l'on note `Ċ_2`. Celui-ci est muni d'une addition `"∔"`, et d'une multiplication `"⨰"`. L'élément neutre de l'addition est `1`. L'élément absorbant de la multiplication est `1`, L'élément neutre de la multiplication est `0`. Les lois du corps `Ċ_2` sont donc :
On remarque que l'addition correspond au connecteur logique « équivalent », et que la multiplication correspond au connecteur logique « ou ». Et voici la la correspondance pour les autres connecteurs :
Une équation logique portant sur `n` inconnus `x_1,x_2,...,x_n` est un polynome à `n` variables, égale à zéro dans le corps des booléens. Un polynome à coefficient dans un corps possède une forme normale réduite qui s'obtient en distribuant tous les produits sur les additions présentes, puis en sommant les monômes identiques. Le corps étant de caractéristique `2`, deux règles de simplification sont ajoutées `x x"="x`, `x"+"x"="0`, et il n'y a alors pas de coefficient autre que `1`. Un automate peut procéder à cette réduction en appliquant les règles suivantes aux sous-termes de l'équation jusqu'à épuisement des possibilités :
Distributivité droite Distributivité à gauche Caractéristique `2` Element absorbant Element neutre de `"+"` Element neutre de `"⁎"` Commutativité de `"⁎"` Commutativité de `"+"`
où `x,y,z` désignent des sous-termes, et `X,Y` désignent des inconnues d'indice distincts et dans l'ordre, et `alpha, beta` désignent des monômes dans l'ordre lexicographie.
L'équation est tautologique si et seulement si le polynome réduit est `0`. L'équation est antilogique si et seulement si le polynome réduit est `1`. Sinon elle est indécidable.
On introduit une troisème valeur logique, la valeur inconnue, qui est représentée par le point d'interrogation «`?`». C'est cette troisième valeur logique qui a été historiquement introduite en premier. La proposition `x"="?` apporte une information sur le monde qui s'accapare une part de notre subjectivité. Elle affirme que nous ne savons pas qu'elle est la valeur de vérité de `x`. Les valeurs de vérités sont regroupées dans l'ensemble des triléens `{0,1,?}`
Nous allons construire les mondes les plus simples servant de modèle pour cette nouvelle logique, Ce-sont ceux des univers de dimension `n`, comprenant `n` triléens `(x_1,x_2,x_3,...,x_n)`. Et dans un tel univers il a `3^n` mondes possibles. Dans une telle logique, la logique binaire n'a pas disparue. `0` désigne toujour la contradiction (ou l'antilogie), et `1` désigne toujours la tautologie. Et si les variables n'ont pas cette troisième valeurs de vérité, alors elles se comportent comme en logique classique. La troisième valeur de vérité va compléter la définition des connecteurs :
`x"⁎"y``x "ou" y` `x"⇒" y` `x "⇔" y` `x"="y`
On ajoute le connecteur d'égalité de valeur logique `"="`. Et on constate que :
`¬(x"="0) = (x"="1) "ou" (x"="?)`
`¬(x"="1) = (x"="0) "ou" (x"="?)`
`¬(x"="?) = (x"="0) "ou" (x"="1)`
Notez que le connecteur d'égalité ne retourne jamais la valeur logique «`?`» , et donc que les connecteur `"ou", "¬"`, évoqués dans ces 3 expressions se comportent comme le `"ou"` classique et le `"¬"` classique.
Puis on change la notation, on représente le vrai par `1`, l'inconnu par `0` et le faux par `-1`. L'ensemble des triléens devient `{-1,0,1}`. La négation correspond alors à l'opposé `-`, le `"ou"` correspond au minimum `"min"`, et le `"et"` correspond au maximum `"max"` :
`¬x = -x`
`x "ou" y = "min"(x,y)`
`x "et" y = "max"(x,y)`
Cette logique ternaire peut nous permettre de proposer un système de déduction naturel qui satisfait la propriété intuitive suivante :
`(( T"⊬"P) "et" (T"⊬"¬P)) <=> (P"="?)`
Notez que le connecteur de déduction `|--` ne retourne jamais la valeur logique «`?`», car il traduit une propriété mécanique qui ne peut pas être indéterminée, la propriétée d'être déductible (syntaxiquement) par le système de démonstration choisi. Et donc que les connecteurs `"et", <=>`, évoqués dans cette expression se comportent comme le `"et"` classique et le `<=>` classique.
On pose trois valeurs logiques formant le corps `C_3= ZZ"/"3ZZ`. L'élément neutre de l'addition `0` qui est aussi l'élément absorbant de la multiplication, représente la contradiction, les deux autres valeurs logiques représentes deux sortes de vérités disjointes et exhaustives. La méthode de reconnaissance d'une contradiction ou de l'une ou l'autre sorte de tautologie se fait par développement de polynômes dans le corps `C_3`.
On pose trois valeurs logiques formant le cycle `(0,1,2)`. La négation est définie par `¬x = x"+"1 "mod" 3`. Les trois valeurs sont symétriques. Dans cette logique, il n'y a pas de contradiction, juste 3 valeurs logiques d'égale importance. Voir Trilogique.
On reprend la logique de Kleene et Priest, et on modifie la table de vérité de l'implication afin que la proposition `?"⇒"?` soit vrai.
Pour simulé la superposition d'états quantiques, on considère qu'une variable logique peut avoir plusieurs valeur logique en même temps, et donc il peut y avoir jusqu'à `2^2-1"="3` valeurs logiques élémentaires `{0},{1},{0,1}` regroupées dans l'ensemble `ccP_(>0)({0,1})` `=` `ccP({0,1})-{Ø}`.
Puis un couple de variables logique `(x,y)` possède jusqu'à `2^(2^2)-1"="15` valeurs logiques possibles regroupées dans l'ensemble `ccP_(>0)({0,1}^2)` `=` `ccP({0,1}^2)-{Ø}`.
Puis un `n`-uplet de variable logique possède jusqu'à `2^(2^n)-1` valeurs logiques possibles regroupées dans l'ensemble `ccP_(>0)({0,1}^n)` `=` `ccP({0,1}^n)-{Ø}`.
Au lieu de définir un langage de construction des mondes, on définie un langage de construction des démonstrations, et qui aboutira à une logique au moins ternaire, puisque tout n'est pas démontrable. On utilise la logique classique pour construire une nouvelle logique basée sur des principes minutieusement choisis. Et on part du connecteur de démonstration de cette nouvelle logique `color(red)"⊢"`. Ce connecteur doit satisfaire deux axiomes qui nous parraissent incontournables :
`AAa, acolor(red)"⊢"a`
`AAaAAbAAc, acolor(red)"⊢"b" et " b color(red)"⊢"c => a color(red)"⊢"c`
Il convient de préciser que ces axiomes sont écrits dans la logique classique, où `a,b,c` sont des variables élémentaire en logique classique qui transporte des propositions de la nouvelle logique. Les quantificateurs `AA, EE` et les connecteurs `"et", "⇒"`, font partie de la logique classique tandis que le connecteur `color(red)"⊢"` n'est pas celui de la logique classique mais celui de la nouvelle logique que nous définissons. Les connecteurs de la nouvelle logique seront écrits en rouge, ce qui nous permettra de les différentier des connecteurs de la logique classique.
D'autre part, le connecteur de démonstration `color(red)"⊢"` n'est pas un connecteur librement choisi. Il est déterminé mécaniquement par le mécanisme de déduction de la nouvelle logique que nous définissons. Ainsi, ce connecteur a comme résultat toujours une valeur de vérité `"vrai"` ou `"faux"`, propre à la logique classique. Ce qui n'est pas le cas des propositions et des autres connecteurs de la nouvelle logique. C'est pourquoi les axiomes qui seront posés ne combinent que ce connecteur `"⊢"` avec les connecteurs de la logique classique.
Notez que la priorité syntaxique de l'implication est posée plus faible que celle de la conjonction, et que les priorités syntaxiques des connecteurs de la logique classique sont posées plus faibles que ceux de la nouvelle logique.
Déjà avec cet unique connecteur `"⊢"` et ces deux axiomes, on peut programmer un démonstrateur de théorème. On considère `n` inconnus `(a_1, a_2, a_3,...., a_n)`. Les propositions de la nouvelle logique sont des éléments du magma libre à `n` générateurs `("⊢(.,.)",a_1, a_2, a_3,...., a_n)` c'est à dire ce sont des arbres où les noeuds correspondent au connecteur `"⊢(.,.)"` et où les feuilles sont des éléments parmi `{a_1, a_2, a_3,...., a_n}`. A ce stade, seul le deuxième axiome, dit de transitivité, va être utilisé pour programmer le démonstrateur de théorème. Le premier axiome assure que les hypothèses peuvent être déduites des hypothèses, et se faisant, il n'est pas utile de séparer les hypotèses des déductions.
Etant donné une liste d'hypothèses `L_0`, qui correspond à un sous ensemble fini du magma, on passe en revue tous les couples de propositions `(x,y)` appartenant à `L_0"×"L_0` et on vérifie à l'aide d'un algorithme d'unification s'il est possible d'appliquer la production suivante :
`(acolor(red)"⊢"b", " b color(red)"⊢"c) -> a color(red)"⊢"c`
L'unification de `(x,y)` avec `(acolor(red)"⊢"b", " b color(red)"⊢"c)` va déclencher la production de `a color(red)"⊢"c`. Notez que `a,b,c` jouent le rôle de variables libres, tandis que les éléments du magma dont font partie les inconnues prélogiques `a_1, a_2, a_3,...., a_n` jouent le rôle de constantes distinctes.
Comme la négation n'est pas encore définie, l'axiome de transitivité se traduit bien par cette unique règle de production. On regroupe dans `L_1` les résultats de cette règle de production qui n'appartiennent pas déjà à `L_0`.
Puis on passse à l'étape suivante. On passe en revue tout les couples de propositions `(x,y)` appartenant à `L_0"×"L_1``"+"``L_1"×"L_0``"+"``L_1"×"L_1` et on regroupe dans `L_2` les résultats de cette règle de production qui n'appartiennent pas déjà à `L_0 "+" L_1`.
Puis on passse à l'étape suivante. On passe en revue tout les couples de propositions `(x,y)` appartenant à `(L_0 "+" L_1)"×"L_2``"+"``L_2"×"(L_0 "+" L_1)``"+"``L_2"×"L_2` et on regroupe dans `L_3` les résultats de cette règle de production qui n'appartiennent pas déjà à `L_0 "+" L_1 "+" L_2`.
Et ainsi de suite : On passe en revue tout les couples de propositions `(x,y)` appartenant à `(L_(<n))"×"L_n``"+"``L_n"×"(L_(<n))``"+"``L_n"×"L_n` et on regroupe dans `L_(n+1)` les résultats de cette règle de production qui n'appartiennent pas déjà à `L_(<(n+1))`.
Ainsi toutes les déductions sont énumérées, classées et ordonnées selon le nombre minimum nécessaire d'applications de la règle pour les produire. Ce système de déduction est dit prélogique car il ne contient pas la négation ni la contradiction. Ce procédé constitue une opération fondamentale qui justifie pleinement d'en faire un programme informatique programmation libre et open source, répertoriée comme une commande de base de calcul prélogique. Voir Commandes prélogiques.
On entend par implication forte, une implication syntaxique, qui est déterminée pour des raisons de syntaxe, autrement dit, qui est déductible. Le connecteur de déduction `"⊢"` constitue donc cette implication forte, dit aussi, implication syntaxique. Nous allons définir l'équivalence forte, ou dit aussi, l'équivalence syntaxique, que l'on désignera par le symbole `"⊢⊣"`. Ce connecteur est posé comme étant déterminé mécaniquement par le mécanisme de déduction de la nouvelle logique que nous définissons. Ainsi, il a comme résultat toujours une valeur de vérité propre à la logique classique, et peut donc être défini par l'axiome suivant :
`AAaAAb, a color(red)"⊢⊣"b <=> a color(red)"⊢"b "et" b color(red)"⊢"a`
Noter que la priorité syntaxique de l'équivalence est posée plus faible que celle de la conjonction, et rappelez-vous que les priorités syntaxiques des connecteurs de la logique classique sont posées plus faibles que ceux de la nouvelle logique.
On veut une négation qui soit totale, c'est à dire satisfaisant les deux axiomes :
`AAa, color(red)"¬¬"a color(red)⊢a`
`AAa, a color(red)⊢color(red)"¬¬"a`
---- 2 février 2021 ----
Par convention tout sous-terme de la forme `color(red)"¬"(acolor(red)"⊢"b)` est réécrit en le sous-terme `acolor(red)"⊬"b`, En d'autre terme nous définissons le connecteur de non déductibilité par l'axiome suivant :
`AAaAAb, color(red)"¬"(acolor(red)"⊢"b) <=> acolor(red)"⊬"b`
Mais cet axiome ne sera pas retenu dans la liste des axiomes fondamentaux, car c'est un axiome de définition nécessaire uniquement pour pouvoir utiliser le symbole `"⊬"` , un symbole qui n'est pas indispenssable.
---- 1 février 2021 ----
et donc en appliquant l'axiome nous avons `"¬"(a"⊬"b)⊢(a"⊢"b)`.
Puis on ne veut pas affirmer le principe du tier exclus, qui raménèrait la nouvelle logique à l'ancienne. Mais on admet le principe de la contraposé, qui constitue le quatrième axiome :
`AAaAAb, (acolor(red)"⊢"b) =>(color(red)"¬"bcolor(red)"⊢¬"a) `
---- 1 février 2021 ----
Déjà une partie de ce choix peut être introduit par l'axiome suivant :
`AAaAAb, color(red)"¬"a "et" bcolor(red)"⊢"a => color(red)"¬"b`
Le démonstrateur met alors 5 règles de production en oeuvre :
`color(red)"¬¬"a -> a`
`(color(red)"¬"a, bcolor(red)"⊢"a) -> acolor(red)"¬"b`
`(acolor(red)"⊢"b", " b color(red)"⊢"c) -> a color(red)"⊢"c`
`(acolor(red)"⊢"b", " a color(red)"⊬"c) -> b color(red)"⊬"c`
`(bcolor(red)"⊢"c", " a color(red)"⊬"c) -> a color(red)"⊬"b`
On remarque que l'axiome de transisitivé peut s'écrire sous forme d'une clause, puis sous forme d'implications de 3 façons possibles :
`AAaAAbAAc, "¬"(acolor(red)"⊢"b) "ou" "¬"(b color(red)"⊢"c) "ou" a color(red)"⊢"c`
`AAaAAbAAc, acolor(red)"⊢"b" et " b color(red)"⊢"c => a color(red)"⊢"c`
`AAaAAbAAc, acolor(red)"⊢"b" et " "¬"(a color(red)"⊢"c) => "¬"(b color(red)"⊢"c)`
`AAaAAbAAc, bcolor(red)"⊢"c" et " "¬"(a color(red)"⊢"c) => "¬"(a color(red)"⊢"b)`
Le premier choix qu'il convient de faire, est de faire coïncider la négation de la logique classique avec celle de la logique nouvelle uniquement sur leur rôle qu'elles ont dans ces trois implications, c'est à dire de faire le choix des trois axiomes suivant :
`AAaAAbAAc,`
`acolor(red)"⊢"b" et " b color(red)"⊢"c => a color(red)"⊢"c`
`acolor(red)"⊢"b" et " a color(red)"⊬"c => b color(red)"⊬"c`
`bcolor(red)"⊢"c" et " a color(red)"⊬"c => a color(red)"⊬"b`
Ce qui se trancrit par 4 règles de production :
`color(red)"¬¬"a -> a`
`(acolor(red)"⊢"b", " b color(red)"⊢"c) -> a color(red)"⊢"c`
`(acolor(red)"⊢"b", " a color(red)"⊬"c) -> b color(red)"⊬"c`
`(bcolor(red)"⊢"c", " a color(red)"⊬"c) -> a color(red)"⊬"b`
Et on applique le même algorithme de résolution.
Tout se passe comme si nous avions ajouté deux règles de production supplémentaires. Mais nous ne nous satisfaisons pas d'un tel choix arbitraire. Il existe un choix plus général et moins arbitraire, qui va entrainer de facto ces règles supplémentaires. C'est le choix d'autoriser la démonstration ab absurdo.
On choisit d'autoriser le raisonnement par l'absurde, un nouveau procédé de déduction pour notre nouvelle logique, qu'il nous faut décrire concrètement afin de pouvoir le transcrire sous forme d'axiome. Notre nouvelle logique ne possède que deux connecteurs `"¬(.)", "⊢(.,.)"`. Sans que nous ayant définie la conjonction, le connecteur `"et"`, nous avons un ensemble d'hypothèses qui constitue une conjonction de base et qui va être augmentée des déductions successives. Mais c'est la seule conjonction qui nous est autorisée d'utiliser. Le procédé consiste à chasser la contradiction, et il se décompose en 3 procédés. Le premier procédé introduit l'antilogie, notée `"⟘"` qui représente le faux. On repère la présence dans cet ensemble de base de deux propositions `(x,y)` s'unifiant à `(a, ¬a)`. Si une telle unification est possible alors cela produit la proposition antilogique :
`AAa, (a "et" color(red)"¬"a) color(red)(⊢ ⟘)`
Le second procédé définit le rôle de l'antilogie `"⟘"`. L'antilogie démontre toute proposition.
`AAa,color(red)(⟘ ⊢) a`
Le troisième procédé est le raisonement par l'absurde (ab absurdo) :
`AAa,(acolor(red)(⊢ ⟘) )color(red)(⊢)color(red)"¬"a`
Reste que ce procédé ab absurdo ne peut s'utiliser que si on fait une hypothèse, c'est à dire que l'on avance une proposition ne figurant pas déjà dans la base de connaissance, et qui peut être n'importe quelle proposition...
---- 27 janvier 2021 ----