Calcul des propositions - Définition

Le calcul des propositions ou calcul propositionnel, dont le fondateur fut le logicien allemand Frege, version moderne de la logique stoïcienne, est une théorie logique qui définit les lois formelles du raisonnement. La notion de proposition est assez complexe à définir en général et a fait l'objet de nombreux débats au cours de l'histoire de la logique ; l'idée de base est qu'une proposition est un énoncé pour lequel il fait sens de parler de vérité.

En logique mathématique, le calcul des propositions définit les règles de raisonnement concernant les énoncés clos, c’est-à-dire ne dépendant d'aucun paramètre : par exemple, l'énoncé 3 est un nombre premier est un énoncé clos (une proposition atomique), alors que l'énoncé p est un nombre premier, qui dépend du paramètre p, n'en est pas un. Le calcul des propositions est une première étape dans la construction du calcul des prédicats, une formalisation complète du raisonnement mathématique.

D'un point de vue plus algébrique, le calcul de propositions (pour la logique classique) peut se voir comme un système de notations pour calculer dans les algèbres de Boole.

Introduction générale

Définition d'une proposition

Il est difficile de donner une définition consensuelle du concept de " proposition ". Une première approche (négative) consiste à dire ce qu'une proposition n'est pas. Ce n'est pas un énoncé assumé par un locuteur qui s'adresse à un autre locuteur précis dans un contexte particulier. Par exemple, un énoncé comme " je pense que… " étant une affirmation du locuteur n'est donc pas une proposition. Ou bien comme une proposition fait abstraction du contexte, les actes de langage accompagnant l'énoncé ou les indications renvoyant aux circonstances d'énonciation (tels les déictiques " ici " ou " maintenant ") ne sont pas pris en considération.

Ce qu'est une proposition: d'une part elle donne une information sur un état de chose: " 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. 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.

Définition d'un calcul

Un calcul en logique est un ensemble d'algorithmes c'est-à-dire 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 complexe (c'est-à-dire formée d'au moins deux propositions atomiques) est vraie ou fausse.

Le fait que la logique moderne grâce à Frege ait réussi à faire du traitement traditionnel des propositions depuis les stoïciens un calcul est sans doute ce qui constitue la nouveauté la plus importante de la logique moderne.

Structure

Comme la plupart des théories logico-mathématiques, il est possible de considérer le calcul des propositions des points de vue syntaxique et sémantique :

• aspect syntaxique : il s'agit d'abord de définir le langage du calcul des propositions, les règles de formation des propositions complexes ainsi que les règles d'inférence permettant la déduction des propositions les unes à partir des autres. Ces règles de déduction sont choisies de façon à ce que les propositions engendrées soient effectivement des théorèmes. Dans le cadre d'une présentation axiomatique, on peut même partir d'une série de propositions primitives afin d'engendrer de nouvelles formules à partir de formules déjà produites.
• 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 (par exemple : signifie non). Ce sens est donné, par exemple, par des tables de vérité.

La correspondance parfaite entre la déduction et la sémantique s'appelle la complétude.

Le système exposé ci-dessous se situe dans le cadre de la logique classique. 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

La syntaxe du calcul des propositions comporte un alphabet associé à des règles de formation des formules et à des règles d'inférence. Nous présenterons dans la suite ces trois composantes : les deux composantes syntaxiques (formules et déductions) et la composante sémantique.

Le langage

Le langage du calcul des propositions est un langage formel et symbolique. Langage formel et symbolique dans la mesure où pour désigner les propositions on fait abstraction de la signification particulière des propositions (c'est l'étape de la formalisation) pour travailler uniquement avec des symboles comme les lettres p ou q appelées variables propositionnelles ou formules atomiques, notées p, q, etc., dans un ensemble infini, mais dénombrable, de symboles. À côté de ces lettres on utilise des parenthèses, éléments de ponctuation visant à lever les ambiguïtés dans les formules. À noter qu'on peut se passer des parenthèses en 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 choisie pour se consacrer au fond des choses: la déduction et la sémantique.

Le deuxième élément fondamental du langage du calcul des propositions sont les opérateurs. Ce sont les symboles qui permettent de lier les propositions atomiques entre elles. Leur valeur est fonction de la valeur des propositions atomiques les composant. On dit pour cette raison que les opérateurs sont " vérifonctionnels ". Exemples de connecteurs logiques : et , ou , non , implique , équivaut , etc.

Un ensemble de connecteurs propositionnels est complet si tout connecteur peut se définir au moyen des connecteurs de l'ensemble. Par exemple l'ensemble est complet et typiquement la disjonction se définit au moyen de la négation et de l'implication par : .

Il existe des présentations du calcul des propositions travaillant avec un nombre réduit de connecteurs: notamment l'ensemble constitué du seul connecteur d'incompatibilité de Sheffer, noté par une barre |. Il n'y a qu'un seul axiome :

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

Les connecteurs dérivés de la barre de Sheffer sont définis comme suit :

a même signification que P | P

a même signification que (P | P) | (Q | Q)

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 le calcul propositionnel par la seule équation

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

donc sans besoin de règle.

Les formules bien formées

Le calcul des propositions repose de plus sur des règles de formation indiquant comment construire des propositions complexes. Par exemple une proposition complexe comme " p q ? " n'est pas une proposition bien formée ou formule bien formée (" FBF " ou " well-formed formulae " en anglais) alors que " p ? q " est une " FBF ". De la même façon, à titre de comparaison, une phrase comme " je maison viens " n'est pas en français une phrase correctement construite.

Une formule ou énoncé bien formé est définie itérativement comme suit :

• une variable propositionnelle p est une formule,
• si P et Q sont des formules, alors , , , , , etc. sont des formules.

EXEMPLES :

est une formule.

est une formule.

est une formule.

n'est pas une formule.

Formes normales conjonctives, formes normales disjonctives

Une expression est en forme normale conjonctive si elle est composée de conjonction de disjonction. Une expression est en forme normale disjonctive si elle est composée de disjonction de conjonction.

Exemple :

• est en forme normale conjonctive ;
• est en forme normale disjonctive ;

La syntaxe comme théorie de la démonstration

L'élément le plus important de la syntaxe du calcul des propositions est cependant les règles de transformation des FBF. C'est l'élément le plus important dans la mesure où le calcul des propositions veut déterminer les règles de déduction d'une proposition à partir d'une autre. Or, le fait de déduire une proposition à partir d'une autre est assimilé par la logique à la transformation d'une proposition " A " en une proposition " B ". La syntaxe comme ensemble des règles de transformation peut donc être aussi dite théorie de la preuve. Ces règles de transformation sont composées de règles d'inférence voire d'axiomes dans le cas de la présentation axiomatique du calcul des propositions.

Une proposition déduite à partir d'une autre au moyen des règles d'inférence s'appelle un théorème. Dit autrement: Une formule qui admet une preuve est un théorème du calcul des propositions. Si f est un théorème, on note cela par .

En logique classique une certaine tradition considère les deux connecteurs (négation) et (implication) comme primitifs. On donnera les règles de déduction pour eux seuls. Pour cela, on se donne trois schémas d'axiomes:

où f, g, h peuvent être remplacés par des formules quelconques. La troisième formule est à la base du raisonnement par l'absurde.

On se donne également une règle d'inférence, le modus ponens, qui énonce que si f et sont des formules démontrées, alors g est également démontrée.

Dans l'écriture de Sheffer, le modus ponens est remplacé par la règle d'inférence suivante :

si P et P | (Q | R) sont deux formules déjà prouvées, alors on peut déclarer R comme formule prouvée.

Soit f une formule. Une preuve de f est une liste finie et ordonnée de formules avec f_n = f telle que chaque formule de la liste est ou bien

• un axiome, ou bien
• une formule qui est conséquence par modus ponens de formules antérieures de la liste.

Les trois axiomes et le modus ponens sont donc les règles de base du raisonnement logique, desquelles on peut déduire toutes les autres règles de raisonnement.

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.

	identité
	tiers exclu
	double négation
	loi de Peirce
	loi de non-contradiction
	lois de De Morgan
	contraposition
	modus ponens
	modus tollens
	modus barbara
	distributivité

Donnons un exemple de preuve du théorème de double négation (ou du moins d'une des deux implications), en supposant prouvé le théorème d'identité et le modus barbara :

(1) (identité appliquée sur )

(2) (axiome 3 sur A et )

(3) (modus ponens entre (1) et (2))

(4) (axiome 1 avec et )

(5) (modus barbara entre , et A)

Donc . Cette formule prouvée est équivalente à qui est la propriété du tiers exclu.

Voir déduction naturelle pour d'autres exemples de preuves.

Sémantique

La sémantique est seconde par rapport à la syntaxe car les seules propositions bien formées peuvent être douées de sens. La sémantique ou théorie des modèles détermine les règles d'interprétations des formules. Attribuer des valeurs de vérité à chacune des propositions élémentaires intervenant dans la formule A revient à choisir un modèle de cette formule

De façon plus précise, l'interprétation d'une formule est le fait d'attribuer une valeur aux propositions simples et aux connecteurs (en fonction de la valeur des propositions simples). Il existe alors trois cas d'interprétation:

• Quand il n'y a que des 0, c'est une antilogie ou contradiction. C'est la négation de la tautologie. On dit également que A est insatisfiable.
• S'il y a au moins un 1 et au moins un 0, c'est une formule synthétique ou contingente.
• Lorsque le résultat n'est constitué que de 1, c'est une loi logique ou tautologie. On dira que A est une formule valide, et on notera .

Les tables de vérités développées originellement par Wittgenstein sont un exemple d'une interprétation d'une formule mathématique.

Exemples d'interprétation des connecteurs:

prendra la valeur 1 si et seulement si au moins l'une des deux propositions P ou Q prend la valeur 1.

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

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

prendra la valeur 1 si et seulement si P prend la valeur 0.

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

Exemple 1 :

est une tautologie.

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

Exemple 2 :

n'est pas une tautologie.

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

Le calcul propositionnel dispose donc de deux moyens différents pour valider les formules : la méthode axiomatique qui définit les formules prouvées, et la méthode des valeurs de vérité qui définit les tautologies.

Principales propriétés

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

Le fait que toute formule est prouvable si et seulement si elle est une tautologie exprime le fait que le calcul propositionnel est complet. La présentation déductive du calcul propositionnel est donc équivalent à la présentation sémantique. En effet :

• Toute formule prouvée résulte d'un axiome ou de l'application du modus ponens sur des formules déjà prouvées. Or il est facile de vérifier que les trois schémas d'axiomes fournissent des tautologies, et que le modus ponens conserve les tautologies. Toute formule prouvé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 formule P du calcul propositionnel il existe une formule P' telle que et telle que P' soit sous une forme dite normale où chaque Q_i est de la forme , avec chaque R_i atomique (de la forme p ou ). Si P' est une tautologie, alors dans chaque Q_i, apparaissent nécessairement une variable propositionnelle p et sa négation . 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 est prouvable ( ), 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 prouvable. Le calcul propositionnel est complet.

Voir le théorème de complétude du calcul des propositions pour une autre démonstration, plus détaillée.

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

• Le calcul propositionnel est décidable, dans le sens où il existe un algorithme permettant de décider si une formule 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 propositionnel est cohérent (consistant), c'est-à-dire non contradictoire. Il n'existe aucune formule P telle qu'on puisse avoir en même temps et car ces deux propositions seraient des tautologies et on aurait 1 = 0.
• Le calcul propositionnel est fortement complet (maximalement cohérent), dans le sens où tout ajout d'un nouveau schéma d'axiome, non prouvable dans le système initial, rend ce système incohérent.

Méthodes de calcul, NP-complétude

Nous avons vu que, pour décider si une formule est prouvable, 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 atomes.

Cette approche théorique se heurte cependant au temps de calcul que demande une telle démarche. En effet, si la formule possède n variables propositionnelles atomiques, il faudra calculer 2ⁿ valeurs possibles de la formule complète, ce qui devient rapidement difficile pour n trop grand. Ainsi, si n = 30, il faudra vérifier plus d'un milliard de valeurs. Si n = 100, le temps de calcul nécessaire pour effectuer toutes les vérifications 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 A, on peut attribuer directement la valeur 0 à indépendamment de la valeur ultérieure attribuée à B, 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 formule :

Étant constituée d'une implication, pour la rendre invalide, il suffit que la conclusion puisse prendre la valeur 0 (et donc p la valeur 1) et que l'hypothèse puisse prendre la valeur 1 (et donc et la valeur 1). Mais alors s 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ée une formule 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 atomes de f qui rendraient f invalide.

• Une recherche exhaustive demande 2ⁿ vérifications si f possède n variables propositionnelles atomiques. 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 recherchée par tirage au sort. Une telle démarche est dite non déterministe.

On dit alors que la question de l'insatisfiabilité de f est du type NP (pour polynomial non déterministe). Le problème dual est celui de la satisfiabilité d'une formule, à savoir trouver une configuration qui donne 1 comme valeur de vérité de la formule. 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 prouvabilité d'une formule) est un problème NP-complet.

Compacité

La compacité du calcul propositionnel réside dans la propriété suivante. Supposons donné un nombre infini de formules. On se pose la question de savoir si ces formules sont simultanément satisfiables, c'est-à-dire s'il existe des valeurs de vérité de leurs atomes qui donne 1 comme valeur de vérité à toutes les formules. On montre que, si tel est le cas pour tout sous-ensemble fini de ces formules, alors il en est de même pour toutes les formules. On renvoie à l'article théorème de compacité pour plus d'information.

Algèbre de Boole

Soit donné un ensemble de variables propositionnelles atomiques. Soit E l'ensemble des formules ayant pour atomes ces variables propositionnelles. Soit la relation binaire définie sur E par l'équivalence ( ) entre deux formules. est une relation d'équivalence sur E, compatible avec et . Alors l'ensemble quotient E/ possède une structure d'algèbre de Boole.

Systèmes de démonstration formelle

Il existe plusieurs familles de systèmes de démonstration formelle, notamment:

1. les systèmes à la Hilbert,
2. la déduction naturelle
3. et le calcul des séquents.

Procédure d'évaluation des lois

Il existe plusieurs procédés pour décider si une formule est antilogique (fausse pour toute interprétation), consistante (vraie pour au moins une interprétation) ou bien une tautologie.

1. Les tables de vérité sont un de ces procédés.
2. La méthode de résolution de Herbrand qui se base sur les expressions en forme normale conjonctive.
3. La méthode de résolution qui provient des tableaux sémantiques de Evert Willem Beth.

Logique classique, minimale, intuitionniste

La logique classique et le tiers exclu

Les axiomes du calcul propositionnel que nous avons présentés sont ceux de la logique classique. Ils permettent de prouver la formule , appelée principe du tiers exclu, la formule , appelée élimination de la double négation, ou la formule appelée loi de Peirce. Cette logique repose sur le principe qu'une propriété P est nécessairement vraie ou fausse. C'est le point de vue, qualifié de formaliste, adopté par Hilbert. Or ce point de vue a été contesté par plusieurs mathématiciens, dont le plus connu est Brouwer, créateur de la logique intuitionniste. Essayons de comprendre pourquoi.

Pour Hilbert, il suffit de prouver qu'une propriété P n'entraîne aucune contradiction pour justifier la validité de P. En effet, P n'entraîne aucune contradiction peut être représenté en calcul propositionnel sous la forme suivante (en désignant par une contradiction du type ) :

ce qui, en logique classique, est équivalent à :

et donc à :

Compte tenu que est un théorème, on a :

et puisque est aussi un théorème, on obtient

P.

Si P formule par exemple l'existence d'un objet mathématique, on voit que, pour Hilbert, il suffit que cette existence n'entraîne aucune contradiction pour pouvoir être validée, quand bien même on ne disposerait d'aucun procédé pour mettre en évidence l'objet ainsi introduit. En d'autres termes, l'implication classique se réduit à l'implication matérielle Pour les intuitionnistes, l'existence d'une demonstration repose sur un procédé constructif pour la fabriquer à partir des axiomes.

Les mathématiciens intuitionnistes ou constructivistes ne peuvent que rejeter la démarche évoquée ci-dessus, et en particulier la dernière étape . Ils n'introduisent donc pas dans leur calcul des propositions le troisième axiome du calcul propositionnel classique relatif à la négation. Cette démarche, jugée marginale dans la première moitié du XXème siècle, a pris depuis un intérêt grandissant, pour deux raisons. Primo, la logique intuitionniste se situant "avant" la logique classique permet de mieux comprendre cette dernière. Secundo, la nature calculatoire de la logique intuitionniste allié à la correspondance de Curry-Howard fait de celle-ci la logique la mieux adaptée à l'informatique. Certes des travaux récents des logiciens contemporains parviennent à conférer aussi à la logique classique un contenu calculatoire, mais son caractère plus complexe le fait sortir des limites de cet article.

Logique minimale, logique intuitionniste

Nous présentons deux variantes très proches de logique non classique, la logique minimale de Johansson  ^? (1936) et la logique intuitionniste de Heyting (1930). Les connecteurs primitifs sont , , et . On garde les deux premiers axiomes de la logique classique :

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

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

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

.

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.

pour la logique minimale, et pour la logique intuitionniste.

En présence d'une formule 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 le fait que P est vrai (raisonnement par l'absurde).
• La logique intuitionniste déduit d'une contradiction que toute formule est prouvable. De , elle déduit la validité de , propriété plus faible que P.
• La logique minimale déduit d'une contradiction que toute négation de formule est prouvable, qui est plus faible que ce que propose la logique intuitionniste.

Logique minimale et logique intuitionniste acceptent le théorème . Par contre n'est pas un théorème de ces logiques.

De même, elles permettent de prouver mais pas la réciproque. Par contre, elles prouvent l'équivalence entre et . Enfin, la formule est un théorème de la logique intuitionniste, mais pas de la logique minimale.

Glivenko a démontré en 1929 que f est un théorème du calcul propositionnel classique si et seulement si est un théorème du calcul propositionnel intuitionniste. Ce résultat est faux en calcul propositionnel minimal, ainsi d'ailleurs qu'en calcul des prédicats intuitionniste.