De nos jours, Calcul des propositions est devenu un sujet d'une grande pertinence et d'un grand intérêt dans la société actuelle. Depuis son émergence, Calcul des propositions suscite des débats, des controverses et des réflexions dans différents domaines et secteurs. Son impact ne se limite pas seulement à l’aspect social, mais a également généré des répercussions au niveau politique, économique et culturel. Dans cet article, nous explorerons les différentes facettes et dimensions de Calcul des propositions, en analysant son évolution dans le temps et son influence sur notre réalité actuelle. En approfondissant ses différents aspects, nous tenterons de comprendre de manière globale sa signification et le rôle qu’elle joue dans la société moderne.
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 » 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. Il est considéré comme la forme moderne de la logique stoïcienne.
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 ; 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.
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.
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 | |
ou | |
non | |
implique | |
équivaut à |
On considère souvent aussi la constante notée ⊥, prononcé « taquet vers le haut », « 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 de variables propositionnelles. L'ensemble des formules du calcul des propositions (sur ), ou simplement des propositions, est défini par induction, c'est-à-dire que c'est le plus petit ensemble tel que :
Exemples : Si P, Q et R sont des propositions,
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.
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.
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:
Les sont appelées les prémisses et est appelée la conclusion.
Il n'y a qu'une seule règle appelée le modus ponens, elle s'écrit :
Elle peut se comprendre ainsi : si est un théorème et est un théorème alors est un théorème. À cela, on peut ajouter :
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 est conséquence d'un ensemble d'hypothèses, on écrit . 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.
En outre, il y a une règle de réduction à l'absurde, nécessaire en logique classique:
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 , on ajoute aux hypothèses et si l'on obtient l'absurde, alors on a .
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 où et sont des multiensembles de propositions. Le séquent s'interprète comme l'assertion de la conjonction des on déduit la disjonction des . Les sont appelés les antécédents et les sont appelés les conséquents. Si la liste des antécédents est vide on écrit , si la liste des conséquents est vide on écrit . Un théorème est encore un séquent sans antécédents et avec un seul conséquent.
Une coupure traduit l'attitude du mathématicien qui démontre un lemme (la proposition ) 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. 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.
identité | |
tiers exclu | |
double négation | |
double négation classique | |
loi de Peirce | |
non contradiction | |
lois de De Morgan | |
contraposition | |
modus ponens (propositionnel) | |
modus tollens (propositionnel) | |
modus barbara (propositionnel) | |
modus barbara (implicatif) | |
distributivité | |
Les trois systèmes utilisent le même symbole , mais cette notation est cohérente. Le format 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 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 , 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é à 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, 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:
Nous explicitons le comportement, puis donnons la table de vérité associée
P | Q | |
0 | 0 | 0 |
0 | 1 | 1 |
1 | 0 | 1 |
1 | 1 | 1 |
P | Q | |
0 | 0 | 0 |
0 | 1 | 0 |
1 | 0 | 0 |
1 | 1 | 1 |
P | Q | |
0 | 0 | 1 |
0 | 1 | 1 |
1 | 0 | 0 |
1 | 1 | 1 |
P | |
0 | 1 |
1 | 0 |
P | Q | |
0 | 0 | 1 |
0 | 1 | 0 |
1 | 0 | 0 |
1 | 1 | 1 |
Exemple 1 :
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 :
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) 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.
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 :
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 2n 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 à 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 :
Étant constituée d'une implication, pour la rendre invalide, il suffit que la conclusion puisse prendre la valeur 0 (et donc la valeur 1) et que l'hypothèse puisse prendre la valeur 1 (et donc et la valeur 1). Mais alors prend la valeur 0 et 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.
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.
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 et une conjonction est une proposition de la forme . 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 :
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 :
On peut montrer que toute proposition est équivalente à une FND (en admettant que 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 il existe une proposition en forme normale disjonctive telle que et une proposition en forme normale conjonctive telle que .
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 (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.
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) :
Axiomes de la conjonction :
Axiomes de la disjonction , (duaux des précédents) :
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 ou la loi de Peirce .
Si on adjoint aux axiomes ax.1 à ax.8 l'axiome suivant :
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 :
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 :
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 :
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, 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 :