ICONE

donc dire qu’en 1926 les problèmes de la logique mathématique se posaient encore dans les mêmes termes que les discussions du début du siècle, relatives à l'existence dutransfini. Fidèle en cela à ses origines leibniziennes, le formalisme considérait toujours que le passage de l’essence à l'existence devait consister uniquement dans la démonstration de la «compossibilité » des essences, de la non-contradiction des axiomes qui les définissent.

C’est précisément dans les recherches de la période critique relatives à la non-contradiction de l’arithmétique, qu’il nous semble voir s'affirmer une théorie des rapports de l’essence et de l’existence aussi différente du logicisme des formalistes que du constructivisme intuitioniste. Nous allons tout d’abord rappeler les traits principaux de cette évolution interne de la logique et essaierons ensuite d’en dégager une philosophie des genèses mathématiques, dont la portée dépasse de beaucoup le domaine de la logique. L'ouvrage considérable que M. BERNAYS a écrit sur la logique hilbertienne est à cet égard pour nous une source d’une inépuisable richesse (1).

Nous avons déjà indiqué p. 11, comment HILBERT avait conçu la nécessité d’une métamathématique dont l’objet serait de démontrer la non-contradiction et l’achèvement des systèmes d’axiomes:de la mathématique formalisée. Les recherches de métamathématique ont été entreprises à deux points de vue différents, et la liaison des deux méthodes est à nos yeux un fait essentiel : l’une de ces méthodes emploie les procédés extensifs de la théorie des ensembles, l’autre, plus conforme aux directives données par HILBERT. luimême constitue ce qu'HILBERTr appelle la « théorie de la démonstration » (2). Du point de vue de la théorie de la

(1) Voir pour toute cette partie D. HILBERT und P. BERNAYS, Grundlagen der Mathematik, ainsi que Paul BERNAYS, Hiülberts Untersuchungen über die Grundlagen der Arithmetik, dans HILBERT, Gesamm. Abh., t. III, p. 196 sqq.

(2) Nous traduirons « beweistheoretische Methode » par méthode structurale et « mengentheoretische Methode » par méthode extensive.

ER

démonstration, une théorie mathématique contient, comme actuellement donné avec le système d’axiomes initiaux, l’ensemble des propositions qui peuvent être obtenues à partir de ces axiomes par application des règles de substitutionet

ts S de passage, ainsi que du « schéma concluant » : S F LS

Dans ces conditions, démontrer la non-contradiction d’un système d’axiomes revient à démontrer la compatibilité de l’ensemble de ses conséquences ; c’est obtenir la certitude qu’il n’est pas possible de rencontrer dans cet ensemble la proposition contradictoire : p.92 (p et non p). De même le système est dit achevé si toute proposition de la théorie est soit démontrable, soit réfutable (par la démonstration de sa négation), c'est-à-dire si l’on sait toujours laquelle des deux propositions p ou p est démontrable. On appelle les propriétés de « non-contradictoire » et d’ « achevé » pour un système d’axiomes, de « démontrable », « réfutable », « irréfutable » pour les propositions d’une théorie, des propriétés structurales (1) parce que leur attribution à un système ou à une proposition exige une étude interne de l’ensemble des conséquences du système considéré.

Nous allons définir maintenant la deuxième méthode d'étude métamathématique d’une théorie formalisée, la méthode « extensive », celle qui adjoint aux systèmes d’axiomes étudiés, la considération des champs d'individus susceptibles de servir de valeursaux arguments desfonctions logiques d’une formule de la théorie. Il existe certaines notions métamathématiques qui ne peuvent être définies que dans la méthode extensive ; les principales sont celles de «valabilité universelle » (Allgemeingültigkeit), et de « possibilité de réalisation» (Erfüllbarkeit) (2). Une formule est dite universellement valable si, quelle que soit la manière dont

(1) Cf. R. CARNAP, Die logische Syntax der Sprache; passim. (2) D. HizBERT und P. BERNAYS, 0p. CID AC ReLA20:

Me tu

on y substitue des prédicats aux variables représentant des fonctions logiques et quel que soit le champ d'individus substitués aux variables arguments, on obtient toujours une proposition vraie ; une formule est dite réalisable s’il existe au moins un champ d'individus et un mode de pareilles substitutions capables de faire de la formule une proposition vraie. Ainsi par exemple la formule :

(x)P(x, x) > (x)(Ey)P(x,y)

est universellement valable. Quels que soient la relation P et le champ considéré, pour tout x de ce champ tel que la relation P ait lieu de cet objet à cet objet, il y a toujours au moins un objet y tel que la relation P ait lieu de l’objet x à l’obiet y, ce dernier pouvant n'être autre que x lui-même. Par contre soit le système des trois axiomes suivants (1) :

GRG, 2) (O0) Rx, D & R(y, 2) + R (x, 2) G)(Ey) Rx, 9).

Supposons que À signifie « être plus petit que » ; le premier axiome exige que la relation de « plus petit » n'ait pas lieu d’un individu à cet individu lui-même, le deuxième qu’elle soit transitive, le troisième qu'il y ait toujours pour tout x au moins un y tel que x < y. Il est impossible de vérifier ce système dans un champ fini, car le troisième axiome ne peut y être vérifié, le dernier nombre d’une collection finie n’étant plus petit qu'aucun nombre. Le système n’est donc réalisable que dans un champ infini. Les propriétés de valabilité universelle et de possibilité de réalisation sont en dualité : une proposition n’est universellement valable que si sa négation n’est pas réalisable et en supposant admis le tiers exclu, une formule n'est réalisable que si sa négation n’est pas universellement valable.

(1) HILBERT und BERNAYS, op. cit., D. 4.

Dre pe

La conception structurale et la conception extensive étant ainsi définies, nous allons maintenant exposer l’importance du passage que la logique mathématique moderne opère de l’une à l’autre,

Considérons tout d’abord les liens qui existent entre la notion structurale de non-contradiction et la notion extensive de « réalisation dans un champ donné ». Lorsque le champ donné ne contient qu’un nombre fini d'individus, on peut, en essayant toutes les combinaisons possibles, trancher la question (entscheiden) de savoir s’il existe un choix de valeurs des variables permettant de vérifier la proposition obtenue par la conjonction de tous les axiomes du système proposé. On dit aiors que ce choix réalise le système d’axiomes et l’on démontre facilement en s’appuyant sur le principe du tiers exclu dans le fini, que si une conjonction d’axiomes est ainsi réalisable, sa négation n’est pas démontrable. Cette dernière propriété n’est autre que la non-contradiction du système. Il y a donc équivalence dans le fini entre la séyucture non-contradictoire d’un système d’axiomes et l'existence d’un champ comprenant un nombre d’individus déterminé et tel que le système soit réalisable dans ce champ (x). Ce résultat si simple qu'il en paraît presque évident contient en germe toute une théorie nouvelle des rapports de l’essence et de l’existence. Ces deux notions cessent en effet d’être relatives aux mêmes êtres mathématiques. Il ne s’agit plus de savoir si la définition entraîne l'existence, mais de chercher si la structure d’un système d’axiomes peut donner naissance à un champ d'individus qui soutiennent entre eux les relations définies par les axiomes. L’essence envisagée est bien celle du système d’axiomes, mais ce dont l’étude interne de ce système permet d'affirmer l'existence, ce sont les «interprétations » du système, les champs où ils se réalisent.

(1) HizBERT und BERNAYS, 0p. cit., P. 17.

LEE EE Rte

Lorsque le système d’axiomes ne pourrait être réalisé que dans un champ infini d'individus, il n’y a plus forcément équivalence entre la non-contradiction du système et l’existence d’une interprétation de ce système. Le principe du tiers exclu ne s'applique pas nécessairement sous la forme étroite qu'il prend dans le cas de champs finis et la conjonction des axiomes d’un système peut être irréfutable, donc le système non-contradictoire, sans qu’il existe en fait une interprétation des axiomes du système. En somme, la possibilité de réalisation est une exigence plus forte que la noncontradiction ; une dissociation s'établit entre le point de vue extensif et le point de vue structural ; le problème de la réalisation doit laisser place, pour M. BERNAYS, à une recherche purement interne de l’irréfutabilité. C’est ce que M.BER- NAYS appelle la conception négative de la non-contradiction. M. BERNAYS a en ce sens démontré (1) que pour le calcul des prédicats 1l y avait rigoureusement équivalence entre la non-contradiction et l’irréfutabilité de la conjonction des axiomes, sans que cela implique le moins du monde l'existence d’une interprétation du système.

Les faits montrent qu'il est néanmoins difficile de développer une théorie purement structurale de la non-contradiction. À cet égard la tentative la plus authentiquement structurale de démonstration de non-contradiction de l’arithmétique est celle de M. GENTZEN (2). Nous ne nous proposons pas de l’exposer ici en détail, renvoyant pour cela à la thèse de M. CAVAILLÈS; nous voudrions seulement en rappeler un élément essentiel. Loin de chercher comme dans les méthodes extensives à réaliser les axiomes de l’arithmétique, M. GENTZEN reste fidèle à la conception de la théorie de la démonstration d'HILBERT et se propose de suivre chacune

(1) HILBERT und BERNAYS, 0. cit, p. 156.

(2) G. GENTZEN, Die Widerspruchsfreiheit der veinen Zahlentheorie. Math. Ann., t. II2, P. 493 sqq.

des opérations qui interviennent dans une démonstration, pour démontrer qu’à aucun moment n’a pu se glisser une proposition contradictoire quelconque. M. GENTZEN entreprend pour cela, comme l'avait du reste déjà essayé HER- BRAND, de réduire chacune des opérations d’une démonstration à des opérations de plus en plus simples jusqu’à ce que la formule finale de la démonstration ait été mise sous la forme d’une expression évidemment vraie. Pour cela, M. GENTZEN coordonne à chaque démonstration un nombre ordinal et démontre un théorème essentiel qui revient à peu près à ceci : les réductions aboutissent parce que l’ensemble de ces nombres ordinaux est « bien ordonné » au sens de la théorie des ensembles. La démonstration ne repose donc pas sur l'existence d’une interprétation du système, elle n’en recourt pas moins à la considération d’un ensemble de nombres dont l’existence est équivalente à l’achèvement de la démonstration de non-contradiction. Quelles qu’aient été les intentions de l’auteur, le point de vue extensif reparaît associé au point de vue structural. La structure d’une théorie s'exprime de nouveau par l'existence d’autres êtres que celle des éléments de la théorie.

Ces considérations s'imposent de facon encore plus manifeste quant on passe de l’étude de la non-contradiction à celle de l'achèvement d’un système d’axiomes. Au sens purement structural d'HILBERT, l’achèvement d’un système est équivalent au fait que toute formule de la théorie possède, avons-nous vu, soit la propriété de démontrable, soit la propriété de réfutable. En ce qui concerne le calcul des prédicats, M. GôDEL a démontré (r) un théorème d'achèvement qui a immédiatement des répercussions extensives. Il a en effet établi que toute formule du calcul des prédicats est soit réfutable, soit réalisable dans le domaine des nom-

(1) K. Gôperz, Die Vollständigheit der Axiome des logischen Funktionenkalküls. Monatsh. für Math. und Physik, t. 37.