 |
Sommaire :
Tout problème, aussi complexe soit-il, soumis à notre analyse, se ramène à des sous problèmes élémentaires transcris dans un langage simple et obéissant à une logique triviale. Notre esprit étant limité, il ne serait pas capable d'analyser un problème complexe sans le diviser en parties plus simples. Et la rigueur mathématique nous oblige à utiliser une logique totalement vérifiable et objective, donc triviale. C'est pourquoi la construction de la logique commence par le calcul booléen, le plus simple des calculs.
Un connecteur booléen d'arité `n` est une application de `{0,1}^n->{0,1}`. Voici le nombre de connecteurs booléens existants en fonction de leur arité :
Un connecteur booléen d'arité `n` est dit dégénéré s'il existe une de ses entrées qui ne transmet jamais d'information sur le résultat. Dans ce cas, l'entrée en question peut être enlevée et le connecteur peut d'être défini avec une arité `n"-"1`.
On retient donc comme connecteur unaire, seulement `2` connecteurs que sont l'identité et la négation `{id,"¬"}`
Il apparait alors une symétrie essentielle qu'est la négation.
Il convient alors de ne retenir que le booléen `1` sachant que `0 = "¬"1`, et de ne retenir parmis les connecteurs unaires que la négation `¬` sachant que `id = "¬¬"`
Sur les `16` connecteurs binaires, seuls `10` ne sont pas dégénérées. On les regroupe deux par deux avec leur négation. On classe donc les connecteurs binaires en `5` sous-ensembles :
`{"⇒", "⇏"}, {"⇐", "⇍"}, {"∧", "⊼"}, {"∨", "⊽"}, {"⇔", "⇎"}`
Puis on introduit une autre symétrie propre aux opérations d'arités supérieur à `1` qui consiste à permuter les entrées. On ne retient alors comme groupe de connecteurs binaires, que les `4` groupes suivants que l'on appelle ; implication, conjonction, disjonction et équivalence :
`{"⇒", "⇏", "⇐", "⇍"}, {"∧", "⊼"}, {"∨", "⊽"}, {"⇔", "⇎"}`
Ainsi nous considérons seulement `6` connecteurs booléens de base :
Voici un moyen mémotechnique pour savoir qu'elle symbole représente le ou logique et le et logique : Le ou logique correspond à l'union `uu` et au symbole `vv` tandis que le et logique correspond à l'intersection `nn` et au symbole `^^`.
Sur les `256` connecteurs ternaires, il faut retirer `2+2"*"3+10"*"3` connecteurs dégénérées. Et en les regroupant avec leur négation et à permutation près des entrés, on obtient alors `(256-2-2"*"3-10"*"3)"/"(2"*"6)` `=` `216"/"12` `=` `18` groupes de connecteurs.
On définie le langage de connecteurs booléens par la présentation des `6` connecteurs de base :
`L = {1, ¬"(.)", "⇒(.,.)", "∧(.,.)", "∨(.,.)", "⇔(.,.)"}`
La présentation du langage est simplement un ensemble de connecteurs. L'arité de chaque connecteur est précisée par le suffixe `"(.)"` pour unaire, `"(.,.)"` pour binaire, et par absence de suffixe pour l'arité zéro.
Une formule du langage est une composition close de connecteurs appartenant à la présentation. Une formule constitue un arbre où les noeuds sont des connecteurs booléens et où les fils sont les entrés du connecteurs, et où les feuilles sont l'unique booléen `1`. Par exemple, considérons la formule suivante :
`(("¬"1) vv 1) => (("¬"1) ^^ ("¬"1))`
Cette formule constitue l'arbre suivant :
Chaque formule s'évaluent en une valeur booléenne `0` ou `1`.
Pour simplifier l'écriture on munie les connecteurs booléens d'une priorité syntaxique, de la plus prioritaire à la moins prioritaire comme suit :
Ainsi la formule précédente peut s'écrire :
`"¬"1 vv 1 => "¬"1 ^^ "¬"1`
L'ensemble des formules engendrées par `L` se note `L^•`. Le symbole de Kleene généralisé`•` mis en exposant, représente la clôture par emboitement clos.
On ajoute au langage, `n` variables booléennes `x_1, x_2, x_3, ..., x_n`. Une variable booléenne est un connecteur d'arité zéro qui retourne une valeur booléenne. Mais cette valeur booléenne est inconnue, `0` ou `1`, c'est pourquoi la variable booléenne posssède un nom et n'est pas directement représentée par sa valeur. Les noms des variables sont ordonnés par défaut selon l'ordre lexicographique. Le nombre `n` est appelé la dimension du langage et correspondra à la dimension de l'univers associé.
Une formule de ce langage est dite de dimension `n`. Et comme l'expression d'une formule est implicitement interprété être égale à la valeur booléenne true, c'est à dire égale à `1`, elle représente donc une équation booléenne à `n` variables.
Notez que la conception de la variable booléenne introduite ici est classique, c'est à dire définie selon la mécanique classique. A savoir que la variable inconnue possède assurement une valeur et que cette valeur est exclusive parmi `{0,1}`. En particulier, elle ne peut pas être à la fois `0` et `1`, ni être ni `0` ni `1`.
Le langage de connecteurs booléens `L^•`, augmenté par exemple de `4` variables booléennes `x_1, x_2, x_3, x_4`, se note comme une extension élémentaire :
`L^•[x_1, x_2, x_3, x_4] = (L uu {x_1, x_2, x_3, x_4})^•`
C'est le langage de connecteurs booléens engendré par :
`x_1, x_2, x_3, x_4, 1, "¬", "⇒", "⇔", "∧", "∨"`
Une formule de ce langage est un emboitement clos de connecteurs et de variables booléennes.
Chaque formule du langage `L^•[x_1, x_2, x_3, x_4]` correspond à un nouveau connecteur booléen d'arité `4`, qui peut alors s'appliquer à un quadruplet de valeurs booléennes pour produire un résultat booléen `0` ou `1`. Et la formule ne désigne pas seulement une application de `{0,1}^4"→" {0,1}` mais désigne un programme informatique qui calcul les valeurs de cette application.
Considérons une formule `varphi` du langage `L^•[x,y,z]`. Et considérons `3` booléens `x,y,z`. La formule `varphi` est non seulement une application, qui appliquée au triplet `(x,y,z)` va produire un booléen noté `varphi(x,y,z)`, mais également le programme informatique qui va calculer cette valeur. Elle possède une complexité de calcul que l'on définie comme étant égale à la taille de la formule, c'est à dire au nombre de mentions de connecteurs y figurant. Par exemple, la formule `"¬"x vv y => "¬"z ` est de taille `7`.
Tout connecteur booléen binaire `P"(.,.)"` admet un symétrique obtenu par négation, un symétrique obtenu par négation du premier de ses arguments, un symétrique obtenu par négation du second de ses arguments, et un symétrique obtenu par permutation de ses arguments. On définie formellement ces `4` symétries comme suit :
La permutation `s` est définie par : `s(P)(x,y) = P(y,x)`
La négation `n_1` est définie par : `n_1(P)(x,y) = P("¬"x,y)`
La négation `n_2` est définie par : `n_2(P)(x,y) = P(x,"¬"y)`
La négation `n` est définie par : `n(P)(x,y) = "¬"P(x,y)`
Et nous avons :
Autrement dit, le groupe de symétrie `"<"s,n,n_1 ,n_2">"` est commutatif et chacun de ses éléments est nilpotent d'ordre `2`.
Considérons une formule sous forme d'un arbre. Chacune des symétries `n`, `n_1`, `n_2`, `s` peut transformer un noeud de l'arbre. Et si on modifie inversement, son flag de négativité, les flags de négativité de ses fils, ou l'ordre de ses fils, de telle sorte que la modification s'annule, on obtient alors une formule syntaxiquement différente mais sémantiquement identique. L'arbre est modifié syntaxiquement mais ne change pas sémantiquement.
Schéma |
Exemples |
Symétries génératrices |
||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
  |
P = `x "∧" y` Q = `x "∨" y` R = `(x "∧" y) "∨" z` S = `x <=> y` |
|
On définie ainsi une relation d'équivalence dans le langage de connecteurs, notée `=_sigma`, qui considère équivalent deux formules si on peut passer de l'une à l'autre par une succession de telles transformations. Par exemple la formule `x "∨" y` et la formule `"¬"x" ⊼" "¬"y` sont équivalentes, ce qui se note :
`(x "∨" y) =_sigma ("¬"x "⊼" "¬"y)`
Chaque connecteur binaire * possède des propriétés algébriques plus ou moins intéressantes. Voici un tableau répartissant les connecteurs selon quelques propriétés algébriques utiles :
la propriété algébrique
Dans la construction des outils logiques, il paraît pertinent de construire d'abord les opérations booléennes multi-aires associatives et commutatives, puis de construire leurs négations. Construire signifie programmer. Il convient donc de programmer ces opérations booléennes multi-aires.
Il existe `4` connecteurs booléens binaires qui sont associatifs : `"∧", "∨", "⇔", "⇎"`
Un connecteur associatif peut être considéré comme un connecteur d'arité variable, c'est à dire s'appliquant à une liste finie d'arguments, et s'il est de plus commutatif, le connecteur peut être considéré comme s'appliquant à un multi-ensemble fini d'arguments, et que nous appellons aussi un sac fini d'arguments. Les `4` connecteurs associatifs sont commutatifs et peuvent donc s'appliquer à un sac fini `A` d'arguments.
On adopte la notation suivante. On note entre braquette `(: :)` le nom du sac d'arguments. Et pour simplifier l'écriture, on note simplement entre double accolades `⦃⦄` les arguments. Ainsi, étant donné un sac `A` d'arguments, par exemple `A = ⦃x_1,x_2,x_3⦄`, nous avons :
`"∧"(:A:) = "∧"(:⦃x_1,x_2,x_3⦄:) = "∧"⦃x_1,x_2,x_3⦄ = x_1∧x_2∧x_3`
Les `4` connecteurs booléens binaires associatifs et commutatifs se définissent comme des connecteurs s'appliquant à un sac d'arguments, comme suit :
Toutes les arguments appartenant à `A` valent `1`. Il existe au moins un argument appartenant à `A` qui vaut `1`. Il y a un nombre impair d'arguments appartenant à `A` et valant `1`. Il y a un nombre pair d'arguments appartenant à `A` et valant `0`.
Et des définition ainsi choisies, nous déduisons que :
La conjonction unaire affirme son élément. La disjonction unaire affirme son élément. L'imparité affirmative unaire affirme son élément. La parité réfutative unaire affirme son élément.
La conjonction vide est vrai. La disjonction vide est fausse. L'imparité affirmative vide est fausse. La parité réfutative vide est vrai.
Remarquez qu'il existe deux niveaux d'évaluation, et donc deux niveaux d'égalité, notée `-=` et notée `=`. Etant donné deux formules `varphi_1` et `varphi_2`. L'expression `varphi_1 -= varphi_2` signifie que ce sont les mêmes formules du langage `L^•[x_1, x_2, x_3, ..., x_n]`. Et l'expression `varphi_1 = varphi_2` signifie qu'elles ont même valeurs booléennes c'est à dire que `varphi_1 <=> varphi_2`.
Remarquez qu'une variable booléenne peut désigner la valeur logique de n'importe quelle formule. Ce faisant au lieu de faire référence à une formule quelconque qui constitue un objet un peu abstrait, on fera souvent référence à une nouvelle variable booléenne qui aura alors, d'une certaine façon la même porté symbolique, la variable booléenne pouvant s'unifier à n'importe quelle formule.
La négation de ces `4` connecteurs introduit `4` autres connecteurs s'appliquant à des sacs d'arguments : `"⊼","⊽",bar"⇎",bar"⇔"`
Il existe au moins un argument appartenant à `A` qui vaut `0`. Toutes les arguments appartenant à `A` valent `0`. Il y a un nombre pair d'arguments appartenant à `A` et valant `1`. Il y a un nombre impair d'arguments appartenant à `A` et valant `0`.
Et nous avons :
Le non-et unaire réfute son élément. Le non-ou unaire réfute son élément. La parité affirmative unaire réfute son élément. La imparité réfutative unaire réfute son élément.
Le non-et vide est faux. Le non-ou vide est vrai. La parité affirmative vide est vrai. L'imparité réfutative vide est fausse.
Remarquez que les opérations booléennes "⊼" et "⊽" ne sont pas associatives. Parcontre les opérations booléennes multi-aires `bar"⇎"` et `bar"⇔"` le sont.
La loi De Morgan, qui porte le nom du mathématicien et logicien britanique Auguste (ou Augustus) De Morgan (1806 Madurai - 1871 Londre) né en Inde, décrit les identitées suivantes :
`"¬" (x ^^y) = ("¬"x vv "¬"y)`
`"¬" (x vv y) = ("¬"x ^^ "¬"y)`
Par récurrence, la loi De Morgan affirment qu'une expression logique n'utilisant que des connecteurs `¬, ^^, vv` et des variables, peut être négativée en permuttant les connecteurs `^^`, `vv` et en négativant chaque variable. Ainsi par exemple nous avons :
`"¬"((x ^^ "¬"y) vv "¬"z) = (("¬"x vv y)^^ z)`
Et la loi De Morgan peut s'écrire à l'aide des connecteurs booléens d'arité variables `^^, vv` s'appliquant à un sac fini de variables booléennes :
`"⊼"⦃x_1,x_2,x_3,...,x_n⦄ = "∨"⦃"¬"x_1,"¬"x_2,"¬"x_3,...,"¬"x_n⦄`
`"⊽"⦃x_1,x_2,x_3,...,x_n⦄ = "∧"⦃"¬"x_1,"¬"x_2,"¬"x_3,...,"¬"x_n⦄`
Une loi plus triviale, dite loi de parité, s'applique sur le ou exclusif `"⇎"` et l'équivalence `"⇔"`.
La formule `"⇎"⦃x_1,x_2,x_3,...,x_n⦄` ainsi que la formule `"⇔"⦃x_1,x_2,x_3,...,x_n⦄` sont équivalentes lorsque `n` est impair, et sont donc la négation l'une de l'autre lorsque `n` est pair. De même la formule `bar"⇎"⦃x_1,x_2,x_3,...,x_n⦄` ainsi que la formule `bar"⇔"⦃x_1,x_2,x_3,...,x_n⦄` sont équivalentes lorsque `n` est impair, et sont donc la négation l'une de l'autre lorsque `n` est pair.
De plus, ces deux expressions peuvent être négativées en négativant un nombre impair quelconque de leurs arguments, et sont laissées invariants en négativant un nombre pair quelconque de leurs arguments.
Et cela s'applique également à leur négation multi-aires, formant ainsi `4` connecteurs multi-aires au comportement similaire :
L'imparité affirmative `"⇎"(:A:)`
La parité réfutative `"⇔"(:A:)`
La parité affirmative `bar"⇎"(:A:)`
L'imparité réfutative `bar"⇔"(:A:)`
Ces `4` connecteurs multi-aires sont ici appliqués à un sac fini quelconque d'arguments `A`. Par définition, nous avons :
`bar"⇔"(:A:) = ¬ "⇔"(:A:)`
`bar"⇎"(:A:) = ¬ "⇎"(:A:)`
Si `|A|` est impair, alors `"⇎"(:A:) = "⇔"(:A:)`
Si `|A|` est pair, alors `"⇎"(:A:) = ¬ "⇔"(:A:)`
Si `|A|` est impair, alors `bar"⇎"(:A:) = bar"⇔"(:A:)`
Si `|A|` est pair, alors `bar"⇎"(:A:) = ¬ bar"⇔"(:A:)`
Ces quatres connecteurs multi-aires peuvent être négativées en négativant un nombre impair quelconque de leurs arguments, et sont laissées invariants en négativant un nombre pair quelconque de leurs arguments.
On utilise abusivement l'égalité répétée telle que `a"="b"="c"="d` sans parenthèse pour désigner en faite `(a"="b) "∧" (a"="c) "∧" (a"="d)`. Il en est de même pour l'équivalence `⇔` et la disjonction exclusif `⇎`, mais on s'interdit une telle notation car elle désigne deux autres opérateurs que sont l'imparité réfutative et la parité affirmative.
On définie l'équivalence répété, notée `hat"⇔"`, ainsi que la disjonction exclusive répétée, notée `hat"⇎"`, comme suit :
Toutes les arguments appartenant à `A` sont égaux en valeur. Il existe exactement un seul argument appartenant à `A` valant `1`.
Par exemple, pour 4 arguments, l'imparité réfutative, qui est associative, est définie comme suit :
`"⇔"⦃x,y,z,t⦄ = x"⇔"y"⇔"z"⇔"t`
Et la parité affirmative, qui est associative, est définie comme suit :
`"⇎"⦃x,y,z,t⦄ = x"⇎"y"⇎"z"⇎"t`
Et l'équivalence répétée, qui n'est pas associative, est définie comme suit :
`hat"⇔"⦃x,y,z,t⦄ = (x"⇔"y)"∧" (x"⇔"z) "∧" (x"⇔"t)`
Et la disjonction exclusive répété qui n'est pas associative, est définie comme suit :
`hat"⇎"⦃x,y,z,t⦄ = (x"∧¬"y"∧¬"z"∧¬"t)"∨"("¬"x"∧"y"∧¬"z"∧¬"t)"∨"("¬"x"∧¬"y"∧"z"∧¬"t)"∨" ("¬"x"∧¬"y"∧¬"z"∧"t)`
Et des définitions ainsi choisies, nous déduisons que :
L'équivalence répété unaire est vrai. Le ou exclusif répété unaire affirme son élément.
L'équivalence répété vide est vrai. Le ou exclusif répété vide est faux.
Mais attention, ces deux opérations `hat"⇔"` et `hat"⇎"` ne sont pas associatives.
Leur négation définie deux autres connecteurs multi-aires que sont `barhat"⇔"` et `barhat"⇎"` définis comme suit :
Il existe un argument appartenant à `A` valant `0`,
et il existe un argument appartenant à `A` valant `1`.Tous les aguments appartenant à `A` valent `0`,
ou bien il existe deux arguments appartenant à `A` et valant `1`.
Le langage utilisé pour définir ces opérateurs booléens multi-aires peut être formalisé pour constituer un langage sous-jacent pertinant.
L'univers contient tous les mondes possibles. Un monde détermine la valeur boléenne de chaque variable du langage. Les mondes sont les modèles de la logique booléenne.
Dans un langage de dimension `n`, il y a `n` variables booléennes. Chaque monde précise la valeur de ces `n` variables et correspond donc au `n`-uplet de booléens constitué des valeurs des variables booléennes disposées selon un ordre des noms de variables préalablement défini et qui est par defaut l'ordre lexicographique. L'univers est l'ensemble de tous les mondes c'est à dire l'ensemble des `n`-uplets de booléens `{0,1}^n`.
Dans un langage de dimension `4` tel que `L^•[x,y,z,t]`, une formule constitue un programme qu'est le programme d'évaluation de la formule en question sur l'entrée `(x,y,z,t)`. Une formule constitue un nouveau connecteur d'arité égale à la dimension du langage. Sa table de vérité qui donne sa valeur pour chaque valeur possible de `(x,y,z,t)` se met sous forme d'une liste de vérité en rangeant les mondes selon l'ordre prédéfini des noms de variable et selon l'ordre big-endian. Notez que cette liste de vérité se code en un entier qui est le numéro d'un méga-monde dans l'univers de dimension `2^4`.
La lecture se fait ici conventionellement de gauche à droite. C'est pourquoi, dans une transmission de caractères notée par exemple par la liste `ABCDEFG`, le premier caractère transmis est `A` c'est le caractère situé à gauche de la liste, et le dernier caractère transmis est `G` c'est le caractère situé à droite de la liste.
Les mondes sont codés et numérotés comme suit :
booléens
de booléens
de booléens
Par exemple, l'entier `20` s'écrit en binaire big-endian par `10100`. Big-endian signifie gros bout d'abord. Le premier bit transmis est de poids le plus important, il apporte ici une contribution de `0` ou `2^4` selon qu'il est `0` ou `1`.
Inversement, l'entier `20` s'écrit en binaire little-endian par `00101`. Little-endian signifie petit bout d'abord. Le premier bit transmis est de poids le plus faible, il apporte ici une contribution de `0` ou `1` selon qu'il est `0` ou `1`. Le suivant apportera une contribution de `0` ou `2^1`. Le suivant apportera une contribtion de `0` ou `2^2`, etc..
Les mondes sont codés et rangés selon l'ordre des noms de variables `x_1,x_2,x_3,x_4,x_5...` et selon l'ordre big-endian. Ainsi dans un univers de dimension `5`, le monde désigné par l'entier `20` s'obtient en décomposant binairement l'entier `20` en `5` booléens `10100`. Le monde n°`20` est le monde où nous avons `x_1"="1, x_2"="0, x_3"="1, x_4"="0, x_5"="0`.
Par exemple dans le langage `L^•[x,y,z]`, considérons la formule `x ^^ y => z`. Les mondes sont numérotés dans cet ordre :
La liste de vérite de la formule `x ^^ y => z` est `11111101`, et correspond donc à l'entier `1+4+8+16+32+64+128` `=` `253`. Cet entier est le numéro d'un méga-monde dans l'univers de dimension `2^3`.
Dans le cas générale, le numéro d'un monde en big-endian est :
On remarque alors qu'il existe une autre codification plus simple, qui est en little-endian et où les variables sont numérotées en commençant par zéro.
L'abstraction passe par l'univers à `n` dimensions booléennes, qui est l'ensemble des mondes noté `Omega`, et par l'ensemble des ensembles de mondes noté `ccP(Omega)`
Ensemble des mondes : Ensemble des ensembles de mondes :
Considérons le langage `L^•[x,y,z,y]`. Dans chaque monde `(x,y,z,t)`, chaque formule s'évalue en une valeur booléenne. On dira qu'un monde `(x,y,z,t)` satisfait la formule `varphi`, ou que `varphi` est satisfaite dans le monde `(x,y,z,t)`, ou simplement que `varphi` est vrai dans le monde `(x,y,z,t)` si et seulement si `varphi(x,y,z,t) = 1`, et on notera :
`(x,y,z,t)|==varphi <=> varphi(x,y,z,t)"="1 <=> varphi(x,y,z,t)`
Comme toute formule `varphi` est un connecteur booléen dont le résultat dans chaque monde `m` est soit `varphi(m)"="0` ou soit `varphi(m)"="1`, si un monde `m` ne satisfait pas `varphi` alors c'est que `m` satisfait `¬varphi`. Nous avons :
`(x,y,z,t)⊭varphi <=> varphi(x,y,z,t)"="0 <=> ¬varphi(x,y,z,t) <=> (x,y,z,t)|==¬varphi`
Cette notion de satisfaisabilité va nous permettre de définir ce qu'est une vérité sémantique, ce qu'est une conséquence sémantique, et de façon plus générale ce qu'est une opération sémantique et ce qu'est la valeur sémantique d'une formule.
La valeur sémantique d'une formule est l'ensemble des mondes satisfaisant la formule en question.
On généralise la notion de satisfaisabilité `|==` en l'étendant pour son premier membre aux ensembles de mondes comme suit : Etant donné `W` un ensemble de mondes appartenant à l'univers, et `varphi` une formule appartenant au langage. On dit que `W` satisfait `varphi` et on note `W|==varphi` si et seulement si tous les mondes appartenant à `W` satisfont `varphi`.
`W|==varphi <=> AAm "∈" W, m|==varphi <=> AAm "∈" W, varphi(m)`
Et donc comme toute formule `varphi` est un connecteur booléen dont le résultat dans chaque monde et soit `0` ou soit `1`, si un ensemble fini de mondes `W` ne satisfait pas `varphi` alors c'est qu'il existe un monde `m "∈" W ` qui satisfait `¬varphi`. Notez que l'univers étant fini, ce monde `m` est calculable. Nous avons :
Puis, étant donnée deux formules `T` et `varphi`. On dira que `varphi` est une conséquence sémantique de `T` si et seulement si `varphi` est vrai dans tout monde où `T` est vrai, et on notera :
`T|==varphi`
Pour pouvoir écrire cette expression, on adopte une conversion implicite. Là où on attend un monde ou un ensemble de monde, si une formule est apportée, elle est interprétée alors par sa valeur sémantique, comme l'ensemble des mondes la satisfaisant. Ainsi, à gauche du méta-opérateur `|==`, une formule `T` est interprétée comme l'ensemble des mondes satisfaisant `T`.
On remarque alors qu'en interprétant également le second membre comme un ensemble de mondes et en adoptant la même conversion implicite, alors l'opérateur de conséquence logique sémantique `|==` est identique à l'opérateur d'inclusion `sube` opérant sur l'ensemble des ensembles de mondes. Ainsi l'expression `T|==varphi`, qui se prononce « `T` satisfait `varphi` », signifie que l'ensemble des mondes satisfaisant `T` est inclus dans l'ensemble des mondes satisfaisant `varphi` ce que l'on note `T sube varphi`.
`T"⊨" varphi <=> AAm "⊨" T, m"⊨"varphi`
`T"⊨" varphi <=> AAm, m"⊨"T => m"⊨"varphi`
`T"⊨" varphi <=> AAm, T(m) => varphi(m)`
Par ailleurs :
`T = {m "/" m|==T} = {m "/" T(m)}`
`varphi = {m "/" m|==varphi} = {m "/" varphi(m)}`
Donc :
`T"⊨" varphi <=> AAm, T(m) => varphi(m)`
`T"⊨" varphi <=> {m "/" T(m)} ⊆ {m "/" varphi(m)}`
`T"⊨" varphi <=> T"⊆"varphi`
Et donc l'expression `T sub varphi` signifie non seulement que `varphi` est une conséquence sémantique de `T` mais que `T` n'est pas une conséquence sémantique de `varphi`, ou autrement dit, que tout monde satisfaisant `T` satisfait `varphi` mais qu'il existe au moins un monde satisfaisant `varphi` qui ne satisfait pas `T`.
Il y a deux points de vue de la vérité ; un point de vue syntaxique qu'est la formule `varphi` à transformation près selon les règles syntaxiques de déduction que nous allons décrire, et un point de vue sémantique qui est l'ensemble des mondes satisfaisant la formule `varphi`.
Etant donnée une formule `varphi`. On dira que `varphi` est une vérité sémantique si et seulement si `varphi` est vrai dans tous les monde et on notera :
`|==varphi`
Pour pouvoir écrire cette expression, on donne un sens à la formule vide. La formule vide est considérées comme vrai dans tous les mondes. La formule vide est équivalente à la formule `1`. Et s'il n'y a pas d'argument à gauche de l'opérateur `|==`, cela correspond à l'argument constitué par la formule vide, et cela est interprété comme l'ensemble de tous les mondes. Ainsi l'expression `|==varphi` signifie que `varphi` est vrai dans tous les mondes, et constitue donc une vérité sémantique.
`"⊨"varphi <=> 1"⊨"varphi <=> AAm, m"⊨"varphi <=> AAm, varphi(m)`
Notez qu'il ne faut pas confondre l'ensemble vide notée `Ø`, avec la formule vide notée `1`. En effet, un ensemble vide de monde `Ø` satisfait toutes les formules et leur négation car il est inclus dans tout ensemble de mondes, alors que la formule vide représente la formule `1` et donc représente l'ensemble de tous les mondes `Omega`, et donc ne satisfait que les formules vrais dans tous les mondes.
A chaque connecteur booléen binaire correspond une opération sémantique de `Omega"×"Omega->Omega` écrite pareillement mais en rouge pour la distinguer :
Le `0` désigne l'ensemble vide, c'est à dire `Ø`. L'ensemble vide est inclus dans tous les ensembles de mondes, c'est pourquoi il satisfait toutes les formules et donc leurs négations aussi. Le `0` constitue la valeur sémantique d'incohérence.
Le `1` désigne `Omega`. C'est l'ensemble de tous les mondes, et donc il ne satisfait que les formules qui sont vrais dans tous les mondes. Ces formules sont appelées des tautologies sémantiques. Le `1` constitue la valeur sémantique du vrai.
La négation `¬``A` correspond au complément de `A` dans `Omega` que l'on note `barA`.
Le « et » noté `"∧"` correspond à une intersection des valeurs sémantiques.
Le « ou » noté `"∨"` correspond à une réunion des valeurs sémantiques.
On, constate que les opérations logiques sémantiques de `Omega"×"Omega->Omega` correspondent aux opérations ensemblistes associées, appliquées aux ensembles de mondes.
Puis, par symétrie, il convient de définir une seconde notion dite de possibilité sémantique qui est l'autre définition de la satisfaisabilité à partir d'un ensemble de mondes en utilisant le quantificateur existentiel. Une théorie `T` admet `varphi` comme une possibilité sémantique si et seulement si :
`EEm"⊨"T, m"⊨"varphi <=> EEm"⊨"T, m"⊭¬"varphi`
`<=> "¬"(AAm"⊨"T, m"⊨¬"varphi)`
`<=> "¬"(T"⊨¬"varphi)`
`<=> T"⊭¬"varphi`
Ainsi la propriété qu'une théorie `T` admet `varphi` comme une possibilité sémantique se note :
`T⊭"¬"varphi`
Nous avons ainsi mis en exergue `4` connecteurs sémantiques de `Omega"×"Omega->{0,1}`:
Connecteur sémantique booléen |
Formule sur les ensembles de mondes |
Description |
||
`T"⊨"varphi` |
`T` satisfait `varphi` | Conséquence |
`AAm"⊨"T, m"⊨"varphi` |
Tout les mondes satisfaisant `T` satisfont `varphi`.
|
`T"⊭"varphi` |
`T` ne satisfait pas `varphi` | Non conséquence |
`EEm"⊨"T, m"⊭"varphi` |
Il existe un monde satisfaisant `T` et ne satisfaisant pas `varphi`. |
`T"⊭¬"varphi` |
`T` ne satisfait `"¬"varphi` | Possibilité |
`EEm"⊨"T, m"⊨"varphi` |
Il existe un monde satisfaisant `T` qui satisfait `varphi`. |
`T"⊨¬"varphi` |
`T`satisfait `"¬"varphi` | Impossibilité |
`AAm"⊨", m"⊭"varphi` |
Aucun monde satisfaisant `T` ne satisfait `varphi`. |
D'autres tels connecteurs sémantiques sont envisageables :
`A` est une antilogie sémantique
`A` est une tautologie sémantique
`A` est une tautologie sémantique
`A` est une antilogie sémantique
`A` et `B` sont contradictoires sémantiquement
`A` et `B` sont des tautologies sémantiques
`A"="B"="Omega`
`"⊨"B``A` et `B` sont des antilogies sémantiques
`A"="B"="Ø`
`B"⊨"0`Tout monde est satisfait par `A` ou `B`
`B` satisfait `A`
`A` satisfait `B` Tout monde est satisfait exclusivement dans `A` ou dans `B`.
`A"∨"B"⊨0"``A` et `B` ont même valeur sémantique
Il existe deux façons de construire un corps commutatifs sur les booléens. Il découle de cela deux représentation des connecteurs booléens par des polynomes booléens.
Dans un corps commutatif `(K,"+","∗")`, on construit l'anneau des polynomes à plusieurs variables qui est noté, par exemple pour trois variables, `K[x_1 ,x_2,x_3]`.
Un élément de `K[x_1 ,x_2,x_3]` est une application de `K^3"→"K`, les variables numérotés dans l'ordre servant d'entrée de l'application.
Un produit fini composé de variables en nombre quelconques parmis `{x_1 ,x_2,x_3}` et d'un élément de `K`, s'appelle un monôme.
Du fait de la distributivité de `"∗"` relativement à `"+"` et du fait de la commutativité de chaque opération, chaque élément de `K[x_1 ,x_2,x_3]` se développe en somme de monômes de façon unique à permutation près des monômes dans la somme et à permutation près des variables dans chaque monôme. Cela constitue une forme normale appelé polynôme.
Et on démontre que deux polynomes distincts, c'est à dire deux éléments de `K[x_1 ,x_2,x_3]` de formes normales distinctes, admettent au moins un point `(k1,k2,k3)` de `K^3` pour lequel leur images diffèrent, c'est à dire que les deux polynômes sont bien distinct en tant qu'application de `K^3"→"K`.
Le polynôme à plusieurs variables est définie par un tenseur de coefficients dans `K`
`P(x_1,x_2,x_3) = sum_(n_1=0)^(oo) sum_(n_2=0)^(oo) sum_(n_3=0)^(oo) k_(n_1,n_2,n_3) x_1^(n_1)x_2^(n_2)x_3^(n_3)`
Le polynôme `P` est déterminé par le tenseur `(k_(n_1,n_2,n_3))_((n_1,n_2,n_3)inNN^3)`
---- 23 mars 2018 ----
Souvent on désignera par la même lettre le corps et son ensemble sous-jacent. Et donc, dans l'exression `E = (E,+,**)`, il faut voir le premier `E` comme désignant une structure, et le second `E` comme désigant un ensemble sous-jacent. On laissera le soin au contexte de lever l'ambiguité.
Un corps commutatif se présente en notation programmative sous forme d'une liste de `6` arguments, qui est libéllée par l'expression Corps commutatif, suivi d'une éventuelle extension par `1`, `n` ou une infinité énumarable d'éléments générateurs, puis quotienté par une théorie d'égalité :
`E = `Corps commutatif `"("+ , 0, - , **, 1," / )"[a,b,c...]" / "{...}`
Le premier argument désigne l'addition, le second argument désigne l'élément neutre de l'addition, le troisième argument désigne l'opposé `-x` et aussi la soustraction `x-y` comme étant égale à `x + (-y)`, le quatrième argument désigne la multiplication, le cinquième argument désigne l'élément neutre de la multiplication et le sixième argument désigne l'inverse `x^-1` et aussi la division `x"/"y` comme étant égale à `x(y^-1)`. Notez que l'inverse est définie sur `E"\"{0}`.
La notation programmative permet de définir des corps aux théories incomplètes. Par exemple considérons le corps définie par :
`E = `Corps commutatif `"("+ , 0, - , **, 1," / ) / "{1+1+1 = 0 " ou " 1+1=0}`
Ce corps est à la fois le corps `Z"/"2Z` et le corps `Z"/"3Z`. Tout se passe comme si la question n'était pas tranchée. C'est à dire que la théorie du coprs `E`, que l'on désigne par la même lettre, ne peut pas démontrer ni `1+1+1=0` ni `1+1=0`, mais parcontre, peut démontrer `1+1+1 = 0 " ou " 1+1=0`.
`E ⊬ 1+1+1 = 0`
`E ⊬ 1+1 = 0`
`E |-- 1+1+1 = 0 " ou " 1+1=0`
Un demi-treillis `(G, ^^)`
C'est à dire :
1. Associativité de `^^` : `x^^(y*^^z) = (x^^y)^^z` 2. Commutatif de `^^` : `x^^y=y^^x` 3. Reflexivité de <= : `x^^x=x` 4. Antisymétrie de <= : `x^^y=y => `
Un treillis distributif se présente en notation classique sous forme d'une liste de 2 arguments qui est ensuite qualifiée de treillis distributif :
`E = (E,<=)` `E` est un treillis distributif
Le premier argument est l'ensemble sous-jacent et le second argument est la relation d'ordre partilel. On définis Il est d'usage que la multiplication `**` soit notée également par absence de symbole, par exemple `xyz = x**y**z` et il n'y a pas besoin de parenthèse car dans un corps la multiplication est associative.
La théorie du treillis distributif `(E,<=)` est :
La structure de corps étant une structure sur laquelle nous avons beaucoup de connaissance, on commence par regarder comment munir l'ensemble des booléens `{0,1}` d'une structure de corps. Et il y a exactement deux façons possibles de munir cet ensemble d'une structure de corps. Cela produit deux corps symétriques l'un de l'autre que l'on note selon un code couleur :
`C_2 = ({0,1},`w`,`et`)`
`C_2``= ({0,1},<=>, `ou`)``C_2` est un corps
`C_2` est un corps
Il existe un isomorphisme entre ces deux corps qui est la négation :
`¬ : C_2->``C_2`
`x|->¬x`
Les corps sur l'ensemble sous-jacent `{0,1}` sont construit en choisissant un éléments neutre pour l'opération `+`. L'autre éléments est alors l'élément neutre pour la multiplication. Car dans un corps les éléments neutres de l'addition et de la multiplication sont nécessairement distincts.
En notation programmative, les opérateurs n'ont pas de définitions et sont donc libres en dehors des contraintes portés par le patron, le patron de corps commutatif. On construit le corps commutatif petit à petit.
On muni l'ensemble `{0,1}` de l'addition `+` avec `0` comme élément neutre, et on rend cette addition interne en posant la caractéristique `2` c'est à dire que `1+1=0`. On muni l'ensemble `{0,1}` de la multiplication `**` avec `1` comme élément neutre, et avec `0` comme élément absorbant, pour former le corps `C_2`. Et donc l'addition `+` correspond au ou exclusif noté w. L'opposé correspond à l'identité `id`. La multiplication `**` correspond au et. L'inverse correspond à l'identité `id|` restreinte au seul élément `1`.
`C_2 = `Corps `"("+ , 0, `id` , **, 1, `id|`")"`
`C_2 = `Corps `"("` w`, 0,` id`,` et`, 1,` id| `")"``x +1=¬x`
`x+y = x` w `y`
`x**y = x` et `y`
Symétriquement, dans le corps `C2`. L'addition `+` correspond à l'équivalence <=>. La multiplication `**` correspond au `"ou"`.
`C_2``= `Corps `"("``+``,``0``,`id`,``**``,``1``,`id|`")"`
`C_2`` = `Corps `"("`<=>`,1,`id`,`ou`,0,`id|`")"``x` `+ 1``=`` ¬``x`
`x``+``y = x` <=> `y`
`x``**``y = x` ou `y`
Ces deux corps sont symétriques l'un de l'autre. La négation `¬` est l'isomorphisme entre ces deux corps.
`¬0 =``0`
`¬1 =``1`
`¬(x + y) = ¬x` `+`` ¬y`
`¬(x` w `y) = ¬x <=> ¬y`
`¬(x ** y) = ¬x` `**``¬y`
`¬(x` et `y) = ¬x` ou `¬y``¬``0`` = 0`
`¬``1`` = 1`
`¬(x``+``y) = ¬x + ¬y`
`¬(x <=> y) = ¬x` w `¬y`
`¬(x``**``y) = ¬x ** ¬y`
`¬(x` ou `y) = ¬x` et `¬y`
Pour un opérateur quelconque `f` et pour un opérateur unaire quelconque `u`, la conjugaison de `f` par `u` se note `f^u` et est l'opérateur appliquant d'abord`u^-1` à chaque argument, puis appliquant `f` à la liste des arguments résultants, puis appliquant `u` au résultat. Tandis que la négation de `f` se note `¬f`.
Affirmation de `f ` `(x,y,z,...)->f(x,y,z,...)` `(x,y,z,...)->¬(f(x,y,z,...))` `(x,y,z,...)->u(f(u^-1(x),u^-1(y),u^-1(z),...))`
Lorsque `"u"` est la négation, alors `"f"^"u"` désigne l'opérateur dual de `"f"`. Ainsi le dual de `f` est `f^¬`. L'isomorphisme entre les deux corps s'étend à l'ensembles de tous les opérateurs en la conjugaison par la négation :
Cette conjugaison (appellée isomorphisme étendu) permet de définir les opérateurs duaux quelques soit leur arité.
Etant donné le corps `C_2` et étant donné 4 variables booléennes `x,y,z,t`, on définie l'anneaux de polynômes par extension élementaire : `C_2[x,y,z,t]`
----- 22 décembre 2016 ----
Dans un corps de caractéristique `2`, c'est à dire tel que `x*x=x`, les monomes sont des sous-ensembles de l'ensemble des variables.
----- 17 décembre 2016 ----
On donne les définitions des 16 opérateurs binaires dans les deux corps `C2 = ({0,1},+,**)` et `C_2 = ({0,1},+,**)` :
Code |
Opérateur binaire |
Définition dans C2 |
Code
maxien |
Code
minien |
Définition dans C2 |
Code
maxien |
Code
minien |
|||||
0000 |
0 |
`x` 0 `y` |
0 |
0000 |
0 |
0000 |
0 |
`1` |
0001 |
1 |
1000 |
8 |
0001 |
1 |
`x` et `y` |
`xy` |
1000 |
8 |
0001 |
1 |
`xy``+``x``+``y` |
1110 |
14 |
0111 |
7 |
0010 |
2 |
`x "¬"`=> `y` |
`xy``+``x` |
1100 |
12 |
0101 | 5 |
`xy``+``y` `+ 1` |
1011 |
11 |
1011 |
11 |
0011 |
3 |
`x` g `y` |
`x` |
0100 |
4 |
0100 |
4 |
`x` |
0100 |
4 |
0100 |
4 |
0100 |
4 |
`x "¬"`<= `y` |
`xy``+``y` |
1010 |
10 |
0011 |
3 |
`xy``+``x` `+ 1` |
1101 |
13 |
1101 |
13 |
0101 |
5 |
`x` d `y` |
`y` |
0010 |
2 |
0010 |
2 |
`y` |
0010 |
2 |
0010 |
2 |
0110 |
6 |
`x` w `y` |
`x``+``y` |
0110 |
6 |
0110 |
6 |
`x``+``y` `+ 1` |
0111 |
7 |
1110 |
14 |
0111 |
7 |
`x` ou `y` |
`xy``+``x``+``y` |
1110 |
14 |
0111 |
7 |
`xy` |
1000 |
8 |
0001 |
1 |
1000 |
8 |
`x "¬"`ou `y` |
`xy``+``x``+``y``+`1 |
1111 |
15 |
1111 |
15 |
`xy` `+ 1` |
1001 |
9 |
1001 |
9 |
1001 |
9 |
`x` <=> `y` |
`x``+``y``+`1 |
0111 |
7 |
1110 |
14 |
`x``+``y` |
0110 |
6 |
0110 |
6 |
1010 |
10 |
`x "¬"`d `y` |
`y``+``1` |
0011 |
3 |
1010 |
10 |
`y` `+ 1` |
0011 |
3 |
1010 |
10 |
1011 |
11 |
`x` <= `y` |
`xy``+``y``+`1 |
1011 |
11 |
1011 |
11 |
`xy``+``x` |
1100 |
12 |
0101 |
5 |
1100 |
12 |
`x "¬"`g `y` |
`x``+`1 |
0101 |
5 |
1100 |
12 |
`x` `+ 1` |
0101 |
5 |
1100 |
12 |
1101 |
13 |
`x` => `y` |
`xy``+``x``+`1 |
1101 |
13 |
1101 |
13 |
`xy``+``y` |
1010 |
10 |
0011 |
3 |
1110 |
14 |
`x "¬"`et `y` |
`xy``+`1 |
1001 |
9 |
1001 |
9 |
`xy``+``x``+``y` `+ 1` |
1111 |
15 |
1111 |
15 |
1111 |
15 |
`x` 1 `y` |
1 |
0001 |
1 |
1000 |
8 |
`0` |
0000 |
0 |
0000 |
0 |
La multiplication se note parfois par absence de symbôle. Il faut alors faire attention à bien distinguer la multiplication utilisée dans `C2` qui est l'opérateur `"*"`, de la multiplication utilisée dans `C2` qui est l'opérateur `"*"`.
Les pôlynomes à deux variables `x, y`, dans un corps de caractéristique 2, peuvent se mettent sous la forme :
`b_0"*"x"*"y + b_1"*"x + b_2"*"y + b_3"*"1`
Les mônomes sont rangées du degré le plus grand au degré le plus petit en respectant l'ordre des noms de variables `(x, y)`. Le n-uplet de booléens `(b_0, b_1, b_2, b_3)` ainsi défini s'appel le code maxien. Mais on peut choisir de ranger les monomes du degrés le plus petit au degrés le plus élevé tout en respectant l'ordre des noms de variables `(x, y)`. Les pôlynomes se mettent alors sous la forme :
`a_0"*"1 + a_1"*"x + a_2"*"y + a_3"*"x"*"y`
Et le n-uplet de booléens `(a_0, a_1, a_2, a_3)` ainsi défini s'appel le code minien. Le principe du code big-endian ne permet pas vraiment de trancher lequel des deux codes est le plus pertinents.
Chaque opérateur booléen correspond à un polynôme dans le corps `C2` et à un polynome dans le corps `C2`, et possède donc un code minien et maxien pour chacun des deux corps. Cela se généralise pour un opérateurs d'arité `n` en utilisant `n` variables.
Les langages d'opérateurs {1, w, et} et {0, <=>, ou}constituent deux axiomatiques d'opérateurs. On peut donc exprimer toutes les opérations booléenne du langage L dans ces deux langages. Cela correspond aux deux corps C2 et C2.
binaire
dans {1, w, et}
dans {0, <=>, ou}
Le langage d'opérateurs {¬, et, ou} constitue une axiomatique d'opérateurs. On peut donc exprimer toutes les opérations booléennes du langage L dans ce langage. Cela correspond à une structure de treillis. La négation d'un terme dans ce langage s'obtient en remplaçant les "et" par des "ou" et les "ou" par des "et", et en négativant tous les littéraux.
binaire
dans {¬, et, ou}
---- 13 décembre 2016 ----
Il existe deux systèmes complets minimaux à un seul connecteur que sont le non-et `{"⊽"}` et le non-ou `{"⊼"}`. Puis il existe trois systèmes complets minimaux à deux connecteurs que sont `{"¬","∧"}`, `{"¬","∨"}`, `{"¬","⇒"}`.
`{"¬","∧"}` |
`{"¬","∨"}` |
`{"¬","⇒"}` |
|||
0 |
0000 |
`0` |
`x"∧¬"x` |
`"¬"("¬"x"∨"x)` |
`"¬"(x"⇒"x)` |
1 |
0001 |
`x"∧"y` |
`x"∧"y` |
`"¬"("¬"x"∨¬"y)` |
`"¬"(x"⇒¬"y)` |
2 |
0010 |
`x"⇏"y` |
`(x"∧¬"y)` |
`"¬"("¬"x"∨"y)` |
`"¬"(x"⇒"y)` |
3 |
0011 |
`x` |
`x` |
`x` |
`x` |
4 |
0100 |
`x"⇍"y` |
`("¬"x"∧"y)` |
`"¬"(x"∨¬"y)` |
`"¬"(y"⇒"x)` |
5 |
0101 |
`y`
|
`y`
|
`y`
|
`y`
|
6 |
0110 |
`x"⇎"y`
|
`"¬"(x"∧"y)"∧¬"("¬"x"∧¬"y)` |
`"¬"("¬"("¬"x"∨¬"y)"∨¬"(x"∨"y))` |
`("¬"x"⇒¬"y)"⇒¬"(x"⇒"y)`
|
7 |
0111 |
`x"∨"y` |
`"¬"("¬"x"∧¬"y)` |
`x"∨"y` |
`"¬"x"⇒"y` |
8 |
1000 |
`x "⊽" y` |
`("¬"x"∨¬"y)` |
`"¬"(x"∨"y)` |
`"¬"("¬"x"⇒"y)` |
9 |
1001 |
`x"⇔"y` |
`"¬"("¬"(x"∧"y)"∧¬"("¬"x"∧¬"y))` |
`"¬"("¬"x"∨¬"y)"∨¬"(x"∨"y)` |
`("¬"x"⇒"y)"⇒¬"(x"⇒¬"y)` |
10 |
1010 |
`"¬"y` |
`"¬"y` |
`"¬"y` |
`"¬"y` |
11 |
1011 |
`x"⇐"y` |
`"¬"("¬"x"∧"y)` |
`x"∨¬"y` |
`y"⇒"x` |
12 |
1100 |
`"¬"x` |
`"¬"x` |
`"¬"x` |
`"¬"x` |
13 |
1101 |
`x"⇒"y` |
`"¬"(x"∧¬"y)` |
`"¬"x"∨"y` |
`x"⇒"y` |
14 |
1110 |
`x"⊼"y` |
`"¬"(x"∧"y)` |
`("¬"x"∨¬"y)` |
`x"⇒¬"y` |
15 |
1111 |
`1` |
`"¬"(x"∧¬"x)`
|
`x"∨¬"x`
|
`(x"⇒"x)` |
Le langage d'opérateurs {¬, =>} constitue une axiomatique d'opérateurs. On peut donc exprimer toutes les opérations booléennes du langage L dans ce langage. Ce langage est utilisé dans le système des démonstrations axiomatiques
`{"⊽"}` |
`{"⊼"}` |
|||
0 |
0000 |
`0` |
`(x"⊽"x)"⊽"x` |
`((x"⊼"x)"⊼"x)"⊼"((x"⊼"x)"⊼"x)` |
1 |
0001 |
`x"∧"y` |
`(x"⊼"y")⊼("x"⊼"y)` |
|
2 |
0010 |
`x"⇏"y` |
||
3 |
0011 |
`x` |
`x` |
`x` |
4 |
0100 |
`x"⇍"y` |
||
5 |
0101 |
`y`
|
`y`
|
`y`
|
6 |
0110 |
`x"⇎"y`
|
||
7 |
0111 |
`x"∨"y` |
`(x"⊼"x")⊼("y"⊼"y)` |
|
8 |
1000 |
`x "⊽" y` |
`x "⊽" y` |
|
9 |
1001 |
`x"⇔"y` |
||
10 |
1010 |
`"¬"y` |
`y "⊽" y` |
`y "⊼" y` |
11 |
1011 |
`x"⇐"y` |
||
12 |
1100 |
`"¬"x` |
`x "⊽" x` |
`x "⊼" x` |
13 |
1101 |
`x"⇒"y` |
`x"⊼"(y"⊼"y)` `x"⊼"(x"⊼"y)` |
|
14 |
1110 |
`x"⊼"y` |
`x"⊼"y` |
|
15 |
1111 |
`1` |
`((x"⊽"x)"⊽"x)"⊽"((x"⊽"x)"⊽"x)`
|
`(x"⊼"x)"⊼"x` |
Puis il existe des systèmes minimaux sans la négation, et donc ne comprenant pas à la fois d'opérateur et sa négation, mais en aurorisant les littéraux négatifs. {∧"}`, `{"¬","∨"}
Arbres binaires commutatifs
formes normales
Conjonction de dijonctions |
Disjonction de conjonctions |
Polynôme |
Polynôme | |
| `x^^y` | ||||
| `xvvy` | ||||
| `x=>y` | ||||
| `x<=>y` |
---- 10 décembre 2017 ----
La formule vide est considérées comme vrai et correspond à la formule `1`. Déjà dans ce choix se pressent le paradigme conjonctif, l'idée de représenter la somme des connaissances comme une conjonction de connaissances, et de considérer ainsi la conjonction `^^` comme la première opération logique de construction des théories.
Une conjonction vide est toujours vrai, tandis qu'une disjonction vide est toujours fausse.
Nous procédons par accumulation des connaissances, comme une conjonction de formules s'agrandissant petit à petit, un ensemble de formules dans lequel on ajoute les nouvelles formules découvertes les unes après les autres.
Une règle d'inférence, et une règle de production s'appuyant sur la syntaxe, prenant comme argument un certain nombre de formules parmis les formules déjà démontrées, pour produire une nouvelle formule à rajouter parmi les formules déjà démontrées. La plus célèbre des règles d'inférences est le modus ponens que l'on présente sous forme d'un couple de formule produisant une formule, et où ces formules utilisent des variables `A` et `B` suceptible de s'unifier à n'importe quelle formule :
`(A, A`=>`B) |-> B`
Cette règle de production est définie sous forme d'une fonction prenant deux arguments qui doivent être des formules et qui doivent s'unifier à ce couple de formules `(A, A`=>`B)`, et qui retourne comme conclusion la formule `B`. Le modus ponens signifie littéralement : « Si dans notre ensemble de connaissances se trouve une formule `A` quelconque et se trouve une seconde formule de la forme `A=>B` alors nous pouvons produire la formule `B` et l'ajouter dans notre ensemble de connaissances. »
D'autre règles d'inférences peuvent être construites telle que la suppression de la double négation :
`(¬¬A) |-> A`
Et dans l'autre sens aussi, l'introduction de la double négation :
`A |-> (¬¬A)`
La contraposé par ajout de négation :
`(A`=>`B) |-> (¬B`=>`¬A)`
La disjonction implicative :
`(A vv B, A`=>`C, B`=>`C) |-> ((A vv B) `=>`C)`
La transitivité de l'implication :
`(A`=>`B, B`=>`C) |-> (A`=>`C)`
Etc...
Une démonstration est un arbre dont chaque noeud représente la résolution d'une règle d'inférence. Chaque noeud retourne une conclusion qui est la formule produite par la règle d'inférence en question. Les fils sont les arguments de la règle d'inférence en question. Les feuilles sont des axiomes ou des hypothèses. Et la racine de l'arbre retourne la conclusion de la démonstration qui est une formule produite par la règle d'inférence associée au noeud racine.
Un système de démonstration est définie par ses axiomes et par ses règles d'inférence.
La prémisse d'une démonstration comprend les règles d'inférences et axiomes du système de démonstration et les hypothèses choisies par l'utilisateur.
Etant donné un système de démonstration, s'il existe une démonstration utilisant la formule `T`, les axiomes et les règles d'inférences du système, pour produire comme conclusion la formule `varphi`, alors on dit que `T` démontre `varphi` et donc que `varphi` est une conséquence syntaxique de `T`, et on note :
`T|--varphi`
L'opérateur binaire `|--` relate une conséquence syntaxique, tandis que l'opérateur binaire`|==` relate une conséquence sémantique.
L'expression `T|--varphi` signifie que l'on peut passer de la formule `T` à la formule `varphi` en utilisant uniquement des règles d'inférence, des axiomes du système de démonstration et l'hypothèse `T`. Notez qu'il peut être nécessaire d'utiliser la formule `T`, à plusieurs endroits dans l'arbre faisant office de démonstration.
L'expression `T|==varphi` signifie que l'ensemble des mondes satisfaisant `T` est inclus dans l'ensemble des mondes satisfaisant `varphi`.
Lorsqu'il existe une démonstration sans hypothèse qui produit la formule `varphi`, alors on dit que l'on peut démontrer `varphi` et donc que `varphi` est une vérité syntaxique, et on note :
`|--varphi`
Pour pouvoir écrire cette expression, on rappelle le sens de la formule vide. La formule vide est considérées comme toujours vrai, comme une vérité sémantique et syntaxique première. Elle est donc identique à la formule `1`. Ainsi s'il n'y a pas d'argument à gauche de l'opérateur `|--` cela correspond à l'argument constitué par la formule vide. La formule vide est équivalente à la formule `1`, et cela est interprétée comme la valeur logique vrai. Ainsi l'expression `|--varphi` signifie que `varphi` est syntaxiquement vrai sans avoir à poser d'hypothèse supplémentaire, et constitue donc une vérité syntaxique.
L'opérateur unaire `|--` relate une vérité syntaxique, tandis que l'opérateur unaire `|==` relate une vérité sémantique :
On veut que le système de démonstration soient cohérent c'est à dire que la conséquence syntaxique entraine la conséquence sémantique.
Cohérence : `(A|--B)` => `(A|==B)`
Et réciproquement on veut que le système de démonstration soit complet c'est à dire que la conséquence sémantique entraine la conséquence syntaxique :
Complétude : `(A|--B)` <= `(A|==B)`
On remarque que quelque soit les formules `A, B` du langage, nous avons `A |== B` si et seulement si `|==(A=>B)` et nous avons `A |-- B` si et seulement si `|--(A=>B)` . Autrement dit les conditions précédentes se réécrivent comme suit :
On veut que le système de démonstration soient cohérent c'est à dire que la vérité syntaxique entraine la vérité sémantique. Autrement dit, on veut que toutes démonstrations sans hypothèse ne puissent produire que des formules vrais dans tous les mondes.
Cohérence : `(|--varphi)` => `(|==varphi)`
Et réciproquement on veut que le système de démonstration soit complet c'est à dire que la vérité sémantique entraine la vérité syntaxique. Et donc que si une formule est vrai dans tous les mondes, elle doit pouvoir être démontrées sans hypothèse :
Complétude : `(|--varphi)` <= `(|==varphi)`
---- 16 novembre 2017 ----
L'opérateur unaire, id, n'ayant aucun effet, id`(x) = x`, chaque noeud id peut être supprimé de l'arbre. On considère un aspect, un protocole de bas niveau, qui va résoudre systématiquement ces cas, de tel sorte que l'arbre ne contiendra plus de noeud id.
A chaque fois que se trouve une feuille 0 ou une feuille 1 dans un noeud de l'arbre, l'arbre peut se simplifier. En effet un opérateur binaire dont une entrée est connue et constante se transforme en un opérateur unaire. On considère un second aspect (un protocole de bas niveau) qui va résoudre systématiquement ces cas, de tel sorte que l'arbre ne contiendra plus de noeud contenant 0 ou 1 comme fils.
Les seuls feuilles autorisées sont alors les variables booléennes sauf pour la racine, car en effet il se peut que l'arbre soit à lui tout seul la formule 0 ou la formule 1.
Les opérateurs booléens générateurs retenus sont :
`L = {¬, `=>`, `<=` , `<=>`, `et`, `ou`, ¬`=>`, ¬`<=`, `w`, ¬`et`, ¬`ou`}`
Les opérateurs 0 et 1 ne sont plus considéré comme opérateurs générateurs mais comme deux formules spéciales.
Le principe de construction du langage peut se décrire par la structure suivante : :
`L[] uu {`0`,`1`}`
À cette étape il n'y a que deux seuls formules possibles que sont les formules spéciales 0, 1.
Le seul opérateur unaire restant, `¬`, étant son propre inverse `¬¬x = x`, il peut être traité comme un flag venant se greffer sur les noeuds et les feuilles. Un troisième aspect va résoudre la composition de deux négations successives par leur suppression dès quelles apparaissent quelque part dans l'arbre de tel sorte que l'arbre ne contiendra plus de double négation. La formule est donc perçue comme un arbre composée de noeuds binaires et de feuilles, chaque noeud et feuille ayant en plus un flag affirmatif ou négatif.
Ainsi un noeud correspond à un opérateur binaire avec un flag affirmatif ou négatif. Il faut donc choisir pour chacun des `5` couples d'opérateurs affirmatif-négatifs `(`=>`, ¬`=>`)`, `(`<=` , ¬`<=`)`, `(`et`, ¬`et`)`, `(`ou`, ¬`ou`)`, `(`<=>`, `w`)` lequel est considéré comme ayant un flag affirmatif et l'autre un flag négatif. Et les choix canoniques ne coïncident pas avec les choix pratiques. Nous sommes pragmatiques, nous faisons le choix pratique en sachant qu'il n'est pas canonique, c'est à dire qu'il faudra apporter la même importance aux opérateurs possèdant un flag négatif. Le langage d'opérateurs sous-jacent que nous utilisons ne comporte plus que `6` opérateurs.
`L = {¬, `=>`, `<=`, `<=>`, `et`, `ou`}`
Par exemple, l'opérateur `¬`et sera considéré comme la combinaison du flag négatif `¬` et de l'opérateur et, l'opérateur w (c'est le "ou exclusif") sera considéré comme la combinaison du flag négatif `¬` et de l'opérateur <=>.
Le principe de construction du langage se complexifie encore, puisque maintenant la composition de deux opérateurs `¬` est interdite. Pour un langage de dimension 4, cela peut se décrire par la structure suivante :
`L[x,y,z,t] uu {`0`,`1`}`/`{¬¬x=x}`
Ou bien cela peut se décrire par la grammaire suivante :
`A = { {¬,epsilon}B(A,A), {¬,epsilon}C, 0, 1}`
`B = { `=>`, `<=`, `<=>`, `et`, `ou` }`
`C = { x, y, z, t }`
La grammaire utilise des ensembles d'alternatives.
Le méta-élément `epsilon` désigne le rien.
La méta-variable `C` désigne les variables booléennes de l'univers.
La méta-variable `B` désigne les `5` opérateurs binaires booléens pris comme générateurs.
La méta-variable `A` désigne toutes les formules du langage.
Par exemple la règle de grammaire `{¬,epsilon}x` désigne les 2 formules `¬x` et `x`.
Parmi les `5` opérateurs binaires il existe deux opérateurs non commutatifs, symétriques l'un de l'autre `(`=>`, `<=`)`
`x`=>`y = y`<=`x`
Il faut donc en choisir un et considérer l'autre comme obtenue par permutation des arguments. Et il n'y a pas de choix canoniques. Nous faisons un choix pratique en gardant l'opérateur d'implication =>, en sachant qu'il n'est pas canonique, c'est à dire qu'il faudra apporter la même importance à l'opérateur symétrique <=. Le langage d'opérateurs sous-jacent que nous utilisons ne comporte plus que `5` opérateurs.
`L = {¬, rArr, hArr, `et`, `ou`}`
Le langage correspond toujours à la structure suivante :
`L[x,y,z,t] uu {`0`,`1`}`/`{¬¬x=x}`
On a simplement retiré un opérateur générateur de l'ensemble `L`
Un littéral est composé d'une éventuelle opération de négation ¬ suivie d'une valeur logique 0 ou 1 ou bien d'une variable booléenne {x,y,z,t...}. Exemples : ¬x, y, 0, 1 sont 4 littéraux.
Une clause est une disjonction de littéraux. Exemple : x ou ¬y ou z. La clause vide vaut 0.
Un état est une conjonction de littéraux. Exemple : x et ¬y et z. L'état vide vaut 1.
Un terme est une composition close d'opérateurs parmi le langage d'opérateurs L = {0, 1, ¬, =>, <=, <=>, et, ou, ¬=>, ¬<=, w, ¬et, ¬ou}. Le terme s'évalue en une valeur booléenne.
Une formule est une composition close d'opérateurs de L[x,y,z,t...] où le nombre de variables rajouté au langage L s'appel la dimension du langage. La formule admet une forme simplifié qui est une composition close d'opérateur parmi le langage {1, ¬, =>, <=, <=>, et, ou} augmenté des variables {x,y,z,t...} où toutes les compositions ¬¬ apparaissant à l'intérieur de la formule sont enlevées.
Une proposition est la signification logique d'une formule c'est à dire sa table de vérité. La proposition désigne une formule à équivalence près.
Sujet :
Le langage propositionnel
Symétrie opérées par négation et permutation des arguments. Propriétés algébriques des opérateurs. Axiomatique d'opérateurs. Nomenclature
Sujets liés :
La logique
Opérateurs booléens. Liste exhaustive des opérateurs booléens d'arité 0, 1 et 2. La logique booléenne. Nombre d'opérateurs d'arité 3,4,5,6. Codage des opérateurs booléens. L'adressage indirecte. Classification des opérateursLe langage d'opérateurs
Structure libre. Partage et complexité.Taille, niveau et complexité. Enumération. Composition d'opérateurs. Implémentation selon la logique polonaise. Implémentation récursive. Les axiomatiques d'opérateurs. L-taille, L-niveau et L-complexité.L'univers et les mondes
Les univers. Le produit d'univers. Le codage des mondes. La satisfaction d'une formule dans un monde. Totologie, contradiction et cohérence. Les formes normales disjonctive et conjonctive. Les formes normales polynomiales.Les règles de raisonnements
Les extensions intérieurs. La qualité. Le système axiomatique de Hilbert. La règle d'inférence dite du Modus Ponens. Les 3 shémats d'axiomes. La déduction naturelle. Les 9 règles d'inférences
Un opérateur est booléen s'il opère sur des booléens pour produires un booléen. Un langage d'opérateurs booléens engendre une logique d'ordre 0, car chaque variable ne pouvant avoir qu'un nombre fini d'états, ici 2, toutes les formules peuvent être remplacés par des tables de vérité sans variable.
Dans un langage d'opérateurs booléens, chaque opérateur booléen est préalablement défini, et il existe donc un procédé mécanique permettant de calculer la valeur booléenne de chaque terme. chaque terme peut être remplacé par sa valeur booléenne qui est 0 ou 1.
Considérons par exemple le langage d'opérateurs booléens L = <0, 1, ¬(.), et(.,.)>. Le langage ne comprend que des opérateurs booléens connus puisqu'ils doivent être préalablement définis.
Considérons des variables (x,y,z) ∈ L 3 qui représentent des termes variables. L'utilisation de ses variables va produire des formules dont le résultats logique sera plus complexes que pour les termes. La formule et(x,y) ne peut pas être résolue en un booléen sans connaitre la valeur booléenne des variables x et y. Dans ce cas, on considère que l'évaluation de et(x,y) sera la formule et(x,y) et non une valeur booléenne.
Considérons des variables (A,B,C) ∈ L[x,y,z] 3 qui représentent des formules variables. Si nous posons A = et(x,y) et que les variables x et y n'ont pas de valeur définie, alors l'évaluation de A sera la formule et(x,y) et non une valeur booléenne. L'utilisation de ses variables va produire des schémats dont le résultats logique sera plus complexes que pour les formules. Par exemple, le schéma et(A,B) ne peut pas être résolue ni en un booleen ni en une formule sans connaitre la valeur des variables A et B
Considérons des variables (U,V,W) ∈ L[x,y,z][A,B,C] 3 qui représentent des schémas variables. Si nous posons U = et(A,B), et que A et B n'ont pas de valeur définie, alors l'évaluation de U sera le schémat et(A,B) et non une valeur booléenne, ni même une formule. Par contre si A est égale à une formule telle que A=et(x,y) alors U s'évalura en un shémat et(et(x,y),B).
On définie la qualité d'un terme comme étant sa valeurs booléennes. Les qualités possibles des termes sont les valeurs booléennes {1,0} que l'on nomme respectivement {vrai, faux}.
On définie la qualité d'une formule comme étant l'ensemble des valeurs booléennes parcourues par la formule lorsque l'ensemble des variables booléenne (variable de type 1) de l'univers parcourent leurs différentes valeurs booléennes possibles. Il y a alors autant de qualités possibles qu'il y a de sous-ensemble non vide de {0,1} soit 3 qualités possible {{0}, {0, 1}, {1}} que l'on nomment respectivement {tautologique, indéterminé, contradictoire} et qui correspondent à :
sous-qualités
formule ayant
cette qualité
Chaque configuration des variables booléennes de l'univers correspond à un monde possible.
On définie la probabilité d'une formule comme la somme des probabilités de chaque monde où la formule est vrai, en posant par défaut l'équiprobabilité des mondes.
On définie la qualité d'un schémat comme étant l'ensemble des qualités parcourues par le schéma lorsque l'ensemble des variables de type 2 parcourent toutes les formules possibles. Il y a alors autant de qualités possibles qu'il y a de sous-ensemble non vide de {tautologique, indéterminé, contradictoire} soit 7 qualités possibles que l'on nomme {faux, vrai, bivalant, nonfaux, nonvrai, nonbivalant, libre} et qui correspondent à :
sous-qualités
schéma ayant
cette qualité
Sur ces 7 qualités, seulement 6 sont rencontrées.
11) L'extention naturelle de la logique d'ordre 0 à la logique d'ordre 1.
L'extention naturelle de la logique d'ordre zéro à la logique d'ordre 1 consiste à prendre comme variable les propositions. De telles variables désignants des propositions logiques d'ordre zéro, utilisent un nombre fini mais non borné de variables booléennes, et peuvent donc avoir un nombre infini de valeurs possibles. Elles constituent des variables universelles, leurs quantificateurs quel que soit et il existe ne peuvent pas être remplacés par une énumération finie de possibilité.
Les formules dans cette logique d'ordre 1 sont appelée shémas. Ici, le terme de proposition est réservé à la logique d'ordre zéro. Décrivons les qualités que peuvent prendre un shéma ainsi décrit mais sans quantificateur quel que soit ni il existe. Les variables propositionelles sont remplacées par des constantes propositionelles inconnues. Cette opération est appelé skolémisation et consiste à remplacer les inconnues par des constantes supplémentaires ajoutées au langage. (Noter que ces constantes n'ont pas le même type que les constante booléennes.)
Considérons un shémas K utilisant n variables propositionnelles {A1, A2, A3 ..., An}et trois variables booléennes {x,y,z}dites non muettes. Le langage utilisé sera une extention de la logique d'ordre zéro précédement décrite, obtenue en ajoutant sous forme de constante ces n variables propositionnelles et ces trois variables booléennes non muettes. On obtient le langage {¬, et, ou, =>, <=, <=>, w, +, *, x, y, z, A1, A2, A3 ..., An}. x est une constante booléenne. A1 est une constante propositionelle. K est un shéma. Lors d'une évaluation, A1 peut prendre comme valeur toute proposition logique sur un nombre fini quelconque de variables booléennes muettes supplémentaire au langage présent, ou déja existantes dans l'instantiation d'une autre variable propositionnelle utilisée, ou soit non muettes.
Cela signifit que l'on ne peut pas concidérer une à une les variables propositionnelles d'un shéma, car elle sont potentiellements liées entre elles. Nous parlerons donc d'instantiation du jeux complet des n variables propositionnelles {A1, A2, A3 ..., An}dans le langage infini {¬, et, ou, =>, <=, <=>, w, +, *, x, y, z, x1, x2, x3, x4 ...}, mais où chaque valeur propositionnelle est de taille finie.
11.1) Les sept qualités possibles d'un schéma
Dans ce nouveau langage permettant de définir les schémas, il y a deux types de constantes ; Celles correspondantes aux variables booléennes qui ont deux valeurs possibles {0,1}correspondant aux deux qualités possibles {vrai, faux}, et celles correspondants aux variables propositionnelles qui ont une infinité de valeurs possibles, mais possédant trois qualités possibles {contradictoire, indéterminé, tautologique} selon qu'une fois développé, leur polynôme associé est nul, non trivial, ou égale à 1, et qui correspond aux sous-ensembles des qualités rencontrées lorsqu'on évalue la proposition pour chaque valeur possible de ses variables booléennes. C'est à dire tautologique = {vrai}, indéterminé = {vrai, faux}, contradictoire = {faux}
Pour une valeur donnée des n constantes propositionnelles, le schéma K(x,y,z,A1,A2,A3...,An) possède une des qualités ; contradictoire, indéterminé, ou tautologique, selon qu'une fois développé, K(x,y,z,A1,A2,A3...,An) est un polynôme nul, ou possédant au moins une variable booléennes (muettes ou non), ou égale à 1.
Dans l'univers des schémas, Il y a autant de qualité qu'il y a de partie non vide de l'ensemble {contradictoire, indéterminé, tautologique}, soit 7 qualités possibles que l'on nomme {absurde, trivial, bivalant, nonabsurde, nontrivial, nonbivalant, libre}et qui correspondent aux sous-ensembles des qualités rencontrées lorsqu'on évalue le schéma pour chaque valeur possible de ses variables propositionnelles. C'est à dire absurde = {contradictoire}, trivial = {tautologique}, bivalant = {indéterminé}, nonabsurde = {tautologique, indéterminé}, nontrivial = {contradictoire, indéterminé}, nonbivalant = {tautologique, contradictoire}, libre = {tautologique, contradictoire, indéterminé}.
Sur ces 7 qualités, seulement 6 sont rencontrées. Voici les exemples canoniques pour les six, et une solution pour la septième.
Cette logique d'ordre 1 ne possède pas de possibilité d'expression supérieure à notre logique d'ordre 0. Il est nécessaire d'adjoindre de nouveaux opérateurs pour étendre sous domaine d'expression, en tout cas pour atteindre la septième qualité manquante. Cette dernière est atteinte en définissant l'opérateur de démontrabilité |-.
11.2) Le méta opérateur de démontrabilité
On définit le méta opérateur binaire constant, |- , qui représente la relation de démontrabilité, par le procédé récursif suivant :
Soit K, G deux schémas n'utilisant pas l'opérateur |-. Pour chaque valeur possible de leurs variables propositionnelles, nous posons : (K |- G) retourne 1 si (K et ¬G) est contradictoire, c'est à dire une fois développé, est égale au polynôme nul. (K |- G) retourne 0 si (K et ¬G) n'est pas contradictoire, c'est à dire tautologique ou indéterminé, c'est à dire une fois développé, est différent du polynôme nul.
Si l'opérateur |- est appliqué plusieurs fois de façon emboîtée, il faut d'abord évaluer les opérateurs |- appliqué à des schémas sans opérateur |-, et remonter ainsi de suite.
Puis il faut intégrer toutes les valeurs possibles des variables propositionnelles et procéder à la réunion de toutes les qualités produites possibles. Ce qui donne une définition non constructible du méta opérateur |-.
Schéma |
Schéma |
Schéma évalué |
Qualité du Schéma |
(A |- 0) |
c(A) |
A est contradictoire |
Nonbivalant |
(¬A |- 0) |
c(¬A) |
A est tautologique |
Nonbivalant |
(A |- 1) |
c(0) |
1 |
Trivial |
(¬A |- 1) |
c(0) |
1 |
Trivial |
(0 |- A) |
c(0) |
1 |
Trivial |
(0 |- ¬A) |
c(0) |
1 |
Trivial |
(1 |- A) |
c(¬A) |
A est tautologique |
Nonbivalant |
(1 |- ¬A) |
c(A) |
A est contradictoire |
Nonbivalant |
¬(A |- 0) |
¬c(A) |
A est tautologique ou indéterminé |
Nonbivalant |
¬(¬A |- 0) |
¬c(¬A) |
A est contradictoire ou indéterminé |
Nonbivalant |
¬(A |- 1) |
¬c(0) |
0 |
Absurde |
¬(¬A |- 1) |
¬c(0) |
0 |
Absurde |
¬(0 |- A) |
¬c(0) |
0 |
Absurde |
¬(0 |- ¬A) |
¬c(0) |
0 |
Absurde |
¬(1 |- A) |
¬c(¬A) |
A est contradictoire ou indéterminé |
Nonbivalant |
¬(1 |- ¬A) |
¬c(A) |
A est tautologique ou indéterminé |
Nonbivalant |
(A |- A) |
c(0) |
1 |
Trivial |
(A |- ¬A) |
c(A) |
A est contradictoire |
Nonbivalant |
(¬A |- A) |
c(¬A) |
A est tautologique |
Nonbivalant |
(¬A |- ¬A) |
c(0) |
1 |
Trivial |
¬(A |- A) |
¬c(0) |
0 |
Absurde |
¬(A |- ¬A) |
¬c(A) |
A est tautologique ou indéterminé |
Nonbivalant |
¬(¬A |- A) |
¬c(¬A) |
A est contradictoire ou indéterminé |
Nonbivalant |
¬(¬A |- ¬A) |
¬c(0) |
0 |
Absurde |
(A |- B) |
c(A et ¬B) |
(A et ¬B) est contradictoire |
Nonbivalant |
Nous pouvons également définire d'autre méta opérateurs :
Le système des démonstrations axiomatiques de Hilbert utilise le langage d'opérateurs L = {¬, =>} qui constitue une axiomatique d'opérateurs, et à laquelle on ajoute les variables booléennes de l' Univers (x,y,z,t...).
On considère l'extension intérieur du troisième ordre suivante :
L[x,y,z...][A,B,C...][U,V,W...]
(x,y,z...) ∈ Ln
(A,B,C...) ∈ L[x,y,z...] n
(U,V,W...) ∈ L[x,y,z...][A,B,C...] n
Le premier type de variable dite "booléenne" notée en minuscule x, y, z... contient un terme de L évaluable en une qualité booléenne. Le second type de variable dite "propositionnelle" notée en majuscule A,B,C... contient une formule de L, c'est à dire un terme de L[x,y,z...], évaluable en une qualité ternaire. Le troisième type de variable dite "schématique" notée en majuscule intalique U,V,W,... contient un schéma de L, c'est à dire un terme de L[x,y,z...][A,B,C...], évaluable en une qualité septenaire..
Hilbert utilise la règle du Modus Ponens. Cette règle permet de construire la formule B, à partir du couple de formules (A, A=>B). Les variables A et B contiennent des formules quelconques. Cette règle met en oeuvre un procédé d'unification entre le couple de schémas (A, A=>B) et les couples de formules déjà démontrés. Si l'unification réussie la règle construit la formule contenu dans B, sinon elle ne produit rien, c'est à dire 1 dans une conjonction.
À l'aide du méta-opérateur binaire •, on note C•D le résultat de la règle du Modus Ponens appliqué aux deux formules contenues dans la varibale C et la variable D dans un sens ou dans l'autre. Si les arguments ne satisfont pas la règle, alors l'opération returne la formule 1, sinon l'opération retourne la formule produite par la règle. Voici quelques exemples :
x • y = 1
(x => y) • x = y
(x => y) • ¬x = 1
(¬x => y) • ((¬x => y) => ¬z) = ¬z
L'ensemble des formules démontrables à partir du Modus Ponens et de quelques formules initiales F, G, H se note alors par <F, G, H, •>.
Mais il nous faut davantage que simplement noter la règle, il nous faut la programmer, écrire son programme. Cela peut ce faire en utilisant l'opérateur d'unification ~u~(...), la séquence d'instructions, l'opérateur FAIL, une condition, et l'instruction qui retourne le résultat.
• : (X,Y) --> (~u~(X, A), ~u~(Y, A=>B), si FAIL return 1 sinon retourne B)
Puis dans un langage de programmation plus évolué cela peut s'écrire par
• : (A, A=>B), B | 1
L'appel de la fonction procède à deux unifications et retourne B et si elle échoue alors elle retourne 1.
Cette seul règles du Modus Ponens ne suffit pas à épuiser toutes les formes de raisonnement en logique propositionnelle. On doit ajouter des axiomes supplémentaires.
Hilbert ajoute à son système, une infinité énumérable d'axiomes. Il le fait en utilisant ces trois schémas comme procédé de construction de formules :
A => (B => A)
(¬A => ¬B) => (B => A)
(A => (B => C)) => ((A => B) => (A => C))
Chacun des trois schémas génère, sans se préoccuper des autres schémas, une liste infini énumérable de formules, lorsque (A,B,C) parcours L[x,y,z...] 3 .
D'une manière générale, un schéma désigne un ensemble énumérable de formules, regroupant toutes les formules que l'on peut constituer en remplaçant dans le schèma les variables A,B,C... par des formules quelconques de L. On peut alors y appliquer un des opérateurs "et", "ou". Un tel opérateur regroupe tous ses arguments en un ensemble, et peut être considéré comme un opérateur unaire s'appliquant à cet ensemble. Par exemple
et{ A=>(B=>A) } = et{ x=>(y=>x), ¬x=>(y=>¬x), y=>(x=>y), (x=>((y=>z)=>x)... }
= (...(((x=>(y=>x) et ¬x=>(y=>¬x)) et y=>(x=>y)) et (x=>((y=>z)=>x)) et...)
Ainsi les trois shémas d'axiomes doivent être noté comme suit :
et{ A => (B => A) }
et{ (¬A => ¬B) => (B => A) }
et{ (A => (B => C)) => ((A => B) => (A => C)) }
ou ce qui revient au même par :
∀(A,B,C)∈L[x,y,z...] 3
A => (B => A)
(¬A => ¬B) => (B => A)
(A => (B => C)) => ((A => B) => (A => C))
---- 24 août 2014 ----
Et on note {A,B}|-C si il est possible de construire C à l'aides des termes de l'ensemble {A,B} en utilisant une ou plusieurs fois la règle de production du Modus Ponens. Nous avons par exemples :en utilisant le méta-opérateur |- par la propriété suivante :
{A, A=>B} |- B
le méta-opérateur |- prend deux arguments une formule ou un ensemble fini de formules ce qui correspond à une conjonction finie de formules
La démonstration est l'expression (y • y=>x) • (z • z=>(x=>t)) où les termes en rouge sont les éléments du langage de programmation, et la conclusion t en est l'évaluation. La démonstration est de taille 7, de niveau 3, et de complexité 7.
On peut ainsi définir la taille, le niveau d'emboitement, le partage et la complexité des constructions dans le langage de programmation, telles quelles sont définies au chapitres III.4. Il y a deux niveaux de construction, celle des éléments que sont les termes logiques, et celle des démonstrations.
On peut définir les axiomatiques, des ensembles de termes minimals tel que défini au chapitres III.9.
Etant donné un ensemble fini de termes logiques A. Noter que cet ensemble fini constitue un terme égale à la conjonction de tous ses termes élément. On peut définir la A-taille, le A-niveau et la A-complexité d'un terme U tel que défini au chapitres III.10. La logique propositionnelle ne rencontre pas de difficulté, tant quelle est fini, pour définir ces complexités minimales.
A = {y, y=>x, z, z=>(x=>t)}
A-taille(t) = 7
A-niveau(t) = 3
A-complexité(t) =7A |-t7 t
A |-n4 t
A |-c6 t
Et nous pouvons également considérer que A = et{y, y=>x, z, z=>(x=>t)}.
Le moteur générateur des démonstrations n'est constitué que de d'une seul règle de construction qu'est la règle du Modus Ponens. Il faut alors ajouter des termes logiques de départs, sinon on ne peut pas appliquer la règle de construction et on ne peut rien construire. Hilbert propose une axiomatique permettant de déduire toutes les totologies du calcul propositionnelle. Elle contient 3 termes appelés axiomes.
La 0-complexité d'une formule est la complexité de son calcul lorsqu'elle est implémentée par un arbre et en supposant que l'évaluation de chaque opérateur générateur porte une complexité élémentaire de valeur `1`. La complexité des formules implémentées sous forme d'arbre est donc égale à leur taille, c'est à dire au nombre d'opérateurs qu'elles contiennent. Pour l'exemple
`varphi = (0` ou `1) => ¬(1` et `0)`
La formule `varphi` possède une 0-complexité de 8.
L'étude de la complexité nous amène à considérer le partage des données. Une données calculés une fois n'a pas besoin d'être recalculée et peut être réutilisée plusieurs fois à différent endroits de la formule. On introduit un mécanisme de partage de données dans l'implémentation des formules, transformant leur représentation sous forme d'arbre, en représentation sous forme de graphes orientés sans boucle dit arbres partagés.
La 1-complexité d'une formule est la complexité de son calcul lorsqu'elle est implémentée par un arbre partagé qui partage tous ses noeuds de valeur identique. La 1-complexité de `varphi ` vaut 1 car `varphi ` vaut une valeur booléenne déterminée, ici `1`. Autre exemple
`phi = (x` ou `y) => ¬(y` ou `x)`
La 1-complexité de `phi ` vaut 6. Et la formule s'écrit `phi = (x` ou `y)_a => ¬(a)` ou l'indice `a` indique qu'il y a partage.
Un système axiomatique à la Hilbert est un ensemble de schémas d'axiomes qui ajouté à la seul règle du modus ponens permet de définir l'ensembles des règles de déduction propre au langage propositionnelle. Si par soucis de simplification on se restreint au langage `{`=>`,¬,x,y,z,t,...}`, alors les shémas d'axiomes à considérer sont les suivants :
`A`=>`(B`=>`A)`
`(A`=>`(B`=>`C)) `=>` ((A`=>`B)`=>`(A`=>`C))`
`(¬A `=>` ¬B) `=>` (B`=>`A)`
Chaque schéma d'axiomes est un énumérateur d'axiomes où `A, B, C` parcourent toutes les formules écrivables, qu'elles soient satisfaisables ou non. Si on ajoute au langage la formule vide symbolisée par la formule 1, alors il faut ajouter l'axiome suivant `1`.
alors il faut ajouter le shéma d'axiome suivant `¬1`=>`A` qui est la définition du vrai car le faux implique tout.
On étudira plus tard, en logique du premier ordre, comment faire opérer ces deux opérateurs "et", "ou", sur des ensembles infinis énumérables d'arguments.
La différence dans ces extensions tient dans la définition de la structure `L` qui porte les principes de construction du langage et qui incorpore les nouveaux aspects décrits (Suppression de 0, 1, `id`, Suppresion de la double négation, Réduction des couples d'opérateurs affirmatif-négatifs, Réduction du couple d'opérateurs non commutatifs).
Si on se restreint à notre langage défini en §5, dont l'aspect correspond à la règle `¬¬x -> x`, l'ensemble des ces symétries qui modifient l'arbre syntaxiquement mais ne le changent pas sémantiquement, est équivalent à l'ensemble des règles de transformation suivantes, applicables à un noeud quelconque de l'arbre et appliquées un nombre de fois quelconque :
Commutativité du ou : Commutativité du <=> : Transformation du ou en => : Contraposé avec => : Contraposé avec <=> : Négation du ou : Négation du et : Négation du => : Négation du <=> :
Si on se restreint à notre langage défini en §5 alors nous avons :
P = x et y
S = x <=> y
S = ¬x <=> ¬y
Q = x ou y
Q = ¬x => y
Q = ¬y => x
R = (x et y) ou z
R = (y => ¬x) => z
R = (x => ¬y) => z
R = (¬x ou ¬y) => z
R = ¬z => (x et y)
Il est possible de définir à l'intérieur de la logique booléenne, une logique qui ressemble à une logique du premier ordre, en prenant comme éléments, les formules du langage.
On pose un ensemble `A` composé d'un nombre fini de formules de `L^•[x_1, x_2, x_3, ..., x_n]`.
On commence par définir les quantificateurs du langage. On définie `4` quantificateurs que sont les quantificateurs universel noté `AA`, existentiel noté `EE`, d'imparité affirmative noté `sfI` et de parité réfutative noté `sfP` qui portent sur des ensembles finis de formules comme suit :
Toutes les formules appartenant à `A` valent `1`. Il existe au moins une formules appartenant à `A` qui vaut `1`. Il y a un nombre impaire de formules appartenant à `A` et valant `1`. Il y a un nombre paire de formules appartenant à `A` et valant `0`.
Notez que :
Avec cette définition, le passage à la négation se fait comme suit :
En appliquant les définitions précédentes, nous avons :
La conjonction. La disjonction. L'imparité affirmative. La parité réfutative.
La conjonction unaire affirme son élément. La disjonction unaire affirme son élément. L'imparité affirmative unaire affirme son élément. La parité réfutative unaire affirme son élément.
La conjonction vide est vrai. La disjonction vide est fausse. L'imparité affirmative vide est fausse. La parité réfutative vide est vrai.
Ces quantificateurs sont dits finis car leur porté élémentaire se limite à des ensembles finis d'éléments.
Il existe deux systèmes de démonstration courants basée sur des structures algébriques que l'on applique aux booléens, que sont la structure de treillis distributifs et la struture de corps commutatifs. On commencera par décrire ces deux structures.