DÉFINITIONS D'INDIVIDUS

l'introduction d’une relation nouvelle. Mais c’est une relation où — comme on voit — la négation joue un rôle essentiel : elle ne permet que de démontrer fort peu dans le plan des propositions à variables lorsqu'on a une démonstration pour une certaine individualisation. Cette hétérogénéité entre les 2 espèces de propositions — caractéristique des systèmes formels représentant les mathématiques et origine des difficultés soulevées par les intuitionnistes — n'empêche d’ailleurs pas un enchevêtrement, par l’intervention de propositions à variables dans les définitions d'individus (d’où l'impossibilité d’une solution radicale, comme l’élimination des propositions à variables, à quoi ne peuvent songer les intuitionnistes) (1).

Les définitions d'individus ou de catégories de variables (2) s'effectuent de deux façons différentes : les unes sont de simples abréviations d'écriture ; un signe nouveau remplace une expression dont la catégorie (espèce de variable ou d’individu, type) est bien déterminée (*). L’axiome définition est alors toujours une équivalence et ne représente aucune extension de puissance pour le formalisme : axiome et signe introduits pouvant toujours être éliminés, il n’y a pas de démonstration de non contradiction à présenter pour l’adjonction. Au contraire, les autres définitions mettent en rapport des parties distinctes du formalisme : elles énoncent qu'une certaine expression — réunion originale de signes — peut être représentée par un signe d’une catégorie déjà connue ; tous les modes de raisonnements va-

(1) Cf. HEYTING (IL), p. 57 et 158, les signes de quantité ne sont pas, pour lui, comme on pourrait le croire, de simples abréviations de conjonctions et disjonctions itérées.

(2) On peut, bien entendu, distinguer dans chaque type diverses catégories de variables, caractérisées par des axiomes.

(3) Exemple, définition dans chaque type # de l'individu =

Æn—1 on Yn—1 pr I #n (Xn—:) > Xn (Yn—5) ] Xh (nous mettons ici, pour simplifier, le prédicat-individu —, entre ses 2 arguments).

IIO AXIOME DE RÉDUCTIBILITÉ

lables pour cette catégorie seront donc étendus au système nouveau d'expressions : possibilité de démontrer davantage. On voit alors que la non contradiction avec les axiomes antérieurs n’est plus évidente. Ces définitions — dans le système que nous considérons — peuvent être fondées de façon uniforme par l’axiome-schéma dit de réductibilité :

DR 1 RAA AE AAA Starr à (2)

x X LL n—1 dur LD

(X étant une proposition quelconque — l'expression à remplacer — où ne figurent comme variables /ibres que des variables de type inférieur ou égal à #—1; en revanche, peuvent y paraître des variables liées de type quelconque). L’axiome donne au formalisme son caractère général prédicatif, c’està-dire garantit la possibilité de ramener toute relation à une proposition-élément de type immédiatement supérieur (en langage de théorie des ensembles, toute propriété s'exprime par l’appartenance à un ensemble). En particulier, il autorise les définitions non prédicatives indispensables en mathématique : un individu de type # peut se définir par référence à tous les individus de son type (si dans À apparaît comme variable liée la variable de type »). Il est complété par l’axiomze-schéma d'extension, garantie que les définitions d'individus ou caractérisations de variables sont univoques :

IT JE SN EURE Msn DRE 20 7e À PRE ER NN ES Ty Vpn. (en langage de ia théorie des classes : une classe est déterminée par ses éléments). On peut, lorsqu'il s’agit d’un individu, mettre la définition sous forme explicite (1) grâce à

(1) Une définition est explicite lorsque l’objet (individu) à définir, k, peut être lié à l'expression définissante au moyen d’une égalité. Si Pexpression définissante est X (x), A représentant une architecture logique quelconque où figure la variable x, l’axiome-définition s'écrit :