Calcul des propositions

Un article de Wikipédia, l'encyclopédie libre.

Pour les articles homonymes, voir Déduction.

Le calcul des propositions ou calcul propositionnel est une théorie logique qui définit les lois formelles du raisonnement. C'est la version moderne de la logique stoïcienne. C'est aussi la première étape dans la construction des outils de la logique mathématique.

[modifier] Introduction générale

Assez complexe à définir en général, 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 pour laquelle il fait sens de 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.

Si l'on se place dans la logique classique, le calcul de propositions est une structure algébrique que l'on appelle algèbre de Boole.

[modifier] Définition d'une proposition

Quoique le calcul des propositions ne s'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 » pour prendre deux exemples très simples sont deux propositions en ce sens. De façon générale un état de chose peut être une vérité scientifique, un fait empiriquement observable, une formule mathématique. D'autre part, une proposition peut être vraie ou fausse (ou bien de statut indéterminé si l'on accepte de quitter la logique classique). C'est pourquoi une phrase optative (qui exprime un souhait comme par exemple « Que Dieu nous protège !») ou une phrase impérative (« viens !», « tais-toi !») ou une interrogation ne sont pas des propositions. « Que Dieu nous protège !» par exemple ne peut être ni vraie ni fausse: elle ne fait qu'exprimer un souhait du locuteur. En revanche, une phrase comme « toujours dans ce calcul, toutes les variables informatiques sont strictement positives » est une proposition dont le contenu a été modifié par la « modalité » toujours, ce type de proposition est étudié dans la logique modale, plus précisément la logique temporelle dans ce cas.

Tous les énoncés mathématiques n'ont pas vocation à être des propositions, ainsi l'énoncé « x > 0 » n'a pas cette vocation, car il dépend de la variable x, en revanche un énoncé comme $(\forall x:\mathbb{N}) x=0$ ne dépend plus de $x$ , car $x$ y est d'une certaine façon caché, on aurait pu écrire tout aussi bien $(\forall y:\mathbb{N}) y=0$ et, comme pour les propositions, on peut se poser la question de savoir s'il est vrai ou s'il est faux^[1]. Au lieu de l'appeler une proposition, le calcul des prédicats appelle un tel énoncé une formule close.

[modifier] Définition d'un système déductif

Un calcul ou un système déductif est, en logique, un ensemble de règles permettant en un nombre fini d'étapes, selon des règles explicites et selon des procédés mécanisables de déterminer 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 est constituée des deux éléments vrai et faux (souvent notés 1 et 0), quand on donne du sens à une proposition on lui donne soit la valeur vrai on dit alors qu'il s'agit d'une tautologie, soit la valeur faux, on dit alors qu'il s'agit d'une antilogie.

[modifier] Structure

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.

Aspect syntaxique : il s'agit d'abord de définir le langage du calcul des propositions par les règles de formation des propositions, puis de décrire les règles d'inférence permettant la déduction de propositions à partir d'autres. Ces règles de déduction permettent d'engendrer des propositions spécifiques que l'on appelle des théorèmes.
Aspect sémantique : on donne un sens aux symboles représentant les connecteurs logiques en fonction de la valeur de vérité des propositions de base (ainsi $\lnot$ signifie non). Ce sens est donné, par exemple, par des tables de vérité ou par des modèles de Kripke.

Le fait que la déduction corresponde parfaitement à la sémantique s'appelle la complétude.

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 ».

[modifier] Présentation

[modifier] Syntaxe

[modifier] Les constituants du langage

A la base de la syntaxe du calcul des propositions il y a les variables propositionnelles ou propositions atomiques, notées p, q, etc., formant 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 $\land$ , ou $\lor$ , non $\lnot$ , implique $\to$ , équivaut $\leftrightarrow$ . On considère souvent aussi la constante $\perp$ qui vise à représenter le faux. À côté de ces symboles on utilise des parenthèses pour lever les ambigüités dans les formules quoiqu'on puisse s'en passer, comme dans la notation polonaise, inventée par le logicien polonais Jan Łukasiewicz. Cependant à la suite, par exemple, de Christopher Strachey, les logiciens accordent de moins en moins d'attention à la syntaxe concrète choisie pour se consacrer au fond des choses^[2]: la déduction et la sémantique. Ils utilisent ainsi des conventions comme l'associativité pour lever des ambiguïtés et économiser des parenthèses.

Un ensemble de connecteurs propositionnels est complet ^[3]si tout connecteur peut se définir au moyen des connecteurs de l'ensemble. Par exemple, en logique classique, l'ensemble $\{\neg, \to\}$ est complet. Ainsi par exemple la disjonction se définit par : $A\lor B = \neg A\to B$ . L'ensemble constitué du seul connecteur d'incompatibilité de Sheffer, noté par une barre | est aussi complet, car les connecteurs peuvent être définis comme suit :

$\lnot P$ est équivalent à $P \big| P$
$P \lor Q$ est équivalent à $(P \big| P) | (Q \big| Q)$ .

[modifier] Les formules bien formées ou propositions

Le calcul des propositions repose de plus sur des règles de formation indiquant comment construire des propositions complexes syntaxiques bien construites ou « bien formées ».

Une proposition ou formule bien formée (notée par la suite $A$ , $B$ , $C$ ou $P$ , $Q$ , $R$ ) est définie par induction sur la structure des expressions^[4] comme suit :

une variable propositionnelle $p$ est une proposition^[5],
$\perp$ est une proposition.
si $\quad P$ et $\quad Q$ sont des propositions, alors $(P \land Q)$ , $(P \lor Q)$ , $\big(P \rightarrow Q\big)$ , $(P \leftrightarrow Q)$ et $\lnot P$ sont des propositions.

Exemples : Si $\quad P$ , $\quad Q$ et $\quad R$ sont des propositions,

$(P \to Q) \to (\lnot Q \to \lnot P)$ est une proposition.

$(P \to \perp) \to \perp$ est une proposition.

$P \land \lnot P$ est une proposition.

$(P \land Q) \lor R$ est une proposition.

$P \land Q \lor$ n'est pas une proposition.

[modifier] Quelques conventions syntaxiques

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. Ainsi, on omet généralement les parenthèses extrêmes des formules. On supprime les parenthèses en associant les expressions de droite à gauche quand il s'agit du même connecteur. D'autre part, on donne un priorité au connecteurs $\lor$ et $\land$ sur les connecteurs $\to$ et $\leftrightarrow$ .

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

[modifier] Les systèmes déductifs

Article détaillé : Théorie de la démonstration.

Le calcul des proposition va nous permettre de présenter les trois systèmes déductifs les plus connus. Pour cela, nous nous limiterons aux propositions contenant, outre les variables propositionnelles, seulement des implications, des disjonctions et des occurrence de faux autrement dit de $\perp$ . On admet que $\lnot P$ est un abréviation de $P \to \perp$ . Si $\quad P$ est un théorème, autrement dit une proposition qui a une démonstration, on note cela par $\vdash P$ .

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

$\frac{\varphi_1 \quad ... \quad \varphi_n}{\psi}.$

Les $\varphi_i$ sont appelées les prémisses et $ψ$ est appelée la conclusion.

[modifier] La déduction à la Hilbert

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

$\frac{\vdash P \to Q \quad \vdash P}{\vdash Q}.$

Elle peut se comprendre ainsi si $P \to Q$ est un théorème et $P$ est un théorème alors $Q$ est un théorème. À cela, on peut ajouter trois axiomes pour l'implication et le faux et trois axiomes pour la disjonction:

$\vdash P \to (Q \to P)$ ,
$\vdash (P \to (Q \to R)) \to ((P \to Q) \to (P \to R))$ ,
$\vdash (\lnot P \to \lnot Q) \to (Q \to P)$ ,
$(P\to R) \to ((Q\to R) \to ((P\vee Q) \to R))$ ,
$P\to (P \vee Q)$ ,
$Q\to (P \vee Q)$ .

[modifier] La déduction naturelle

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 $P$ est conséquence d'un ensemble $Γ$ d'hypothèses, on écrit $\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 $\Gamma, P \vdash P$ .
La règle d'introduction de l'implication:

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

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

$\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:

$\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:

$\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:

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

En outre, il faut une règle qui est la réduction à l'absurde, nécessaire en logique classique:

$\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 $P$ , on ajoute $\neg P$ aux hypothèses et si l'on obtient l'absurde, alors on a $P$ .

[modifier] Le calcul des séquents

L'une des idées qui à 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 $\Gamma\vdash\Delta$ où $Γ$ et $Δ$ sont des multiensembles de propositions. Le séquent $P_1,...,P_m\vdash Q_1,...,Q_n$ s'interprète comme l'assertion de la conjonction des $P i$ on déduit la disjonction des $Q j$ . Les $P i$ sont appelés les antécédents et les $Q j$ sont appelés les conséquents. Si la liste des antécédents est vide on écrit $\vdash \Delta$ , si la liste des conséquent est vide on écrit $\Gamma \vdash$ . Un théorème est encore un séquent sans antécédents et avec un seul conséquent.

L'axiome est $A \vdash A$ .

Introduction de l'implication à droite :

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

Introduction de l'implication à gauche :

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

Introduction de la disjonction à droite :

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

Introduction de la disjonction à gauche :

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

Introduction du faux à droite :

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

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

Coupure :

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

Affaiblissements :

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

Contractions

$\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 $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^[6]. Un affaiblissement correspond à l'ajout d'une proposition superflue soit comme antécédent, soit comme conséquent.

[modifier] Exemples de théorèmes

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.

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

[modifier] Commentaires

On aura remarqué que les trois systèmes utilisent le même symbole $\vdash$ , mais en fait cette notation est cohérente. Le format $\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 $\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 $\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.

[modifier] Sémantique

Ce que j'ai appris de la logique, c'est cette dissociation entre vérité et prouvabilité. Alain Connes, in Triangle de pensées Ed. Odile Jacob, (2000).

Article détaillé : théorie des modèles.

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

De façon plus précise, 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 un valeur 0 ou 1 à chaque propositions 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 valur 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 insatisfiable.
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 $\vDash A$ .
Si la proposition prend au moins une fois la valeur 1, on dit que A est satisfiable.
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.

[modifier] Interprétation des connecteurs

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

$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.

$\vee$	0	1
0	0	1
1	1	1

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

$\land$	0	1
0	0	0
1	0	1

$P \to Q$ prendra la valeur 0 si et seulement si P prend la valeur 1 et Q la valeur 0.

$\to$	0	1
0	1	1
1	0	1

$\lnot P$ prendra la valeur 1 si et seulement si P prend la valeur 0.

$\lnot$
0	1
1	0

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

$\leftrightarrow$	0	1
0	1	0
1	0	1

$\perp$ prend la valeur 0.

Exemple 1 :

$(\lnot A \to A) \to A$ est une tautologie.

En effet, si on attribue à A la valeur 0, alors $\lnot A$ prend la valeur 1, $(\lnot A \to A)$ prend la valeur 0, et $(\lnot A \to A) \to A$ prend la valeur 1. De même, si on attribue à $A$ la valeur 1, alors $\lnot A$ prend la valeur 0, $(\lnot A \to A)$ prend la valeur 1, et $(\lnot A \to A) \to A$ prend la valeur 1.

Exemple 2 :

$A \to (A \to \lnot A)$ n'est pas une tautologie.

En effet, si on attribue à A la valeur 1, alors $\lnot A$ prend la valeur 0, $A \to \lnot A$ prend la valeur 0, et $A \to (A \to \lnot A)$ prend la valeur 0.

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

[modifier] Principales propriétés

[modifier] Décidabilité, cohérence, complétude, compacité

Le fait que toute proposition soit démontrable si et seulement 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 $P$ du calcul propositionnel il existe une proposition $P'$ telle que $P \leftrightarrow P'$ et telle que $P'$ soit sous une forme dite normale $Q_1 \land Q_2 \land \cdots \land Q_n$ où chaque $Q i$ est de la forme $R_1 \lor R_2 \lor \cdots \lor R_k$ , où chaque $R i$ est un littéral (c'est-à-dire une proposition de la forme $p$ ou $\lnot p$ ). Si $P'$ est une tautologie, alors dans chaque $Q i$ , apparaissent nécessairement une variable propositionnelle $p$ et sa négation $\lnot p$ . Sinon il existerait $Q i$ qui ne vérifierait pas cette condition et il serait possible d'attribuer des valeurs aux $p j$ de façon à donner la valeur 0 à $Q i$ , et donc à $P'$ lui-même. Mais on peut montrer que $p \lor \lnot p$ est démontrable ( $\vdash p \lor \lnot p$ ), puis qu'il en est de même de chaque $Q i$ , puis de $P'$ lui-même et enfin de $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 $P$ telle qu'on puisse avoir en même temps $\vdash P$ et $\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. Est-ce que ces propositions sont simultanément satisfiables? 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é.

[modifier] Méthodes de calcul, NP-complétude

Nous avons vu que, pour décider si une proposition est démontrable, 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. Si n = 100, le temps de calcul nécessaire pour énumérer toutes ces combinaisons de valeurs dépasse de loin l'âge de l'Univers.

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 à $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 :

$((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 $\lnot p$ puisse prendre la valeur 0 (et donc $p$ la valeur 1) et que l'hypothèse $((p \to (q \land r \land s))\land \lnot s)$ puisse prendre la valeur 1 (et donc $\lnot s$ et $p \to (q \land r \land s)$ la valeur 1). Mais alors $s$ prend la valeur 0 et $(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ée 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. Le temps de calcul cesse d'être exponentiel, à condition de savoir quelle configuration tester. Celle-ci pourrait par exemple être donnée par un oracle ou un être omniscient. Une telle démarche est dite non déterministe.

La question de l'insatisfiabilité 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). Le problème dual est celui de la satisfiabilité d'une proposition, à savoir trouver une configuration qui donne 1 comme valeur de vérité de la proposition. Cette question, appelée problème SAT 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. On dit que SAT (et donc également le problème de la démontrabilité d'une proposition) est un problème NP-complet.

[modifier] Algèbre de Boole

Soit E l'ensemble des propositions sur un ensemble de variables propositionnelles. Soit $\mathfrak R$ la relation binaire définie sur E par l'équivalence ( $\leftrightarrow$ ) entre deux propositions. $\mathfrak R$ est une relation d'équivalence sur E, compatible avec $\lor$ et $\land$ qui donne à l'ensemble quotient E/ $\mathfrak R$ une structure d'algèbre de Boole.

Les algèbres de Boole peuvent être formalisées avec un seul axiome :

(P | (Q | R)) | ((T | (T | T)) | ((S | Q) | ((P | S) | (P | S))))

autrement dit, il suffit de dire que cette proposition vaut 1 pour que toutes les autres identités des algèbres de Boole en découlent.

Veroff et McCune ont démontré en 2000 en utilisant leur système de démonstration automatique de théorèmes Otter que l'on peut formaliser les algèbres de Boole par la seule équation

((P | R) | Q) | ((P | (P | Q)) | P) = Q.

[modifier] Formes normales conjonctives, formes normales disjonctives

Une disjonction est une proposition de la forme $P\lor Q$ et une conjonction est une proposition de la forme $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 :

$p, \lnot p,$ $p \lor q$ et $p \land q$ sont à la fois des FNC et des FND.
$(p \lor q) \land (\lnot p \lor r) \land s$ est en forme normale conjonctive.
$(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 :

$(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.
$(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 $\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 $P$ il existe une proposition $Q$ en forme normale disjonctive telle que $P$ $\leftrightarrow$ $Q$ et une proposition $R$ en forme normale conjonctive telle que $P$ $\leftrightarrow$ $R$ .

[modifier] Logique classique, minimale, intuitionniste

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 \lor \lnot p$ , appelée principe du tiers exclu, la proposition $\lnot\lnot p \to p$ , appelée élimination de la double négation et la proposition $((p \rightarrow\; q) \rightarrow\; p) \rightarrow\; 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.

Nous présentons maintenant deux variantes très proches de logique non classique, la logique minimale de I. Johansson^[9] (1936) et la logique intuitionniste de Heyting (1930). Les connecteurs primitifs sont $\to$ , $\land$ , $\lor$ et $\lnot$ . On garde les deux premiers axiomes de la logique classique :

$p \rightarrow\; (q \rightarrow\; p)$

$(p \rightarrow\; (q \rightarrow\; r)) \rightarrow\; ((p \rightarrow\; q) \rightarrow\; (p \rightarrow\; r))$

Avant d'introduire la négation, on énonce les axiomes relatifs à $\land$ :

$(p \land q) \to p$

$(p \land q) \to q$

$(p \to q) \to ((p \to r) \to (p \to (q \land r)))$

et ceux relatifs à $\lor$ , (duaux des précédents) :

$p \to (p \lor q)$

$q \to (p \lor q)$

$(p \to r) \to ((q \to r) \to ((p \lor q) \to r))$

On introduit enfin deux axiomes relatifs à la négation. Le premier exprime que, si f implique sa propre négation, alors f est invalide.

$(p \to \lnot p) \to \lnot p$ .

Le second définit le comportement de chaque logique vis-à-vis d'une contradiction et la seule différence entre la logique minimale et la logique intuitionniste porte sur cet axiome.

$\lnot p \to (p \to \lnot q)$ pour la logique minimale et $\lnot p \to (p \to q)$ pour la logique intuitionniste.

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

La logique classique déduit de $\lnot P \to \bot$ 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 $\lnot P \to \bot$ , elle déduit la validité de $\lnot\lnot 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 $\lnot (p \land \lnot p)$ comme théorème. En revanche, $p \lor \lnot p$ n'est pas un théorème de ces logiques.

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

Glivenko a démontré^[10] en 1929 que $\quad p$ est un théorème du calcul propositionnel classique si et seulement si $\lnot \lnot 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 directement au calcul des prédicats non plus; un codage est toutefois possible, mais c'est plus compliqué.

↑ Sans avoir fait beaucoup de mathématiques, on sait qu'il est faux!
↑ Dans les outils logiciels qui mécanisent la logique sur ordinateur, des outils très développés permettent des syntaxes souples et non ambigües, associés à d'autres outils qui permettent de modifier la syntaxe pour l'adapter aux gouts de l'utilisateur.
↑ Cela ne doit pas être confondu avec la complétude du système déductif par rapport à une sémantique.
↑ On parle parfois de clause de clôture qui signifie que l'ensemble des propositions est le plus petit ensemble satisfaisant les trois règles ci-dessus.
↑ Par la suite, les variables propositionnelles seront notées $p$ , $q$ , $r$ , $s$ .
↑ mais qui peuvent néanmoins la racourcir considérablement !
↑ Les tables de vérités ont été développées originellement par Wittgenstein.
↑ Outre la méthode des tables de vérités, il existe une approche sémantique fondée sur les modèles de Kripke.
↑ I Johansson, Ingebrigt Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compositio Mathematica, 4 (1937), p. 119-136.
↑ Gödel a aussi proposé un codage de la logique classique dans la logique intuitionniste.

[modifier] Voir aussi

Gottfried Leibniz - George Boole - Auguste De Morgan - Gottlob Frege - Bertrand Russell - Ludwig Wittgenstein
Calcul des prédicats
Déduction naturelle
Logique mathématique
Logique intuitionniste
Sémantique de Kripke, qui est une présentation des modèles de Kripke
Logique modale
Logique polyvalente
Fonction logique
Porte logique

[modifier] Bibliographie

Quine, Elementary Logic, Harvard University Press - 1980 (1941).
Robert Blanché, Introduction à la logique contemporaine, Armand Colin - 1951
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 2876470055
Yannis Delmas-Rigoutsos et René Lalement, La Logique ou l'art de raisonner, 2000 [détail des éditions]
R. David, K. Nour et C. Raffalli, Introduction à la logique. Théorie de la démonstration. Cours et exercices corrigés, Dunod, 2001, ISBN 2100067966
G. Dowek, La logique, Coll. Dominos, Flammarion (1995).