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 »Une proposition est un énoncé clos, c'est-à-dire ne dépendant d'aucun paramètre extérieur, comme « il y a une infinité de nombres premiers » ou « 57 est un nombre premier ». La définition précise du concept de proposition est l'un des objectifs du calcul des 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..
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. Le calcul des propositions, ou calcul propositionnel est encore appelé logique des propositions, logique propositionnelle ou calcul des énoncés.
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.
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.
Proposition et prédicat 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 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 , qui est vraie ; si le lecteur est canadien, on obtiendra la proposition , qui est fausse « », Answers.com. ; 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'AsieA noter que l'on aurait aussi pu considérer la Turquie..
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 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.
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.
Syntaxe des formules propositionnelles : il s’agit de définir le langage du calcul des propositions par les règles d’écriture des propositions. Le sens des formules propositionnelles (qui sont les expressions syntaxiquement correctes) est donné par le sens des connecteurs. Il peut être décrit de deux façons. Par la sémantique : il s’agit ici d'interpréter les symboles représentant les connecteurs logiques par des fonctions de la valeur de vérité des propositions de base (ainsi signifie non). Ce sens est donné en logique classique par des tables de vérité, dans d'autres logiques par exemple par des modèles de Kripke. Par la déduction : le sens des connecteurs est décrit de façon opératoire, par des règles purement syntaxiques dites règles d'inférence. Ces règles permettent la déduction de propositions à partir d'autres. Elles engendrent des propositions spécifiques que l'on appelle des théorèmes. Pour une logique donnée, les règles de déductions envisagées sont correctes vis-à-vis de la sémantique, au sens où à partir de propositions vraies on ne peut déduire que des propositions vraies. Si la déduction correspond parfaitement à la sémantique le système est dit complet.
Le système exposé ci-dessous se situe dans le cadre de la logique classique, qui est la branche de la logique mathématique la plus utilisée en mathématiques. On trouvera plus loin une présentation de logiques non classiques. L'adjectif « classique » ne doit pas être pris dans un sens de « normalité », mais comme un attribut que lui a donné l'histoire de la logique, elle aurait tout aussi bien pu s'appeler « booléenne ».
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 équivaut à
On considère souvent aussi la constante notée ⊥, prononcé « taquet vers le haut » « Divers symboles mathématiques - A | Intervalle : 27C0–27EF »., « type vide », « » ou « », 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 de variables propositionnelles. L'ensemble des propositions (ou formule propositionnelle) (sur ) est défini par induction, c'est-à-dire que c'est le plus petit ensemble tel que : une variable propositionnelle p de est une proposition ; ⊥ est une proposition ; si P et Q sont des propositions, alors (P ∧ Q), (P ∨ Q), (P → Q), (P ↔ Q) et ¬P sont des propositions.
Exemples : Si P, Q et R sont des propositions,
(P → Q) → (¬Q → ¬P) est une proposition. (P → ⊥) → ⊥ est une proposition. P ∧ ¬P est une proposition. (P ∧ Q) ∨ R est une proposition. P ∧ Q ∨ n'est pas une proposition.
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 propositions. On supprime souvent les parenthèses en associant les expressions de gauche à droite quand il s'agit du même connecteur : A ∧ B ∧ C pour ((A ∧ B) ∧ C). L'implication constitue un cas particulier. Par convention, elle est associative à droite : A → B → C → D se lit A → (B → (C → D)).
Pour la lisibilité, on utilise également plusieurs formes de parenthèses (taille, remplacement par des crochets...)
Par ailleurs, on démontre que seules les parenthèses ouvrantes sont nécessaires à la non-ambiguïté de la lecture des propositions qui pour cette raison sont remplacées par un point "." dans certaines notations.
Les systèmes déductifs
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.
La déduction à la Hilbert
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 : trois axiomes pour l'implication et le faux : , ,
trois axiomes pour la disjonction : , , . trois axiomes pour la conjonction : , . .
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 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. L'axiome est . La règle d'introduction de l'implication:
La règle d'élimination de l'implication:
Les deux règles d'introduction de la disjonction, droite et gauche:
La règle d'élimination de la disjonction:
La règle d'élimination du faux:
En outre, il y a une règle de réduction à l'absurde, nécessaire en logique classique: