En calcul de propositions, la barre de Sheffer, nommée d'après Henry M. Sheffer, notée « | » (voir barre verticale, à ne pas confondre avec « || » qui est souvent utilisé pour représenter la disjonction), « Dpq », ou « ↑ » (une flèche pointant vers le haut), désigne une opération logique qui est équivalente à la négation de la conjonction logique, exprimée « pas les deux à la fois » dans le langage ordinaire. Il est aussi appelé nand (« non et »), car il dit en effet qu'au moins l'un de ses opérandes est faux. En algèbre booléenne et en électronique numérique, il est connu sous le nom de l'opération NON-ET.
L'opération NON-ET est une fonction logique sur deux valeurs logiques. Elle produit une valeur vrai, si — et seulement si — au moins une des propositions est fausse.
Table de vérité
La table de vérité de A NON-ET B (aussi noté A | B, Dpq, ou A ↑ B) est la suivante :
Charles Sanders Peirce (1880) avait découvert la complétude fonctionnelle de NON-ET ou NON-OU plus de 30 ans auparavant, mais il n'a jamais publié ses résultats.
Introduction, élimination, et équivalences
La barre de Sheffer est la négation de la conjonction :
↑Moses Schönfinkel, « Über die Bausteine der mathematischen Logik », Mathematische Annalen92, (1924) p. 305-316. Traduit par Stefan Bauer-Mengelberg comme « On the building blocks of mathematical logic » in Jean van Heijenoort, 1967. A Source Book in Mathematical Logic, 1879-1931. Harvard Univ. Press: 355-66.
(en) Jean G. P. Nicod, « A Reduction in the Number of Primitive Propositions of Logic », Proceedings of the Cambridge Philosophical Society, vol. 19, , p. 32–41