À 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.
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
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 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
Les systèmes déductifs utilisent des règles de déduction (appelées aussi règles d'inférence) qui s'écrivent:
Les
Il n'y a qu'une seule règle appelée le modus ponens, elle s'écrit:
Elle peut se comprendre ainsi si
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
En outre, il faut une règle qui est la 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 P, on ajoute
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
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.
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é |
![]() |
On aura remarqué que les trois systèmes utilisent le même symbole
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
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:
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'et-à-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) 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 suffisant alors pour concevoir tous les circuits existants.