Calcul des propositions

Le calcul des propositions ou calcul propositionnel, (ou encore logique des propositions) fait partie de la logique mathématique. Il a pour objet l'étude des relations logiques entre « propositions »^[1] et définit les lois formelles selon lesquelles les propositions complexes sont formées en assemblant des propositions simples au moyen des connecteurs logiques et celles-ci sont enchaînées pour produire des raisonnements valides. Il est un des systèmes formels, piliers de la logique mathématique dont il aide à la formulation des concepts^[2]. Il est considéré comme la forme moderne de la logique stoïcienne^[3].

La notion de proposition a fait l'objet de nombreux débats au cours de l'histoire de la logique ; l'idée consensuelle est qu'une proposition est une construction syntaxique censée parler de vérité. En logique mathématique, le calcul des propositions est la première étape dans la définition de la logique et du raisonnement. Il définit les règles de déduction qui relient les propositions entre elles, sans en examiner le contenu ; il est ainsi une première étape dans la construction du calcul des prédicats, qui lui s'intéresse au contenu des propositions et qui est une formalisation achevée du raisonnement mathématique. Le calcul des propositions, ou calcul propositionnel est encore appelé logique des propositions, logique propositionnelle ou calcul des énoncés.

Quoique le calcul des propositions ne se préoccupe pas du contenu des propositions, mais seulement de leurs relations, il peut être intéressant de discuter ce que pourrait être ce contenu. Une proposition donne une information sur un état de chose. Ainsi « 2 + 2 = 4 » ou « le livre est ouvert » sont deux propositions.

En logique classique (logique bivalente), une proposition peut prendre uniquement les valeurs vrai ou faux. Une phrase optative (qui exprime un souhait comme « Que Dieu nous protège ! »), une phrase impérative (« viens ! », « tais-toi ! ») ou une interrogation n'est pas une proposition. « Que Dieu nous protège ! » ne peut être ni vraie ni fausse : elle exprime uniquement un souhait du locuteur.

Par contre, une phrase comme « Dans ce calcul, toutes les variables informatiques sont toujours strictement positives » est une proposition dont le contenu a été modifié par le quantificateur toutes les et la modalité temporelle toujours et qui est donc supposée s'avérer dans la durée. Ce type de proposition relève de la logique modale et plus précisément de la logique temporelle. En effet, la modalité toujours affirme sa pérennité dans le temps et elle sera donc toujours vraie, tandis que le quantificateur tous les stipule que la proposition sont toujours positives s'applique à toutes les variables informatiques, ce qui d'ailleurs sort du domaine du calcul des propositions.

Si une proposition est une assertion ayant une valeur de vérité, un prédicat est lui une expression dont la valeur de vérité dépend de variables qu'elle renferme. Le prédicat « Mon pays se situe en Europe » sera vrai, faux ou indéterminé en fonction de la valeur de la variable « Mon pays ». Si le lecteur est suisse, on obtiendra la proposition « La Suisse se situe en Europe », qui est vraie ; si le lecteur est canadien, on obtiendra la proposition « Le Canada se situe en Europe », qui est fausse^[4] ; si le lecteur est russe, on obtiendra la proposition « La Russie se situe en Europe » qui est indéterminée, car, comme on sait la Russie est à cheval sur l'Europe et l'Asie^[5].

Un calcul ou un système déductif est, en logique, un ensemble de règles permettant en un nombre fini d'étapes et selon des règles explicites de pouvoir affirmer si une proposition est vraie. Un tel procédé s'appelle une démonstration. On associe aussi aux propositions une structure mathématique qui permet de garantir que ces raisonnements ou démonstrations ont du sens, on dit qu'on lui a donné une sémantique. En calcul des propositions classique, cette sémantique n'utilise que deux valeurs, vrai et faux (souvent notées 1 et 0). Une proposition entièrement déterminée (c'est-à-dire dont les valeurs des constituants élémentaires sont déterminées) ne prend qu'une seule de ces deux valeurs.

Dans les théories de la logique mathématique, on considère donc deux points de vue dits syntaxique et sémantique, c'est le cas en calcul des propositions.

• Syntaxe des formules propositionnelles : il s’agit de définir le langage du calcul des propositions par les règles d’écriture des propositions.
• Le sens des formules propositionnelles (qui sont les expressions syntaxiquement correctes) est donné par le sens des connecteurs. Il peut être décrit de deux façons.
  • Par la sémantique : il s’agit ici d'interpréter les symboles représentant les connecteurs logiques par des fonctions de la valeur de vérité des propositions de base (ainsi ${\displaystyle \lnot }$ signifie non). Ce sens est donné en logique classique par des tables de vérité, dans d'autres logiques par exemple par des modèles de Kripke.
  • Par la déduction : le sens des connecteurs est décrit de façon opératoire, par des règles purement syntaxiques dites règles d'inférence. Ces règles permettent la déduction de propositions à partir d'autres. Elles engendrent des propositions spécifiques que l'on appelle des théorèmes.

Pour une logique donnée, les règles de déductions envisagées sont correctes vis-à-vis de la sémantique, au sens où à partir de propositions vraies on ne peut déduire que des propositions vraies. Si la déduction correspond parfaitement à la sémantique le système est dit complet.

Le système exposé ci-dessous se situe dans le cadre de la logique classique, qui est la branche de la logique mathématique la plus utilisée en mathématiques. On trouvera plus loin une présentation de logiques non classiques. L'adjectif « classique » ne doit pas être pris dans un sens de « normalité », mais comme un attribut que lui a donné l'histoire de la logique, elle aurait tout aussi bien pu s'appeler « booléenne ».

À la base de la syntaxe du calcul des propositions sont les variables propositionnelles ou propositions atomiques, notées p, q, etc., qui constituent généralement un ensemble infini dénombrable.

Les deuxièmes constituants de base du langage du calcul des propositions sont les opérateurs ou connecteurs. Ce sont des symboles qui permettent de construire des propositions plus élaborées. Les plus courants de ces connecteurs logiques sont :

et	${\displaystyle \wedge }$
ou	${\displaystyle \vee }$
non	${\displaystyle \neg }$
implique	${\displaystyle \rightarrow }$
équivaut à	${\displaystyle \leftrightarrow }$

On considère souvent aussi la constante notée ⊥, prononcé « taquet vers le haut »^[6], « type vide », « bottom » ou « bot », qui vise à représenter le faux.

À côté de ces symboles on utilise des parenthèses pour lever les ambiguïtés dans les formules (choix adopté ci-dessous), ou une notation comme la notation polonaise, inventée par le logicien polonais Jan Łukasiewicz. Il est important que la définition des formules soit simple et sans ambiguïtés, pour permettre en particulier les définitions inductives sur la structure des formules, mais pratiquement il est possible d'économiser les parenthèses, soit en adoptant certaines conventions pour lever les ambiguïtés, soit parce que le contexte fait que ces ambiguïtés sont sans importance.

Le calcul des propositions repose de plus sur des règles de formation indiquant comment construire des propositions complexes à partir des propositions élémentaires, ou atomes, que sont les variables propositionnelles, et d'éventuelles constantes comme ⊥. Ces règles déterminent quels assemblages de signes, quels mots, sont bien formés et désignent des propositions. La définition dépend d'un choix de connecteurs, et d'un choix d'atomes.

On se donne un ensemble ${\displaystyle {}{\mathcal {P}}}$ de variables propositionnelles. L'ensemble des propositions (ou formule propositionnelle) (sur ${\displaystyle {}{\mathcal {P}}}$) est défini par induction, c'est-à-dire que c'est le plus petit ensemble tel que :

• une variable propositionnelle p de ${\displaystyle {}{\mathcal {P}}}$ est une proposition ;
• ⊥ est une proposition ;
• si P et Q sont des propositions, alors (P ∧ Q), (P ∨ Q), (P → Q), (P ↔ Q) et ¬P sont des propositions.

Exemples : Si P, Q et R sont des propositions,

(P → Q) → (¬Q → ¬P) est une proposition.

(P → ⊥) → ⊥ est une proposition.

P ∧ ¬P est une proposition.

(P ∧ Q) ∨ R est une proposition.

P ∧ Q ∨ n'est pas une proposition.

Afin d'alléger la présentation des expressions sans mettre en péril l'absence d'ambiguïté, on autorise par des conventions syntaxiques certaines entorses à la définition ci-dessus.

• On omet généralement les parenthèses extrêmes des propositions.
• On supprime souvent les parenthèses en associant les expressions de gauche à droite quand il s'agit du même connecteur : A ∧ B ∧ C pour ((A ∧ B) ∧ C).
• L'implication constitue un cas particulier. Par convention, elle est associative à droite : A → B → C → D se lit A → (B → (C → D)).

Pour la lisibilité, on utilise également plusieurs formes de parenthèses (taille, remplacement par des crochets...)

Par ailleurs, on démontre que seules les parenthèses ouvrantes sont nécessaires à la non-ambiguïté de la lecture des propositions qui pour cette raison sont remplacées par un point "." dans certaines notations.

Le calcul des propositions permet de présenter les trois systèmes déductifs les plus connus. On se limite pour cela aux propositions contenant, outre les variables propositionnelles, seulement des implications, des disjonctions et des occurrences de faux autrement dit de ⊥. On admet que ¬P est une abréviation de P → ⊥. Si P est un théorème, autrement dit une proposition qui a une démonstration, on note cela par ⊢P.

Les systèmes déductifs utilisent des règles de déduction (appelées aussi règles d'inférence) qui s'écrivent:

${\displaystyle {\frac {\varphi _{1}\quad ...\quad \varphi _{n}}{\psi }}.}$

Les ${\displaystyle \varphi _{i}}$ sont appelées les prémisses et ${\displaystyle \psi }$ est appelée la conclusion.

Il n'y a qu'une seule règle appelée le modus ponens, elle s'écrit :

${\displaystyle {\frac {\vdash (P\to Q)\quad \vdash P}{\vdash Q}}.}$

Elle peut se comprendre ainsi : si ${\displaystyle P\to Q}$ est un théorème et ${\displaystyle P}$ est un théorème alors ${\displaystyle Q}$ est un théorème. À cela, on peut ajouter :

trois axiomes pour l'implication et le faux :

• ${\displaystyle \vdash P\to (Q\to P)}$,
• ${\displaystyle \vdash (P\to (Q\to R))\to ((P\to Q)\to (P\to R))}$,
• ${\displaystyle \vdash (\lnot P\to \lnot Q)\to (Q\to P)}$ ;

trois axiomes pour la disjonction :

• ${\displaystyle {\big (}P\to R)\to ((Q\to R)\to ((P\vee Q)\to R))}$,
• ${\displaystyle P\to {\big (}P\vee Q)}$,
• ${\displaystyle Q\to {\big (}P\vee Q)}$.

trois axiomes pour la conjonction :

• ${\displaystyle {\big (}R\to P)\to ((R\to Q)\to (R\to (P\wedge Q)))}$,
• ${\displaystyle {\big (}P\wedge Q)\to P}$.
• ${\displaystyle {\big (}P\wedge Q)\to Q}$.

Alors que la déduction à la Hilbert manipule et démontre des théorèmes, la déduction naturelle démontre des propositions sous des hypothèses et quand il n'y a pas (plus) d'hypothèses, ce sont des théorèmes. Pour dire qu'une proposition ${\displaystyle P}$ est conséquence d'un ensemble ${\displaystyle \Gamma }$ d'hypothèses, on écrit ${\displaystyle \Gamma \vdash P}$. Alors que dans la déduction à la Hilbert, il n'y a qu'une règle et plusieurs axiomes, dans la déduction naturelle il y a un seul axiome et plusieurs règles. Pour chaque connecteur, on classe les règles en règles d'introduction et en règles d'élimination.

• L'axiome est ${\displaystyle \Gamma ,P\vdash P}$.
• La règle d'introduction de l'implication:

${\displaystyle {\frac {\Gamma ,P\vdash Q}{\Gamma \vdash P\to Q}}}$

• La règle d'élimination de l'implication:

${\displaystyle {\frac {\Gamma \vdash P\to Q\qquad \Gamma \vdash P}{\Gamma \vdash Q}}}$

• Les deux règles d'introduction de la disjonction, droite et gauche:

${\displaystyle {\frac {\Gamma \vdash P}{\Gamma \vdash P\vee Q}}\qquad \qquad {\frac {\Gamma \vdash Q}{\Gamma \vdash P\vee Q}}}$

• La règle d'élimination de la disjonction:

${\displaystyle {\frac {\Gamma \vdash P\vee Q\qquad \Gamma ,P\vdash R\qquad \Gamma ,Q\vdash R}{\Gamma \vdash R}}}$

• La règle d'élimination du faux:

${\displaystyle {\frac {\Gamma \vdash \perp }{\Gamma \vdash P}}}$

En outre, il y a une règle de réduction à l'absurde, nécessaire en logique classique:

${\displaystyle {\frac {\Gamma ,\neg P\vdash \perp }{\Gamma \vdash P}}}$

On remarquera que la règle d'élimination de l'implication est très proche du modus ponens, d'ailleurs on l'appelle aussi modus ponens. On remarquera qu'il n'y pas de règle d'introduction du faux et que la règle d'élimination du faux revient à dire que si d'un ensemble d'hypothèses je déduis le faux (ou l'absurde) alors de ce même ensemble je peux déduire n'importe quoi. On remarquera que la réduction à l'absurde est la règle qui correspond au raisonnement par l'absurde: pour démontrer ${\displaystyle P}$, on ajoute ${\displaystyle \neg P}$ aux hypothèses et si l'on obtient l'absurde, alors on a ${\displaystyle P}$.

L'une des idées qui ont conduit au calcul des séquents est de n'avoir plus que des règles d'introduction en plus d'une règle que l'on appelle coupure et de règles structurelles. Pour cela, on utilise des formules que l'on appelle des séquents et qui sont de la forme ${\displaystyle \Gamma \vdash \Delta }$ où ${\displaystyle \Gamma }$ et ${\displaystyle \Delta }$ sont des multiensembles de propositions. Le séquent ${\displaystyle P_{1},...,P_{m}\vdash Q_{1},...,Q_{n}}$ s'interprète comme l'assertion de la conjonction des ${\displaystyle P_{i}}$ on déduit la disjonction des ${\displaystyle Q_{j}}$. Les ${\displaystyle P_{i}}$ sont appelés les antécédents et les ${\displaystyle Q_{j}}$ sont appelés les conséquents. Si la liste des antécédents est vide on écrit ${\displaystyle \vdash \Delta }$, si la liste des conséquents est vide on écrit ${\displaystyle \Gamma \vdash }$. Un théorème est encore un séquent sans antécédents et avec un seul conséquent.

• L'axiome est ${\displaystyle A\vdash A}$.
• Introduction de l'implication à droite :

${\displaystyle {\frac {\Gamma ,A\vdash \Delta ,B}{\Gamma \vdash \Delta ,A\to B}}}$

• Introduction de l'implication à gauche :

${\displaystyle {\frac {\Gamma ,A\vdash \Delta \qquad \Gamma '\vdash \Delta ',B}{\Gamma ,\Gamma ',B\to A\vdash \Delta ,\Delta '}}}$

• Introduction de la disjonction à droite :

${\displaystyle {\frac {\Gamma \vdash \Delta ,A,B}{\Gamma \vdash \Delta ,A\vee B}}}$

• Introduction de la disjonction à gauche :

${\displaystyle {\frac {\Gamma ,A\vdash \Delta \qquad \Gamma ',B\vdash \Delta '}{\Gamma ,\Gamma ',A\vee B\vdash \Delta ,\Delta '}}}$

• Introduction du faux à droite :

${\displaystyle {\frac {\Gamma \vdash \Delta }{\Gamma \vdash \Delta ,\perp }}}$

• Introduction du faux à gauche, il a la forme d'un axiome : ${\displaystyle \quad \perp \ \vdash }$
• Coupure :

${\displaystyle {\frac {\Gamma \vdash \Delta ,A\qquad \Gamma ',A\vdash \Delta '}{\Gamma ,\Gamma '\vdash \Delta ,\Delta '}}}$

• Affaiblissements :

${\displaystyle {\frac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\qquad {\frac {\Gamma \vdash \Delta }{\Gamma \vdash \Delta ,A}}}$

• Contractions

${\displaystyle {\frac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\qquad {\frac {\Gamma \vdash \Delta ,A,A}{\Gamma \vdash \Delta ,A}}}$

Une coupure traduit l'attitude du mathématicien qui démontre un lemme (la proposition ${\displaystyle A}$) dont il se sert ailleurs dans la démonstration d'un théorème. Ce lemme peut exprimer quelque chose qui n'a rien à voir avec le théorème principal, d'où le souhait d'éliminer ces lemmes qui sont comme des détours dans la progression vers le résultat principal^[7]. Un affaiblissement correspond à l'ajout d'une proposition superflue soit comme antécédent, soit comme conséquent.

Nous indiquons ci-dessous une liste de théorèmes qu'on peut démontrer à l'aide des règles précédentes, ainsi que le nom usuel qui leur est attribué par la tradition.

${\displaystyle {\big (}A\rightarrow \;A)}$	identité
${\displaystyle A\lor \lnot A}$	tiers exclu
${\displaystyle A\rightarrow \lnot \lnot A}$	double négation
${\displaystyle \lnot \lnot A\rightarrow A}$	double négation classique
${\displaystyle {\big (}{\big (}A\to B{\big )}\to A{\big )}\to A}$	loi de Peirce
${\displaystyle \lnot (A\land \lnot A)}$	non contradiction
${\displaystyle \lnot (A\land B)\leftrightarrow (\lnot A\lor \lnot B)}$	lois de De Morgan
${\displaystyle \lnot (A\lor B)\leftrightarrow (\lnot A\land \lnot B)}$
${\displaystyle (A\to B)\to (\lnot B\to \lnot A)}$	contraposition
${\displaystyle {\big (}(A\to B)\land A)\to B}$	modus ponens (propositionnel)
${\displaystyle ((A\to B)\land \lnot B)\to \lnot A}$	modus tollens (propositionnel)
${\displaystyle {\big (}(A\to B)\land (B\to C))\to (A\to C)}$	modus barbara (propositionnel)
${\displaystyle (A\to B)\to {\big (}(B\to C)\to (A\to C){\big )}}$	modus barbara (implicatif)
${\displaystyle {\big (}A\land (B\lor C))\leftrightarrow ((A\land B)\lor (A\land C))}$	distributivité
${\displaystyle {\big (}A\lor (B\land C))\leftrightarrow ((A\lor B)\land (A\lor C))}$

Les trois systèmes utilisent le même symbole ${\displaystyle \vdash }$, mais cette notation est cohérente. Le format ${\displaystyle \Gamma \vdash P}$ utilisé pour la déduction naturelle est en fait un séquent dans lequel il n'y a qu'une seule conclusion, on parle alors d'un séquent naturel. Le format ${\displaystyle \vdash P}$ utilisé pour les théorèmes dans les systèmes à la Hilbert correspond à un séquent naturel où il n'y a pas d'hypothèse.

On peut montrer que ces trois systèmes sont équivalents dans le sens où ils ont exactement les mêmes théorèmes.

L'aspect « classique » du calcul des propositions est obtenu, dans le système à la Hilbert, par l'axiome de contraposition ${\displaystyle \vdash (\lnot P\to \lnot Q)\to (Q\to P)}$, il apparaît dans la déduction naturelle à travers la réduction à l'absurde. Le calcul des séquents est classique, mais si l'on se restreint aux séquents avec un seul conséquent, il devient intuitionniste.

La sémantique détermine les règles d'interprétations des propositions. Attribuer des valeurs de vérité^[8] à chacune des propositions élémentaires intervenant dans une proposition revient à choisir un modèle de cette proposition.

De façon plus précise, si l'on se place en logique classique^[9], l'interprétation d'une proposition A est le fait d'attribuer une valeur de vérité (0 ou 1) aux variables propositionnelles et à expliquer comment les connecteurs se comportent vis-à-vis des valeurs de vérité. On donne ce comportement par une table de vérité. De cette manière on peut donner une valeur 0 ou 1 à chaque proposition qui dépend des valeurs prises par les tables de vérité. Il existe trois cas d'interprétation:

• Quand la proposition prend toujours la valeur 0 quelles que soient les valeurs des variables propositionnelles, la proposition est dite être une antilogie ou une contradiction. On dit également qu'elle est insatisfaisable.
• Lorsque la proposition A prend toujours la valeur 1, A est une tautologie. On dit aussi que A est valide et on notera cette assertion ${\displaystyle \vDash A}$.
• Si la proposition prend au moins une fois la valeur 1, on dit que l'on peut satisfaire A, ou que A est satisfaisable (ou encore "satisfiable" par mimétisme avec le terme anglais).
• Si la proposition prend au moins une fois la valeur 1 et au moins une fois la valeur 0, c'est une proposition synthétique ou contingente.

Nous explicitons le comportement, puis donnons la table de vérité associée

• ${\displaystyle P\lor Q}$ prendra la valeur 1 si et seulement si au moins l'une des deux propositions P ou Q prend la valeur 1.

P	Q	${\displaystyle P\lor Q}$
0	0	0
0	1	1
1	0	1
1	1	1

• ${\displaystyle P\land Q}$ prendra la valeur 1 si et seulement si les deux propositions P et Q prennent simultanément la valeur 1.

P	Q	${\displaystyle P\land Q}$
0	0	0
0	1	0
1	0	0
1	1	1

• ${\displaystyle P\to Q}$ prendra la valeur 0 si et seulement si P prend la valeur 1 et Q la valeur 0.

P	Q	${\displaystyle P\to Q}$
0	0	1
0	1	1
1	0	0
1	1	1

• ${\displaystyle \lnot P}$ prendra la valeur 1 si et seulement si P prend la valeur 0.

P	${\displaystyle \lnot P}$
0	1
1	0

• ${\displaystyle P\leftrightarrow Q}$ prendra la valeur 1 si et seulement si P et Q ont la même valeur.

P	Q	${\displaystyle P\leftrightarrow Q}$
0	0	1
0	1	0
1	0	0
1	1	1

• ${\displaystyle \perp }$ prend la valeur 0.

Exemple 1 :

(¬A → A) → A est une tautologie.

En effet, si on attribue à A la valeur 0, alors ¬A prend la valeur 1, (¬A → A) prend la valeur 0, et (¬A → A) → A prend la valeur 1. De même, si on attribue à A la valeur 1, alors ¬A prend la valeur 0, (¬A → A) prend la valeur 1, et (¬A → A) → A prend la valeur 1.

Exemple 2 :

A → (A → ¬A) n'est pas une tautologie.

En effet, si on attribue à A la valeur 1, alors ¬A prend la valeur 0, (A → ¬A) prend la valeur 0, et A → (A → ¬A) prend la valeur 0.

Une table de vérité à n entrées définit un connecteur n-aire. Un ensemble de connecteurs propositionnels est dit complet si tout connecteur peut se définir au moyen des connecteurs de l'ensemble. Toute table de vérité se décrit à l'aide de conjonctions de disjonctions et de négation, par exemple on décrit entièrement la table de vérité de l'équivalence ci-dessus par « p ↔ q prend la valeur vrai si et seulement si p et q prennent la valeur faux ou p et q prennent la valeur vraie », c'est-à-dire que p ↔ q ≡ (¬p ∧ ¬q) ∨ (p ∧ q). Cette méthode est générale et permet de montrer que le système {¬, ∧, ∨} est un système complet de connecteurs. On en déduit que {¬, ∧}, {¬, ∨} sont aussi des systèmes complets (à cause des lois de de Morgan, A∨B ≡ ¬ (¬A ∧ ¬B), A ∧ B ≡ ¬ (¬A ∨ ¬B). L'ensemble {¬, →} est également complet : A ∨ B ≡ ¬A → B.

L'ensemble constitué du seul connecteur NON-ET (noté « | » par Henry Sheffer et par conséquent appelée la barre de Sheffer^{[réf. souhaitée]}) est également complet, ¬P étant équivalent à P|P et P∨Q à (P|P) | (Q|Q). Cette particularité est utilisée pour la construction de circuits logiques, une seule porte logique suffit alors pour concevoir tous les circuits existants.

Le calcul propositionnel dispose donc de plusieurs moyens différents pour « valider » les propositions : les systèmes de déduction qui démontrent les théorèmes et les méthodes sémantiques qui définissent les tautologies. La question qui se pose est de savoir si ces méthodes coïncident.

Le fait que toute proposition soit démontrable si elle est une tautologie exprime une propriété du calcul propositionnel que l'on appelle la complétude, cela signifie que la présentation déductive du calcul propositionnel est équivalente à la présentation sémantique. La complétude repose sur les remarques suivantes.

• Toute proposition démontrée résulte d'un axiome ou de l'application d'une règle sur des propositions déjà démontrées. Or il est facile de vérifier que les axiomes fournissent des tautologies et que les règles conservent les tautologies. Toute proposition démontrée est donc une tautologie. Le calcul propositionnel est correct.
• La réciproque repose sur le fait suivant : on peut démontrer que pour toute proposition ${\displaystyle P}$ du calcul propositionnel il existe une proposition ${\displaystyle P'}$ telle que ${\displaystyle P\leftrightarrow P'}$ et telle que ${\displaystyle P'}$ soit sous une forme dite normale ${\displaystyle Q_{1}\land Q_{2}\land \cdots \land Q_{n}}$ où chaque ${\displaystyle Q_{i}}$ est de la forme ${\displaystyle R_{1}\lor R_{2}\lor \cdots \lor R_{k}}$, où chaque ${\displaystyle R_{i}}$ est un littéral (c'est-à-dire une proposition de la forme ${\displaystyle p}$ ou ${\displaystyle \lnot p}$). Si ${\displaystyle P'}$ est une tautologie, alors dans chaque ${\displaystyle Q_{i}}$, apparaissent nécessairement une variable propositionnelle ${\displaystyle p}$ et sa négation ${\displaystyle \lnot p}$. Sinon il existerait ${\displaystyle Q_{i}}$ qui ne vérifierait pas cette condition et il serait possible d'attribuer des valeurs aux ${\displaystyle p_{j}}$ de façon à donner la valeur 0 à ${\displaystyle Q_{i}}$, et donc à ${\displaystyle P'}$ lui-même. Mais on peut montrer que ${\displaystyle p\lor \lnot p}$ est démontrable (${\displaystyle \vdash p\lor \lnot p}$), puis qu'il en est de même de chaque ${\displaystyle Q_{i}}$, puis de ${\displaystyle P'}$ lui-même et enfin de ${\displaystyle P}$. Toute tautologie est alors démontrable. Le calcul propositionnel est complet.

L'article théorème de complétude du calcul des propositions propose une autre démonstration plus détaillée.

Il résulte de la complétude du calcul des propositions que :

• Le calcul des propositions est décidable, dans le sens où il existe un algorithme permettant de décider si une proposition est un théorème ou non. Il suffit de dresser sa table de vérité et de voir s'il s'agit d'une tautologie.
• Le calcul des propositions est cohérent (consistant), c'est-à-dire non contradictoire. Il n'existe aucune proposition ${\displaystyle P}$ telle qu'on puisse avoir en même temps ${\displaystyle \vdash P}$ et ${\displaystyle \vdash \lnot P}$ car ces deux propositions seraient des tautologies et on aurait 1 = 0.
• Le calcul des propositions est fortement complet (maximalement cohérent), dans le sens où tout ajout d'un nouveau schéma d'axiome, non démontrable dans le système initial, rend ce système incohérent.

Supposons donné un nombre infini de propositions. Peut-on satisfaire simultanément ces propositions ? Autrement dit, existe-il des valeurs de vérité pour leurs variables propositionnelles qui donnent 1 comme valeur de vérité à toutes les propositions? Si la réponse est positive pour tout sous-ensemble fini de ces propositions, alors elle l'est pour toutes les propositions. Cette propriété, qui assure que l'on peut passer de tous les sous-ensembles finis à l'ensemble infini tout entier, est appelée la compacité.

Nous avons vu que, pour décider si une proposition est démontrable classiquement, il suffit de vérifier si c'est une tautologie, c'est-à-dire de vérifier si elle prend la valeur de vérité 1 quelles que soient les valeurs de vérité de ses variables propositionnelles.

Cette approche brutale se heurte cependant au temps de calcul qu'elle requiert. En effet, si la proposition possède n variables propositionnelles, il faut calculer 2ⁿ combinaisons de valeurs possibles pour les variables propositionnelles, ce qui devient rapidement infaisable pour n grand. Ainsi, si n = 30, il faudra énumérer plus d'un milliard de combinaisons de valeurs.

Il existe certes des améliorations possibles. Par exemple, si on attribue la valeur de vérité 0 à une variable propositionnelle p, on peut attribuer directement la valeur 0 à ${\displaystyle p\land q}$ indépendamment de la valeur ultérieure attribuée à q, ce qui diminue le nombre de calculs à effectuer.

On peut également chercher à voir s'il est possible d'invalider les implications. Considérons par exemple la proposition :

${\displaystyle ((p\to (q\land r\land s))\land \lnot s)\to \lnot p}$

Étant constituée d'une implication, pour la rendre invalide, il suffit que la conclusion ${\displaystyle \lnot p}$ puisse prendre la valeur 0 (et donc ${\displaystyle p}$ la valeur 1) et que l'hypothèse ${\displaystyle ((p\to (q\land r\land s))\land \lnot s)}$ puisse prendre la valeur 1 (et donc ${\displaystyle \lnot s}$ et ${\displaystyle p\to (q\land r\land s)}$ la valeur 1). Mais alors ${\displaystyle s}$ prend la valeur 0 et ${\displaystyle (p\to (q\land r\land s)}$ ne peut plus prendre que la valeur 0. Il est donc impossible d'invalider l'implication et celle-ci est une tautologie.

Mais les améliorations précédentes ne changent pas fondamentalement la difficulté du problème. On est donc devant la situation suivante. Étant donné une proposition f, on se demande si f est une tautologie ou non et pour cela, on se demande s'il existe des valeurs de vérité attribuables aux variables propositionnelles de f qui rendraient f invalide.

• Une recherche exhaustive demande 2ⁿ vérifications si f possède n variables propositionnelles. Cette démarche est dite déterministe, mais son temps de calcul est exponentiel.
• Par contre, si f n'est pas une tautologie, il suffit d'une vérification à faire, à savoir tester précisément la configuration qui invalide f. Cette vérification demande un simple calcul booléen, qui se fait en temps polynomial (essentiellement linéaire en fait). Le temps de calcul cesse donc d'être exponentiel, à condition de savoir quelle configuration tester. Celle-ci pourrait par exemple être donnée par un être omniscient auquel on ne ferait pas totalement confiance. Une telle démarche est dite non déterministe.

La question de l'invalidité de f, ainsi que tous les problèmes qui se résolvent suivant la méthode que nous venons d'esquisser, sont dits NP (pour polynomial non déterministe). Tester l'invalidité de f équivaut par des calculs très simples (en temps polynomial) à tester la satisfaisabilité de sa négation. Le problème de la satisfaisabilité d'une proposition, à savoir trouver une configuration qui donne 1 comme valeur de vérité de la proposition est appelé problème SAT (de l'anglais boolean SATisfiability problem). Il joue un rôle fondamental en théorie de la complexité, puisqu'on peut montrer que la découverte d'un algorithme déterministe en temps polynomial pour ce problème permettrait d'en déduire des algorithmes déterministes en temps polynomial pour tous les problèmes de type NP (théorème de Cook). On dit que SAT (et donc également le problème de la non-démontrabilité d'une proposition) est un problème NP-complet. Le problème de la démontrabilité d'une proposition est dit co-NP (pour complémentaire de NP).

Le problème SAT désigne en fait le plus souvent celui de la satisfaisabilité d'une conjonction de clauses (un cas particulier parmi les propositions), mais on ramène le problème de la satisfaisabilité d'une proposition à celui-ci par une réduction polynomiale (une mise sous forme clausale par équisatisfaisabilité, celles par équivalence logique ne fonctionnent pas).

Soit E l'ensemble des propositions sur un ensemble de variables propositionnelles. La relation binaire définie sur E par l'équivalence (classique) entre deux propositions est notée ≡. C'est une relation d'équivalence sur E, compatible avec la conjonction (qui donne la borne inférieure de deux éléments), la disjonction (qui donne la borne supérieure de deux éléments), et la négation (qui donne le complément). L'ensemble quotient E/_≡ du calcul propositionnel.^[pas clair]

Dès que l'ensemble des variables propositionnelles est infini, l'algèbre de Lindenbaum des formules propositionnelles ne possède aucun atome, c'est-à-dire aucun élément non nul minimal (pour toute formule qui n'est pas une antilogie, on obtient un élément strictement inférieur par conjonction avec une variable propositionnelle non présente dans la formule). Ceci la distingue de l'algèbre de Boole de toutes les parties d'un ensemble, qui a pour atomes les singletons de celui-ci.

Les algèbres de Heyting ont été définies par Arend Heyting pour interpréter la logique intuitionniste.

Une disjonction est une proposition de la forme ${\displaystyle p\lor q}$ et une conjonction est une proposition de la forme ${\displaystyle p\land q}$. Une proposition est en forme normale conjonctive (FNC) si elle est composée de conjonctions de disjonctions. Une proposition est en forme normale disjonctive (FND) si elle est composée de disjonctions de conjonctions.

Exemples :

• ${\displaystyle p,\lnot p,}$ ${\displaystyle p\lor q}$ et ${\displaystyle p\land q}$ sont à la fois des FNC et des FND.
• ${\displaystyle (p\lor q)\land (\lnot p\lor r)\land s}$ est en forme normale conjonctive.
• ${\displaystyle (p\land q\land r)\lor (\lnot p\land \lnot s)\lor \lnot q}$ est en forme normale disjonctive.

Lorsque chaque bloc disjonctif d'une FND comporte une et une seule occurrence des mêmes variables propositionnelles, on parle alors de FND distinguée.

Lorsque chaque bloc conjonctif d'une FNC comporte une et une seule occurrence des mêmes variables propositionnelles, on parle alors de FNC distinguée.

Exemples :

• ${\displaystyle (p\lor q\lor r)\land (\lnot p\lor \lnot q\lor r)\land (\lnot p\lor \lnot q\lor \lnot r)}$ est en forme normale conjonctive distinguée.
• ${\displaystyle (p\land q\land r)\lor (\lnot p\land q\land \lnot r)\lor (\lnot p\land \lnot q\land r)}$ est en forme normale disjonctive distinguée.

On peut montrer que toute proposition est équivalente à une FND (en admettant que ${\displaystyle \perp }$ est la disjonction d'un ensemble vide de propositions) et est équivalente à une FNC (en admettant que T est la conjonction d'un ensemble vide de propositions). Autrement dit, pour toute proposition ${\displaystyle p}$ il existe une proposition ${\displaystyle q}$ en forme normale disjonctive telle que ${\displaystyle p}$${\displaystyle \leftrightarrow }$${\displaystyle q}$ et une proposition ${\displaystyle r}$ en forme normale conjonctive telle que ${\displaystyle p}$${\displaystyle \leftrightarrow }$${\displaystyle r}$.

Les axiomes et règles du calcul propositionnel que nous avons présentés sont ceux de la logique classique. Ils induisent la proposition p ∨ ¬p, appelée principe du tiers exclu, la proposition ¬¬ p → p, appelée élimination de la double négation et la proposition ((p → q) → p) → p appelée loi de Peirce. Cette logique repose sur le principe qu'une propriété P est nécessairement vraie ou fausse. Il est l'un des piliers de la position qualifiée de formaliste, adoptée par Hilbert et d'autres. Or cette position qui implique qu'il y a des démonstrations qui ne construisent pas l'objet satisfaisant la proposition prouvée a été remise en cause par plusieurs mathématiciens, dont le plus connu est Brouwer conduisant à créer par la suite la logique intuitionniste.

Il existe des variantes de logique non classique, notamment la logique minimale de Ingebrigt Johansson^[10] (1936) et la logique intuitionniste de Heyting (1930). Les connecteurs primitifs sont →, ∧, ∨ et ¬. Ces variantes diffèrent l'une de l'autre par le choix des axiomes qu'elles utilisent^[11].

La logique absolue utilise les axiomes suivants relatifs à l'implication, la conjonction et la disjonction. Elle ne traite pas de la négation.

Axiomes de l'implication (ce sont les deux premiers axiomes de la logique classique) :

ax.1 : ${\displaystyle p\rightarrow \;(q\rightarrow \;p)}$

ax.2 : ${\displaystyle (p\rightarrow \;(q\rightarrow \;r))\rightarrow \;((p\rightarrow \;q)\rightarrow \;(p\rightarrow \;r))}$

Axiomes de la conjonction ${\displaystyle \land }$ :

ax.3 : ${\displaystyle (p\land q)\to p}$

ax.4 : ${\displaystyle (p\land q)\to q}$

ax.5 : ${\displaystyle (p\to q)\to ((p\to r)\to (p\to (q\land r)))}$

Axiomes de la disjonction ${\displaystyle \lor }$, (duaux des précédents) :

ax.8 : ${\displaystyle p\to (p\lor q)}$

ax.9 : ${\displaystyle q\to (p\lor q)}$

ax.10: ${\displaystyle (p\to r)\to ((q\to r)\to ((p\lor q)\to r))}$

L'ensemble des théorèmes de cette logique est inclus strictement dans l'ensemble des théorèmes de la logique classique qui n'utilisent pas la négation. Il est impossible par exemple d'y prouver la formule ${\displaystyle p\lor (p\to q)}$ ou la loi de Peirce ${\displaystyle ((p\to q)\to p)\to p}$.

Si on adjoint aux axiomes ax.1 à ax.8 l'axiome suivant :

ax.9 : ${\displaystyle p\lor (p\to q)}$

on obtient la logique positive. L'ensemble des théorèmes de cette logique est identique à l'ensemble des théorèmes de la logique classique qui n'utilisent pas la négation.

Si on adjoint aux axiomes ax.1 à ax.8 les deux axiomes suivants, relatifs à la négation :

ax.10 : ¬p → (p → ¬q)

ax.11 : (p → ¬p) → ¬p

on obtient la logique minimale. Le premier axiome définit le comportement de la logique vis-à-vis d'une contradiction. Le second axiome exprime que, si p implique sa propre négation, alors p est invalide.

La seule différence entre la logique intuitionniste et la logique minimale porte sur l'axiome ax.10 qu'on remplace par :

ax.12 : ¬p → (p → q)

En présence d'une proposition et de sa négation, les trois logiques, classique, intuitionniste et minimale, concluent toutes trois à une contradiction ⊥. Mais la différence porte sur l'utilisation que l'on fait de cette contradiction :

• La logique classique déduit de ¬P → ⊥ le fait que P est vrai (raisonnement par l'absurde).
• La logique intuitionniste déduit d'une contradiction que toute proposition est démontrable. De ¬P → ⊥, elle déduit la validité de ¬¬P, propriété plus faible que P.
• La logique minimale déduit d'une contradiction que toute négation de proposition est démontrable, ce qui est plus faible que ce que propose la logique intuitionniste.

Logique minimale et logique intuitionniste ont toutes deux la proposition ¬(p ∧ ¬p) comme théorème. En revanche, p ∨ ¬p n'est pas un théorème de ces logiques.

De même, elles permettent de démontrer p → ¬¬p mais pas la réciproque. Par contre, elles permettent de démontrer l'équivalence entre ¬p et ¬¬¬p. Enfin, la proposition (¬p ∨ q) → (p →q) est un théorème de la logique intuitionniste, mais pas un théorème de la logique minimale.

Glivenko (en) a démontré en 1929 que p est un théorème du calcul propositionnel classique si et seulement si ¬¬p est un théorème du calcul propositionnel intuitionniste. Ce résultat ne s'étend pas si l'on remplace « intuitionniste » par « minimal ». Il ne s'applique pas non plus au calcul des prédicats ; une traduction est toutefois possible^[12], mais dépend de la structure des formules.

Enfin, pour avoir une démonstration de p ∨ q en logique intuitionniste, il faut soit une démonstration de p soit une démonstration de q, alors qu'en logique classique, une démonstration de ¬(¬p ∧ ¬q) suffit.

On peut introduire les quantificateurs ∃ (il existe) et ∀ (quel que soit) pour quantifier les propositions (ce qui est à distinguer de la quantification du calcul des prédicats). Ainsi, pour exemples, on aura comme formules valides du calcul propositionnel quantifié, appelé aussi calcul propositionnel du second ordre :

• ∀p (⊥ → p) : Pour toute proposition, le faux l'implique ;
• ∀p (p → T) : Le vrai est impliqué par toute proposition ;
• ∃p (p ∨ q) : Prendre p ↔ ¬q (en logique classique) ou p ↔ T (plus généralement), pour exemples.

• Robert Blanché, Introduction à la logique contemporaine, Armand Colin - 1951
• (de) Józef Maria Bocheński et Albert Menne, Grundriß des Logistik, UTB, Stuttgart, 1973 (ISBN 3-506-99153-1)
• René Cori et Daniel Lascar, Logique mathématique I. Calcul propositionnel, algèbres de Boole, calcul des prédicats [détail des éditions], ch I et II
• R. David, K. Nour et C. Raffalli, Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés, Dunod, 2001 (ISBN 2-10006-796-6)
• Yannis Delmas-Rigoutsos et René Lalement, La Logique ou l'art de raisonner, 2000 [détail de l’édition]
• G. Dowek, La Logique, Coll. Dominos, Flammarion (1995).
• A. Heyting, Les Fondements des mathématiques. Intuitionnisme. Théorie de la connaissance, Paris, Gauthiers-Villars, 1955.
• Logique et Connaissance scientifique, Collection de la Pléiade, Gallimard, 1967
• Stephen Kleene, Logique mathématique, Armand Colin, 1971 ou Gabay 1987 (ISBN 2-87647-005-5)
• (en) Quine, Elementary Logic, Harvard University Press - 1980 (1941).

• Gottfried Wilhelm Leibniz, George Boole, Auguste De Morgan, Gottlob Frege, Charles Sanders Peirce, Bertrand Russell, Ludwig Wittgenstein
• Logique polyvalente
• Fonction logique
• Idéographie
• Porte logique
• Formule propositionnelle

• Portail des mathématiques
• Portail de la logique
• Portail de l'informatique théorique