Formule propositionnelle — Wikipédia

Cet article doit être recyclé (septembre 2016).

Une réorganisation et une clarification du contenu paraissent nécessaires. Améliorez-le, discutez des points à améliorer ou précisez les sections à recycler en utilisant {{section à recycler}}.

En logique mathématique une proposition, ou formule propositionnelle, ou expression propositionnelle est une expression construite à partir de connecteurs et de variables propositionnelles.

En logique propositionnelle classique^[1], une formule propositionnelle, ou expression propositionnelle, est une formule bien formée qui possède une valeur de vérité. Si les valeurs de toutes les variables propositionnelles dans une formule propositionnelle sont données, une unique valeur de vérité peut être déterminée.

Une formule propositionnelle est construite à partir de propositions simples, telles que « cinq est supérieur à trois », ou de variables propositionnelles telles que P et Q, en utilisant des connecteurs logiques tels que NON, ET, OU et IMPLIQUE ; par exemple :

(P ET NON Q) IMPLIQUE (P OU Q).

Dans le calcul des propositions, les propositions de base sont simples ou atomiques (on ne peut pas les décomposer)^[2]. Les propositions atomiques sont liées par des connecteurs propositionnels, les plus courants sont «ET», «OU», «SI ... ALORS ...», «ni ... ni ...», « ... EST ÉQUIVALENT À ...» . En langue vernaculaire des mathématiciens, le point-virgule « ; » et le conjonctif « MAIS » sont considérés comme des expressions de « ET ». L'analyse formelle applique une « règle de parenthèses » récursive^[pas clair].

Les propositions simples sont de nature déclarative, elles affirment quelque chose au sujet de l'état du monde, par exemple « Cette vache est bleue », « Il y a un coyote! », « ce triangle est isocèle », « 3 ≥ 5 ».

Un système formel est un ensemble de symboles, appelés variables, un ensemble de symboles appelés connecteurs (*, +, ~ , &, V, =, ≡, ⋀, ¬) et un système de règles pour manipuler les symboles.

Analyse : Dans le raisonnement déductif, les philosophes, rhéteurs et mathématiciens réduisent les arguments à des formules, puis les étudient pour vérifier leur exactitude.

« Étant donné que la conscience est suffisante pour une intelligence artificielle, et que seules les entités conscientes peuvent passer le test de Turing, avant que nous puissions conclure qu'un robot est une intelligence artificielle, le robot doit d'abord passer le test de Turing. »

Les ingénieurs analysent les fonctions logiques qu'ils ont conçues en utilisant des techniques de synthèse, puis appliquent diverses techniques de réduction et de minimisation afin de simplifier leurs conceptions.

Synthèse : Les ingénieurs synthétisent en particulier les formules propositionnelles (qui finissent par se retrouver sous forme de circuits de symboles) des tables de vérité. Par exemple, on pourrait créer une table de vérité pour savoir comment l'addition binaire doit se comporter étant donné l'ajout de variables « b », « a », « carry_in » (transposé dans) « ci », et les résultats « carry_out » (transposé hors) « co » et la « somme » Σ :

Exemple : dans la 5^e rangée, ( (b+a) + ci ) = ( (1+0) + 1 ) = le nombre «2». Écrit en nombre binaire, il est égal à 10₂, où «co»=1 et Σ=0, comme écrit dans le tableau ci-dessous.

Le type le plus simple de formule propositionnelle est une variable propositionnelle. Les propositions qui sont simples (atomique) telles que les expressions symboliques sont souvent désignées par des variables nommées a, b, ou A, B, etc. Une variable propositionnelle est destinée à représenter une proposition atomique (assertion), telle que « on est samedi » = a (ici le symbole = signifie « ... est attribué la variable nommée ... ») ou « Je ne vais au cinéma que le lundi » = b.

En logique propositionnelle classique l’évaluation d'une formule propositionnelle commence par l'affectation d'une valeur de vérité à chaque variable.

Les formules propositionnelles sont construites à partir des variables propositionnelles en utilisant des connecteurs propositionnels, par exemple

• Le connecteur unaire de la négation. Si ${\displaystyle \alpha }$ est une formule, alors ${\displaystyle \lnot \alpha }$ est une formule.
• Les connecteurs binaires ${\displaystyle \land ,\lor ,\to ,\leftrightarrow ,\leftrightarrow }$. Ainsi, par exemple, si ${\displaystyle \alpha }$ et ${\displaystyle \beta }$ sont des formules propositionnelles, alors ${\displaystyle (\alpha \to \beta )}$ est une formule propositionnelle.
• Des connecteurs binaires, tels que NON-ET, NON-OU, et XOR.
• Le connecteur ternaire SI ... ALORS ... SINON ...
• Les connecteurs nullaires ⊤ et ⊥

Voici les connecteurs communs à la rhétorique, philosophie et aux mathématiques, ainsi que leurs tables de vérité. Les symboles utilisés varient d'un auteur à un autre et entre les domaines d'activité. En général, les abréviations «V» et «F» représentent l'évaluation des variables de la formule propositionnelle (par exemple, l'affirmation : « Cette vache est bleue » aura la valeur de vérité « V » pour Vrai ou « F » pour Faux, dans le cas contraire.)

Les connecteurs s'énoncent de nombreuses façons, par exemple « a IMPLIQUE b » se dit également « SI a ALORS b ». Certains d'entre eux sont présentés dans le tableau ci-dessous.

						b only if a
						b EST SUFFISANT POUR a
						a EST NÉCESSAIRE POUR b	b SI ET SEULEMENT SI a ; b SSI a
					OU inclusif	SI b ALORS a	b EST NÉCESSAIRE ET SUFFISANT POUR a
		négation	négation	conjonction	disjonction	implication	biconditionel
variable	variable	NON b	NON a	b ET a	b OU a	b IMPLIQUE a	b EST logiquement équivalent À a	f EST UNE tautologie	NI a NI b	b barre a	OU exclusif
b	a	${\displaystyle \lnot }$(b)	${\displaystyle \lnot }$(a)	(b ${\displaystyle \land }$ a)	(b ${\displaystyle \lor }$ a)	(b ${\displaystyle \to }$ a)	(b ${\displaystyle \leftrightarrow }$ a)	(f = formule)	(a NON-OU b)	(b|a)	varie
F	F	V	V	F	F	V	V	V	V	V	F
F	V	V	F	F	V	V	F	V	F	V	V
V	F	F	V	F	V	F	F	V	F	V	V
V	V	F	F	V	V	V	V	V	F	F	F

si ... alors ... sinon ... est un connecteur ternaire. En logique classique^[3], tous les autres connecteurs peuvent être construits à partir de ce connecteur et des constantes ⊥ (pour le « faux ») et T (pour le « vrai ») ; si A alors B sinon C équivaut à (A ∧ B) ∨ (¬A ∧ C) ou encore à (A → B) ∧ (¬A → C).

Comme indiqué ci-dessus, le connecteur SI c ALORS b SINON a est construit, soit à partir de connecteurs à 2 arguments SI ... ALORS ... et ET, soit de OU et ET et le connecteur unaire NON. Les connecteurs tels que l'argument n-aire ET (a & b & c & ... & n), OU (V b V c V ... V n) sont construits à partir des chaînes des deux arguments ET et OU et écrits sous forme abrégée sans parenthèses. Ceux-ci, et d'autres connecteurs, peuvent alors servir de blocs de construction pour former encore d'autres connecteurs. Les rhéteurs, philosophes et mathématiciens utilisent des tables de vérité et les divers théorèmes d'analyse dans le but de simplifier leurs formules.

Une définition crée un nouveau symbole ainsi que son comportement, souvent dans le but de l’abréviation. Une fois que la définition est présentée, soit sous forme de symboles soit de formule équivalente, elle peut être utilisée. Le symbole suivant =_Df fait partie de la convention de Reichenbach^[4]. Quelques exemples de définitions pratiques tirées de l'ensemble de symbole { ~, &, (,) }. Chaque définition est la création d'une formule logiquement équivalente et peut être utilisée pour la substitution ou pour le remplacement.

• définition d'une nouvelle variable : (c & d) =_Df s
• OU : ~(~a & ~b) =_Df (a V b)
• IMPLICATION : (~a V b) =_Df (a → b)
• XOR : (~a & b) V (a & ~b) =_Df (a ⊕ b)
• ÉQUIVALENCE LOGIQUE : ( (a → b) & (b → a) ) =_Df ( a ≡ b )

Substitution : La variable ou la sous-formule pouvant être substituées à une autre variable, une constante ou sous-formule doit être remplacée tout au long de la formule générale.

Exemple : (c & d) V (p & ~(c & ~d)), mais (q1 & ~q2) ≡ d. Maintenant, chaque fois que la variable « d » se produit, substitut (q₁ & ~q₂) :

(c & (q₁ & ~q₂)) V (p & ~(c & ~(q₁ & ~q₂)))

Remplacement : (i) la formule à remplacer doit être logiquement équivalente (reliée par ≡ ou ↔) à la formule qui le remplace, et (ii) à la différence de la substitution, le remplacement ne se produit que dans un seul endroit.

Exemple : Utilisez cet ensemble de formules équivalentes : 1 : ( (a V 0) ≡ a ). 2 : ( (a & ~a) ≡ 0 ). 3 : ( (~a V b) =_Df (a → b) ). 6. ( ~(~a) ≡ a )

• débuter avec « a » : a
• Utiliser 1 pour remplacer « a » avec (a V 0) : (a V 0)
• Utiliser la notion de « schéma » pour substituer b de a dans 2 : ( (a & ~a) ≡ 0 )
• Utiliser 2 pour remplacer 0 avec (b & ~b) : ( a V (b & ~b) )
• (voir ci-dessous pour comment distribuer « un V » sur (b & ~b), etc.

La présentation usuelle de la logique propositionnelle (voir Enderton 2002) utilise les connecteurs ${\displaystyle \lnot ,\land ,\lor ,\to ,\leftrightarrow }$. L'ensemble des formules sur un ensemble donné de variables propositionnelles est inductivement défini comme le plus petit ensemble d'expressions telles que :

• Chaque variable propositionnelle contenue dans l'ensemble est une formule,
• ${\displaystyle (\lnot \alpha )}$ est une formule quand ${\displaystyle \alpha }$ en est une, et
• ${\displaystyle (\alpha \,\Box \,\beta )}$ est une formule quand ${\displaystyle \alpha }$ et ${\displaystyle \beta }$ sont des formules et ${\displaystyle \Box }$ est l'un des connecteurs logiques binaires ${\displaystyle \land ,\lor ,\to ,\leftrightarrow }$.

Cette définition inductive peut être facilement étendue pour couvrir des connecteurs supplémentaires.

La définition inductive peut également être reformulée sous forme d'opération de clôture (Enderton, 2002). Soit V un ensemble de variables propositionnelles et X_V désignent l'ensemble de toutes les chaînes à partir d'un alphabet, y compris les symboles de V, les parenthèses de gauche et de droite, et tous les connecteurs logiques nécessaires. Chaque connecteur logique correspond à une opération de construction de formule, une fonction de XX_V à XX_V :

• Étant donné une chaîne z, l'opération ${\displaystyle {\mathcal {E}}_{\lnot }(z)}$ retourne ${\displaystyle (\lnot z)}$.
• Étant donné une chaîne z, l'opération ${\displaystyle {\mathcal {E}}_{\land }(y,z)}$ retourne ${\displaystyle (y\land x)}$. Il existe des opérations similaires ${\displaystyle {\mathcal {E}}_{\lor }}$, ${\displaystyle {\mathcal {E}}_{\to }}$, et ${\displaystyle {\mathcal {E}}_{\leftrightarrow }}$ correspondant aux autres connecteurs binaires.

Les « principes » (ou « lois ») suivants du calcul propositionnel classique sont utilisés pour « réduire » les formules complexes^[5]. Les « principes » peuvent être facilement vérifiés avec des tables de vérité. Pour chaque principe, le connecteur principal est associé à l'équivalence logique ≡ ou à l'identité =. Une analyse complète des  2ⁿ valeurs de vérité pour ses n variables distinctes se traduira par une colonne de 1 sous ce connecteur. Cette constatation fait de chaque principe, par définition, une tautologie. Et, pour un principe donné, puisque sa formule à gauche et à droite sont équivalentes (ou identiques), peuvent être remplacés par un autre.

Exemple : La table de vérité suivante est la loi de De Morgan portant sur le NON sur OU : ~(a V b) ≡ (~a & ~b). À gauche du connecteur principal ≡ (colonne jaune « taut ») la formule ~(b V a) évaluée à (1, 0, 0, 0) dans la colonne « P». Sur la droite de « taut » la formule (~(b) V ~(a)) est aussi évaluée à (1, 0, 0, 0) dans la colonne « Q ». Comme les deux colonnes possèdent des évaluations équivalentes, l'équivalence logique ≡ sous « taut » est évaluée à (1, 1, 1, 1), i.e. P ≡ Q. 

Notez que si les symboles 1 et 0 (ou T et F) sont utilisés dans un système axiomatique, ils sont considérés comme des fbfs et obéiront donc aux mêmes règles que celles des variables : ancienneté Connective (symbole rang).

En général, pour éviter toute confusion lors de l'analyse et de l'évaluation des formules propositionnelles, on fait usage des parenthèses. Cependant, très souvent, les auteurs ne les utilisent pas. Pour analyser une formule complexe, il faut d'abord connaître la priorité, ou le rang, de chaque connecteur présent dans celles-ci. Pour une formule bien-formée, il faut commencer par le connecteur ayant la priorité la plus élevée et ajouter des parenthèses autour de ses composants, puis se déplacer vers le connecteur à la priorité inférieure dans le classement^[pas clair]. De l'opérateur possédant le plus de priorité à celui qui en possède le moins, les signes ∀x et ∃x, l'IDENTITÉ = et les signes arithmétiques ajoutés^[6] :

≡ (ÉQUIVALENCE LOGIQUE), → (IMPLICATION), & (ET), V (OU), ~ (NON), = (IDENTITÉ), + (somme arithmétique), *(multiplication arithmétique), ' (s, successeur arithmétique).

Ainsi, la formule peut être analysée, mais noter que, parce que NON n'obéit pas à la loi de la distributivité, les parenthèses autour de la formule (~ c & ~ d) sont obligatoires :

Exemple : « d & c V w » réécrit donne ( (d & c) V w )

Exemple : « a & a → b ≡ a & ~a V b » réécrit (rigoureusement) est 

• ≡ à la priorité : ( ( a & a → b ) ≡ ( a & ~a V b ) )
• → à la priorité : ( ( a & (a → b) ) ≡ ( a & ~a V b ) )
• & à la priorité des deux côtés : ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~a V b) ) )
• ~ à la priorité : ( ( ( (a) & (a → b) ) ) ≡ ( ( (a) & (~(a) V b) ) )

Exemple :

d & c V p & ~(c & ~d) ≡ c & d V p & c V p & ~d réécrit est ( ( (d & c) V ( p & ~((c & ~(d)) ) ) ) ≡ ( (c & d) V (p & c) V (p & ~(d)) ) )

Les opérateurs ET et OU sont tous deux soumis aux lois commutative et associative :

• Loi commutative pour OU : (a V b) ≡ (b V a)
• Loi commutative pour ET : (a & b) ≡ (b & a)
• Loi associative pour OU : ((a V b) V c) ≡ (a V (b V c))
• Loi associative pour ET : ((a & b) & c) ≡ (a & (b & c))

L'opérateur OU se distribue sur l'opérateur ET, et l'opérateur ET se distribue sur l'opérateur OU.

• Distributivité de OU : (c ∨ (a & b)) ≡ ((c ∨ a) & (c ∨ b))
• Distributivité de ET : (c & (a ∨ b)) ≡ ((c & a) ∨ (c & b))

L’opérateur ~ lorsqu'il est appliqué à une disjonction produit une conjonction et similairement l’opérateur ~ lorsqu'il est appliqué à une conjjonction produit une disjonction. Ce sont les lois de de Morgan.

• Loi de De Morgan pour OU : ~(a V b) ≡ (~a & ~b)
• Loi de De Morgan pour ET : ~(a & b) ≡ (~a V ~b)

L'idempotence dit que quand on applique un élément à lui-même, on obtient l'élément en question^[7] :

• Absorption pour OU : (a V a) ≡ a
• Absorption pour ET : (a & a) ≡ a

En logique classique :

• ~(~a) = a

Telles qu'elles ont été présentées, ces formules peuvent être analysées de manière unique pour déterminer leur structure en termes de variables propositionnelles et de connecteurs logiques. Lorsque les formules sont écrites en notation infixe, comme ci-dessus, la désambiguïsation est assurée grâce à une utilisation appropriée de parenthèse. Alternativement, les formules peuvent être écrites en notation polonaise ou en notation polonaise inverse, ce qui élimine le besoin de parenthèses. Elles peuvent aussi être décrites par un arbre syntaxique.

La définition inductive des formules infixes dans la section précédente peut être convertie en une grammaire formelle sous la forme de Backus-Naur :

<formule> : := <variable propositionnelle>

| ( ${\displaystyle \lnot }$ <formule> )

| ( <formule> ${\displaystyle \land }$ <formule>)

| ( <formule> ${\displaystyle \lor }$ <formule> )

| ( <formule> ${\displaystyle \to }$ <formule> )

| ( <formule> ${\displaystyle \leftrightarrow }$ <formule> )

On peut montrer que toute expression appariée par la grammaire a le même nombre de parenthèses à gauche qu'à droite, et toute partie initiale non vide d'une formule a plus de parenthèses à gauche qu'à droite^[8]. Ce fait peut être utilisé pour donner un algorithme pour l'analyse syntaxique des formules. Cette idée peut être utilisée pour générer un analyseur de descente pour les formules récursives.

Exemple de comptage de parenthèses :

Cette méthode localise « 1 » comme le connectif principal^[9]. Il localise aussi le connecteur le plus interne, où l'on commencerait l'évaluation de la formule sans l'utilisation d'une table de vérité, par exemple au « niveau 6 ».

Un ensemble de connecteurs logiques est dit complet si chaque formule propositionnelle est tautologiquement équivalente à une formule avec seulement les connecteurs de cet ensemble. Il y a beaucoup d'ensembles complets de connecteurs, y compris ${\displaystyle \{\land ,\lnot \}}$, ${\displaystyle \{\lor ,\lnot \}}$, et ${\displaystyle \{\to ,\lnot \}}$^[10]. Certaines paires ne sont pas complètes, par exemple ${\displaystyle \{\land ,\lor \}}$.

Le connecteur binaire correspondant NON-ET est appelé la barre de Sheffer, et écrit avec une barre verticale | ou verticale flèche ↑. L'intégralité de ce connecteur a été noté dans les Principia Mathematica (1927 : xvii). Étant donné qu'il est complet sur lui-même, tous les autres connecteurs peuvent être exprimés en utilisant uniquement celui-ci. Par exemple, lorsque le symbole « ≡ » représente l'équivalence logique :

~p ≡ p|p

p → q ≡ p|~q

p V q ≡ ~p|~q

p & q ≡ ~(p|q)

En particulier, les connecteurs nullaires ${\displaystyle \top }$ (représentant la vérité) et ${\displaystyle \bot }$ (représentant la fausseté) peuvent être exprimés en utilisant la barre :

${\displaystyle \top \equiv (a|(a|a))}$

${\displaystyle \bot \equiv (\top |\top )}$

Ce connecteur, avec {0, 1} (ou { ${\displaystyle \bot }$, ${\displaystyle \top }$ }), forme un ensemble complet. Dans ce qui suit, la relation SI ... ALORS ... SINON(c, b, a) = d représente ((c → b) V (~c → a)) ≡ ((c & b) V (~c & a)) = d

(c, b, a) :

(c, 0, 1) ≡ ~c

(c, b, 1) ≡ (c → b)

(c, c, a) ≡ (c V a)

(c, b, c) ≡ (c & b)

Exemple : L'exemple suivant montre comment une preuve basée sur un théorème « (c, b, 1) ≡ (c → b) » est démontrée. (Note : (c → b) est défini comme (~ c V b)) :

• Commencez par la forme réduite : ( (c & b) V (~c & a) )
• Substituez « 1 » pour a : ( (c & b) V (~c & 1) )
• Identité (~c & 1) = ~c : ( (c & b) V (~c) )
• Loi de commutativité pour V : ( (~c) V (c & b) )
• Distribuez « ~c V » sur (c & b) : ( ((~c) V c ) & ((~c) V b )
• Principe du tiers exclu (((~c) V c ) = 1 ) : ( (1) & ((~c) V b ) )
• Distribuez « (1) & » sur ((~c) V b) : ( ((1) & (~c)) V ((1) & b )) )
• Commutativité et Identité (( 1 & ~c) = (~c & 1) = ~c, et (( 1 & b) ≡ (b & 1) ≡ b : ( ~c V b )
• ( ~c V b ) est défini comme c → b C. Q. F. D.

Dans la table de vérité suivante, la colonne intitulée « taut », pour tautologie, évalue l'équivalence logique (symbolisé ici par le signe ≡) entre les deux colonnes nommées d. Parce que les quatre rangées sous « taut » sont des 1, l'équivalence représente en effet une tautologie.

Une formule propositionnelle arbitraire peut avoir une structure très compliquée. Il est souvent commode de travailler avec des formules qui ont des formes plus simples, connus sous le nom de formes normales. Certaines formes normales courantes comprennent la forme normale conjonctive et la forme normale disjonctive. Toute formule propositionnelle peut être réduite à sa forme normale conjonctive ou disjonctive.

La réduction à la forme normale est relativement simple une fois la table de vérité de la formule concernée prête. Mais de nouvelles tentatives pour réduire au minimum le nombre de littéraux (voir ci-dessous) nécessitent quelques outils : la réduction par les lois de De Morgan et des tables de vérité peut être difficile à réaliser, mais les tables de Karnaugh sont très appropriées pour étudier un petit nombre de variables (5 ou moins). Certaines méthodes tabulaires sophistiquées ; pour plus de détails, voir la méthode de Quine-Mc Cluskey.

Bertrand Russell (1912 :74) énumère trois lois de la pensée dérivées d'Aristote : (1) Le principe d'identité : « Tout ce qui est, est », (2) Le principe de la non-contradiction : « Rien ne peut pas à la fois être et ne pas être » et (3) Le principe du tiers exclu : « Tout doit être ou ne pas être ».

Exemple : Ici O est une expression autour d'un objet :

(1) Principe d'identité : O = O

(2) Principe de non-contradiction : ~(O & ~(O))

(3) Principe du tiers exclu : (O V ~(O))

Bien qu'un calcul propositionnel soit né avec Aristote, la notion d'une algèbre appliquée à des propositions a dû attendre le début du XIX^e siècle. Dans une réaction (défavorable) à la tradition de 2000 ans des syllogismes d'Aristote, l'Essai sur l'entendement humain de John Locke (1690) a utilisé le mot sémiotique (théorie de l'utilisation de symboles). En 1826, Richard Whately a fait une analyse critique de la logique syllogistique avec une sympathie envers la sémiotique de Locke. Le travail de George Bentham (1827) a donné lieu à la notion de « quantification du prédicat » (1827) (aujourd'hui symbolisée par ∀ ≡ « pour tout »). Une « ligne » lancée par William Hamilton sur un conflit de priorité avec Auguste De Morgan « a inspiré George Boole pour écrire ses idées sur la logique, et de les publier en tant AML [Analyse Mathématique de la Logique] en 1847 » (Grattin-Guinness et Bornet 1997 : xxviii).

À propos de leur contribution, Grattin-Guinness et Bornet commentent :

« La principale innovation de Boole était [le] principe [ xⁿ = x ] pour la logique : celui-ci déclare que les actes mentaux de choisir la propriété x et en choisissant à nouveau x et encore est le même que le choix de x fois ... a comme conséquence la formation des équations x•(1-x)=0 et x+(1-x)=1 qui, pour lui, expriment respectivement le principe de non-contradiction et le principe du tiers exclu » (p. xxviiff). Pour Boole « 1 » était l'univers du discours et « 0 » n'était rien.

L'œuvre massive de Gottlob Frege (1879) a donné lieu à un calcul formel des propositions, mais son symbolisme est si décourageant qu'il a eu peu d'influence à l'exception d'une seule personne : Bertrand Russell. Tout d'abord comme élève d'Alfred North Whitehead, il étudia le travail de Frege et suggéra une correction (célèbre et notoire en 1904) autour du problème d'une antinomie qu'il a découvert dans le traitement de Frege (cf. paradoxe de Russell). Le travail de Russell a conduit à une collaboration avec Whitehead qui, dans l'année 1912, a produit le premier volume des Principia Mathematica (PM). Cet ouvrage est le précurseur à ce que nous considérons aujourd'hui la logique propositionnelle « moderne ». En particulier, les PM introduisent le NON, le OU et l'affirmation ⊦ comme primitifs. Exprimée à l'aide de ces notions, l'IMPLICATION → est ainsi définie (def. *1.01 : ~p V q), puis le ET (def. *3.01 : ~(~p V ~q)), et enfin, l'ÉQUIVALENCE p ←→ q (*4.01 : (p → q) & (q → p)).

• Henry M. Sheffer (1921) et Jean Nicod démontrent que seulement un connecteur, la « barre » | est suffisant pour exprimer toutes les formules propositionnelles.
• Emil Post (1921) développe la méthode de table de vérité d'analyse dans son « Introduction à une théorie générale des propositions élémentaires ». Il prend note de la barre de Nicod | .
• Whitehead et Russell ajoutent une introduction à leur re-publication des Principia Mathematica, en 1927, ajoutant un traitement, en partie, favorable à la « barre ».

Calcul et logique commutative :

• George Stibitz (1937) invente l'additionneur binaire en utilisant des relais mécaniques. Il construisit cela sur sa table de cuisine.
• Alan Turing construit un multiplicateur utilisant des relais (1937-1938).
• Les manuels sur les « circuits de commutation » apparaissent au début des années 1950.
• Willard Quine 1952 et 1955, E. W. Veitch 1952, et M. Karnaugh (1953) développent des méthodes de tables pour simplifier les fonctions propositionnelles.
• George H. Mealy (1955) et Edward F. Moore (1956) abordent la théorie des « machines » séquentielles (par exemple, la commutation de circuit).
• E. J. McCluskey et H. Shorr développent une méthode pour simplifier les circuits (de commutation) propositionnels (1962).

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Propositional formula » (voir la liste des auteurs).
• Bender, Edward A. and Williamson, S. Gill, 2005, A Short Course in Discrete Mathematics, Dover Publications, Mineola NY, (ISBN 0-486-43946-1).
• Enderton, H. B., 2002, A Mathematical Introduction to Logic. Harcourt/Academic Press. (ISBN 0-12-238452-0)
• Goodstein, R. L., (Pergamon Press 1963), 1966, (Dover edition 2007), Boolean Algebra, Dover Publications, Inc. Minola, New York, (ISBN 0-486-45894-6). pp. 76–93.
• Ivor Grattan-Guinness et Gérard Bornet 1997, George Boole: Selected Manuscripts on Logic and its Philosophy, Birkhäuser Verlag, Basil, (ISBN 978-0-8176-5456-6) (Boston).
• A. G. Hamilton 1978, Logic for Mathematicians, Cambridge University Press, Cambridge UK, (ISBN 0-521-21838-1).
• E. J. Edward J. McCluskey 1965, Introduction to the Theory of Switching Circuits, McGraw-Hill Book Company, New York. No ISBN. Library of Congress Catalog Card Number 65-17394. McCluskey était un étudiant de Willard Quine et développé quelques théorèmes notables avec Quine.
• Marvin L. Minsky 1967, Computation: Finite and Infinite Machines, Prentice-Hall, Inc, Englewood Cliffs, N.J.. No ISBN. Library of Congress Catalog Card Number 67-12342.
• Paul C. Rosenbloom 1950, Dover edition 2005, The Elements of Mathematical Logic, Dover Publications, Inc., Mineola, New York, (ISBN 0-486-44617-4).
• Joel W. Robbin 1969, 1997, Mathematical Logic: A First Course, Dover Publications, Inc., Mineola, New York, (ISBN 0-486-45018-X) (pbk.).
• Patrick Suppes 1957 (1999 Dover edition), Introduction to Logic, Dover Publications, Inc., Mineola, New York. (ISBN 0-486-40687-3) (pbk.). This book is in print and readily available.
• E. V. Huntington, "Sets of Independent Postulates for the Algebra of Logic", Transactions of the American Mathematical Society, Vol. 5 91904) pp. 288-309.
• Alfred Tarski 1941 (1995 Dover edition), Introduction to Logic and to the Methodology of Deductive Sciences, Dover Publications, Inc., Mineola, New York. (ISBN 0-486-28462-X) (pbk.).
• Jean van Heijenoort 1967, 3rd printing with emendations 1976, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Harvard University Press, Cambridge, Massachusetts. (ISBN 0-674-32449-8) (pbk.), lettres de Russell à Frege (1902) et lettres de Frege à Russell (1902), Paradoxe de Richard (1905), Post (1921).
• Alfred North Whitehead and Bertrand Russell 1927 2nd edition, paperback edition to *53 1962, Principia Mathematica, Cambridge University Press.
• William E. Wickes 1968, Logic Design with Integrated Circuits, John Wiley & Sons, Inc., New York. (p. 18ff).

• Portail de la logique
• Portail de l’algèbre
• Portail de l'informatique théorique