AL, 8, D, G, À

La formule commune € est dite formule d'intersechon. Le principe de la réduction est d’éliminer les signes logiques en leur donnant leur sens intuitif de façon à obtenir une séquence-conclusion ayant pour formule postérieure, une formule numérique vraie, ou ayant une formule élémentaire fausse postérieure et, parmi les formules antérieures, une élémentaire vraie. Ainsi on remplacera II X (x) par À (2)

: étant quelconque (?) si … X (x) est à l'arrière, au contraire #

convenablement choisi de manière que %X (z:) soit faux si II Y (x) est à l'avant, de même A A 8 par À ou par 8 (arbi-

trairement ou suivant un choix déterminé suivant qu’on est

(1) X, 3, E sont les formules antérieures (en nombre quelconque), 9 la formule postérieure de la séquence. Il est en général possible de transformer une séquence en implication (théorème de déduction. Cf. HILBERT-BERNAYS (l"" p. 155) ; on change alors les virgules en A. Mais il est plus commode d’avoir les virgules: elles sauvegardent aux formules ainsi unies une sorte d’indépendance logique : la réduction peut ne porter que sur l’une d'elles. Dans la forme canonique ne figurent que -, A et II.

(2) D'où l’infinie variété des modalités de réduction signalée plus haut : le sens même de la réduction exige que la substitution soit arbitraire, que la propriété 2 soit atteinte quel que soit le choix — sans quoi la propriété 3 serait perdue. De là viennent toutes les difficultés de la démonstration — et la nécessité de faire appel au transfini.

160 DÉMONSTRATION GENTZEN

à l'avant ou à l'arrière), — Y à l’arrière par 0 = 1, À passant à l'avant, — Y à l’avant par Y à l'arrière. Dans les cas où il faut choisir — réduction portant sur une formule antérieure, — on peut être obligé de laisser subsister la formule initiale (si le choix n’a pas permis de trouver la valeur z rendant Y (2) faux par exemple) : de toute façon le choix doit être déterminé par les précédentes opérations de la démonstration. C’est le théorème de GENTZEN que pour toute démonstration l'opération de réduction à accomplir immédiatement est déterminée de façon univoque par sa structure : si la dernière application de règle d’où procède la conclusion est une généralisation, on supprime la séquence-conclusion et on substitue à la variable portante dans la séquence précédente (et partout où elle apparaît antérieurement) un nombre arbitraire. Si c’est une induction complète on remplace la séquence-conclusion II X (x) par A (2), 2 étant arbi-

traire, et, dans la démonstration, le schéma d’induction par une chaîne d’intersections dont la longueur est déterminée par 2. Si enfin, c’est une intersection la réduction de la conclusion reproduit la réduction de la ou des formules des prémisses qui y figurent. Il peut se présenter une difficulté : lorsque la réduction (déterminée par les démonstrations d’où sont issues les prémisses) porte sur la formule d’intersection (qui ne paraît plus dans la conclusion). On peut bien s'arranger pour avoir une nouvelle démonstration encore valable mais la conclusion est restée la même : rien ne prouve qu'on ait avancé vers le résultat final.

C’est ici qu'intervient la notion de complication d’une démonstration : GENTZEN l’évalue au moyen d’un nombre décimal, le degré, dont caractéristique et mantisse dépendent du nombre des signes logiques figurant dans les séquences initiales et du nombre des règles logiques appliquées au cours de la démonstration. Toute opération de réduction diminue le degré : ainsi, dans le cas précédent, la complication est d'autant moindre que la formule d’inter-

DÉMONSTRATION GENTZEN 161

section comporte moins de signes logiques. Les degrés de complication étant rangés (par ordre de grandeur croissante) en une suite bien ordonnée, on démontre — par induction transfinie — que toute démonstration est réduite au bout d’un nombre fini d'opérations). En effet si toutes les démonstrations, de complication moindre qu’un degré donné, jouissent de la propriété, les démonstrations correspondant à ce degré la possèderont aussi (puisque la première opération de réduction abaïssera leur degré). L'intervention du transfini est rendue nécessaire par l’axiome (ici règle) d’induction totale : une induction totale est de complication immédiatement supérieure à celle de toutes les chaînes d’intersections de longueur arbitraire en lesquelles la réduction la transforme. Si le degré de celles-ci est figuré par des entiers — et non plus des nombres décimaux — on voit qu'il faudra pour celles-là utiliser les w. Toutefois, lorsque l’axiome est élémentaire ou lorsque le nombre des signes de quantité de la formule portante est borné, on peut encore formaliser dans l’arithmétique tous les raisonnements précédents, y compris l’induction finale. Ce n’est que lorsque l’axiome est pris dans toute sa généralité que le transfini est proprement incorporé au raisonnement : on échappe alors bien au critère de GüDEL et si l’on voulait formaliser dans les mathématiques il faudrait utiliser l’analyse. La suite bien ordonnée des degrés de complication a pour type d'ordre le nombre cantorien e, (1).

La méthode n’exige pas que le formalisme examiné soit clos : on peut laisser indéterminés (comme faisait HER- BRAND) les schémas de définition de fonction, ajouter aussi de nouvelles règles de raisonnement ; 1l suffit que les prédicats introduits soient décidables, les fonctions calculables

(x) Le premier nombre ordinal transfini + tel que wf — €. C’est la limite — le type d'ordre — de la suite x

ou) (5 ©, 0 007, où

162 DÉMONSTRATION GENTZEN

en termes finis, enfin que pour chaque règle soit donné en même temps un procédé de réduction. Aïnsi la propriété non décidable isolée par GÔDEL peut être immédiatement réduite : comme elle est de la forme I Y (x), X (2) étant

démontrable pour tout entier , la séquence» 11 X (x) fait

partie des séquences valables de cette théorie des nombres non close. Pour d’autres théories mathématiques où prédicats et fonctions sont décidables ou calculables en termes finis, la méthode s'étend sans modification : ainsi pour la partie constructive de l’analyse. Est-il possible, en considérant dans la classe IT (des ordinaux transfinis) un segment assez long, de dominer grâce à la même induction transfinie un fragment plus considérable de l’analyse classique ? la question est pour l'instant sans réponse. Au moins pour la théorie des nombres avec axiome général d’induction complète, le résultat est-il clair: GENTZEN passe soigneusement au crible les notions, les raisonnements métamathématiques employés. Tous appartiennent à la zone finie sauf la démonstration terminale de la finitude du nombre des opérations de réduction. La mise en ordre des degrés de complication répond à la représentation de l'infini potentiel ; il n’est pas nécessaire d'emprunter la notion générale de bon ordre à la théorie des ensembles : il suffit de considérer la transmission progressive de l’ordre : si tous les degrés, de caractéristique 7, sont déjà rangés, on en déduit (:), par des opérations

(1) Les degrés de caractéristique o sont pris parmi les nombres 0,1 o,I1 0,111... 0,2 ; les degrés de caractéristique 7 + 1 parmi les nombres dont la mantisse est constituée par des mantisses de nombres déjà définis, de caractéristique 7, rangées par grandeur décroissante et séparées chaque fois par PI DIZÉTOS M AÏNSINIDOUTNINON TT ISTIEONEE CIO TIMEALRE NE TSENTOT NI CEC: L'ordre est ainsi obtenu : à tout nombre « de caractéristique 7, correspond un système S («) de nombres de caractéristique 7 + 1 dont l’ordre se déduit de celui de l’ensemble des nombres de caractéristique 7 déjà rangés (en effet il s'obtient en ajoutant à la mantisse de « successivement ces nombres). Enfin les S (a) ont entre eux le même ordre (de grandeur) que les «. On voit que le type d'ordre des nombres de caractéristiques o est w + 1, pour 1: : 2041 = ww, puis2 20 Nate:

DÉMONSTRATION GENTZEN 163

chaque fois finies, la mise en ordre des degrés de caractéristique 7 + 1. Quant au moment décisif, la démonstration de la finitude de la réduction, elle est comme on a vu, immédiate une fois les degrés rangés. Ce qui lui permet de réussir est, comme le remarque GENTZEN lui-même, qu'il n’y a pas pour chaque séquence (comme faisait von NEUMANN) détermination directe d’un procédé de réduction, mais démonstration « de la possibilité d’une telle détermination ». Ainsi seulement peut-on dominer les superpositions de choix libres dont, comme on a vu, certains conditionnent la modalité des réductions ultérieures.

Il ne semble pas que d’autres recherches puissent procurer mieux : le critère de GÔDEL interdit qu’on opère à moindres frais : le mérite de la démonstration de GENTZEX est d’avoir fixé exactement jusqu'où il fallait aller. Sans doute la représentation du segment 0... «, échappe-t-elle à l’intuition. Du moins «ne peut-on refuser une certaine évidence au procédé qui l’engendre ». Il suffit de considérer les petits nombres transfinis : «le sens finitiste précis de leur succession peut dans... une certaine mesure être embrassé d’un coup d'œil... la difficulté vient de ce que dans le cas général... apparaît une trop grande complication d’infinis superposés pour qu’on en ait une représentation déterminée (1) ». Mais entre les cas initiaux et les autres « rien de nouveau n’est apparu ». Aussi bien les intuitionnistes n’ont-ils pas d’objection à présenter : du moment qu'il ne s’agit que d’un segment déterminé de la classe IT (d’où la nécessité de fixer exactement jusqu'où on va) une loi peut le donner ; seule est contradictoire la classe dans sa totalité. Si l’on se refuse même à cette représentation, l'avantage est qu’y soient concentrés tous les doutes sur la validité de la théorie.

(x) GENTZEN (Il), p. 559.

Tel est, semble-t-il, jusqu’à ce qu’un résultat nouveau apparaisse, le maximum de clarté que l’on puisse obtenir sur le problème du fondement. La solution de HILBERT avait le mérite singulier d’indiquer elle-même le critère précis dont dépendait sa validité. « Malgré des recherches intensives et maintes idées de démonstration nul n’est parvenu au but » (1) primitivement visé. C’est qu'ici l’actualisation effective transformait considérations sur les mathématiques en constructions mathématiques : «dans le domaine des réflexions métamathématiques le danger des illusions s’est avéré particulièrement grand » (2). Aucune réflexion philosophique n’a effectivement soupçonné (f), ne pouvait, semble-t-il, soupçonner avant GGDEL l’impossibilité d'étendre des méthodes comme celles d'ACKERMANN et von NEUMANN à la théorie générale des nombres. Au moins pour le formalisme radical tel que le présentait von NEUMANN, le résultat de GÔÜDEL est décisif : si la mathématique reçoit sa validité objective de sa représentation comme système ou collection de systèmes de signes dépourvus de tout autre sens que ceux que leur confèrent règles de structure et règles de déduction, avec l’impossibilité

(1) BERNAYS (VI), p. 210.

(2) Zbid.

(3) FRAENKEL, cependant, dès 1928, exprimait des « doutes sérieux sur le succès de la méthode... pour la démonstration de non contradiction de la théorie générale des ensembles ou même seulement de la théorie classique du continu ». FRAENKEL (V), p. 383.

LE LOGICISME 165

d'une preuve de non contradiction, l'édifice s’écroule : c'est la notion de démonstration formelle qui donnait son unique signification au système et qui n’est plus précisable (puisqu'on ne peut prouver que tout n’est pas démontrable dans un système formel). Il ne saurait d’ailleurs être ici question d’une extension de la zone finie métamathématique : puisqu'il faut définir les mathématiques, la zone préalable ne doit comporter que des démarches intuitives expérimentaies — cest-à-dire rigoureusement finies — comme celles dont usait von NEUMANN. L’induction transfinie même réduite de GENTZEN n’est en aucune façon expérimentale : elle appartient déjà aux mathématiques. Ainsi les deux autres solutions au problème du fondement, logicisme et intuitionnisme, semblent avantagées par le résultat même des travaux de l’école de HILBERT. Pour le logicisme, tel qu’il était exposé dans le Cercle de Vienne jusque vers 1929 (date à laquelle GÜDEL communiqua sa démonstration) d’une part les symboles formels sont pourvus d’un sens qui justifie leur usage, au lieu d’en découler, d'autre part la notion de tautologie reprise de RuSs- SELL, et précisée, détermine la validité inconditionnée de la logique, et par suite des mathématiques qui en sont une partie : les démonstrations de non contradiction ne sont que confirmation, non fondement. Tout signe logique est la représentation d’une notion intuitivement claire et « pour tout signe mathématique il y a un ou plusieurs sens purement logiques » (1). Quant aux tautologies, elles représentent les transformations purement combinatoires des propositions : un énoncé tautologique affirme l’équivalence de deux expressions qui — le sens des signes manifesté — s'avèrent identiques à la forme de la combinaison près. Dans le calcul des propositions la théorie des fonctions de

(1) CARNAP (II), p. 143.

J, CAVAILLÈS 11

166 LE LOGICISME

vérité donnait, pour WITTGENSTEIN (1), le type même des enchaïînements logiques. D'où i’extension du tautologique à tout énoncé qui résulte uniquement des lois logiques, celles-ci étant pourvues comme chez FREGE et RUSSELL d’une évidence immédiate. La théorie de la langue, comme image du monde, vient enfin donner au tautologique son sens négatif (2) : les propositions logiques puisque syntaxiques n’ont pas de contenu (empirique), elles ne nous apprennent rien sur les faits (°).

… À cette définition un peu brève de la logique, les travaux de CARNAP sont venus apporter élargissements et complications nécessités par le développement même de la technique formaliste. La relation de consécution cesse d’être univoque : on peut la définir arbitrairement par l'énoncé des règles de structure et de déduction. Chaque détermination engendre une syntaxe particulière : la logique n’est plus la syntaxe d’une langue, mais le système de toutes les syntaxes possibles. La non saturation de l’arithmétique et des théories qui l’englobent ne les exclut donc pas de la logique : « tout concept mathématique peut être défini dans un système approprié et toute proposition mathématique peut être décidée dans un système approprié. Mais il n’y a pas un système unique qui contienne tous les concepts mathématiques et les démonstrations de toutes les propositions mathématiques valables. La mathématique exige une suite infinie de langues toujours plus riches » (4). Il peut v avoir d’ailleurs juxtaposition : ainsi CARNAP envi-

(1) Nous résumons quelques thèses essentielles de WITTGENSTEIN ©# CAVAILLÈS (1), p. 137-141. On trouvera un exposé français des discussions à l’intérieur du Cercle de Vienne et entre lui et les groupes voisins in A. LAUT- MAN (I).

(2) Pour le 28 et le 3€ sens « qui ne correspondent pas à l'usage ordinaire » CARNAP emploie le mot analytique. CARNAP (III), p. 30.

(3) WITTGENSTEIN (I) proposition 5.43 : « Toutes les propositions de la logique disent la même chose, c’est-à-dire rien ».

(4) CARNAP (III), p. 165.

LE LOGICISME 167

sage des relations de consécution infinie (une proposition est conséquence d’une classe infinie d’autres propositions), comme la dernière règle de HILBERT. C'est le principe de tolérance de la syntaxe ; on ne doit pas se demander : telle règle ou tels signes sont-ils admissibles ? mais : comment voulons-nous bâtir une langue déterminée ? —— Mais cette tolérance ne risque-t-elle pas de détruire les thèses essentielles du logicisme ? D'abord l'évidence logique disparaît, ou du moins est repoussée des fondements (départ axiomatique) à l’enchaînement des procédés par lesquels est tirée de ces fondements la structure d’une syntaxe. Ici — deuxième conséquence — se produit un curieux renversement : ces enchaînements sont d'ordre mathématique. La logique devient une partie des mathématiques. La traduction de GôDEL — que CARNAP utilise pour définir deux exemples de langues (les langues I et IT) — l’imposait. « 11 n’y a pas de propositions particulières de la logique de la science. Les propositions de la syntaxe sont, partie, des propositions de l’arithmétique, partie, des propositions de la physique [dans la mesure où la syntaxe est descriptive c’est-à-dire étudie des discours effectivement donnés dans l’espace et le temps] qui ne sont appelées propositions syntaxiques que parce qu'’eiles sont rapportées à des configurations linguistiques ou à leur structure formelle » (1). « La syntaxe pure [ou logique] est... une partie de l’arithmétique » (2). Sur ce point le hilbertisme triomphe : d’une part la formalisation des mathématiques ne peut s'effectuer par traduction dans la logique mais par reconstruction simultanée des deux disciplines. D'autre part cette reconstruction doit être rigoureusement formelle, au sens hilbertien, «c’est-à-dire sans rapport avec le sens des signes. il suffit de fixer la validité de certaines propositions et les relations

(1) Zbid., p. 210.

108 LE LOGICISME

de consécution, on n’a pas à poser... de question qui dépasse la structure formelle du système » (°).

Le formalisme strict n’est pourtant pas adopté par là : contre lui le logicisme transformé garde une objection décisive : il est incapable de rendre compte de l’application des mathématiques à la physique. Qu’ont à faire les jeux non contradictoires de symboles avec les phénomènes du monde ? « On ne voit absolument pas la raison, écrivait FRAENKEL en 1928, pourquoi les lois de l’arithmétique formelle correspondent exactement aux expériences de l’enfant devant son boulier » (?). Il n’y a pas de passage entre le. proposition : dans cette salle il y a maintenant Pierre et Jacques et eux seuls, et la proposition : dans cette salle il y a maintenant deux personnes. La définition du nombre 2 telle que la donnait FREGE le permettait. « On ne donnera un fondement logique aux mathématiques qu’en construisant un système qui rende possibles de telles déductions » () Telle est la tâche qui déborde l’entreprise formaliste, et que l’école logiciste reconnaît comme sienne : rempiacer la métamathématique ou « syntaxe de la mathématique par une syntaxe de la langue totale qui unit propositions logicomathématiques et propositions synthétiques » (#). Mais d'une part on ne voit pas comment, ayant renoncé à distinguer logique et mathématique, donc ne possédant — comme la syntaxe de FREGE — aucune base de référence préalable aux mathématiques, cette syntaxe pourra « contenir des déterminations formelles générales sur l’apparition des signes mathématiques dans les propositions synthétiques descriptives, et des relations de consécution pour ces propositions » (#). À moins de supposer déjà une partie non précisée — ni peut-être précisable, à la différence du ior-

(2) FRAENKEL (V), p. 383.

(3) CARNAP (III), p. 254.

L'INTUITIONNISME 169

malisme qui ne supposait que l’arithmétique finie — des mathématiques, elle ne peut guère que codifier ce qui a été effectivement réalisé dans les écrits des physiciens, à quelques simplifications et unifications près : rien n’engage pour une nouvelle théorie physique. Quel que soit l'intérêt propre des ingénieuses esquisses de CARNAP à ce sujet, il semble qu'elles l’entraïnent plutôt vers une sorte de philologie scientifique que vers un fondement logique — donc différent d’une simple constatation — de l’application des mathématiques à la réalité. D’autre part elles font intervenir la «langue totale », surprenant retour à WITTGENSTEIN. Il ne peut s’agir d’une langue générale, schéma commun à toutes les langues : dans l’esquisse de la syntaxe générale (1) il n’y a que des cadres vides. C’est bien une sorte de réceptacle pour toutes les langues qui est visé, nécessairement puisqu'aucune langue ne peut contenir toutes les mathématiques, illégitimement puisque n'étant pas une langue il ne saurait être l’objet de recherches syntaxiques. Du logicisme ainsi compris — et guidé par le même réalisme caché qui pour FREGE et RUSSELL posait un en soi de l’univers — aucune solution au problème du fondement ne peut être attendue.

Resterait donc seulement l’intuitionnisme. On a vu d’ailleurs son rôle dans les démonstrations de non contradiction. Elles revenaient — sauf celles d’'ACKERMANN et von NEUMANN — à donner un moyen de coordonner une interprétation intuitionniste aux propositions valables. La méthode des champs — tirée du théorème d'HERBRAND — n’est que construction intuitionniste d’un modèle satisfaisant aux axiomes. Pour la démonstration GENTZEN le caractère est particulièrement net : « la partie essentielle

de ma démonstration... consiste en ceci qu’un sens f?n1tiste [c’est-à-dire acceptable par l’intuitionnisme] est coor-

(1) Etudiée in CARNAP (III), p. 106-202.