Calcul des propositions
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

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 manière générale, le mot objet (du latin objectum, 1361) désigne une entité définie dans un espace à trois dimensions, qui a une fonction précise, et qui...) 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 (SENS (Strategies for Engineered Negligible Senescence) est un projet scientifique qui a pour but l'extension radicale de l'espérance de vie humaine. Par une évolution progressive allant du ralentissement du...) de parler de vérité.

En logique mathématique (La logique mathématique est née à la fin du XIXe siècle de la logique au sens philosophique du terme. Ses débuts furent marqués par la rencontre entre deux idées nouvelles :), le calcul des propositions (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...) 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 (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) premier, qui dépend du paramètre (Un paramètre est au sens large un élément d'information à prendre en compte pour prendre une décision ou pour effectuer un calcul.) p, n'en est pas un. Le calcul des propositions est une première étape dans la construction du calcul des prédicats (Le calcul des prédicats du premier ordre, ou calcul des relations, ou logique du premier ordre, ou tout simplement calcul des prédicats est une formalisation du langage des mathématiques proposée par les logiciens du début du...), une formalisation complète du raisonnement mathématique.

D'un point (Graphie) de vue (La vue est le sens qui permet d'observer et d'analyser l'environnement par la réception et l'interprétation des rayonnements lumineux.) plus algébrique, le calcul de propositions (pour la logique (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est...) classique) peut se voir comme un système de notations pour calculer dans les algèbres de Boole.

Introduction générale

Définition (Une définition est un discours qui dit ce qu'est une chose ou ce que signifie un nom. D'où la division entre les définitions réelles et les définitions...) 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 (Les adresses forment une notion importante en communication, elles permettent à une entité de s'adresser à une autre parmi un ensemble d'entités. Pour...) à un autre locuteur précis dans un contexte (Le contexte d'un évènement inclut les circonstances et conditions qui l'entourent; le contexte d'un mot, d'une phrase ou d'un texte inclut les mots qui l'entourent....) 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 ( En philosophie, l'abstraction désigne à la fois une opération qui consiste a isoler par la pensée une ou plusieurs qualités d'un objet concret pour en former une...) 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 scientifique est une personne qui se consacre à l'étude d'une science ou des sciences et qui se consacre à l'étude d'un domaine avec la rigueur et les méthodes scientifiques.), un fait empiriquement observable (Dans le formalisme de la mécanique quantique, une opération de mesure (c'est-à-dire obtenir la valeur ou un intervalle de valeurs d'un paramètre physique, ou plus...), 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 (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme un tout », comme...) 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é (La notion de valeur de vérité consiste à attribuer aux énoncés des valeurs numériques au travers de fonctions dont il faudra définir les règles de composition : c'est le principe de...) des propositions de base (par exemple : \lnot signifie non). Ce sens est donné, par exemple, par des tables de vérité.

La correspondance (La correspondance est un échange de courrier généralement prolongé sur une longue période. Le terme désigne des échanges de courrier personnels plutôt...) parfaite entre la déduction et la sémantique s'appelle la complétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être ajouté, en un sens qu'il faut préciser dans chaque...).

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 (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) 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 (Dans de nombreux contextes (scientifique, légal, etc.) l'on désigne par langage formel un mode d'expression plus formalisé et plus précis (les deux n'allant pas nécessairement de pair) que le langage de tous les jours (voir...) 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 (En mathématiques, un ensemble est infini s'il n'est pas fini, c'est-à-dire s'il contient un nombre infini d'éléments. En d'autres termes, si E est un ensemble infini alors  : Le cardinal...), 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 (Le genre Passer a été créé par le zoologiste français Mathurin Jacques Brisson (1723-1806) en 1760.) des parenthèses en notation polonaise, inventée par le logicien polonais Jan ?ukasiewicz. Cependant à la suite, par exemple, de Christopher Strachey (Christopher Strachey (né en 1916, décédé en 1975) est un informaticien britannique.), 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 \land, ou \lor, non \lnot, implique \to, équivaut \leftrightarrow, 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 \{\neg, \to\} est complet et typiquement la disjonction se définit au moyen de la négation et de l'implication par : A\lor B = \neg A\to B.

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 :

\lnot P a même signification que P | P
P \lor Q 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 (En mathématiques, une démonstration permet d'établir une proposition à partir de propositions initiales, ou précédemment démontrées à partir de...) automatique (L'automatique fait partie des sciences de l'ingénieur. Cette discipline traite de la modélisation, de l'analyse, de la commande et, de la régulation des systèmes dynamiques. Elle a pour...) de théorèmes Otter que l'on peut formaliser le calcul propositionnel par la seule équation (En mathématiques, une équation est une égalité qui lie différentes quantités, généralement pour poser le problème de leur identité. Résoudre l'équation consiste à déterminer...)

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

donc sans besoin (Les besoins se situent au niveau de l'interaction entre l'individu et l'environnement. Il est souvent fait un classement des besoins humains en trois grandes...) 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 (Une maison est un bâtiment de taille moyenne destiné à l'habitation d'une famille, voire de plusieurs, sans être considérée comme un immeuble collectif.) 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 (En mathématiques et en logique, une variable est représentée par un symbole. Elle est utilisée pour marquer un rôle dans une...) propositionnelle p est une formule,
  • si P et Q sont des formules, alors P \land Q, P \lor Q, P \to Q, \lnot P, P \leftrightarrow Q, etc. sont des formules.

EXEMPLES :

(P \to Q) \to (\lnot Q \to \lnot P) est une formule.
P \land \lnot P est une formule.
(P \land Q) \lor R est une formule.
P \land Q \lor n'est pas une formule.

Formes normales conjonctives, formes normales disjonctives

Une expression est en forme normale ( Forme normale (bases de données relationnelles) Forme normale (lambda-calcul) En calcul des propositions: formes normales conjonctives et formes normales disjonctives En théorie des langages formels : Forme...) 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 :

  • (a \lor b \lor c) \land (\lnot a \lor \lnot b \lor c) \land (\lnot a \lor \lnot b \lor \lnot c) est en forme normale conjonctive ;
  • (a \land b \land c) \lor (\lnot a \land b \land \lnot c) \lor (\lnot a \land \lnot b \land c) est en forme normale disjonctive ;

La syntaxe comme théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative, souvent basée sur l’observation ou...) 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 (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique construit à partir d'axiomes. Un théorème est à...). 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 \vdash f.

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

f \to (g \to f)
(f \to (g \to h)) \to ((f \to g) \to (f \to h))
(\lnot f \to g) \to ((\lnot f \to \lnot g) \to f)

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 f \to g 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 f_1,\ldots,f_n avec fn = f telle que chaque formule de la liste est ou bien

  • un axiome (Un axiome (du grec ancien αξιωμα/axioma, « considéré comme digne, convenable, évident en...), 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.

A \to A identité
A \lor \lnot A tiers exclu
\lnot\lnot A \leftrightarrow A double négation
((A \to B) \to A) \to A loi de Peirce
\lnot(A \land \lnot A) loi de 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)
(A \to B) \to(\lnot B \to \lnot A) contraposition
((A \to B) \land A)\to B modus ponens
((A \to B) \land \lnot B) \to \lnot A modus tollens
((A \to B) \land (B \to C)) \to (A \to C) modus barbara
(A \land (B \lor C)) \leftrightarrow ((A \land B) \lor (A \land C)) distributivité (En mathématiques, on dit qu'un opérateur est distributif sur un opérateur si pour tous x, y, z on a la propriété suivante : et de même à droite)
(A \lor (B \land C)) \leftrightarrow ((A \lor B) \land (A \lor C))

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) \lnot A \to \lnot A (identité appliquée sur \lnot A)
(2) (\lnot A \to \lnot A) \to ((\lnot A \to \lnot \lnot A) \to A) (axiome 3 sur A et \lnot A)
(3) (\lnot A \to \lnot \lnot A) \to A (modus ponens entre (1) et (2))
(4) \lnot \lnot A \to (\lnot A \to \lnot \lnot A) (axiome 1 avec \lnot \lnot A et \lnot A)
(5) \lnot \lnot A \to A (modus barbara entre \lnot \lnot A, \lnot A \to \lnot \lnot A et A)

Donc \vdash \lnot \lnot A \to A. Cette formule prouvée est équivalente à \lnot A \lor A qui est la propriété du tiers exclu.

Voir déduction naturelle (La déduction naturelle est une façon d'exposer les principes de la logique du premier ordre pour les rendre aussi proches que possible des façons naturelles de raisonner) pour d'autres exemples de preuves.

Sémantique

La sémantique est seconde ( Seconde est le féminin de l'adjectif second, qui vient immédiatement après le premier ou qui s'ajoute à quelque chose de nature identique. La seconde est une unité de mesure du temps. La seconde d'arc est une mesure...) 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 (La théorie des modèles est une théorie de la vérité mathématique. Elle consiste essentiellement à dire qu’une théorie est...) 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 (Une contradiction existe lorsque deux affirmations, idées, ou actions s'excluent mutuellement.). 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 \vDash P.

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:

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 \land Q prendra la valeur 1 si et seulement si les deux propositions P et Q prennent simultanément la valeur 1.
P \to Q prendra la valeur 0 si et seulement si P prend la valeur 1 et Q la valeur 0.
\lnot P prendra la valeur 1 si et seulement si P prend la valeur 0.
P \leftrightarrow Q prendra la valeur 1 si et seulement si P et Q ont la même valeur.

Exemple 1 :

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

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

Exemple 2 :

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

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

Le calcul propositionnel dispose donc de 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 (La réciproque est une relation d'implication.) repose sur le fait suivant: on peut démontrer que pour toute formule P du calcul propositionnel il existe une formule 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 Qi est de la forme R_1 \lor R_2 \lor \cdots \lor R_k, avec chaque Ri atomique (de la forme p ou \lnot p). Si P' est une tautologie, alors dans chaque Qi, apparaissent nécessairement une variable propositionnelle p et sa négation \lnot p. Sinon il existerait Qi qui ne vérifierait pas cette condition et il serait possible d'attribuer des valeurs aux pj de façon à donner la valeur 0 à Qi, et donc à P' lui-même. Mais on peut montrer que p \lor \lnot p est prouvable (\vdash p \lor \lnot p), puis qu'il en est de même de chaque Qi, 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 (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.), 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 (Le temps est un concept développé par l'être humain pour appréhender le changement dans le monde.) \vdash P et \vdash \lnot P 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 (Un atome (du grec ατομος, atomos, « que l'on ne peut diviser ») est la plus petite partie d'un corps simple pouvant se combiner chimiquement avec une autre. Il est généralement...).

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 2n 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 (Un milliard (1 000 000 000) est l'entier naturel qui suit neuf cent quatre-vingt-dix-neuf millions neuf cent quatre-vingt-dix-neuf mille neuf cent quatre-vingt-dix-neuf (999 999 999) et précède...) 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 (L'Univers est l'ensemble de tout ce qui existe et les lois qui le régissent.).

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 à A \land B 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 :

((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 (En géographie, la situation est un concept spatial permettant la localisation relative d'un espace par rapport à son environnement proche ou non. Il inscrit un lieu dans un cadre plus général afin de le...) suivante. Étant donnée (Dans les technologies de l'information, une donnée est une description élémentaire, souvent codée, d'une chose, d'une transaction, d'un événement, etc.) 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 (La recherche scientifique désigne en premier lieu l’ensemble des actions entreprises en vue de produire et de développer les connaissances scientifiques. Par extension...) exhaustive demande 2n 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 (La joue est la partie du visage qui recouvre la cavité buccale, fermée par les mâchoires. On appelle aussi joue le muscle qui sert principalement à ouvrir et fermer la...) un rôle fondamental en théorie de la complexité (La théorie de la complexité s'intéresse à l'étude formelle de la difficulté des problèmes en informatique. Elle se distingue de la théorie de la calculabilité qui s'attache à savoir si un...), 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 (Le mot « infini » (-e, -s ; du latin finitus, « limité »), est un adjectif servant à qualifier quelque chose qui n'a pas de limite en nombre ou en taille.) 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 (En mathématiques, un ensemble A est un sous-ensemble ou une partie d’un ensemble B, ou encore B est sur-ensemble de A, si tout élément du 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é (Il s'agit d'énoncer et de prouver le théorème de compacité du calcul des propositions. Ce théorème a un rôle très important pour la logique du premier ordre, notamment pour la preuve du théorème de...) pour plus d'information.

Algèbre (L'algèbre, mot d'origine arabe al-jabr (الجبر), est la branche des mathématiques qui étudie, d'une façon générale, les...) de Boole

Soit donné un ensemble de variables propositionnelles atomiques. Soit E l'ensemble des formules ayant pour atomes ces variables propositionnelles. Soit \mathfrak R la relation binaire (Une relation binaire est un concept mathématique qui systématise des notions comme « ... est supérieur ou égal à ... » en arithmétique, ou « ... est élément de l’ensemble ... » en théorie des...) définie sur E par l'équivalence (\leftrightarrow) entre deux formules. \mathfrak R est une relation d'équivalence sur E, compatible avec \lor et \land. Alors l'ensemble quotient E/\mathfrak R 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 (En 1935 Gentzen a proposé la déduction naturelle, un formalisme pour décrire les preuves du calcul des prédicats, dont l'idée était de coller au plus près à la...).

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 P \lor \lnot P, appelée principe du tiers exclu, la formule \lnot\lnot P \to P, appelée élimination de la double négation, ou la formule ((P \to Q) \to P) \to P 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 \bot une contradiction du type Q \land \lnot Q) :

\lnot(P \to \bot)

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

\lnot(\lnot P \lor \bot)

et donc à :

\lnot \lnot P \land \lnot \bot

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

\lnot \lnot P

et puisque \lnot \lnot P \to P 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 P \vee \neg P. 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 \lnot \lnot P \to P. 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 (Un siècle est maintenant une période de cent années. Le mot vient du latin saeculum, i, qui signifiait race, génération. Il a ensuite indiqué la durée d'une génération humaine et faisait 33 ans 4...), 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 (L´informatique - contraction d´information et automatique - est le domaine d'activité scientifique, technique et industriel en rapport avec le traitement automatique de...). 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 Lien vers un homonyme? (1936) et la logique intuitionniste de Heyting (1930). Les connecteurs primitifs sont \to, \land, \lor et \lnot. On garde les deux premiers axiomes de la logique classique :

f \to (g \to f)
(f \to (g \to h)) \to ((f \to g) \to (f \to h))

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

(f \land g) \to f
(f \land g) \to g
(f \to g) \to ((f \to h) \to (f \to (g \land h)))

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

f \to (f \lor g)
g \to (f \lor g)
(f \to h) \to ((g \to h) \to ((f \lor g) \to h))

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

(f \to \lnot f) \to \lnot f.

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

\lnot f \to (f \to \lnot g) pour la logique minimale, et \lnot f \to (f \to g) 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 \bot. Mais la différence porte sur l'utilisation que l'on fait de cette contradiction :

  • La logique classique déduit de \lnot P \to \bot le fait que P est vrai (raisonnement par l'absurde).
  • La logique intuitionniste déduit d'une contradiction que toute formule est prouvable. De \lnot P \to \bot, elle déduit la validité de \lnot\lnot P, propriété plus faible que P.
  • La logique minimale déduit d'une contradiction que toute négation de formule est prouvable, qui est plus faible que ce que propose la logique intuitionniste.

Logique minimale et logique intuitionniste acceptent le théorème \lnot (f \land \lnot f). Par contre f \lor \lnot f n'est pas un théorème de ces logiques.

De même, elles permettent de prouver f \to \lnot \lnot f mais pas la réciproque. Par contre, elles prouvent l'équivalence entre \lnot f et \lnot \lnot \lnot f. Enfin, la formule (\lnot f \lor g) \to (f \to g) 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 \lnot \lnot f 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.

Page générée en 0.292 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique