Grande Encyclopédie Larousse 1971-1976Éd. 1971-1976
C

calcul des propositions (suite)

Axiomatisation

Pour axiomatiser le calcul des propositions nous nous donnerons tout d’abord la liste des signes primitifs répartis en trois catégories :
(1) la suite infinie des lettres p1, p2, ..., pn,..., dites variables de proposition ;
(2) les signes dits foncteurs propositionnels ;
(3) les parenthèses gauche ( et droite ).

Définissons maintenant les expressions bien formées, ou ebf :
(1) une variable de proposition est une ebf ;
(2) si P est une ebf, est une ebf ;
(3) si P et Q sont des ebf, (P ⊃ Q) est une ebf ;
(4) rien n’est une ebf, sinon par (1) à (3).

Nous venons de poser une définition inductive (v. métamathématique) qui permet d’engendrer de proche en proche autant d’ebf que l’on veut.

Exemples. sont des ebf.

Remarquons que les parenthèses servent ici à inscrire à l’intérieur d’une ebf la façon dont elle a été engendrée. Ainsi, ((p1 ⊃ p2) ⊃ p3) et (p1 ⊃ (p2 ⊃ p3)) sont obtenues de deux façons différentes :

La notation polonaise permettrait d’économiser toutes les parenthèses. La première ebf s’écrirait CCp1p2p3 et la seconde Cp1Cp2p3. Dans ce qui suit, et pour alléger les écritures, nous supprimerons la paire extérieure de parenthèses.

Introduisons maintenant la notion de schéma d’ebf et considérons pour cela les deux ebf suivantes :

On voit qu’elles résultent toutes deux d’un même schéma. Si P et Q sont des variables qui prennent leurs valeurs sur l’ensemble des ebf — ce sont des variables syntaxiques ou encore des métavariables —, le schéma
P ⊃ (Q ⊃ P)
permet de retrouver (1) en donnant à P la valeur p1, et à Q la valeur et il permet de retrouver (2) en donnant à P la valeur (p1 ⊃ p3) et à Q la valeur p1.

Cela dit, nous allons poser trois schémas d’ebf qui seront considérés comme des schémas d’axiomes :

Toute assignation d’ebf à P, Q et M dans les schémas A 1 à A 3 engendrera un axiome. En particulier, les expressions (1) et (2) ci-dessus sont des axiomes.

Il ne reste plus qu’à définir la notion de théorème. Pour cela, nous nous donnerons une règle de transformation, ou règle d’inférence :
R À partir de P et de P ⊃ Q, on peut inférer Q. Il s’agit là de la règle du modus ponens.
Nous poserons enfin la définition inductive suivante :
(1) un axiome est un théorème ;
(2) le résultat de l’application de R à des théorèmes est un théorème ;
(3) rien n’est un théorème, sinon par (1) et (2).

Exemple de théorèmes.
Chacune des ebf 1 à 5 qui suivent sont des théorèmes. L’écriture Ax : P/ebf signifie que, dans le schéma d’axiomes Ax, on a donné à P la valeur de l’ebf écrite à droite de la barre oblique.

Les autres foncteurs principaux seront introduits par les définitions suivantes :

Le choix que nous avons fait des foncteurs primitifs et des schémas d’axiomes A 1 à A 3 est dû à Łukasiewicz (1930). D’autres choix sont possibles. Ils exigent éventuellement une reformulation de la classe des ebf et de nouvelles définitions pour les foncteurs non primitifs. Ils utilisent tous, sauf celui de Nicod, la règle R. Voici quelques systèmes.

• Whitehead-Russell (1910).
Foncteurs primitifs :
Définition :
Schémas d’axiomes :

• Hilbert-Ackermann (1928).
Foncteurs primitifs :
Définition :
Schémas d’axiomes :

On voit que le schéma R 5 était superflu.

• Frege (1879).
C’est le premier système axiomatique du calcul des propositions.
Foncteurs primitifs :
Schémas d’axiomes :

• Nicod (1916).
Foncteur primitif : |.
Règle d’inférence : à partir de P | (Q | M) et de P, on peut inférer M. Schéma d’axiomes (nous utilisons des crochets et des accolades pour faciliter la lecture) :

Ici P, P′, Q, M et N désignent des propositions quelconques.

Remarques.

1. Nous avons présenté tous ces systèmes à l’aide de schémas d’axiomes, mais il est aussi possible — et c’est historiquement le cas — de les présenter à l’aide d’axiomes en se donnant une règle de substitution.

Ainsi, on écrirait par exemple l’axiome
a1 ⊩ p ⊃ (q ⊃ p)
et l’on adjoindrait au système la règle :
S Si P est une ebf qui contient la variable de proposition 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 rigoureuse. Cependant, elle est assez lourde et elle offre de plus des difficultés considérables dans la formulation du calcul des prédicats.

2. Les calculs qui précèdent ne contiennent que des variables de propositions, à l’exclusion de toute constante propositionnelle. Il est toutefois possible d’obtenir un calcul des propositions équivalent en introduisant une constante de proposition. C’est, par exemple, ce que fait Church (1956).
Foncteur primitif : ⊃.
Constante de proposition :f.
Définition :
Axiomes :
Règles : R et S.