CALCUL DES PROPOSITIONS

dépend évidemment des règles de déduction qui fixent la notion de démonstration. La deuxième propriété n’exclut pas la possibilité d’étendre un système formel par l’adjonction de nouveaux signes et de nouvelles règles (et axiomes) (1). Le système formel représentant les mathématiques se définit ainsi par paliers successifs, le premier palier coincidant avec le calcul logique des propositions. HEYTING a donné l’exemple d’un système formeldivergent dès le début de la logique classique (?) ; son calcul intuitionniste des propositions comporte deux sortes de signes : les constantes logiques —, V, À, 3 et les propositions élémentaires, a, b, c,.… Une formule complète consiste soit dans une proposition élément, soit dans un assemblage réglé par les constantes logiques (— a, a \ b,etc.). Les axiomes posent les assemblages valables initialement ; deux règles, la règle de substitution et la règle de séparation (si a et 4 3 b sont valabies, b aussi) permettent d’en obtenir d’autres. Des deux propriétés énoncées plus haut, la première seule est établissable, la deuxième n'existe pas : si on ajoute 4 V — a aux axiomes on obtient le calcul ciassique des propositions.

Pour celui-ci la définition la plus brève est celle de LUKA- SIEWICZ-TARSKI (°) : outre les signes propositions éléments (a, b, c}, deux signes fondamentaux — et. Dans les règles de structure posant comme propositions les assemblages a, a+ b, etc., intervient la définition de signes abréviations

aVb pour a+ b ; aNb pour —(a + c — b)

Enfin règles de substitution, de séparation (comme pour HEYTING), et trois axiomes :

(1) BERNAYS a précisé cette notion d'extension d’un formalisme à propos de l’arithmétique formalisée. Cf. HILBERT-BERNAYS (I), p. 354-356.

(2) HEYTING (I), p. 43.

(3) LuxasiEwicz-TARSKI (1).