Axiomes minimaux pour l'algèbre booléenne - Minimal axioms for Boolean algebra

En logique mathématique , les axiomes minimaux pour l'algèbre booléenne sont des hypothèses qui sont équivalentes aux axiomes de l'algèbre booléenne (ou calcul propositionnel ), choisis pour être aussi courts que possible. Par exemple, si l'on choisit de prendre la commutativité pour acquise, un axiome avec six opérations NAND et trois variables est équivalent à l'algèbre booléenne :

${\displaystyle ((a\mid b)\mid c)\mid (a\mid ((a\mid c)\mid a))=c}$

où la barre verticale représente l'opération logique NAND (également connue sous le nom de trait de Sheffer ).

C'est l'un des 25 axiomes candidats pour cette propriété identifiés par Stephen Wolfram , en énumérant les identités de Sheffer de longueur inférieure ou égale à 15 éléments (à l'exclusion des images miroir) qui n'ont pas de modèles non commutatifs avec quatre variables ou moins, et a d'abord été prouvée équivalente par William McCune , Branden Fitelson et Larry Wos . MathWorld , un site associé à Wolfram, a nommé l'axiome « l'axiome de Wolfram ». McCune et al. ont également trouvé un axiome unique plus long pour l'algèbre booléenne basé sur la disjonction et la négation.

En 1933, Edward Vermilye Huntington a identifié l'axiome

${\displaystyle {\neg ({\neg x}\lor {y})}\lor {\neg ({\neg x}\lor {\neg y})}=x}$

comme étant équivalent à l'algèbre booléenne, lorsqu'elle est combinée avec la commutativité de l' opération OU , , et l'hypothèse d'associativité, . Herbert Robbins a conjecturé que l'axiome de Huntington pourrait être remplacé par ${\style d'affichage x\lor y=y\lor x}$${\displaystyle (x\lor y)\lor z=x\lor (y\lor z)}$

${\displaystyle \neg (\neg (x\lor y)\lor \neg (x\lor {\neg y}))=x,}$

ce qui nécessite une utilisation de moins de l'opérateur de négation logique . Ni Robbins ni Huntington n'ont pu prouver cette conjecture ; ni Alfred Tarski , qui s'y intéresse beaucoup plus tard. La conjecture a finalement été prouvée en 1996 à l'aide d'un logiciel de preuve de théorème . Cette preuve a établi que l'axiome de Robbins, avec l'associativité et la commutativité, forment une 3-base pour l'algèbre booléenne. L'existence d'un 2-base a été établie en 1967 par Carew Arthur Meredith : ${\style d'affichage \neg }$

${\displaystyle \neg ({\neg x}\lor y)\lor x=x,}$

${\displaystyle \neg ({\neg x}\lor {\neg y})\lor (z\lor y)=y\lor (z\lor x).}$

L'année suivante, Meredith a trouvé une base 2 en termes de coup de Sheffer :

${\displaystyle (x\mid x)\mid (y\mid x)=x,}$

${\displaystyle x|(y\mid (x\mid z))=((z\mid y)\mid y)\mid x.}$

En 1973, Padmanabhan et Quackenbush ont démontré une méthode qui, en principe, donnerait une base 1 pour l'algèbre booléenne. L'application directe de cette méthode a donné des « axiomes d'une longueur énorme », soulevant ainsi la question de savoir comment trouver des axiomes plus courts. Cette recherche a donné la base 1 en termes de course de Sheffer donnée ci-dessus, ainsi que la base 1

${\displaystyle \neg (\neg (\neg (x\lor y)\lor z)\lor \neg (x\lor \neg (\neg z\lor \neg (z\lor u))))=z ,}$

qui s'écrit en termes de OU et NON.

Les références