Akademik

INTUITIONNISME

Rien a priori de plus opposé au formalisme (cf. théorie de la DÉMONSTRATION; nous supposons que les deux premières parties de cet article sont familières au lecteur) que l’intuitionnisme . Alors que Hilbert met l’accent sur le côté mécanique des mathématiques, Brouwer, le père de l’intuitionnisme, insiste sur la subjectivité du mathématicien. Alors que, pour Hilbert, l’intuition n’est qu’une manière de compenser l’infériorité du mathématicien réel par rapport au robot, elle devient pour Brouwer la signification ultime de l’acte mathématique: l’intuitionnisme est solipsiste. Le programme de Hilbert laissait la place, de manière très limitée il est vrai, à un réel extérieur au mathématicien (objets réels, énoncés élémentaires...), tandis que, pour Brouwer et son école, il n’y a pas de réalité extérieure au mathématicien (le «sujet créatif») dont celui-ci rendrait compte. On voit donc que, pour l’intuitionniste, il n’est jamais question de vérité , mais seulement de prouvabilité : une propriété ne saurait avoir de sens qu’à travers l’acte qui consiste à la démontrer. Enfin, si l’ontologie hilbertienne était très pauvre, Brouwer accorde une signification à des assemblages très complexes de symboles logiques; par contre, cette signification est très éloignée de la tradition...

L’intuitionnisme se présente actuellement comme une chapelle (localisée pour l’essentiel en Hollande), soucieuse de garder la pureté de l’héritage brouwerien et, pour cette raison, fermée aux influences extérieures et peu accueillante au néophyte. Alors que l’idéologie simpliste de Hilbert règne toujours sur les meilleurs mathématiciens, l’intuitionnisme n’a jamais eu la diffusion qu’il mérite: il faudrait, pour cela, abandonner un certain nombre d’extravagances de Brouwer (la théorie du sujet créatif par exemple), et tout repenser dans une perspective plus ouverte. C’est en partant de cette donnée fondamentale que nous avons conçu cet article: au lieu d’exposer d’abord le «dogme» (ce qui ne pourrait que provoquer des réactions de rejet), nous nous attacherons d’abord à des aspects externes de l’intuitionnisme, qui ne supposent pas d’adhésion profonde, et c’est seulement ensuite que le lecteur pourra, s’il le veut, aborder le sujet d’un point de vue interne.

1. L’intuitionnisme vu du dehors

Un exemple

Depuis la fin du siècle dernier, de nombreuses voix se sont élevées pour refuser, ou du moins critiquer, l’utilisation des méthodes abstraites, cantoriennes, dans les mathématiques. Kronecker refusait d’admettre d’autre infini que potentiel; quant à Borel, il mettait l’accent sur la calculabilité et la définissabilité (cf. KRONECKER, BOREL). Prenons un exemple tiré des mathématiques du XX^e siècle, le théorème de Siegel:

où CM (k , 﨑) est l’énoncé qui dit que 﨑 est un caractère réel non principal modulo k ; la fonction L est définie dans l’article théorie des NOMBRES.

Ce résultat célèbre est obtenu par une démonstration par l’absurde: supposons qu’il n’y ait aucun c 礪 0 tel que..., alors contradiction. Cette démonstration ne donne en particulier, en fonction de n , aucun procédé pour calculer le rationnel c . Sans faire siennes les critiques tendant à nier la réalité d’un tel rationnel qui n’est pas effectivement calculable, on est bien obligé de constater que cela serait un grand progrès si on savait calculer c en fonction de n de manière explicite! Il importe donc de distinguer entre:

– l’existence effective (par exemple, si on savait que c = 1/n !);

– l’existence non effective, comme dans le cas qui se présente.

Les livres de mathématiques courantes rendent la distinction par des périphrases: «La constante c est non effective...» Par contre, la distinction n’a pas de sens formel: en logique classique, soit c existe, soit il n’existe pas, c’est tout. Évidemment, on imagine aisément que, dans une logique où cette distinction s’exprimerait simplement, il suffirait de lire le résultat mathématique obtenu pour voir si il est effectif ou non. Précisément, la logique formelle intuitionniste (calcul des prédicats de Heyting; Heyting fut le principal disciple de L. Brouwer) répond à la question. Dans cette logique, 囹囹 A ne vaut pas A, et 囹囹 說n A[n ] est plus faible que 說n A[n ]. Le théorème de Siegel peut s’y démontrer, mais sous la forme:

alors que la formulation originelle donnée plus haut n’est pas (sur la base de nos connaissances actuelles) démontrable dans ce calcul.

Nous avons donc typiquement une logique plus fine que la logique classique, apte donc à rendre des nuances, qui ont par ailleurs un sens mathématique indéniable. (Par contre les logiques modales rendent encore plus de nuances, mais elles n’ont pas de contenu mathématique.)

La sémantique

Pour se familiariser avec la logique intuitionniste, il n’y a rien de mieux que d’utiliser son interprétation sémantique: cette interprétation se fait dans les mathématiques classiques au moyen d’une notion de modèle (modèles de Kripke, etc.); nous choisirons les modèles topologiques qui sont plus parlants: si, dans la définition de structure pour un langage, on change l’espace des valeurs de vérité deO, 1 en l’espace des ouverts d’un espace topologique X, on obtient alors une notion de modèle topologique. Les opérations &, V, 轢, 囹, 葉, 說 sont interprétées par A 惡 B, A 聆B , 璉A 聆 B, 璉 A, i 惡 Aⁱ , i 聆 Aⁱ . Le lecteur vérifiera facilement l’existence de modèles topologiques dans lesquels A 鈴囹 A, 囹囹 AA, 囹 葉 x A說x 囹 A, 葉x 囹囹A 囹囹葉x A... ne prennent pas la valeur X, c’est-à-dire ne sont pas valides...

Calcul LJ

Le calcul des prédicats intuitionniste est, par définition, le système de déduction complet par rapport aux modèles topologiques; il existe de nombreuses formulations possibles, comme pour le cas classique. Retenons le calcul LJ de Gentzen, obtenu en restreignant LK aux séquents de la forme 臨 料 ou 臨 料 A – mais on admet la règle:

Déduction naturelle

Une formulation concurrente est la déduction naturelle (inventée par G. Gentzen, mais développée par Prawitz). Les déductions y sont des arbres finis dont les nœuds sont occupés par des formules; la formule la plus basse de l’arbre est la conclusion , alors que les hypothèses sont certaines formules apparaissant dans les sommets de l’arbre. Les clauses de formation sont les suivantes:

– l’arbre consistant de la formule A toute seule est une déduction (une hypothèse: A, une conclusion: A);

– règles du &: à partir de déductions:

on peut former la déduction:

les hypothèses sont celles des déductions respectivement notées:

quant à la conclusion, c’est bien sûr A & B; de manière similaire, nous avons les règles:

– règles du 轢:

dans la règle (face=F0019 轢I), un certain nombre d’hypothèses de la déduction:

ont été «déchargées»; autrement dit, elles ne sont plus hypothèses de la nouvelle déduction; cela est indiqué au moyen des crochets [A].

– règles du 鈴:

– règles du 葉:

dans (face=F0019 葉I), x ne doit être libre dans aucune des hypothèses de:

dans (face=F0019 葉E), t est un terme arbitraire.

– règles du 說:

dans (face=F0019 說I), t est un terme arbitraire, alors que, dans (face=F0019 說E), on demande que x ne soit libre ni dans C, ni dans aucune hypothèse de:

autre que les A [x ] déchargés par l’application de la règle.

En général, on n’utilise pas la négation; on introduit un symbole 旅 pour l’absurdité, ainsi que la règle:

et on abrège A旅 en 囹A. (Contrairement au cas classique, les connecteurs et quantificateurs &, 鈴, 轢, 囹, 葉, 說 sont tous indépendants les uns des autres; tout au plus, peut-on exprimer 囹 en fonction deet 旅!)

Il est facile de voir que ce calcul est, en fait, équivalent au calcul des séquents: la démonstrabilité de A¹, ..., Aⁿ |B équivalant à l’existence d’une déduction:

de B sous les seules hypothèses A¹, ..., Aⁿ .

Coupures

La déduction naturelle présente l’avantage (douteux) de ne pas contenir de règle de coupure; ce qu’on appelle coupure ici est donc la succession de deux règles (une règle I, introduction , puis une règle E, élimination ); les possibilités sont les suivantes:

Les coupures sur le & sont remplacées par:

suivant le cas; la coupure sur leest remplacée par:

celles sur le 鈴 deviennent:

suivant le cas; enfin, les coupures sur 葉 et 說 deviennent respectivement:

Ce procédé de remplacement des coupures s’appelle normalisation ; on démontre le théorème de normalisation forte (Prawitz, 1965):

Si on applique le procédé de normalisation juste décrit, on finit toujours par obtenir une déduction normale (sans coupures). De plus, le résultat est indépendant de l’ordre d’application des étapes de normalisation.

Ce résultat est pleinement satisfaisant pour le fragment 葉, 轢, &, qui n’est, hélas! pas typique du calcul intuitionniste; dans ce fragment, nous avons une propriété de sous-formule: toute formule d’une démonstration normale est sous-formule au sens de Gentzen, soit de la conclusion, soit d’une des hypothèses. Malheureusement, cela ne subsiste pour le calcul entier qu’au prix d’une complication de la notion de coupure (introduction de coupures «commutatives»). La déduction naturelle n’est donc pas un système de déduction idéal pour la logique intuitionniste, et c’est pourquoi de nombreux auteurs préfèrent travailler dans le calcul des séquents LJ, qui a cependant l’inconvénient d’être plus lourd et de ne pas permettre les formulations du genre «normalisation» (si on élimine les coupures dans LJ, le résultat dépend de l’ordre dans lequel nous avons procédé).

Théorème (corollaire du Hauptsatz de Gentzen, pour LJ; c’est aussi une conséquence du théorème de Prawitz):

(I) Si 說x A [x ] est démontrable dans le calcul des prédicats intuitionniste, alors, pour un certain terme t , A [t ] est démontrable.

(II) Si A v B est démontrable dans le calcul des prédicats intuitionniste, alors soit A est démontrable, soit B l’est.

Ce résultat important n’a aucun analogue dans le cas classique; ce qui illustre bien la spécificité de la logique intuitionniste. (Au passage, mentionnons que le théorème ci-dessus persiste pour de nombreux systèmes formels intuitionnistes; par exemple (I) et (II) restent vrais dans l’arithmétique de Heyting HA, c’est-à-dire l’arithmétique de Peano PA dans un contexte intuitionniste, pourvu que l’on ne considère que des énoncés clos.)

Relations avec la logique classique

Il importe, cependant, de ne pas surestimer le fossé entre les logiques classique et intuitionniste; en effet, Gödel a observé que l’on peut traduire la logique classique dans la logique intuitionniste: si A est un énoncé, soit A le résultat de l’insertion dans A de doubles négations devant tous les énoncés atomiques, les disjonctions et les existences; par exemple:

Théorème (Gödel, 1932): A est démontrable classiquement si et seulement si A l’est intuitionnistiquement.

Un résultat dans la même pensée est la remarque que HA et PA ont les mêmes théorèmes de forme logique 刺⁰², c’est-à-dire 葉x 說y f (x , y ) = 0, f fonction récursive primitive. En particulier, une démonstration de cohérence dans HA n’a pas plus de valeur que dans PA (puisque les formules de cohérence sont 刺⁰¹, et a fortiori 刺⁰²!). Cette remarque vaut pour le théorème de Dirichlet (L (1, 﨑) 0) qui est de forme 刺⁰²; par contre, le théorème de Siegel, de forme 刺⁰³, a un statut différent dans les deux arithmétiques. Ce résultat sur les énoncés 刺⁰² sert de base théorique pour la question d’extraction de bornes effectives: à partir d’une démonstration classique de A, supposé 刺⁰², on en déduit une démonstration intuitionniste, qui nous donne en principe (techniquement, en utilisant éventuellement des procédés de normalisation), y tel que f (x , y ), en fonction de x . Plus précisément, on substitue une valeur effective 異 dans le résultat 葉x 說y f (x , y ) = 0, soit 說y f ( 異 , y ) = 0, puis on cherche un terme t tel que f ( 異 , t ) = 0 soit démontrable; la recherche de t se fait par normalisation en déduction naturelle, ou élimination des coupures dans LJ. On voit ici les frères ennemis, le formalisme et l’intuitionnisme, se réconcilier au niveau technique (cependant, les techniques récentes de théorie de la démonstration rendent superflu le détour via l’intuitionnisme). Il est important de noter que ces procédés d’extraction de bornes ne sont que théoriques, car ils utilisent des algorithmes (élimination des coupures) impratiquables sur ordinateurs...

Le constructivisme

De manière générale, le constructivisme (c’est-à-dire l’approche effective, calculatoire, aux mathématiques, indépendamment de toute considération idéologique) utilise largement la logique intuitionniste.

1. L’école constructiviste soviétique part du principe «tout est récursif»; par exemple, on fait de l’analyse en se restreignant aux seuls réels récursifs (il y a ici aussi un a priori idéologique, mais différent de l’intuitionnisme: au lieu d’exalter l’«âme», on met l’accent sur le «concret», quitte à obtenir des conséquences inacceptables; en particulier, les résultats les plus essentiels de l’analyse deviennent faux quand on les interprète sur les réels récursifs)! Le principe de Markov:

se justifie très bien sur des bases pragmatiques: si on sait décider effectivement, pour chaque entier n , lequel de A [ 讀 ] ou de 囹 A [ 讀 ] est vrai, et si on a l’existence classique d’un n tel que A [ 讀 ] (soit 囹囹 說x A [x ], alors on peut, en essayant successivement les valeurs 0, 1, 2, ..., trouver effectivement un n tel que A [ 讀 ]. Bien entendu, ce genre de principe ne trouve sa justification que dans une interprétation externe à l’intuitionnisme.

2. Par contre, en Union soviétique même, Kolmogoroff et, en Occident, le constructivisme à la Bishop se proposent d’«effectiviser» de larges proportions des mathématiques, sans limitations idéologiques du type «tout est récursif», ou simplement d’orthodoxie intuitionniste. Ce point de vue a eu une certaine influence sur l’évolution de l’intuitionnisme lui-même (en particulier sur le système de Martin-Löf).

2. L’intuitionnisme vu du dedans Notion de preuve à la Heyting

Ici, nous abandonnons le terrain des mathématiques classiques pour essayer de penser en termes intuitionnistes. Quelle est donc la signification d’un énoncé A pour un intuitionniste? Ce n’est rien d’autre que: «J’ai une peuve de A.» Par preuve, il ne convient pas d’entendre «démonstration formelle», mais plutôt un certain processus mental qui entraîne la conviction. Heyting a proposé la définition suivante, pour la notion de preuve de A, A énoncé clos de l’arithmétique:

1. Une preuve d’un énoncé atomique t = u , t 麗 u , c’est le calcul qui établit explicitement que t = u , t 麗 u , suivant le cas.

2. Une preuve de A v B, c’est soit une preuve de A, soit une preuve de B.

3. Une preuve de A & B, c’est la paire d’une preuve de A et d’une preuve de B.

4. Une preuve de AB, c’est une fonction (effective) associant, à toute preuve de A, une preuve de B.

5. Une preuve de 說x A [x ], c’est un entier n et une preuve de A[ 讀 ].

6. Une preuve de 葉x A [ 異 ], c’est une fonction (effective) associant, à tout entier n , une preuve de A[ 讀 ].

Il importe de remarquer que les clauses 4 et 6 sont de nature infinie; en effet, ces clauses font référence à des fonctions, et à certaines propriétés de ces fonctions: il n’y a pas de moyen effectif de reconnaître si, pour tout n , f (n ) est une preuve de A [ 讀 ], car la vérification demanderait une infinité d’étapes! D’où la suggestion de certains auteurs: ajouter dans 4 et dans 6 la mention «plus une preuve de ce fait». On vérifie alors que la définition est tout bonnement impratiquable (on est en fait presque en train de dire «une preuve de A, c’est..., plus une preuve de A»). Les controverses sur ce sujet sont toujours extrêmement vives, et, comme personne n’a trouvé de réponse satisfaisante, dénuées d’intérêt. Leur vigueur vient sans doute du fait que cette notion de Heyting est vraiment à la base de l’intuitionnisme, et que son manque ultime de clarté jette une lumière douteuse sur l’entreprise tout entière.

En fait l’ontologie des mathématiques classiques n’est pas mieux fondée; si ce manque de clarté jette un doute, c’est sur la prétention des intuitionnistes à fonder leurs mathématiques sur quelque chose de plus solide que les classicistes; cela n’affecte guère l’intérêt de la partie intéressante (non dogmatique) du sujet.

Réalisabilité récursive

Si la notion de Heyting est loin d’être satisfaisante, il importe de remarquer que des notions très voisines ont un grand intérêt théorique; par exemple Kleene a introduit diverses notions de réalisabilité ; donnons un exemple: nous définissons e réalise A (e 﨎 IN, A clos):

1. e réalise un énoncé atomique clos si et seulement si cet énoncé est vrai.

2. e réalise A v B si et seulement si e = 2 練 3^f , et f réalise A, où e = 4 . 3^f , et f réalise B.

3. e réalise A & B si et seulement si e = 2^f . 3^g , et f réalise A, et g réalise B.

4. e réalise AB si et seulement si, pour tout f tel que f réalise A, e f est défini et réalise B.

5. e réalise 說x A si et seulement si e = 2ⁿ 練 3^g et g réalise A [ 讀 ].

6. e réalise 葉x A si et seulement si pour tout n e n est défini et réalise A [ 讀 ] (face=F0019 e n dénote le résultat de l’application de la fonction récusive partielle d’indice e à l’argument n ).

Théorème (Kleene): Si A clos est démontrable dans HA, alors on peut trouver un entier e tel que e réalise A.

Ce théorème permet de donner des démonstrations d’indépendance, par exemple d’exhiber un énoncé A tel que 葉x (A[x ] v 囹 A[x ]) ne soit pas démontrable; à la différence de l’approche sémantique classique de la première partie (les modèles topologiques), les méthodes utilisées pour ces résultats d’indépendance font elles-mêmes partie des mathématiques intuitionnistes.

Mentionnons aussi les interprétations fonctionnelles, qui sont elles aussi des «trahisons » de la définition de Heyting, puisque cette définition vague est remplacée par quelque chose de mathématiquement précis, mais qui ne retient qu’une partie de l’esprit des idées de Heyting.

Nous voyons en tout cas que les énoncés n’ont, pour un intuitionniste, aucune signification en dehors de l’acte qui consiste à les démontrer. De plus, démonstration n’est pas pris au sens formel (mais il ne s’agit ici que d’une pétition de principe, vu que Heyting le premier a proposé des calculs formels – calcul des prédicats, HA... – adaptés à l’intuitionnisme). Le véritable univers intuitionniste est donc celui des démonstrations; malheureusement, nous avons vu que l’on se heurte à des problèmes quasi insolubles dès que l’on veut vraiment préciser cette notion de démonstration non formelle.

Suites libres

Le développement mathématique le plus original de ce point de vue est sans nul doute l’analyse intuitionniste, fondée sur l’idée de suite libre (en anglais: choice sequence ). Il convient ici de remarquer que la paternité de l’idée revient à Borel ; Brouwer (qui connaissait très bien l’œuvre de Borel) en a développé les grandes lignes; plus récemment, Kreisel et Troelstra ont revu la question sous l’angle formel.

Rappelons-nous que les réels sont des suites de Cauchy de rationnels; donc, en utilisant une bijection entre N et Q, on peut remplacer l’étude des réels par celle des suites d’entiers. L’analyse intuitionniste est donc construite en donnant des principes quant à l’existence et aux propriétés des suites d’entiers. Donnons des exemples:

1. Les suites astreintes (lawlike ) sont les suites engendrées par une loi (effective), autrement dit des suites récursives, si on admet la thèse de Church. Cela dit, ne reconnaître (à l’instar de Markov) que ces suites mènerait à des résultats inacceptables.

2. À l’opposé, l’idée de suite anarchique (lawless ): imaginons une suite d’entiers engendrée «au hasard»; c’est une idée qui hante le calcul des probabilités, mais qui ne s’est pas matérialisée dans ce cadre; par contre, la théorie des suites anarchiques, introduite par Kreisel, donne un cadre intuitionniste où l’on peut travailler avec de tels objets. L’idée de l’axiomatique, c’est de dire que tout ce qu’on connaît d’une suite anarchique, c’est un segment initial (a ⁰, ..., a ^{n -1}) de la suite, et rien d’autre. Les suites anarchiques n’ont pas d’équivalent dans les mathématiques classiques.

La notion de suite libre fait le lien entre les deux exemples extrêmes précédents: une suite libre est la donnée d’une suite infinie (C⁰, a ⁰, ..., Cⁿ , a ⁿ , ...) où les a ⁿ sont des entiers et les Cⁿ des conditions que doivent satisfaire les coefficients a ^m , pour m 閭 n . L’idée étant que la suite est «le plus anarchique possible», dans les limites imposées par les conditions. Il importe de remarquer tout de suite que la suite n’est pas envisagée dans sa totalité (infini actuel), mais dans sa potentialité, c’est-à-dire son processus de croissance. Autrement dit, ce sur quoi nous aurons prise, ce sont des segments initiaux s = (C⁰, a ⁰, ..., C^{n -1}, a ^{n -1}) de la suite: si nous savons que s est un segment initial de la suite libre 見, nous possédons des informations non négligeables sur 見:

1. Les valeurs a ⁰, ..., a ^n-1 .

2. Au moyen des conditions C⁰, ..., C^n-1 , un certain nombre de contraintes sur le comportement ultérieur de la suite a ⁿ , a ⁿ⁺¹ , ... (par exemple, on peut demander par C⁰ que a ⁿ = f (n ), où f est une fonction récursive fixée: on obtient ainsi une suite astreinte; on peut tout aussi bien ne rien demander (les conditions Cⁱ étant alors toujours satisfaites): on obtient alors une suite anarchique; Si par exemple C⁰ stipule que tous les a ⁱ sont pairs, et les Cⁱ⁺¹ ne disent rien du tout, alors on obtient une suite de la forme (2 b ⁰, ..., 2 b ⁿ , ...), où (b ⁰, ..., b ⁿ , ...) est anarchique.

Intensionnalité

L’introduction de ces conditions Cⁱ illustre bien la différence de point de vue, quant à l’égalité des objets, qui sépare l’intuitionnisme du classicisme: pour un mathématicien classique, la suite se réduit à ses valeurs (son extension ), autrement dit, on identifierait deux suites qui ont les mêmes valeurs – c’est le point de vue extensionnel , à la base des mathématiques classiques. Par contre, l’intension de la suite libre, ce sont les conditions C⁰, ..., Cⁿ , ... (le mot est formé à partir de «intention» et de «intensité»). Le point de vue intensionnel ne permet que d’identifier des suites qui auraient même intension, c’est-à-dire même principe de définition. Cette intension immatérielle donne la dimension spiritualiste de l’intuitionnisme (que l’on pourra opposer au «scientisme» des formalistes).

L’analyse intuitionniste

La théorie des suites libres permet de concilier (dans la limite du possible) les exigences divergentes que sont:

– les principes intuitionnistes;

– les grands théorèmes de l’analyse classique.

Ces exigences sont contradictoires, comme le montre l’exemple d’une fonction définie de manière effective sur [0, 1] (et continue: on montre qu’une telle fonction est toujours continue!) et qui n’atteint ses bornes en aucun point récursif. Le résultat qui dit que toute fonction continue sur [0, 1] atteint ses bornes n’est alors plus vrai dans le cadre intuitionniste. Plus précisément, ce résultat est visiblement faux dans l’optique soviétique; la théorie des suites libres, quant à elle, n’interdit pas les réels non récursifs, mais, évidemment, toute suite libre que l’on exhibe comme solution d’un problème peut être remplacée par une suite récursive: le théorème ne devient donc pas vrai dans le cadre des suites libres.

Cela dit, la théorie des suites libres permet tout de même de développer une analyse mathématique décente; par exemple, toute fonction définie sur [0, 1] y est uniformément continue, et y admet des bornes supérieure et inférieure; par contre, on ne saurait dire que ces bornes sont atteintes, pour des raisons déjà exposées... Essayons de détailler la démonstration de continuité uniforme: on sait bien que cela découle de la compacité de [0, 1]; formulée en termes de suites, la compacité de [0, 1] n’est rien d’autre que le lemme de König : Soit T un arbre bien fondé et à embranchements finis, alors T est de hauteur finie. (Explications. T est un ensemble de suites (a ⁰ , ..., a ^n-1 ) d’entiers, stable par sous-suites: arbre ; il n’y a pas de suite (a ⁿ ) telle que, pour tout n , (a ⁰, ..., a ^n-1 ) 捻 T: bien fondé ; étant donné (a ⁰, ..., a ^n-1 ) 捻 T, il n’y a qu’un nombre fini de choix pour a ⁿ , de manière que (a ⁰, ..., a ^n-1 , a ⁿ ) 捻 T: à embranchements finis ; il existe un entier N telles que toutes les suites (a ⁰, ..., a ^n-1 ) 捻 T soient de longueur n 諒 N: de hauteur finie .)

La démonstration classique du lemme de König consiste à exhiber, en raisonnant par l’absurde, une suite (non effective) a ⁿ telle que (a ⁰, ..., a ^n-1 ) 捻 T pour tout n . Brouwer fait dériver cet énoncé (qui prend alors le nom de «théorème de l’éventail») d’un principe plus général des suites libres, le «théorème de la barre», qui n’est rien d’autre que le principe d’induction transfinie à la sauce intuitionniste. Ce qui est remarquable, c’est que les suites libres sont suffisamment riches (ou ambiguës) pour s’accommoder de tels principes. Par contre, le lemme de König est faux si on l’interprète à la manière soviétique, et du même coup la continuité uniforme disparaît: si on affaiblit l’hypothèse «T bien fondé» en «il n’y a pas de suite (a ⁿ ) récursive telle que pour tout n , (a ⁰, ..., a ^n-1 ) 捻 T», alors la conclusion du lemme de König devient fausse.

Outre le «théorème de la barre», l’analyse intuitionniste s’appuie sur des principes de continuité dont l’énoncé précis serait fastidieux; nous nous contenterons d’un cas particulier: si A [ 見] est vrai pour une suite anarchique 見, on peut trouver une suite finie s = (a ⁰, ..., a ^n-1 ) telle que 見 prolonge s , et telle que, si 廓 est une quelconque suite anarchique prolongeant s , on ait A [ 廓]. La justification est la suivante: supposons que A [ 見] soit vrai au sens intuitionniste; pour le savoir, j’ai dû utiliser un nombre fini d’informations sur 見, et rien d’autre; donc A restera vrai en 廓 dès que 廓 est une autre suite correspondant au même nombre fini d’informations. Remarquer l’identification entre «A [ 見] est vrai» et «je sais que A [ 見] est vrai», typique de l’intuitionnisme. Il va de soi que ce genre de justification est dangereux; heureusement, dans le cas qui nous intéresse, on sait construire des modèles des axiomes sans utiliser d’argument douteux.

Au cœur de l’intuitionnisme, la théorie des suites libres n’a que médiocrement intéressé les mathématiciens classiques; il n’est pourtant pas exclu qu’elles puissent servir de cadre à une théorie des fonctions aléatoires, théorie qui pourrait alors enrichir le calcul des probabilités de manière décisive; mais on voit bien le fossé qui sépare la théorie de la mesure, très non constructive, et l’intuitionnisme!

Espèces

La théorie des ensembles (d’entiers) ou espèces (species ) est nettement moins spécifique de l’intuitionnisme; dans sa forme la plus forte (HA²), on admet le schéma de compréhension:

pour tout A; c’est un système extrêmement fort, et qui conserve pourtant certaines propriétés formelles des systèmes intuitionnistes (notamment en ce qui concerne la prouvabilité des existences et disjonctions); mais on n’a pas ici vraiment affaire à une pensée originale, comme dans le cas des suites libres.

Le «sujet créatif»

Il faut faire un sort à la théorie du «sujet créatif»; peut-on sérieusement imaginer une théorie mathématique de l’acte mathématique? C’est douteux en l’état actuel de nos connaissances; en tout cas, les deux ou trois axiomes proposés par Brouwer pour ce faire sont pour le moins superficiels! Cette «théorie» est parfois utilisée pour donner des contre-exemples... mais il faut vraiment avoir une foi sans faille pour prendre tout cela au sérieux.

Le système de Martin-Löf

Face à l’école hollandaise, qui se situe pour l’essentiel dans le sillage de Brouwer, s’est développée une école suédoise, active depuis le milieu des années 1960; nous avons déjà vu ce que l’intuitionnisme formel doit à Prawitz, et il nous reste à décrire l’apport de Martin-Löf: il part d’une analyse philosophique des mathématiques, notamment de la signification (meaning ) des opérations logiques; ses recherches l’ont conduit à l’élaboration d’un système formel dont les seuls énoncés sont de la forme t 捻 A (c’est-à-dire «t est de type A»). La richesse du système vient de:

– la grande variété de types admis;

– la possibilité d’une double interprétation pour l’énoncé t 捻 A:

(I) On peut considérer A comme un ensemble, et alors cela veut tout simplement dire que t appartient à A.

(II) Mais on peut aussi considérer A comme un énoncé, et cela veut alors dire que t est une démonstration de A; dans ce cas, il s’agit d’une reformulation de la notion de démonstration au sens de Heyting, sans doute la plus intéressante; bien entendu, la notion de Heyting étant ce qu’elle est, il est difficile de lui être strictement fidèle, du moins si on veut vraiment en faire quelque chose. Le système de Martin-Löf ne peut donc pas prétendre à l’orthodoxie...

Pour donner une idée du système, nous nous contenterons de décrire les deux opérations et 刺 qui en constituent l’armature: si xB [x ] est une fonction qui à tout x de type A associe un type B [x ], alors il est permis d’introduire les types x 捻 A B[x ] et 刺 x 捻 A B [x ].

Si on adopte l’interprétation (I) (types = ensembles), alors:

– Un élément de type x 捻 A B [x ] est une paire (a , b ), avec a 捻 A, b 捻 B[a ]. Autrement dit, x 捻 A B [x ] est la somme disjointe des B [x ], pour x 捻 A. Cas particulier: si B ne dépend pas de x , x 捻 A B [x ] est le produit cartésien A 憐 B.

– Un élément de type 刺 x 捻 A B [x ] est une fonction f qui associe, à tout élément a de type A, un élément f (a ) de type B [a ]. Autrement dit, 刺 x 捻 A B [x ] est le produit des B [x ], pour x 捻 A. Cas particulier: si B ne dépend pas de x , 刺x 捻 A B [x ] est l’ensemble des fonctions (constructives) de A vers B.

Si on adopte l’interprétation (II) (types = formules), alors:

– Un élément de type x 捻 A B [x ] est la donnée d’une démonstration de A (soit un élément a de A) et d’une démonstration de A [a ]. Autrement dit, un élément de ce type n’est rien d’autre qu’une démonstration de 說 x 捻 A B [x ] au sens de Heyting. Donc x 捻 A B [x ] veut aussi dire 說 x 捻 A B [x ]. Dans le cas particulier où B ne dépend pas de x , un élément de ce type est la paire d’une démonstration de A et d’une démonstration de B; c’est donc une démonstration de la conjonction A & B: dans ce cas, x 捻 A B [x ] veut dire A & B!

– Un élément de type 刺 x 捻 A B [x ] est une fonction f , qui à toute démonstration a de A (c’est-à-dire tout élément de A) associe une démonstration f (a ) de B [a ]. Autrement dit, Heyting dirait qu’il s’agit d’une démonstration de 葉 x 捻 A B [x ]. Donc 刺 x 捻 A B [x ] veut aussi dire 葉 x 捻 A B [x ]. Dans le cas particulier où B ne dépend pas de x , un élément de ce type est une fonction qui associe à toute démonstration de A une démonstration de B; c’est donc une démonstration de AB: ici 刺 x 捻 A B [x ] veut dire AB.

À ces schémas de formation de types, correspondent des schémas de formation de termes, qui sont les suivants:

(I) Si t est de type A, si u est de type B [t ], alors (t , u ) est de type x 捻 A B [x ].

(II) Si t [x , y ] est, quand y est un terme de type B [x ], un terme de type C (C ne dépendant pas de x ), alors ST xyt [x , y ] u est un terme de type C, u étant un terme de type x 捻 A B [x ]. (Dans cette expression, x et y sont des variables muettes.)

(III) Si t [x ] est de type B [x ] pour tout x de type A, alorsxt [x ] est de type 刺 x 捻 A B [x ].

(IV) Si t est de type 刺 x 捻 A B [x ], si u est de type A, alors t (u ) est de type B [u ].

Ces schémas de formation de termes s’accommodent bien des deux interprétations du système.

Le système contient finalement des règles pour identifier des termes; c’est ainsi qu’on identifiera:

Pour l’instant, le système de Martin-Löf n’est pas allé assez loin pour pouvoir donner une approche convaincante de l’analyse intuitionniste, en particulier des suites libres; par contre, l’application du système en direction de l’informatique théorique est une nouvelle direction qui semble pleine d’avenir.

• 1908; de intuition

♢ Théorie d'après laquelle les mathématiques ont recours à l'intuition et pas seulement à l'hypothèse et à la déduction. — N. et adj. INTUITIONNISTE , 1874 .

⇒INTUITIONNISME, subst. masc.

A. — PHILOS. Doctrine qui accorde à l'intuition une importance essentielle dans la connaissance. Intuitionnisme bergsonien. L'intuitionnisme génial de Frédéric Schlegel se rapproche de la philosophie de Fichte (A. SCHLAGDENHAUFFEN, Frédéric Schlegel et son groupe, Paris, Les Belles Lettres, 1934, p. 124). L'intuitionnisme contemporain est, en effet, la recherche d'un au-delà de la logique (Encyclop. univ. t. 9 1971, p. 45) :

• 1. ... de là aussi, les essais très nombreux de se passer des preuves rationnelles de l'existence de Dieu : le traditionalisme, l'intuitionisme, le sentimentalisme ont dû une grande partie de leurs succès à cette préoccupation.

Théol. cath. t. 4, 1, 1920, p. 875.

B. — LOG. MATH. [P. oppos. à formalisme] Théorie selon laquelle les mathématiques ont recours à l'intuition et pas seulement à l'hypothèse et à la déduction. La lutte contre l'intuitionnisme de Weyl et de Brouwer, avec ses tendances mystiques, et le formalisme de Russell au scepticisme stérilisant (Gds cour. pensée math., 1948, p. 385) :

• 2. Si l'on débarrasse l'« intuitionnisme » de ses présupposés philosophiques (...) il en reste l'idée de l'autonomie des objets mathématiques par rapport à la logique.

Encyclop. univ. t. 10 1971, p. 624.

Prononc. et Orth. : []. Forme intuitionisme, supra. Cf. -isme. Étymol. et Hist. 1908 philos. (A. FOUILLÉE, Morale des idées-forces, I, 2 ds QUEM. DDL t. 4). Dér. de intuition; suff. -isme. Bbg. DUB. Dér. 1962, p. 35. - QUEM. DDL t. 12.

intuitionnisme [ɛ̃tɥisjɔnism] n. m.

ÉTYM. 1908, Fouillée; de intuition.

❖

1 Philos. Doctrine attribuant un rôle essentiel à l'intuition. || L'intuitionnisme bergsonien.

2 Sc. Théorie d'après laquelle les mathématiques ont recours à l'intuition et n'ont pas seulement recours à l'hypothèse et à la déduction. || Selon Heyting, les principes de l'intuitionnisme mathématique sont : « 1) la mathématique n'a pas seulement une signification formelle, mais aussi un contenu; 2) les objets mathématiques sont saisis immédiatement par l'esprit pensant. » — Var. graphique : intuitionisme.