Calcul des propositions - Définition

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

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., formant un ensemble infini dénombrable.

Les deuxièmes constituants de base du langage du calcul des propositions sont les opérateurs ou connecteurs. Ce sont des symboles qui permettent de construire des propositions plus élaborées. Les plus courants de ces connecteurs logiques sont et ∧, ou ∨, non ¬, implique → ou ⇒, équivaut ↔ ou ⇔. On considère souvent aussi la constante ⊥ qui vise à représenter le faux.

À côté de ces symboles on utilise des parenthèses pour lever les ambiguïtés dans les formules (choix adopté ci-dessous), ou une notation comme la notation polonaise, inventée par le logicien polonais Jan Łukasiewicz. Il est important que la définition des formules soit simple et sans ambiguïtés, pour permettre en particulier les définitions inductives sur la structure des formules, mais pratiquement il est possible d'économiser les parenthèses, soit en adoptant certaines conventions pour lever les ambiguïtés, soit parce que le contexte fait que ces ambiguïtés sont sans importance.

Les formules propositionnelles

Le calcul des propositions repose de plus sur des règles de formation indiquant comment construire des propositions complexes à partir des propositions élémentaires, ou atomes, que sont les variables propositionnelles, et d'éventuelles constantes comme ⊥. Ces règles déterminent quels assemblages de signes, quels mots, sont bien formés et désignent des propositions. La définition dépend d'un choix de connecteurs, et d'un choix d'atomes.

On se donne un ensemble {}^\mathcal P de variables propositionnelles. L'ensemble des formules du calcul des proposition (sur {}^\mathcal P ), ou simplement des propositions, est défini par induction, c'est-à-dire que c'est le plus petit ensemble tel que :

  • une variable propositionnelle p de {}^\mathcal P est une formule ;
  • ⊥ est une formule ;
  • si P et Q sont des formules, alors (PQ), (PQ), (PQ), (PQ) et ¬P sont des propositions.

Exemples : Si P, Q et R sont des propositions,

(PQ) → (¬Q → ¬P) est une proposition.
(P → ⊥) → ⊥ est une proposition.
P ∧ ¬P est une proposition.
(PQ) ∨ R est une proposition.
PQ ∨ n'est pas une proposition.
Quelques conventions syntaxiques

Afin d'alléger la présentation des expressions sans mettre en péril l'absence d'ambiguïté, on autorise par des conventions syntaxiques certaines entorses à la définition ci-dessus.

  • On omet généralement les parenthèses extrêmes des formules.
  • On supprime souvent les parenthèses en associant les expressions de droite à gauche quand il s'agit du même connecteur : ABC pour ((AB) ∧ C)

Pour la lisibilité, on utilise également plusieurs formes de parenthèses (taille, remplacement par des crochets, ...)

Par ailleurs, on démontre que seules les parenthèses ouvrantes sont nécessaires à la non-ambiguïté de la lecture des formules qui pour cette raison sont remplacées par un point "." dans certaines notations.

Les systèmes déductifs

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 occurrence 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 \vdash P.

Les systèmes déductifs utilisent des règles de déduction (appelées aussi règles d'inférence) qui s'écrivent:

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

Les \varphi_i sont appelées les prémisses et ψ 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:

\frac{\vdash P \to Q \quad \vdash P}{\vdash Q}.

Elle peut se comprendre ainsi si P \to Q est un théorème et P est un théorème alors Q est un théorème. À cela, on peut ajouter trois axiomes pour l'implication et le faux et trois axiomes pour la disjonction:

  • \vdash P \to (Q \to P) ,
  • \vdash (P \to (Q \to R)) \to ((P \to Q) \to (P \to R)) ,
  • \vdash (\lnot P \to \lnot Q) \to (Q \to P) ,
  • \big(P\to R) \to ((Q\to R) \to ((P\vee Q) \to R)) ,
  • P\to \big(P \vee Q) ,
  • Q\to \big(P \vee Q) .
La déduction naturelle

Alors que la déduction à la Hilbert manipule et démontre des théorèmes, la déduction naturelle démontre des propositions sous des hypothèses et quand il n'y a pas (plus) d'hypothèses, ce sont des théorèmes. Pour dire qu'une proposition P est conséquence d'un ensemble Γ d'hypothèses, on écrit \Gamma\vdash P . Alors que dans la déduction à la Hilbert, il n'y a qu'une règle et plusieurs axiomes, dans la déduction naturelle il y a un seul axiome et plusieurs règles. Pour chaque connecteur, on classe les règles en règles d'introduction et en règles d'élimination.

  • L'axiome est \Gamma, P \vdash P .
  • La règle d'introduction de l'implication:
\frac{\Gamma, P \vdash Q}{\Gamma\vdash P \to Q}
  • La règle d'élimination de l'implication:
\frac{\Gamma\vdash P\to Q\qquad \Gamma \vdash P}{\Gamma\vdash Q}
  • Les deux règles d'introduction de la disjonction, droite et gauche:
\frac{\Gamma \vdash P}{\Gamma\vdash P\vee Q}\qquad \qquad \frac{\Gamma \vdash Q}{\Gamma\vdash P\vee Q}
  • La règle d'élimination de la disjonction:
\frac{\Gamma \vdash P\vee Q \qquad \Gamma,P\vdash R\qquad \Gamma,Q\vdash R}{\Gamma\vdash R}
  • La règle d'élimination du faux:
\frac{\Gamma \vdash \perp}{\Gamma\vdash P}

En outre, il faut une règle qui est la réduction à l'absurde, nécessaire en logique classique:

\frac{\Gamma,\neg P \vdash \perp}{\Gamma \vdash P}

On remarquera que la règle d'élimination de l'implication est très proche du modus ponens, d'ailleurs on l'appelle aussi modus ponens. On remarquera qu'il n'y pas de règle d'introduction du faux et que la règle d'élimination du faux revient à dire que si d'un ensemble d'hypothèses je déduis le faux (ou l'absurde) alors de ce même ensemble je peux déduire n'importe quoi. On remarquera que la réduction à l'absurde est la règle qui correspond au raisonnement par l'absurde: pour démontrer P, on ajoute \neg P aux hypothèses et si l'on obtient l'absurde, alors on a P.

Le calcul des séquents

L'une des idées qui à conduit au calcul des séquents est de n'avoir plus que des règles d'introduction en plus d'une règle que l'on appelle coupure et de règles structurelles. Pour cela, on utilise des formules que l'on appelle des séquents et qui sont de la forme \Gamma\vdash\Delta Γ et Δ sont des multiensembles de propositions. Le séquent P_1,...,P_m\vdash Q_1,...,Q_n s'interprète comme l'assertion de la conjonction des Pi on déduit la disjonction des Qj. Les Pi sont appelés les antécédents et les Qj sont appelés les conséquents. Si la liste des antécédents est vide on écrit \vdash \Delta , si la liste des conséquents est vide on écrit \Gamma \vdash . Un théorème est encore un séquent sans antécédents et avec un seul conséquent.

  • L'axiome est A \vdash A .
  • Introduction de l'implication à droite :
\frac{\Gamma,A \vdash \Delta, B}{\Gamma \vdash \Delta, A \to B}
  • Introduction de l'implication à gauche :
\frac{\Gamma,A \vdash \Delta \qquad \Gamma' \vdash \Delta',B}{\Gamma, \Gamma', B \to A \vdash \Delta, \Delta'}
  • Introduction de la disjonction à droite :
\frac{\Gamma \vdash \Delta,A,B}{\Gamma \vdash \Delta, A \vee B}
  • Introduction de la disjonction à gauche :
\frac{\Gamma,A  \vdash \Delta\qquad \Gamma',B \vdash \Delta'}{\Gamma, \Gamma', A \vee B \vdash \Delta,\Delta'}
  • Introduction du faux à droite :
\frac{\Gamma\vdash \Delta}{\Gamma \vdash \Delta, \perp}
  • Introduction du faux à gauche, il a la forme d'un axiome : \quad \perp \ \vdash
  • Coupure :
\frac{\Gamma \vdash \Delta, A\qquad \Gamma',A \vdash \Delta'}{\Gamma, \Gamma'\vdash \Delta,\Delta'}
  • Affaiblissements :
\frac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \qquad \frac{\Gamma \vdash \Delta}{\Gamma \vdash \Delta, A}
  • Contractions
\frac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta}\qquad \frac{\Gamma \vdash \Delta, A, A}{\Gamma \vdash \Delta, A}

Une coupure traduit l'attitude du mathématicien qui démontre un lemme (la proposition A) dont il se sert ailleurs dans la démonstration d'un théorème. Ce lemme peut exprimer quelque chose qui n'a rien à voir avec le théorème principal, d'où le souhait d'éliminer ces lemmes qui sont comme des détours dans la progression vers le résultat principal. Un affaiblissement correspond à l'ajout d'une proposition superflue soit comme antécédent, soit comme conséquent.

Exemples de théorèmes

Nous indiquons ci-dessous une liste de théorèmes qu'on peut démontrer à l'aide des règles précédentes, ainsi que le nom usuel qui leur est attribué par la tradition.

\big(A \rightarrow \; A) identité
A \lor \lnot A tiers exclu
 A \rightarrow \lnot\lnot A double négation
\lnot\lnot A \rightarrow A double négation classique
\big(\big(A \to B\big) \to A\big) \to A loi de Peirce
\lnot(A \land \lnot A) non contradiction
\lnot(A \land B) \leftrightarrow (\lnot A \lor \lnot B) lois de De Morgan
\lnot(A \lor B) \leftrightarrow (\lnot A \land \lnot B)
(A \to B) \to(\lnot B \to \lnot A) contraposition
\big( (A \to B) \land A)\to B modus ponens (propositionnel)
((A \to B) \land \lnot B) \to \lnot A modus tollens (propositionnel)
\big( (A \to B) \land (B \to C)) \to (A \to C) modus barbara (propositionnel)
(A \to B) \to \big((B \to C) \to (A \to C)\big) modus barbara (implicatif)
\big(A \land (B \lor C)) \leftrightarrow ((A \land B) \lor (A \land C)) distributivité
\big(A \lor (B \land C)) \leftrightarrow ((A \lor B) \land (A \lor C))
Commentaires

On aura remarqué que les trois systèmes utilisent le même symbole \vdash , mais en fait cette notation est cohérente. Le format \Gamma \vdash P utilisé pour la déduction naturelle est en fait un séquent dans lequel il n'y a qu'une seule conclusion, on parle alors d'un séquent naturel. Le format \vdash P utilisé pour les théorèmes dans les systèmes à la Hilbert correspond à un séquent naturel où il n'y a pas d'hypothèse.

On peut montrer que ces trois systèmes sont équivalents dans le sens où ils ont exactement les mêmes théorèmes.

L'aspect « classique » du calcul des propositions est obtenu, dans le système à la Hilbert, par l'axiome de contraposition \vdash (\lnot P \to \lnot Q) \to (Q \to P) , il apparaît dans la déduction naturelle à travers la réduction à l'absurde. Le calcul des séquents est classique, mais si l'on se restreint aux séquents avec un seul conséquent, il devient intuitionniste.

Sémantique

    Ce que j'ai appris de la logique, c'est cette dissociation entre vérité et prouvabilité. Alain Connes, in Triangle de pensées Ed. Odile Jacob, (2000).

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, 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 un valeur 0 ou 1 à chaque propositions qui dépend des valeurs prises par les tables de vérité. Il existe trois cas d'interprétation:

  • Quand la proposition prend toujours la valeur 0 quelles que soient les valeurs des variables propositionnelles, la proposition est dite être une antilogie ou une contradiction. On dit également qu'elle est insatisfaisable.
  • Lorsque la proposition A prend toujours la valeur 1, A est une tautologie. On dit aussi que A est valide et on notera cette assertion \vDash A .
  • Si la proposition prend au moins une fois la valeur 1, on dit que l'on peut satisfaire A, ou que A est satisfaisable (ou encore "satisfiable" par mimétisme avec le terme anglais).
  • Si la proposition prend au moins une fois la valeur 1 et au moins une fois la valeur 0, c'est une proposition synthétique ou contingente.

Interprétation des connecteurs

Nous explicitons le comportement, puis donnons la table de vérité associée

  • P \lor Q prendra la valeur 1 si et seulement si au moins l'une des deux propositions P ou Q prend la valeur 1.
P Q P \lor Q
0 0 0
0 1 1
1 0 1
1 1 1
  • P \land Q prendra la valeur 1 si et seulement si les deux propositions P et Q prennent simultanément la valeur 1.
P Q P \land Q
0 0 0
0 1 0
1 0 0
1 1 1
  • P \to Q prendra la valeur 0 si et seulement si P prend la valeur 1 et Q la valeur 0.
P Q P \to Q
0 0 1
0 1 1
1 0 0
1 1 1
  • \lnot P prendra la valeur 1 si et seulement si P prend la valeur 0.
P \lnot P
0 1
1 0
  • P \leftrightarrow Q prendra la valeur 1 si et seulement si P et Q ont la même valeur.
P Q P \leftrightarrow Q
0 0 1
0 1 0
1 0 0
1 1 1
  • \perp prend la valeur 0.

Exemple 1 :

AA) → A est une tautologie.

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

Exemple 2 :

A → (A → ¬A) n'est pas une tautologie.

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

Systèmes complets de connecteurs

Une table de vérité à n entrées définit un connecteur n-aire. Un ensemble de connecteurs propositionnels est dit complet si tout connecteur peut se définir au moyen des connecteurs de l'ensemble. Toute table de vérité se décrit à l'aide de conjonctions de disjonctions et de négation, par exemple on décrit entièrement la table de vérité de l'équivalence ci-dessus par « pq prend la valeur vrai si et seulement si p et q prennent la valeur faux ou p et q prennent la valeur vraie », c'et-à-dire que pq ≡ (¬p ∧ ¬q) ∨ (pq). 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, AB ≡ ¬ (¬A ∧ ¬B), AB ≡ ¬ (¬A ∨ ¬B)). L'ensemble {¬, →} est également complet : AB ≡ ¬AB.

L'ensemble constitué du seul connecteur NON-ET (noté « | » par Henry Sheffer) est également complet, ¬P étant équivalent à P|P et PQ à (P|P) | (Q|Q). Cette particularité est utilisée pour la construction de circuits logiques, une seule porte suffisant alors pour concevoir tous les circuits existants.

Page générée en 0.173 seconde(s) - site hébergé chez Contabo
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
A propos - Informations légales
Version anglaise | Version allemande | Version espagnole | Version portugaise