Calcul des propositions

Pour les articles homonymes, voir Déduction.

Le calcul des propositions ou calcul propositionnel est une théorie logique ayant pour objet l'étude des relations logiques entre « propositions »^[1] et définissant les lois formelles selon lesquelles, au moyen de connecteurs logiques, les propositions se coordonnent et s'enchaînent pour produire des raisonnements valides.

Avec la logique du premier ordre, elle est un des langages formels privilégiés de la logique mathématique pour la formulation de ses concepts en systèmes formels, en raison de son applicabilité aux fondements des mathématiques et de la richesse de ses propriétés relevant de la théorie de la démonstration^[2]. Elle peut être considérée comme la forme moderne de la logique stoïcienne^[3].

Introduction générale

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. La calcul des propositions est parfois appelé logique des propositions, logique propositionnelle ou calcul des énoncés, et parfois théorie des fonctions de vérité^{[réf. nécessaire]}.

Définition d'une proposition

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. En revanche, une phrase comme « Dans ce calcul, toutes les variables informatiques sont strictement positives » est une proposition dont le contenu a été modifié par le quantificateur toutes et qui est supposée s'avérer dans la durée. Ce type de proposition est étudié dans la logique modale, plus précisément dans la logique temporelle dans ce cas, à cause de l'affirmation de sa pérennité^[4].

Proposition et prédicat

Si une proposition est une assertion ayant une valeur de vérité, un prédicat est lui une proposition dont la valeur de vérité dépend de variables qu'elle renferme. Le prédicat « Mon pays se situe en Europe » sera vrai ou faux en fonction de la valeur de la variable « Mon pays ». Si le lecteur est français, on obtiendra la proposition « La France 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^[5].

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 et selon des règles explicites 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 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.

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 de définir le langage du calcul des propositions par les règles d’écriture des propositions.

Aspect sémantique : il s’agit ici de donner 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. 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.

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

Présentation

Syntaxe

Les constituants du langage

À 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	∧
ou	∨
non	¬
implique	→ ou ⇒
équivaut	↔ ou ⇔

On considère souvent aussi la constante noté ⊥, 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.

Les formules propositionnelles

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 ${}^\mathcal P$ de variables propositionnelles. L'ensemble des formules du calcul des propositions (sur ${}^\mathcal P$ ), ou simplement des propositions, est défini par induction, c'est-à-dire que c'est le plus petit ensemble tel que :

une variable propositionnelle p de ${}^\mathcal P$ est une formule ;
⊥ est une formule ;
si P et Q sont des formules, 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.

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.

On omet généralement les parenthèses extrêmes des formules.

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 formules qui pour cette raison sont remplacées par un point "." dans certaines notations.

Les systèmes déductifs

Article détaillé : Logique mathématique#Systèmes de déduction.

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:

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

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

La déduction à la Hilbert

Article détaillé : système à 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 :

$\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)$ ;

trois axiomes pour la disjonction :

$\big(P\to R) \to ((Q\to R) \to ((P\vee Q) \to R))$ ,
$P\to \big(P \vee Q)$ ,
$Q\to \big(P \vee Q)$ .

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

Le calcul des séquents

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

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.

$\big(A \rightarrow \; 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
$\big( (A \to B) \land A)\to B$	modus ponens (propositionnel)
$((A \to B) \land \lnot B) \to \lnot A$	modus tollens (propositionnel)
$\big( (A \to B) \land (B \to C)) \to (A \to C)$	modus barbara (propositionnel)
$(A \to B) \to \big((B \to C) \to (A \to C)\big)$	modus barbara (implicatif)
$\big(A \land (B \lor C)) \leftrightarrow ((A \land B) \lor (A \land C))$	distributivité
$\big(A \lor (B \land C)) \leftrightarrow ((A \lor B) \land (A \lor C))$	distributivité

Commentaires

Les trois systèmes utilisent le même symbole $\vdash$ , mais 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.

Sémantique

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é^[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 $\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.

Interprétation des connecteurs

Nous explicitons le comportement, puis donnons la table de vérité 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.

P	Q	$P \lor Q$
0	0	0
0	1	1
1	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.

P	Q	$P \land Q$
0	0	0
0	1	0
1	0	0
1	1	1

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

P	Q	$P \to Q$
0	0	1
0	1	1
1	0	0
1	1	1

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

P	$\lnot P$
0	1
1	0

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

P	Q	$P \leftrightarrow Q$
0	0	1
0	1	0
1	0	0
1	1	1

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

Systèmes complets de connecteurs

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 du coup 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 suffisant alors pour concevoir tous les circuits existants.

Principales propriétés

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.

Décidabilité, cohérence, complétude, compacité

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

Méthodes de calcul, NP-complétude

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

Algèbre de Boole

Article détaillé : Algèbre de Boole (structure).

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.

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 (en) ont été définies par Arend Heyting pour interpréter la logique intuitionniste.

Formes normales conjonctives, formes normales disjonctives

Articles détaillés : Forme normale disjonctive et Forme normale conjonctive.

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

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 ∨ ¬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.

Nous présentons maintenant deux variantes très proches de logique non classique, la logique minimale de Ingebrigt Johansson^[10] (1936) et la logique intuitionniste de Heyting (1930). Les connecteurs primitifs sont →, ∧, ∨ et ¬. 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 p implique sa propre négation, alors p est invalide.

(p → ¬p) → ¬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.

¬p → (p → ¬q) pour la logique minimale et ¬p → (p → 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 ⊥. 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^[11], 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.

Calcul propositionnel quantifié

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

Notes et références

↑ Une proposition est une formule ou une expression ayant comme seul contenu des variables et des opérations logiques (appelées aussi connecteur). La définition précise du concept de proposition est l'un des objectifs du calcul des propositions.
↑ Jose Ferreiros, « The Road to Modern Logic-An Interpretation », The Bulletin of Symbolic Logic, vol. 7,‎ 1^er décembre 2001, p. 441-484 (DOI 10.2307/2687794, lire en ligne)
↑ Jean Largeault, Logique mathematique: textes., A. Colin,‎ 1^er janvier 1972 (OCLC 301440117), « Contribution à l'histoire de la logique des propositions (Jan Łukasiewicz) », p. 9-25
↑ Elle est supposée vraie tout le temps.
↑ http://wiki.answers.com/Q/What_is_the_difference_between_proposition_and_predicate
↑ http://www.unicode.org/fr/charts/PDF/U27C0.pdf
↑ mais qui peuvent néanmoins la raccourcir considérablement !
↑ Les tables de vérités ont été développées originellement par Wittgenstein.
↑ Pour la logique intuitionniste, on se reportera par exemple à l'article Sémantique de Kripke.
↑ I Johansson, Ingebrigt Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus. Compositio Mathematica, 4 (1937), p. 119-136.
↑ Gödel et Kolmogorov en ont proposé.

Voir aussi

Gottfried Leibniz - George Boole - Auguste De Morgan - Gottlob Frege - Bertrand Russell - Ludwig Wittgenstein
Logique polyvalente
Fonction logique
Porte logique

Bibliographie

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-99151-1^{[à vérifier : ISBN invalide]})
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)
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)
Yannis Delmas-Rigoutsos et René Lalement, La Logique ou l'art de raisonner, Paris, Le Pommier,‎ 2000 [détail de l’édition] (ISBN 2746500353)
(en) Quine, Elementary Logic, Harvard University Press - 1980 (1941).

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

This article is issued from Wikipédia - version of the Wednesday, October 14, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.