AVC Sheffer - Sheffer stroke

AVC Sheffer
NAND
Diagramme de Venn de l'AVC de Sheffer
Définition
Table de vérité
Porte logique NAND ANSI.svg
Formes normales
Disjonctif
Conjonctif
polynôme de Zhegalkin
Les treillis de poste
0-conservation non
1-conservation non
Monotone non
Affine non

Dans les fonctions booléennes et le calcul propositionnel , le trait de Sheffer désigne une opération logique qui équivaut à la négation de l' opération de conjonction , exprimée en langage ordinaire par « pas les deux ». On l'appelle aussi nand ("pas et") ou le déni alternatif , puisqu'il dit en effet qu'au moins un de ses opérandes est faux. En électronique numérique , il correspond à la porte NAND . Il est nommé d'après Henry M. Sheffer et écrit comme ↑ ou comme | (mais pas comme ||, souvent utilisé pour représenter la disjonction ). En notation Bocheński, il peut être écrit sous la forme D pq .

Son double est l' opérateur NOR (également connu sous le nom de flèche de Peirce ou dague de Quine ). Comme son dual, NAND peut être utilisé seul, sans autre opérateur logique, pour constituer un système formel logique (rendant NAND fonctionnellement complet ). Cette propriété rend la porte NAND cruciale pour l' électronique numérique moderne , y compris son utilisation dans la conception de processeurs informatiques .

Définition

L' opération NAND est une opération logique sur deux valeurs logiques . Il produit une valeur de vrai, si - et seulement si - au moins une des propositions est fausse.

Table de vérité

La table de vérité de (également écrite comme , ou D pq ) est la suivante

T
T
F
T
F
T
F
T
T
F
F
T

Équivalences logiques

Le coup de Sheffer et est la négation de leur conjonction

    
Venn1110.svg      Venn0001.svg

Par les lois de De Morgan , cela équivaut aussi à la disjonction des négations de et

    
Venn1110.svg      Venn1010.svg Venn1100.svg

Histoire

Le trait est nommé d'après Henry M. Sheffer , qui en 1913 a publié un article dans les Transactions de l'American Mathematical Society fournissant une axiomatisation des algèbres booléennes en utilisant le trait, et a prouvé son équivalence à une formulation standard de celle-ci par Huntington en utilisant les opérateurs familiers de logique propositionnelle ( et , ou , pas ). En raison de l'auto- dualité des algèbres booléennes, les axiomes de Sheffer sont également valables pour l'une ou l'autre des opérations NAND ou NOR à la place du trait. Sheffer a interprété le trait comme un signe de non-disjonction ( NOR ) dans son article, mentionnant la non-conjonction uniquement dans une note de bas de page et sans signe spécial pour cela. C'est Jean Nicod qui a utilisé le premier le trait comme signe de non-conjonction (NAND) dans un article de 1917 et qui est depuis devenu une pratique courante. Russell et Whitehead ont utilisé le trait de Sheffer dans la deuxième édition de Principia Mathematica de 1927 et l'ont suggéré en remplacement des opérations « ou » et « non » de la première édition.

Charles Sanders Peirce (1880) avait découvert la complétude fonctionnelle de NAND ou NOR plus de 30 ans plus tôt, en utilisant le terme ampheck (pour « couper dans les deux sens »), mais il n'a jamais publié sa découverte.

Propriétés

NAND ne possède aucune des cinq propriétés suivantes, dont chacune doit obligatoirement être absente, et dont l'absence de toutes est suffisante pour, au moins un membre d'un ensemble d' opérateurs fonctionnellement complets : préservation de la vérité, fausseté- préservation, linéarité , monotonie , auto-dualité . (Un opérateur préserve la vérité (la fausseté) si sa valeur est la vérité (la fausseté) chaque fois que tous ses arguments sont la vérité (la fausseté).) Par conséquent, {NAND} est un ensemble fonctionnellement complet.

Cela peut également être réalisé comme suit : les trois éléments de l'ensemble fonctionnellement complet {AND, OR, NOT} peuvent être construits en utilisant uniquement NAND . Ainsi, l'ensemble {NAND} doit également être fonctionnel.

Autres opérations booléennes en termes de trait de Sheffer

Exprimés en termes de NAND , les opérateurs habituels de la logique propositionnelle sont :

        
Venn10.svg          Venn01.svg Venn01.svg
   
                 
Venn1011.svg          Venn0101.svg Venn1100.svg          Venn0101.svg Venn1110.svg
   
        
Venn1001.svg          Venn1110.svg Venn0111.svg
 
        
Venn0001.svg          Venn1110.svg Venn1110.svg
   
        
Venn0111.svg          Venn1010.svg Venn1100.svg

Système formel basé sur l'AVC Sheffer

Ce qui suit est un exemple d'un système formel entièrement basé sur le trait de Sheffer, mais ayant l'expressivité fonctionnelle de la logique propositionnelle :

Symboles

p n pour les entiers naturels n :

( | )

Le trait de Sheffer commute mais ne s'associe pas (par exemple, (T | T) | F = T , mais T | (T | F) = F ). Par conséquent, tout système formel incluant le trait de Sheffer comme symbole infixe doit également inclure un moyen d'indiquer le regroupement (le regroupement est automatique si le trait est utilisé comme préfixe, donc : || TTF = T et | T | TF = F ). Nous emploierons '(' et ')' à cet effet.

On écrit aussi p , q , r , … au lieu de p 0 , p 1 , p 2 .

Syntaxe

Règle de construction I : Pour chaque entier naturel n , le symbole p n est une formule bien formée (wff), appelée atome.

Règle de construction II : Si X et Y sont des wffs, alors ( X  |  Y ) est un wff.

Règle de fermeture : Toutes les formules qui ne peuvent pas être construites au moyen des deux premières règles de construction ne sont pas des wffs.

Les lettres U , V , W , X et Y sont des métavariables représentant wffs.

Une procédure de décision pour déterminer si une formule est bien formée se déroule comme suit : "déconstruire" la formule en appliquant les règles de construction à l'envers, divisant ainsi la formule en sous-formules plus petites. Répétez ensuite ce processus de déconstruction récursive pour chacune des sous-formules. Finalement, la formule devrait être réduite à ses atomes, mais si une sous-formule ne peut pas être ainsi réduite, alors la formule n'est pas un wff.

Calcul

Tous les wffs de la forme

(( U | ( V | W )) | (( Y | ( Y | Y )) | (( X | V ) | (( U | X ) | ( U | X )))))

sont des axiomes. Exemples de

sont des règles d'inférence.

Simplification

Puisque le seul connecteur de cette logique est |, le symbole | pourrait être complètement supprimé, ne laissant que les parenthèses pour regrouper les lettres. Une paire de parenthèses doit toujours entourer une paire de wff s. Des exemples de théorèmes dans cette notation simplifiée sont

( p ( p ( q ( q (( pq )( pq ))))))),
( p ( p (( qq )( pp )))).

La notation peut être simplifiée davantage, en laissant

( U ) := ( UU )

pour tout U . Cette simplification entraîne la nécessité de modifier certaines règles :

  1. Plus de deux lettres sont autorisées entre parenthèses.
  2. Les lettres ou les wff entre parenthèses sont autorisés à faire la navette.
  3. Les lettres répétées ou les wffs dans un même ensemble de parenthèses peuvent être éliminés.

Le résultat est une version entre parenthèses des graphes existentiels de Peirce .

Une autre façon de simplifier la notation est d'éliminer les parenthèses en utilisant la notation polonaise . Par exemple, les exemples précédents avec uniquement des parenthèses pourraient être réécrits en utilisant uniquement des traits comme suit

( p ( p ( q ( q (( pq )( pq )))))) devient
| p | p | q | q || pq | pq , et
( p ( p (( qq )( pp )))) devient,
| p | p || qq | pp .

Cela suit les mêmes règles que la version parenthèse, avec la parenthèse ouvrante remplacée par un trait de Sheffer et la parenthèse fermante (redondant) supprimée.

Ou (pour certaines formules) on pourrait omettre à la fois les parenthèses et les traits et permettre à l'ordre des arguments de déterminer l'ordre d' application de la fonction de sorte que, par exemple, appliquer la fonction de droite à gauche (notation polonaise inversée - toute autre convention non ambiguë basée sur commander ferait l'affaire)

Voir également

Remarques

Les références

  • Bocheński, Józef Maria (1960), Précis de logique mathématique , rév., Albert Menne, édité et traduit des éditions française et allemande par Otto Bird, Dordrecht , Hollande-Méridionale : D. Reidel .
  • Église, Alonzo (1956). Introduction à la logique mathématique. Tome 1 . Presse de l'Université de Princeton .
  • Nicod, Jean GP (1917). « Une réduction du nombre de propositions primitives de logique ». Actes de la Cambridge Philosophical Society . 19 : 32-41.
  • Charles Sanders Peirce , 1880, " A Boolian [sic] Algebra with One Constant ", in Hartshorne, C. et Weiss, P. , eds., (1931–35) Collected Papers of Charles Sanders Peirce , Vol. 4 : 12-20, Cambridge : Harvard University Press .
  • Sheffer, HM (1913), "Un ensemble de cinq postulats indépendants pour les algèbres booléennes, avec application aux constantes logiques", Transactions of the American Mathematical Society , 14 : 481-488, doi : 10.2307/1988701 , JSTOR  1988701

Liens externes