Une axiomatisation

Nous allons construire un système formel pour la logique des propositions. Le « jeu » consiste à faire comme si l’on ne savait pas de quoi il s’agit, comme si les signes utilisés n’avaient pas de signification. Ce n’est que dans une seconde étape que l’on interprète les signes et l’on est alors en droit de dire que l’on a formalisé la logique des propositions, ou autre chose. Cela dépend de l’interprétation.

La première chose à faire est de se donner un alphabet. Le nôtre contiendra trois catégories de signes :

1) Les lettres $p_{1}$ , $p_{2}$ , … $p_{n}$ ,… . Nous les appellerons des variables de propositions.

Remarque

Cette appellation anticipe sur l’interprétation standard que nous avons en vue. Nous pourrions nous contenter de les appeler des variables, ou même des lettres.

2) Les signes $\sim$ et $\supset$ que nous appellerons des foncteurs.
3) Les signes ( et ) que nous appellerons, comme tout le monde, des parenthèses.

Nous allons définir maintenant une classe qu’on nomme celle des expressions bien formées ou ebf.

1) Une variable est une ebf.
2) Si P est une ebf, $\sim P$ est une ebf.
3) Si $P$ et $Q$ sont des ebf, $(P\supset Q)$ est une ebf.
4) Rien n’est une ebf, sinon par (1) à (3).

Une définition du genre ci-dessus est une définition inductive. Elle comporte trois sortes de clauses :

une ou plusieurs clause(s) initiale(s), ici (1) ;

une ou plusieurs clause(s) inductive(s), ici (2) et (3) ;

une clause terminale, ici (4).

Une telle définition permet d’engendrer de proche en proche autant d’éléments que l’on veut de la classe qu’elle définit. Pour éviter l’usage des indices nous poserons $p$ =df $p_{1}$ , $q$ =df $p_{2}$ et $m$ =df $p_{3}$ .

Exemples

$p$ , $q$ , $\sim p$ , $\left(\sim p\supset q\right)$ , $\left(q\supset\left(\sim p\supset q\right)\right)$ , $\left(p\supset\left(q\supset p\right)\right)$ sont des ebf.

La clause finale a l’air pédant. En fait, elle est d’une importance essentielle. Considérons en effet, la suite de signes $\sim(\supset pq)$ . Elle est exclusivement constituée de signes de notre alphabet. On ne peut toutefois pas l’obtenir en appliquant les clauses (1) à (3). C’est la clause terminale (4) qui nous assure que, en conséquence, il ne s’agit pas d’une ebf.

Remarque

Ceci est général. Quelle que soit la suite donnée de signes de l’alphabet, nous sommes à même de décider, en un nombre fini d’essais, si cette suite est une ebf ou non. On dit que la classe des ebf est une \emph{classe décidable}.

L’écriture des ebf devient rapidement encombrante. Aussi allons-nous convenir de certaines abréviations. Soit l’ebf suivante :

$\sim\left(\sim\sim\left(\left(\sim p\supset q\right)\supset\left(\sim q\supset p\right)\right)\supset\sim\left(\left(\sim q\supset p\right)\supset\left(\sim p\supset q\right)\right)\right)$

Posons : $P\vee Q$ =df $\sim P\supset Q$ .

Il vient :

$\sim\left(\sim\sim\left(\left(p\vee q\right)\supset\left(q\vee p\right)\right)\supset\sim\left(\left(q\vee p\right)\supset\left(p\vee q\right)\right)\right)$

Posons : $P\wedge Q$ =df $\sim(\sim P\vee\sim Q)$ donc $\sim(\sim\sim P\supset\sim Q)$ .

Il vient :

$((p\vee q)\supset(q\vee p))\wedge((q\vee p)\supset(p\vee q))$

Posons : $P\equiv Q$ =df $(P\supset Q)\wedge(Q\supset P)$ .

Il vient :

$((p\vee q)\equiv(q\vee p))$

Convenons enfin de ne pas toujours écrire la paire extérieure de parenthèses ; l’ebf initiale peut s’écrire :

$(p\vee q)\equiv(q\vee p)$

Remarque

Ces jeux d’écriture formels ne réclament aucune réflexion, mais ils exigent beaucoup d’attention. Le lecteur aura intérêt à refaire lui-même les diverses transformations, ne serait-ce que pour s’assurer que le texte ne contient pas de coquilles !

Soit $P$ , $Q$ , $M$ des ebf quelconques. Introduisons les trois expressions suivantes, que nous appellerons des schémas d’axiomes.

(A1) $P\supset(Q\supset P)$
(A2) $(P\supset(Q\supset M))\supset((P\supset Q)(P\supset M))$
(A3) $(\sim P\supset\sim Q)\supset(Q\supset P)$

On obtiendra des axiomes en spécifiant quelles ebf désignent les lettres $P$ , $Q$ et $M$ . A ce propos il faut noter deux choses :

1) Dans un même schéma, la même majuscule doit désigner la même ebf.
2) Mais dans un même schéma, deux majuscules différentes peuvent désigner la même ebf.

Remarque

Ces deux pratiques sont conformes à l’usage algébrique. Soit ainsi l’expression $x+y+x$ . Si l’on attribue une valeur à $x$ , disons 3, il faut écrire $3+y+3$ . Mais rien n’empêche d’attribuer aussi la valeur 3 à $y$ .

Voici quelques axiomes. Nous indiquons par la notation (An) : $P/$ ebf que dans le schéma (An), la variable $P$ désigne : l’ebf qui suit la barre oblique.

$p\supset(q\supset p)$ (Al) : $P/p$ , $Q/q$

$q\supset(q\supset q)$ (Al) : $P/q$ , $Q/q$

$((p\supset q)\supset(m\supset p))\supset(((p\supset q)\supset m)\supset((p\supset q)\supset p))$ (A2) : $P/(p\supset q)$ , $Q/m$ , $M/p$

$(\sim m\supset\sim\sim p)\supset(\sim p\supset m)$ (A3) : $P/m$ , $Q/p$

Il reste enfin à se donner au moins une règle d’inférence.
Nous poserons :

(R1) De $P$ et de $P\supset Q$ , il est loisible d’inférer $Q$ .

Cela dit, la notion de théorème se définit comme suit :

1) Un axiome est un théorème.
2) Toute ebf qui résulte de deux théorèmes par l’application de la règle (R1) est un théorème.
3) Rien n’est un théorème, sinon par (1) et (2).

Exemples

Chacune des cinq ebf suivantes est un théorème.

$\begin{tabular}{clcl} 1. & $p\supset((q\supset p)\supset p)$ & & (\textbf{A1}) : $P/p$, $Q/(q\supset p)$\tabularnewline 2. & $p\supset(q\supset p)$ & & (\textbf{A1}) : $P/p$, $Q/q$\tabularnewline 3. & \multicolumn{3}{l}{$p\supset((q\supset p)\supset p)\supset\left(\left(p\supset(q\supset p)\right)\supset\left(p\supset p\right)\right)$ }\tabularnewline & & & (\textbf{A2}) : $P/p$, $Q/(q\supset p)$, $M/p$\tabularnewline 5. & $\left(p\supset(q\supset p)\right)\supset\left(p\supset p\right)$ & & 1, 3, \textbf{R1}\tabularnewline 6. & $p\supset p$ & & 2, 4, \textbf{R1}\tabularnewline \end{tabular}$

Remarques

1. Si $P$ est un théorème, nous écrirons encore $\vdash P$ .
2. La classe des théorèmes est introduite par une définition inductive, comme celle des ebf. Nous verrons \eqref{sec :-Quelques-propri=0000E9t=0000E9s} qu’elle est aussi décidable. Toutefois ceci exige une démonstration.
3. Au lieu de se donner les schémas d’axiomes (A1 – A3), il serait possible de se donner directement des axiomes. Par exemple :

(a1) $p\supset(q\supset p)$
(a2) $(p\supset(q\supset m))\supset((p\supset q)\supset(q\supset m))$
(a3) $\left(\sim p\supset\sim q\right)\supset\left(q\supset p\right)$

Mais pour obtenir le même ensemble de théorèmes, il faudrait se donner une règle supplémentaire :

Si $P$ est une ebf qui contient la variable $p$ et si $Q$ est une ebf, on peut inférer l’ebf que l’on obtient en substituant $Q$ à chaque mention de $p$ dans $P$ . Cette façon de procéder est assez compliquée et elle exige de grandes précautions dans la logique des prédicats. C’est la raison pour laquelle nous ne l’avons pas adoptée.

Il est aussi possible de déduire des règles dérivées, ce qui est très commode pour la pratique. Convenons que si, à partir des prémisses $P_{1}$ , $P_{2}$ ,… , $P_{n}$ , il est possible d’inférer $Q$ , nous écrirons :

$P_{1}$ , $P_{2}$ ,… , $P_{n}\vdash Q$ .

Nous pourrions ainsi reformuler la règle (R1) de la façon suivante :

$P$ , $P\supset Q\vdash Q$ .

Voici alors une règle dérivée :

$\sim P\supset\sim Q$ , $Q\vdash P$ .

On a en effet :
$\begin{tabular}{clcl} 1. & $\left(\sim P\supset\sim Q\right)\supset\left(Q\supset P\right)$ & & (A3)\tabularnewline 2. & $\sim P\supset\sim Q$ & & Première prémisse\tabularnewline 3. & $Q\supset P$ & & 1, 2, (R1)\tabularnewline 4. & $Q$ & & Seconde prémisse\tabularnewline 5. & $P$ & & 3, 4, (R1)\tabularnewline \end{tabular}$

Un tel calcul n’offre d’intérêt réel qu’une fois interprété. Son interprétation standard est évidente :

&nbsp ; aux variables $P_{1}$ , $P_{2}$ ,… , $P_{n}$ on fait correspondre
des propositions ;
&nbsp ; aux signes $\sim$ et $\supset$ , on fait correspondre respectivement l’opérateur de négation et celui de conditionnel ;
&nbsp ; les parenthèses.jouent le rôle de ponctuation.

Dès lors, si les schémas d’axiomes et la règle d’inférence sont bien choisis, aux théorèmes correspondront des tautologies (V. 1.7).

D’autres interprétations sont toutefois possibles. Nous allons en esquisser une, en interprétant les signes $\wedge$ , $\vee$ et $\sim$ . Supposons que p, q, m, représentent des interrupteurs électriques. Si p est fermé, il laisse donc passer le courant, nous écrivons $p$ . Dans ce cas, à $p\wedge q$ correspond un montage en série (Fig. 4) et à $p\vee q$ correspond un montage en parallèle (Fig. 5).

Nous avons noté $q$ et $p$ les interrupteurs et non leur état.

L’ebf suivante est un théorème du calcul :

$\vdash((p\wedge q)\vee(p\wedge m))\equiv(p\wedge(q\vee m))$

Cela signifie que le montage de la figure 6 peut être remplacé par le montage de la figure 7.

Il est clair que les ordinateurs ne travaillent pas avec des interrupteurs mécaniques. Leurs principes logiques reposent bien toutefois sur une interprétation électrique du système précédent.

Remarque

L’axiomatisation que nous avons proposée est empruntée à Lukasiewicz. Elle n’est pas la seule possible. Ainsi dans leurs Principia Mathematica, Whitehead et Russell sont partis des opérateurs $\sim$ et $\vee$ et Nico du seul opérateur $\mid$ .