Résumés
Résumé
La thèse selon laquelle la signification d’un énoncé mathématique est donnée par sa preuve a été soutenue à la fois par Wittgenstein et par les intuitionnistes, à la suite de Heyting et de Dummett. Dans ce texte, nous nous attachons à clarifier le sens de cette thèse chez Wittgenstein, afin de montrer en quoi sa position se distingue de celle des intuitionnistes. Nous montrons par ailleurs que cette thèse prend sa source chez Wittgenstein dans sa réflexion, durant la période intermédiaire, sur la notion de preuve par induction. Nous esquissons aussi les grandes lignes de la réponse que Wittgenstein fait à un certain nombre d’objections, dont celle selon laquelle cette thèse, dans le sens qu’il lui donne, remet en question la possibilité même de formuler une conjecture en mathématique. Nous terminons en montrant comment les propos de Wittgenstein trouvent un écho favorable dans le paradigme contemporain de la “proposition comme type” et les extensions de l’isomorphisme de Curry-Howard dont il est issu.
Abstract
The thesis according to which the meaning of a mathematical sentence is given by its proof was held by both Wittgenstein and the intuitionists, following Heyting and Dummett. In this paper, we clarify the meaning of this thesis for Wittgenstein, showing how his position differs from that of the intuitionists. We show how the thesis originates in his thoughts, from the middle period, about proofs by induction, and we sketch his answers to a number of objections, including the idea that, given the particular meaning he gives to this thesis, he cannot account for mathematical conjectures. We conclude by showing how his views find a favourable echo today in the paradigm of “proposition-as-type” and extensions of the Curry-Howard isomorphism from which this paradigm originates.
Corps de l’article
1. La question de la signification d’un énoncé mathématique dans le cadre de la querelle entre constructivisme et platonisme
En philosophie des mathématiques, le constructivisme s’oppose au « platonisme ». Pour un platoniste, les énoncés mathématiques ne requièrent pas de sémantique particulière, à supposer que nous possédions une sémantique vériconditionnelle pour une langue naturelle comme le français, alors que ces énoncés ont pourtant cette particularité, qui ne sont reconnus comme vrais qu’uniquement en vertu d’une preuve. Le mathématicien G. H. Hardy a exprimé ce point de vue platoniste d’une manière imagée en se comparant à un « observateur » regardant au loin une chaîne de montagnes, son rôle étant de décrire celle-ci du mieux qu’il peut ; il peut aider un étudiant en pointant du doigt, et lorsque celui-ci aperçoit ce dont il est question, son travail est terminé : la preuve n’est donc qu’une « fioriture rhétorique », dont le but n’est que de « stimuler l’imagination des étudiants[1] ». Le point de vue de Hardy est certes radical et ne représente pas la meilleure façon de formuler la position platoniste, mais il est utile pour établir un contraste avec le point de vue constructiviste, qui s’oppose à toute conception des mathématiques où la preuve ne joue au bout du compte qu’un rôle secondaire, en liant la signification des théorèmes mathématiques de façon plus étroite avec leur preuve : en termes plus contemporains, pour un constructiviste le « vérifacteur » (truth-maker) d’un énoncé mathématique est sa preuve elle-même[2]. On retrouve ici le slogan,
Cependant, lorsqu’on tente de clarifier la signification de ce slogan, on se bute à plusieurs difficultés, dont certaines seront soulevées dans ce qui suit. Nous aimerions par contre nous concentrer uniquement sur la façon dont ces difficultés surgissent dans le cas de Wittgenstein, et non pour toute position constructiviste que l’on puisse imaginer. Qu’il ait soutenu la thèse selon laquelle « la signification d’un énoncé mathématiques est donné par sa preuve » est indéniable, malgré les propos sans fondement d’une autorité comme Hilary Putnam[3]. (Ce dernier n’a en fait que peu de crédibilité comme lecteur de Wittgenstein[4].) Nous lisons, par exemple, dans les Remarques philosophiques :
Si nous voulons voir ce qui a été prouvé, nous ne devons regarder que la preuve[5]
traduction modifiée
[T]oute proposition dotée de sens doit nous indiquer par son sens comment nous convaincre de sa vérité ou de sa fausseté. « Toute proposition dit ce qui est le cas si elle est vraie. » Et ce « ce qui est le cas » doit forcément, en ce qui concerne la proposition mathématique, se rapporter à la façon dont elle est prouvée[6]
traduction modifiée
Tandis que dans la Grammaire philosophique, on trouve des affirmations comme celle-ci, tirée d’une section intitulée « Si tu veux savoir ce qui a été prouvé, regarde la preuve[7] » :
Pourquoi dis-je que nous ne trouvons pas mais construisons une proposition tel le théorème fondamental de l’algèbre ? — Parce que, en la prouvant, nous lui conférons un sens nouveau dont elle était auparavant entièrement dépourvue. Avant ce que nous appelons preuve, nous n’avions qu’un patron approximatif de ce sens dans le langage des mots
Wortsprache[8]
Ces remarques datent de la période dite « intermédiaire », qui s’étend du retour de Wittgenstein à Cambridge, en 1929, à la rédaction de la première version des Recherches philosophiques en 1936 ; on peut encourir le reproche, assez automatique lorsqu’on cite des textes de cette période, selon lequel ces écrits ne font état que des positions abandonnées par la suite, les positions de Wittgenstein ayant apparemment évolué vers une « deuxième philosophie ». Ce genre de reproche n’a en général que le mérite de pointer du doigt l’ignorance de son auteur. Non seulement n’y a-t-il pas de chose telle qu’une « deuxième philosophie des mathématiques[9] » de Wittgenstein, mais, dans le cas précis de la thèse (1), on trouve des remarques tardives, comme celle-ci, datant de 1944, mais dont l’existence est insoupçonnée pour les lecteurs des Remarques sur les fondements des mathématiques, puisque les éditeurs ne l’ont pas imprimée dans ce choix de textes, sans pour autant avertir le lecteur de leurs nombreuses décisions éditoriales, plus étranges les unes que les autres :
Si on me prouvait le théorème de Fermat, alors je le comprendrais mieux qu’auparavant.
Le problème consistant à trouver une décision mathématique pour un théorème peut à bon droit être appelé celui de donner un sens mathématique à une formule[10].
Inutile de multiplier les citations de ce genre. Nous nous intéresserons donc dans ce qui suit au fait que Wittgenstein a bel et bien écrit de telles phrases, et non, comme Putnam, à ce que nous aimerions qu’il dise, donc aux raisons qu’il a pu avoir de les écrire. Pour cela, il faut d’abord montrer en quoi la position de Wittgenstein se distingue de celles des autres constructivistes, qui soutiennent (1).
Pour le platoniste, les énoncés mathématiques portent sur des objets mathématiques, qui sont bien entendu des entités abstraites, dont l’existence est indépendante de nos propres activités ou constructions, de telle sorte que les énoncés mathématiques possèdent une valeur de vérité qui outrepasse notre capacité à reconnaître si leurs conditions de vérité sont satisfaites ou non par ces objets. Nous laissons de côté ici la question de savoir s’il faut simplement parler d’objets ou plutôt de structures, ou encore celle de savoir si les énoncés réfèrent ou non à leur valeur de vérité, comme dans une sémantique « tarskienne ». Nous pourrions donc donner une caractérisation minimale du platonisme comme suit :
Un constructiviste comme Dummett ne s’objecte pas à cette thèse : il réclame seulement de ces entités qu’elles dépendent de l’activité des mathématiciens, et il insiste par conséquent sur le fait que notre compréhension de la signification des énoncés mathématiques n’outrepasse pas notre capacité à reconnaître si leurs conditions de vérité sont satisfaites ou non[11]. À cet égard, Wittgenstein semble soutenir une thèse constructiviste plus radicale, dans la mesure où il rejette l’idée que les énoncés mathématiques puissent porter sur des entités abstraites, que celles-ci soient dépendantes ou non de l’activité des mathématiciens. En effet, il soutient dans le Tractatus Logico-Philosophicus que :
6.211 — Dans la vie, ce n’est pas de propositions mathématiques dont nous avons besoin, mais nous usons de la proposition mathématique pour déduire, de propositions qui n’appartiennent pas à la mathématique, d’autres propositions, qui ne lui appartiennent pas non plus[12].
Et il rejette l’application de la distinction de Frege entre sens (Sinn) et référence (Bedeutung) aux équations de la théorie des nombres. Pour ce dernier, une équation comme celle-ci :
exprime le fait que ses deux membres sont deux sens différents qui ont une même référence, en l’occurrence l’entité abstraite qu’est le nombre « 29083 ». Ce point de vue devrait apparaître à quiconque terriblement déficient : pour reconnaître que les deux membres de l’équation sont équivalents, il faut « faire une opération » ou « faire un calcul », et c’est précisément ce « calcul » qui est rejeté à l’arrière-plan de la conception de Frege, comme si ce dernier était sans grande importance. Wittgenstein devait justement penser en ces termes from the word go, puisque sa conception remet l’opération ou le calcul à l’avant-plan dès le début[13]. De façon certes fort maladroite et incomplète, il propose en fait des règles de réécriture (6.241), qui permettent de transformer le membre gauche de cette équation en son membre droit, et la perception de cette réécriture elle-même suffit à en reconnaître la rectitude (6.2321) ; nul besoin, donc, de faire appel à une entité abstraite :
6.232 — Frege dit que les deux expressions ont la même référence, mais des sens différents.
Mais l’essentiel dans l’équation est qu’il n’est pas nécessaire de montrer que les deux expressions mises en connexion par le signe d’égalité ont la même référence, car cela se laisse percevoir à partir des deux expressions elles-mêmes
traduction modifiée
Il exprimera ce point de vue de la façon suivante dans sa période « intermédiaire » :
Je crois que la mathématique, une fois la crise des fondements terminée, prendra l’aspect qu’elle a dans les écoles primaires, où l’on travaille avec les bouliers russes. […] La mathématique est toujours une machine, un calcul. Le calcul ne décrit rien[14].
En mathématiques, tout est algorithme et rien n’est signification [Bedeutung] même lorsque cela ne semble pas être le cas parce qu’on semble utiliser des mots pour parler à propos d’objets mathématiques. Même ces mots sont utilisés pour construire un algorithme[15].
Wittgenstein rejette donc (1) ; pour lui, les énoncés mathématiques ne décrivent rien, ils ne portent pas sur des entités abstraites. Mais quelle position soutient-il en retour, s’il en soutient une[16] ?
La clef se trouve dans la clarification de ce qu’on entend par « calcul ». Dans un premier sens, le mot « calcul » s’entend comme une généralisation de la notion ordinaire de calcul numérique, c’est-à-dire comme une suite d’opérations sur des signes, selon une « procédure effective » ou « mécanique ». Pour être « effective », une procédure doit se terminer en un nombre fini d’étapes et doit être telle qu’un être humain puisse l’effectuer « à la main » (avec un crayon sur du papier), tandis que chaque étape doit consister en l’application d’une règle (prise parmi un ensemble fini de règles elles-mêmes énoncées de manière finie), de telle sorte que l’application de la règle ne réclame pas de conjecture de la part de l’être humain[17]. Cette suite d’opérations peut prendre la forme d’une « machine de Turing », d’un « lambda terme » dans le calcul lambda, d’une fonction récursive (générale), ou encore d’un programme écrit dans un langage informatique. Dans un second sens, celui des expressions « calcul des propositions » et « calcul des prédicats », le mot « calcul » réfère à la formalisation des démonstrations, c’est-à-dire à l’étude des relations entre les énoncés qui forment une démonstration du point de vue « formel », c’est-à-dire en ne considérant que les aspects syntaxiques des suites de signes. On peut donc décrire les systèmes axiomatiques de Frege-Hilbert et les systèmes non axiomatiques de déduction naturelle, ainsi que les calculs des séquents, que l’on doit à Gentzen[18], comme des « calculs logiques ». On peut cependant voir un « calcul fonctionnel » comme le calcul lambda, formalisant les opérations qui doivent être effectuées pour l’évaluation d’une fonction, comme tombant aussi sous cette définition, d’où l’ambiguïté du terme « calcul »[19].
2. L’écart entre ce que l’énoncé mathématique dit et ce que sa preuve montre
La distinction entre « calcul logique » et « calcul fonctionnel » est très utile pour comprendre le point de vue de Wittgenstein. Nous l’utiliserons dans cette section pour présenter certains résultats de notre collaboration, dont l’importance pour la compréhension du point de vue de Wittgenstein sur les problèmes soulevés par la thèse (1) ne peut être sous-estimée[20].
Avec sa définition des nombres naturels en termes de répétition de l’application d’une opération au 6.02, et ses règles de réécriture pour l’addition et la multiplication au 6.241, Wittgenstein a plus ou moins jeté les bases de ce que nous avons appelé un « calcul fonctionnel », une sorte de « calcul des équations » du genre de celui que développa par la suite son étudiant Goodstein, et qui a des liens avec le calcul lambda — la définition des nombres naturels au 6.02, par exemple, est essentiellement la même que celle des « Church numerals » dans le calcul lambda[21]. Il considérait par ailleurs qu’un « calcul logique », comme le système axiomatique dans le style « Frege-Hilbert » des Principia Mathematica de Russell et Whitehead était superflu (6.031), tout en étant conçu à partir d’un certain nombre d’erreurs philosophiques, comme celle, par exemple, de n’avoir pas conçu la logique comme « théorie de l’inférence » (6.1224)[22], une bonne partie de l’argument du Tractatus étant dirigée contre l’idée même d’une théorie des types. Wittgenstein sépare donc dans son Tractatus « calcul fonctionnel » et « calcul logique », et il rejette l’applicabilité de ce dernier aux mathématiques.
Le « calcul des équations » du Tractatus peut certes rendre compte des équations de la théorie des nombres, mais on laisse souvent entendre qu’il n’a guère de valeur comme « fondement ». En supposant qu’il soit équivalent au calcul lambda, il suffit de se rappeler du fait que la notion de fonction « lambda-définissable » est elle-même équivalente à la notion de fonction récursive générale et à la thèse de Church-Turing[23] pour réaliser que ce n’est probablement pas le cas, quoiqu’on puisse par ailleurs blâmer Wittgenstein de n’avoir même pas été en mesure de chercher à le montrer.
On peut aussi lui reprocher de n’avoir pas tenu compte de la notion de preuve mathématique : il n’y pas de discussion de la notion fondamentale de « preuve par induction » (appelée aussi en français « preuve par récurrence ») dans le Tractatus. Wittgenstein a cependant cherché à pallier ce problème après son retour à la philosophie en 1929, c’est-à-dire dans sa période « intermédiaire », ce qui est une preuve non seulement du fait qu’il était conscient du problème, mais aussi de son intérêt pour ces questions. La solution de Wittgenstein fut, en gros, de proposer dans la Grammaire philosophique[24] le remplacement du « principe d’induction mathématique » (énoncé ici dans une version simplifiée avec « s » pour la fonction de successeur[25]) :
sur lequel les preuves par induction sont basées, par une « règle d’unicité d’une fonction définition par récursion », dont son étudiant R. L. Goodstein a montré par la suite qu’elle implique le principe d’induction mathématique en arithmétique récursive élémentaire[26]. Cette idée de Wittgenstein indique donc une évolution de sa pensée sur les mathématiques, dans la mesure où il ne faisait que rendre compte des calculs numériques dans le Tractatus. C’est aussi fort probablement sa contribution la plus importante à la logique mathématique[27]. Elle procède d’une intention inverse à celle de Frege et de Russell, qui était de montrer jusqu’à quel point on peut se passer d’un « calcul logique » en mathématiques ; autrement dit, ne pouvant pas tout à fait se passer de la logique, Wittgenstein a voulu montrer, entre autres avec cette règle, que le rôle qu’elle est appelée à jouer est en fait le plus minimal possible.
Pour comprendre ce dont il est question, il vaut la peine de s’attarder sur une preuve de l’associativité de l’addition :
qui exprime l’idée fort simple que si vous additionnez trois nombres, peu importe dans quel ordre vous le faites, le résultat sera le même. Cette preuve, due à Thoralf Skolem[28], a servi de point de départ aux réflexions de Wittgenstein (qui possédait un tiré-à-part de l’article de Skolem) ; nous verrons par le fait même ce qui constitue la particularité du point de vue de Wittgenstein par rapport aux positions constructivistes comme celle de Dummett, mentionnées ci-dessus. Cette preuve mérite, pour la compréhension des commentaires de Wittgenstein qui suivront, d’être présentée au long, elle est heureusement très courte et facile à suivre, et ne présuppose que la définition par récursion de l’addition :
La preuve procède comme suit[29] :
Pour la base on a :
(i) |
Si c = 0, alors nous avons (a + b) = (b + a), puisque a + 0 = a |
Pour le pas inductif, on suppose que l’associativité vaille pour une valeur C de c, de sorte que nous ayons l’hypothèse inductive suivante :
à partir de laquelle on prouve le cas C + 1 de la manière suivante :
(ii) |
a + (b + (C + 1)) = a + ((b + C) + 1) (par définition) |
(iii) |
a + ((b + C) + 1) = (a + (b + C)) + 1 (par définition) |
(iv) |
(a + (b + C)) + 1 = (a + b) + C) + 1 (par hypothèse inductive) |
(v) |
((a + b) + C) + 1 = (a + b) + (C + 1) (par définition) |
a + (b + (C + 1)) = (a + b) + (C + 1) (de (ii),(iii), (iv) et (v)) |
Skolem n’explicite pas le principe ou la règle qui est à l’oeuvre dans cette preuve. Pour des termes u et v, on donnerait de nos jours la règle suivante pour l’induction mathématique dans les systèmes de déduction naturelle[30] :
où on retrouve (i) sur la gauche, tandis que le passage de u(x) = v(x) à u(x + 1) = v(x + 1) à droite, sous forme de raisonnement hypothétique, est donné par les étapes (ii)-(v) ci-dessus. C’est-à-dire qu’on a quelque chose comme :
Le lecteur vérifiera aisément que cette règle correspond au principe d’induction mathématique (3) ci-dessus, mais sans la présence des quantificateurs. Est-ce que cela veut dire que Skolem a prouvé quelque chose comme :
ou non ? On serait tenté de le penser : les quantificateurs sont certes absents mais donnent l’impression d’être présupposés, puisqu’on aurait envie de lire la conclusion, sous la barre horizontale, commençant par les mots « Pour tous les… ». Skolem lui-même développait dans cet article un système d’arithmétique élémentaire sans quantificateur, et il faisait profession de foi finitiste dans sa conclusion, se plaçant explicitement dans la lignée de Kronecker ; il considérait les quantificateurs « encombrants[31] ». Wittgenstein veut lui aussi se débarrasser des quantificateurs, pour une raison simple : ils font partie d’un « calcul logique[32] ». S’il veut étendre le point de vue du Tractatus pour tenir compte des preuves par induction mathématique, il ne doit cependant pas faire appel à ce dernier, d’où son intérêt pour la preuve de Skolem et, par la suite, sa tentative d’éliminer le raisonnement hypothétique dans la règle d’induction ci-dessus, qui le mène à proposer, comme nous le disions, une règle d’unicité. Il n’est pas nécessaire de s’étendre ici sur cette dernière[33], il importe seulement de remarquer que Wittgenstein insiste sur l’écart entre la preuve et l’énoncé avec quantificateurs censé décrire ce qui a été prouvé.
Cette remarque est cruciale pour la compréhension de la pensée de Wittgenstein, puisque cet écart est le point de départ de sa réflexion sur la thèse (1) : si on veut connaître la signification d’un énoncé tel que (4), il faut donc en regarder la preuve. La toute première citation de notre texte est justement tirée de ce contexte, celui de la discussion de la preuve de Skolem. Elle continue ainsi :
Si nous voulons voir ce qui a été prouvé, nous ne devons regarder que la preuve.
On ne doit pas confondre la possibilité infinie de son application avec ce qui est réellement prouvé. La possibilité infinie d’une application n’est pas prouvée.
Ce qui est le plus frappant dans la preuve par récurrence, c’est que ce qu’elle prétend prouver n’est pas ce qui en sort[34]
traduction modifiée
Ce passage montre bien dans quel contexte la thèse « La signification d’un énoncé mathématiques est donné par sa preuve » prend son sens pour Wittgenstein. Si notre but est de chercher à comprendre ce qu’il a voulu dire, ce fait est donc incontournable, à moins de vouloir l’extraire de son contexte dans l’oeuvre de Wittgenstein et de la discuter de manière indépendante, auquel cas on ne cherche plus à comprendre Wittgenstein lui-même.
On notera donc que, dans ce contexte, Wittgenstein cherchait à creuser l’écart entre la preuve par induction, dont on peut dire qu’elle est donnée dans un « calcul fonctionnel », et la formule logique avec quantificateurs, dans un « calcul logique », censée décrire ce qui a été prouvé. Selon lui, la preuve de Skolem n’est pas une preuve d’un énoncé tel que (4) :
Si c’est une preuve, la preuve par induction serait une preuve de généralité, et non la preuve d’une certaine propriété pour tous les nombres[35]
traduction modifiée
[T]out d’abord je découvre que dans mes calculs je n’ai nullement eu besoin de la proposition « Pour tous les nombres cardinaux »[36]
traduction modifiée
La preuve par induction. Ce qui frappe d’abord ici, c’est que la proposition qu’il s’agit de prouver n’apparaît nullement dans la proposition elle-même. Aussi la preuve ne prouve-t-elle nullement la proposition. C’est-à-dire que l’induction n’est pas un procédé qui conduit à une proposition. L’induction nous fait voir une possibilité infinie, et c’est en cela seulement que consiste l’essence de la preuve par induction[37]
traduction modifiée
(Le lecteur peut vérifier ce dernier point en relisant la preuve telle que donnée ci-dessus.) Cette preuve ne fait que fournir un « patron » de calculs :
Une preuve par récurrence n’est qu’une directive générale que l’on donne pour des preuves particulières quelconques. Un poteau indicateur qui indique le chemin de la maison, selon un itinéraire déterminé, à toutes les propositions d’une forme particulière[38]
traduction modifiée
Nous pouvons voir l’application infinie de ce patron, mais cela, la preuve le montre mais ne le dit pas d’elle-même[39] :
Un proposition algébrique ne gagne jamais qu’une signification arithmétique si à la place des lettres nous insérons des chiffres, et ce n’est jamais qu’une signification arithmétique particulière.
Sa généralité ne réside pas en elle-même, mais dans la possibilité de son application correcte. Et pour celle-ci, on doit toujours avoir recours à l’induction.
C’est-à-dire : cette proposition ne dit [sagt] pas sa généralité, elle ne l’exprime pas, mais cette généralité se montre [zeigt] dans la relation formelle de substitution, qui se révèle être un terme dans la suite inductive[40]
traduction modifiée ; italique ajouté
« Cette proposition est prouvée pour tous les nombres grâce à la preuve par récurrence. » Voilà l’expression qui est si terriblement trompeuse. Cela sonne comme si on avait démontré la vérité de la proposition selon laquelle ceci et cela vaut pour tous les nombres en empruntant un chemin particulier […].
Alors qu’en réalité la récursion ne montre [zeigt] qu’elle-même […][41].
Traduction modifiée ; italique ajouté
Une vision particulière à Wittgenstein sous-tend ses propos, selon laquelle les divers calculs auxquels on a affaire en mathématiques sont séparés et ne sont pas liés ensemble dans une structure où un calcul sert de fondement à un autre calcul, quoique certains contacts ou liens puissent être établis[42]. (Wittgenstein exprimera la même idée dans les Recherches philosophiques en parlant « d’air de famille » aux § 67-68 ; une idée qu’on croit donc à tort être la marque d’une « deuxième » philosophie, alors qu’elle est présente, comme on peut le voir, dans toute la période « intermédiaire ».) La preuve par induction est justement un de ces liens, entre le langage de la théorie des nombres et celui de l’algèbre, car la preuve algébrique permet justement par son application de faire une infinité potentielle de nouveaux calculs numériques :
L’induction ne prouve pas la proposition algébrique parce que seule une équation peut prouver une équation. Mais elle justifie que l’on établisse les équations algébriques du point de vue de leur application à l’arithmétique[43]
traduction modifiée
Le but de la preuve par récurrence est bien d’établir un lien entre le calcul algébrique et le calcul numérique. Et l’arbre de la preuve par récurrence ne justifie le calcul algébrique que lorsque cela doit signifier qu’il le met en relation avec le calcul arithmétique.
[I]l n’était donc pas nécessaire que Skolem nous promette une preuve des lois d’associativité et de commutativité. Il aurait pu simplement s’engager à nous montrer une connexion entre les paradigmes de l’algèbre et les règles de calcul de l’arithmétique[44]
traduction modifiée
Ces remarques appellent deux brefs commentaires : tout d’abord, que de tels liens puissent être établis entre les calculs, cela ne justifie jamais pour Wittgenstein qu’ils puissent liés ensemble dans une structure où un calcul servirait de « fondement » à un autre, surtout pas dans le cas d’un « calcul logique »[45]. Deuxièmement, les liens que Wittgenstein voit ici sont directs et font l’économie d’un passage par la métamathématique[46] ; c’est là la source de ses objections au programme de Hilbert.
Une formule avec quantificateurs universels, comme (4) par exemple, n’est que le correspondant dans un « calcul logique » d’un énoncé commençant par les mots « Pour tous… », donc d’un énoncé dans ce que Wittgenstein appelle une « Wortsprache », littéralement : un « langage des mots », c’est-à-dire celui des mots d’une langue naturelle telle que le français, qui apparaissent dans le texte mathématique[47]. Le point de vue de Wittgenstein traduit donc une méfiance à l’égard de ce dernier et, de surcroît, à l’égard du « calcul logique » dans lequel on traduit ces mots pour ensuite appliquer au résultat des opérations logiques. (Quiconque connaît les pensées de L. E. J. Brouwer aura reconnu une affinité certaine avec Wittgenstein sur ce point, qui explique bien évidemment l’intérêt de ce dernier pour les idées du fondateur de l’intuitionnisme[48].) Voilà pourquoi Wittgenstein a écrit de telles choses :
De ce fait, nous trouvons curieux qu’on nous dise que l’induction prouve la proposition générale ; nous avons à juste raison le sentiment que nous n’aurions pas pu poser la question générale dans le langage de l’induction. Car au début, nous n’avions pas d’alternative (il semblait seulement y en avoir une tant que nous avions à l’esprit un calcul de classes finies[49]).
On peut, bien sûr, ne pas partager les vues de Wittgenstein et leurs conséquences, mais il importe peu dans le cadre de ce texte de se prononcer sur cette question ; il importe seulement que les remarques qui précèdent suffisent pour faire voir en quel sens Wittgenstein entendait soutenir (1) et par là même en quoi ses positions ne peuvent être assimilées à celles d’un constructiviste tel que Dummett.
3. Signification, preuve et conjecture mathématique
Quoi qu’on entende par (1), cette thèse ne va pas de soi. Le platoniste peut la contrer par des arguments du type de celui-ci : prenez l’énoncé de « conjectures » telles que le dernier théorème de Fermat :
(Cette dernière est prouvée de nos jours, mais ne l’était pas du vivant de Wittgenstein.) Ou encore la conjecture de Goldbach :
Sur la base d’une sémantique vériconditionnelle, couplée pour les besoins de la cause à une grammaire générative, on peut montrer ce qu’on entend par ces phrases ; nous aurions ici une forme de ce que Hanjo Glock appelle un « compositionnalisme[50] ». Le platoniste peut alors simplement faire valoir qu’on ne peut pas soutenir (1) parce que nous devons bien comprendre (5) ou (6) avant d’en trouver la preuve : comment pourrions-nous chercher une preuve s’il en était autrement ? Si la signification est donnée par la preuve, alors la signification a-t-elle changé en cours de route et comment reconnaîtrions-nous une preuve comme étant celle de l’énoncé de départ ? Et que dire du cas où nous possédons plus d’une preuve d’un énoncé mathématique ? Est-ce à dire qu’un énoncé a autant de significations qu’il a de preuves ? Il existe quelque chose comme 367 preuves du théorème de Pythagore ; sont-elles toutes des variantes d’une même preuve ou doit-on parler de 367 théorèmes de Pythagore ? Prenons par ailleurs le « théorème fondamental de l’algèbre » : il existe une preuve analytique de celui-ci utilisant le théorème de Liouville, une preuve topologique utilisant le théorème du point fixe de Brouwer ; l’étudiant de Wittgenstein, Goodstein, a donné une variante constructive de la deuxième des six preuves de Gauss, pour les polynômes à coefficients algébriques, etc.[51] Ces preuves n’ont a priori rien en commun, doit-on parler d’autant de « théorèmes fondamentaux de l’algèbre » ? En prenant l’exemple imaginaire d’un mathématicien qui aurait exprimé sa croyance en l’existence d’un nombre qui réfuterait la conjecture de Goldbach, Friedrich Waismann, qui avait collaboré avec Wittgenstein dans les années trente, avait formulé ces mêmes objections en visant justement ce dernier, en ces mots :
Assurément, on comprend d’une manière quelconque, ce dont parle un tel mathématicien. Si cela n’était pas le cas et qu’il réussissait par la suite à découvrir un contre-exemple, comment pourrions-nous reconnaître qu’il a obtenu ce qu’il cherchait, et qu’il avait eu raison de croire en l’existence de ce nombre ? […] Comment pourrais-je reconnaître une preuve comme preuve de ce théorème ? Et comment un mathématicien qui travaille sur un problème et le résout sait ce sur quoi il travaille au moment où il travaille sur celui-ci[52] ?
On peut faire valoir que le point de vue platoniste ne va pas de soi pour autant. L’équivalent de l’énoncé (5) établi par Fermat apparaît dans un commentaire imprimé dans l’édition de 1670, l’Arithmetica de Diophante, mais de sa preuve il ajoutait : « Hanc marginis exiguitas non caperet » ; nous ne saurons donc jamais ce qu’elle fut. Nous avons aujourd’hui une preuve de cette conjecture, grâce à un théorème d’Andrew Wiles sur les courbes elliptiques, dont la preuve fait plus d’une centaine de pages[53], un théorème démontré auparavant par Ken Ribet[54] ayant montré qu’il a pour conséquence le dernier théorème de Fermat. La preuve de Wiles a de très nombreux développements que Fermat n’aurait jamais pu anticiper, au point où seuls quelques spécialistes peuvent la comprendre ; on ne voit pas en quoi la simple compréhension « compositionnaliste » de la phrase (5) de la langue française contient en elle-même ces résultats dans un « corps de signification » (Bedetungskörper), que la preuve n’aurait fait que « déballer ». Il ne fait donc guère sens de réduire la signification d’un énoncé mathématique tel que (5) ou (6) à celle, « compositionnelle », de leur correspondant dans la langue française.
On retombe en fait ici exactement sur la position de départ de Wittgenstein : la simple compréhension de l’énoncé (5) est-elle une illusion ou non ? Il ne cherche pas une réponse à cette question dans la mesure où il adhère à un programme « anti-réaliste » ou « constructiviste » quelconque, mais simplement parce qu’il continue à explorer les conséquences de ses positions de départ[55], que nous avons présentées dans la section précédente. Nous avons vu qu’il ne nie certes pas que (5) ou (6) possèdent une signification qui puisse être capturée par une sémantique « compositionnaliste »[56], il insiste uniquement sur l’écart entre cet énoncé et ce qui a été établi par la preuve, donc sur les dangers inhérents à la description du résultat de la preuve dans la Wortsprache. Ayant refusé, comme nous l’avons vu, de reconnaître qu’un énoncé avec quantificateur puisse décrire le résultat d’une preuve par induction, il se retrouve donc face aux problèmes soulevés par le platoniste, et il en est parfaitement conscient. Voilà pourquoi il s’inquiète :
Mon explication ne doit pas faire disparaître les conjectures mathématiques. C’est-à-dire qu’elle ne doit pas avoir pour conséquence que seules les propositions mathématiques qui ont été prouvées sont certainement pourvues de sens[57].
Il relève en effet dès les Remarques philosophiques (composé de remarques datant de 1929-1930), les difficultés liées aux deux cas de figure suivant :
La question se pose donc de savoir si la thèse (1) implique qu’à chaque preuve correspond un énoncé différent, ou si on peut concilier cette thèse avec la possibilité que le même énoncé peut admettre plusieurs preuves sans que son sens change, comme Wittgenstein semble le penser à l’occasion[59]. L’autre cas de figure est bien évidemment celui des « conjectures » :
Le cas (8) des conjectures pose pour Wittgenstein deux difficultés : y a-t-il, avant la donnée d’une preuve, une véritable signification ou seulement des « images » dans notre tête, c’est-à-dire une illusion de compréhension[61] ? D’autre part, la preuve d’une conjecture ne prouverait-elle pas une autre proposition[62] ? Nous n’avons pas l’intention de proposer un exposé détaillé de la façon dont Wittgenstein cherche à résoudre ces difficultés, et nous nous contenterons de faire valoir quelques points minimaux, certes collectivement insuffisants pour résoudre toutes les difficultés soulevées, en relation avec ce qui a été dit[63].
Wittgenstein semble prendre résolument le parti de :
Si une autre citation est encore nécessaire à ce stade-ci, en voici une :
Pourquoi dis-je que nous ne trouvons pas mais que nous construisons une proposition telle que le théorème fondamental de l’algèbre ? — Parce que, en la prouvant, nous lui conférons un sens nouveau dont elle était auparavant entièrement dépourvue. Avant ce que nous appelons preuve, nous n’avions qu’un modèle approximatif de ce sens dans le langage verbal.
Wortsprache[64]
Wittgenstein donne un exemple de cela dans la Grammaire philosophique, avec la conjecture de Gauss sur la distribution des nombres premiers. Si on dénote la quantité de nombres premiers qui ne sont pas plus grands que n par π(n), la densité de ceux-ci pour n nombres naturels sera donnée par π(n)/n. En regardant des tables de nombres premiers, Gauss a remarqué une équivalence asymptotique entre cette densité et 1/log n (avec « log n » pour le logarithme népérien de n), soit :
La preuve de cette conjecture était un sujet de discussion à Cambridge dans les années trente, en particulier autour du livre d’Albert Ingham[65]. Wittgenstein, qui devait en être au courant, se demande simplement si la signification de cette conjecture, laquelle est en quelque sorte « statistique », s’avérera différente de ce qu’une preuve par induction, qui ne l’est pas, montrera :
Comment pourrait-on statistiquement conjecturer ce que la preuve a montré par la suite ?
Comment la preuve peut-elle produire la généralité même que les tentatives antérieures rendaient probable[66] ?
À propos de (7), il est bien évident qu’un théorème comme le théorème fondamental de l’algèbre peut admettre plusieurs preuves dans des « calculs » différents. Une preuve « analytique » n’a pas sa place, par exemple, dans un « calcul algébrique » ; cela serait entre autres jurer contre le principe de la pureté des méthodes (ce théorème n’est pas en soi un théorème de l’algèbre, car il fait appel à des coefficients complexes), mais il n’y a rien dans ce qui précède qui interdise du point de vue de Wittgenstein ce genre de lien entre les calculs. Il est certain, cependant, que la formulation même du théorème change d’une preuve (et son contexte) à l’autre ; que l’on puisse reconnaître qu’il s’agisse du même théorème n’est pas plus un argument contre ce point de vue que de dire de deux échantillons, un « vert pomme », l’autre « vert olive », qu’ils sont « verts » prouve sans plus qu’il y a un universel « vert » que nous devons posséder lorsque nous comprenons le mot « vert ». Par ailleurs, il se peut très bien qu’à l’intérieur d’un même « calcul » plusieurs preuves soient données, mais qu’elles aient quelque chose en commun (nous revenons sur ce point dans notre conclusion).
À propos de (8), Wittgenstein explore dans de nombreux passages, comme celui tout juste cité, le fait que l’énoncé dans une Wortsprache n’a pas un sens déterminé, mais que la preuve vient le préciser. Cette conception est certes discutable — après tout, le platoniste n’abandonnera pas la partie à ce stade-ci — mais il importe dans le cadre de notre texte simplement de voir en quoi elle est en parfaite conformité avec les vues de Wittgenstein sur la preuve de Skolem : c’est l’induction qui donne son sens à l’énoncé dans la Wortsprache dont (4) serait un correspondant dans un « calcul logique », et non l’inverse, d’où les craintes de Wittgenstein vis-à-vis l’intrusion d’un sens, via (4), qui n’est pas présent dans la preuve.
Mais Wittgenstein éprouve, dans des passages comme celui-ci, beaucoup de difficulté à se dépêtrer d’une des conséquences fâcheuses de son point de vue, à savoir qu’une question ne peut avoir de sens que lorsque nous possédons une méthode pour en trouver la réponse :
Avant la preuve, poser la question à propos de la proposition générale n’avait pas de sens, donc ce n’était même pas une question, car la question n’aurait eu de sens que si nous avions connu une méthode générale de décision avant de connaître la preuve particulière.
La preuve par induction ne tranche pas une question disputée[67]
traduction modifiée
De nombreuses conjectures, comme celle désormais résolue du dernier théorème de Fermat (5) ou celle encore non résolue de Goldbach, ne sont justement pas de cet ordre — en fait, de grands pans des mathématiques ont été conçus par des tentatives, comme celle de Kummer, de prouver le dernier théorème de Fermat[68]. On notera cependant que les difficultés auxquelles Wittgenstein fait face ne donnent pas pour autant la partie au platoniste : si la simple compréhension « compositionnaliste » du dernier théorème de Fermat (5) nous avait donné au départ une signification suffisamment précise de son sens, nous en aurions trouvé un peu plus facilement la preuve[69]. Une explication non superficielle du sens des conjectures mathématiques reste donc un problème d’intérêt commun, et non une simple embûche pour les constructivistes.
4. Remarques sur l’évolution de la logique et notre compréhension de ces problèmes
Ces quelques remarques ne font qu’effleurer les propos de Wittgenstein sur ces questions ; il reste encore beaucoup à faire pour le suivre dans les méandres de sa pensée, mais nous avons en quelque sorte esquissé les prolégomènes pour toute étude future de la défense de (1) par Wittgenstein, face aux contre-exemples que l’on peut tirer de (7) ou (8). Les remarques des sections 2 et 3 sont le bottom line. L’idée centrale de ce texte était donc de faire valoir l’importance des thèses dégagées dans la section 2 pour la compréhension de la particularité du point de vue de Wittgenstein sur la thèse (1), et par suite sur la question des conjectures en mathématiques ; aucune étude sérieuse de ces questions ne peut en faire l’économie[70]. Nous n’avons pas non plus cherché à défendre le point de vue de Wittgenstein, dans la mesure où nous avons pu en présenter les grandes lignes. Cependant, puisque ses remarques sont souvent sujettes à une réfutation facile[71], nous aimerions conclure en tissant rapidement des liens avec des développements en logique que Wittgenstein n’a certes pas anticipé, mais qui confirment en quelque sorte ses thèses.
Ces développements ont pour base ce qu’on appelle « l’isomorphisme de Curry-Howard »[72], dont on pourrait dire sans trop exagérer qu’il s’agit d’une ligne de partage des eaux dans l’histoire de la logique au siècle dernier. Il ne s’agit pas au sens propre d’un « isomorphisme » ou même d’un théorème, mais d’une « correspondance » — comme ce genre de lien entre calculs que semblait privilégier Wittgenstein —, qui est établie entre un « calcul logique » et un « calcul fonctionnel » au sens défini ci-dessus, soit plus précisément entre le système de déduction naturelle intuitionniste et le calcul lambda simplement typé ou encore, plus précisément, entre la normalisation des preuves en déduction naturelle intuitionniste et l’exécution d’un programme par réduction d’un lambda terme. L’établissement de cette correspondance permet de voir l’énoncé mathématique comme « type », c’est-à-dire comme type de ses preuves, et d’extraire de la preuve constructive de cet énoncé en déduction naturelle intuitionniste un algorithme dans un langage de programmation (les liens entre logique et informatique s’en trouvent considérablement resserrés et approfondis). Se dégage ainsi un paradigme, celui de la « proposition comme type », dans lequel la signification d’un énoncé mathématique est directement liée à ses preuves, puisqu’une correspondance entre un « calcul logique » et un « calcul fonctionnel » y est établie, confirmant aussi par là même la sémantique BHK de la logique intuitionniste[73]. La correspondance a été établie vers 1969, et le texte de Howard, publié seulement en 1980, circula entre temps et fut à l’origine de très nombreux développements dont, très rapidement, le système Automath de Nicolaas de Bruijn[74], le système F de Jean-Yves Girard[75] et la théorie des types intuitionniste de Per Martin-Löf[76].
Jean-Louis Krivine a par la suite étendu la correspondance de Curry-Howard à la logique classique et même à la théorie des ensembles[77], confirmant, pourrait-on dire, les tendances anti-révisionnistes de Wittgenstein[78]. Ses travaux sur la correspondance de Curry-Howard sont liés à ce qu’il appelle le « problème de la spécification[79] », qui est celui de trouver le « comportement commun » de toute preuve d’un théorème. Cette notion de « comportement commun » peut être vue comme faisant justice aux idées de Wittgenstein ou plus généralement à la thèse (1) contre ses adversaires « compositionnalistes », puisque le sens d’un théorème y est analysé en termes de « comportement commun » de ses preuves[80].
Le lecteur attentif aura remarqué que la discussion des cas (7) et (8), ci-dessus, s’était déroulée dans un cadre informel, tandis que les remarques des paragraphes précédents portent sur un cadre où les preuves sont formalisées ; on peut se demander si ce glissement de sens est justifié aux yeux de Wittgenstein. L’attitude de ce dernier envers la formalisation des preuves est difficile à cerner, dans la mesure où il s’est opposé, avec des arguments comme celui sur le caractère « synoptique » (Übersichtlichkeit) des preuves[81], à la formalisation des preuves dans le langage des Principia Mathematica. Il se peut donc que ces remarques puissent ne pas refléter fidèlement son point de vue, mais il reste que, selon nous, la discussion d’une thèse comme (1) ne peut admettre véritablement de résolution que dans un cadre de formalisation des preuves, donc, aujourd’hui, dans le cadre des développements qui ont suivi l’établissement de la correspondance de Curry-Howard ; envisager la question sous cette optique devrait permettre de formuler des arguments en faveur de (1), qui montrent au moins que les idées de Wittgenstein ne sont pas naïves et fausses, même s’il n’avait peut-être pas reconnu la valeur de ces arguments[82].
Parties annexes
Notes
-
[1]
Hardy 1929, 18.
-
[2]
Voir Marion 2011a.
-
[3]
Voir Putnam 1996, 249, n. 15, Putnam 2001, Appendice. Putnam semble motivé par un programme « anti-anti-réaliste », c’est-à-dire par la volonté de lire Wittgenstein comme n’ayant pas soutenu de thèses qui sont communes aux « anti-réalistes », tels que Dummett. C’est l’exemple même d’une lecture idéologique de Wittgenstein, où on cherche à lui faire jouer un rôle qui n’était pas le sien, dans un débat dont il ne pouvait même pas soupçonner l’existence, plutôt que de chercher à comprendre ce qu’il a bien pu vouloir dire.
-
[4]
Quiconque porté à penser le contraire devrait lire Putnam 2007.
-
[5]
Wittgenstein 1975, § 163.
-
[6]
Ibid., § 148.
-
[7]
Wittgenstein 1980, 375.
-
[8]
Ibid., 380.
-
[9]
On découpe en général la philosophie de Wittgenstein en au moins trois périodes, soit celle du « premier Wittgenstein », de ses débuts à la publication du Tractatus (1911-1921) et l’abandon de toute activité philosophique, suivie la période « intermédiaire » ou de « transition », s’étendant de son retour à la philosophie en 1929 à (l’année précédant) la rédaction de la première version des Recherches philosophiques, et du « deuxième Wittgenstein », de 1936 jusqu’à sa mort. (Certains commentateurs distinguent une quatrième période, autour des écrits tardifs comme De la certitude.) Cette périodisation, basée sur les deux grandes oeuvres que sont le Tractatus et les Recherches philosophiques, est selon nous extrêmement problématique, car ce n’est qu’un découpage conventionnel : il induit une image nécessairement fausse dont on se sert par la suite dans la littérature secondaire à l’appui de thèses sans fondement. Il faut aussi dénoncer une propension sidérante chez les commentateurs à sous-évaluer les écrits de la période « intermédiaire », sous prétexte d’une évolution vers les positions du « deuxième Wittgenstein », que l’on devrait seules prendre au sérieux, comme si elles pouvaient être interprétées de par elles-mêmes sans explication génétique de leur origine dans le reste de l’oeuvre ; en somme, les écrits de la période « intermédiaire » ne seraient que des brouillons sans grand intérêt intrinsèque. Ce genre de bêtise exégétique devient patent lorsqu’on parle de philosophie des mathématiques, avec la tactique habituelle contre l’attribution de thèses à Wittgenstein sur la base de ses écrits de la période « intermédiaire » : on dit alors que cela n’est que le reflet de cette période sans intérêt et qu’il y aurait eu évolution de sa pensée vers une philosophie des mathématiques du « deuxième Wittgenstein ». Ce propos est pourtant dénué de tout fondement, pour la simple raison qu’il n’y a pas de chose telle qu’une « deuxième » philosophie des mathématiques, comme le souligne avec justesse Michael Potter dans (Potter 2011, 135-136) — ce texte contient par ailleurs une évaluation très négative des positions de Wittgenstein que nous ne partageons pas. Lorsqu’on attribue certaines thèses de philosophie des mathématiques au « deuxième Wittgenstein », ce sont généralement des thèses dont l’origine se trouve dans les manuscrits de la période 1929-1933. Pour ne prendre qu’un exemple, lorsqu’on demande ce que pourrait être une thèse ou un argument typique de cette « deuxième » philosophie des mathématiques, on songe tout naturellement à l’argument sur le caractère « synoptique » des preuves, qui est un des principaux arguments de l’étrange choix de textes posthumes publiés sous le titre Remarques sur les fondements des mathématiques. Cet argument est censé refléter les dernières positions de Wittgenstein, or on ne peut soutenir ce point de vue que par ignorance des textes, puisqu’il est énoncé par Wittgenstein pour la première fois en… 1929 ! Voir (Wittgenstein 1991, 3) et la discussion de cet argument dans (Marion 2011b). Il n’y a donc pas, a fortiori, d’évolution vers des positions « tardives » de Wittgenstein sur les mathématiques, et par le fait même aucune raison valable d’ignorer les écrits de la période « intermédiaire ». Seul le poids des préjugés est en cause ; ceux-ci bloquent l’accès aux textes et à une meilleure compréhension de la pensée de Wittgenstein.
-
[10]
Cette remarque est tirée du MS 127, p. 161 et manque à l’appel dans Wittgenstein 1983, V, § 42.
-
[11]
Cette thèse est à la base de son argument célèbre sur la manifestation de la compréhension, voir Dummett 1991a, 79sq. Dummett est sur ce point plus proche de Frege que de Wittgenstein, et cela ressort clairement dans Dummett 1991, 294-295.
-
[12]
Les passages du Tractatus dans ce texte sont tirés de Wittgenstein (1993).
-
[13]
Voir, par exemple, Marion 2004a, 85-109. On notera que Dummett lui-même avait adopté tardivement une interprétation similaire de Wittgenstein, défendue à l’époque dans Marion 1991, selon laquelle les énoncés mathématiques ne feraient « qu’encoder des instructions pour des calculs » (Dummett 1991b, 294), mais qu’il s’y opposait, prenant plutôt le parti, platoniste, de Frege, comme nous le mentionnions à la note 11.
-
[14]
Wittgenstein 1991, 79.
-
[15]
Wittgenstein 1980, 473 ; voir aussi, par exemple, Wittgenstein 1975, § 157.
-
[16]
Plusieurs lectures de Wittgenstein, dominantes depuis quelques décennies, proposent une vision de sa pensée selon laquelle il n’a pas cherché à prendre part aux débats philosophiques de son époque (sur les mathématiques et leurs fondements en particulier), ni même cherché à énoncer quelque « thèse » que ce soit, son discours se réduisant essentiellement à une critique de l’usage de « thèses » par d’autres philosophes, sans pour autant en soutenir une seule lui-même. Nous ne partageons pas ces lectures, qui sont en fait idéologiques, puisqu’elles consistent à utiliser Wittgenstein pour critiquer certaines thèses en philosophie analytique contemporaine ; leur résultat ayant été non pas d’infléchir le cours de la philosophie, comme tout radicalisme rêve de le faire, mais seulement de marginaliser considérablement Wittgenstein, voire de l’exclure du « canon » analytique. Pour des arguments à l’appui de notre approche, voir Marion, 2004b, et Marion, 2008a.
-
[17]
On doit cette analyse conceptuelle à Turing, voir Gandy 1980, 124.
-
[18]
Pour la distinction entre ces types de « calculs logiques », voir Sundholm, 2001.
-
[19]
Cette distinction est reprise de Wagner, 1998, 159-160.
-
[20]
Voir Marion et Okada (à paraître), portant entre autres sur la conception de la preuve par induction mathématique de Wittgenstein et ses réflexions sur une preuve de Skolem, discutée dans cette section, qui l’ont mené à une « règle d’unicité » qui sera reprise par son étudiant R. L. Goodstein. Ces questions sont discutées dans Marion 1998, 103-109, et Okada (2007) est une contribution essentielle à leur compréhension, discutée par la suite dans Marion (2009), texte qui a servi de base aux recherches actuelles dont Marion et Okada (à paraître) est le premier résultat.
-
[21]
Voir Marion 2011a, 142-144.
-
[22]
Sur cette question, voir Dummett 1981, 432-435, et Hacking 1976, 288sq.
-
[23]
Cette thèse est discutée longuement, dans un autre contexte, dans Marion 2008b.
-
[24]
Wittgenstein 1980, 403.
-
[25]
Frege et Russell donnèrent de ce principe des versions plus complexes, au second ordre, mais cela n’est pas important dans le contexte de ce texte.
-
[26]
Voir Goodstein 1945, 407, pour le premier énoncé de la règle, et Goodstein 1957 (Théorèmes 2.8 & 3.7-3.81).
-
[27]
Voir sur cette question Okada 2007 et Marion et Okada (à paraître), qui corrige et prolonge sur certains points les analyses de Marion 2009.
-
[28]
Dans un article de 1923, intitulé « Begründung der elementaren Arithmetik durch die rekurrierende Denkweise ohne Anwendung scheinbarer Veränderlichen mit unendlichen Ausdehnungsbereich » ; nous utilisons la traduction anglaise de Skolem 1967, puisque l’original allemand est pratiquement impossible à trouver.
-
[29]
Nous donnons ci-dessous une version légèrement modifiée de Skolem 1967, 305-306.
-
[30]
Voir Okada 2007, 123.
-
[31]
Skolem 1967, 332-333.
-
[32]
Tout cela est en accord avec la critique de la théorie de la quantification par Wittgenstein ; voir Marion 1998, chap. 4.
-
[33]
Pour une discussion détaillée, voir Marion et Okada (à paraître).
-
[34]
Wittgenstein 1975, § 163.
-
[35]
Wittgenstein 1975, § 168.
-
[36]
Wittgenstein 1980, § 416.
-
[37]
Wittgenstein 1991, 110-111.
-
[38]
Wittgenstein 1975, § 164.
-
[39]
On notera la présence de la distinction entre « dire » et « montrer », encore à l’oeuvre dans les deux passages suivants, alors même que certaines lectures contemporaines, regroupées sous le nom de « New Wittgenstein », ont pour but de démontrer que dès le Tractatus, Wittgenstein considérait cette distinction comme le prototype du non-sens à l’état pur. Voir sur ce point Marion 2009, 201sq., et Marion et Okada (à paraître).
-
[40]
Wittgenstein 1975, § 168.
-
[41]
Wittgenstein 1980, 412.
-
[42]
Sur cette question, voir Marion et Okada (à paraître).
-
[43]
Wittgenstein 1975, § 167.
-
[44]
Wittgenstein 1980, 428.
-
[45]
Pour la même conclusion à partir de l’argument sur le caractère « synoptique » des preuves, voir Marion 2011b, 156.
-
[46]
À propos de cette remarque très importante, voir Okada 2007, 127-128.
-
[47]
On dirait de nos jours qu’une langue comme le français est le métalangage dans lequel on peut parler d’une théorie mathématique langage objet, mais c’est précisément ce que Wittgenstein se refuse à dire, d’où sa tentative de dissoudre les usages de mots du français dans l’élaboration simple d’algorithmes.
-
[48]
Pour une discussion des rapports entre Wittgenstein et l’intuitionnisme de Brouwer voir Marion 1998, chap. 6, Marion 2003, Marion 2008c, et Marion 2011a.
-
[49]
Wittgenstein 1980, 408. Voir aussi Wittgenstein 1980, 427, à propos de la règle d’unicité discutée dans Marion et Okada (à paraître).
-
[50]
Glock 1996, 231.
-
[51]
Voir Boas 1987, Fine & Rosenberger 1997, Goodstein 1969.
-
[52]
Waismann 1982, 37-38.
-
[53]
C’est le théorème 5.2 dans Wiles 1995, 542.
-
[54]
C’est le corollaire 1.2 de Ribet 1990, 432.
-
[55]
De nombreux commentateurs de Wittgenstein s’opposent aux idées exprimées dans ce texte parce qu’ils craignent l’embrigadement de leur philosophe préférée dans des programmes philosophiques pour lesquels ils éprouvent, pour quelque raison que ce soit, une aversion. Ce que nous essayons de faire n’est justement pas de confondre les idées de Wittgenstein avec, par exemple, l’anti-réalisme de Dummett, mais nous ne le faisons pas au point d’émasculer sa pensée ou encore au point, littéralement, de s’interdire de la comprendre.
-
[56]
Voir les citations de Wittgenstein 1975, § 148 ; Wittgenstein 1980, 375 ; et MS 127, 161, en début d’article, qui présupposent toutes cette thèse.
-
[57]
Wittgenstein 1975, § 148.
-
[58]
Voir, par exemple, Wittgenstein 1975, § 155.
-
[59]
Voir Wittgenstein 1983, III § 58 et 60 ; VII, § 10.
-
[60]
Voir, par exemple, Wittgenstein 1975, § 148, déjà cité.
-
[61]
Voir, par exemple, Wittgenstein 1983, VII, § 10.
-
[62]
Voir, par exemple, Wittgenstein 1975, § 151.
-
[63]
On notera au moins que la discussion de ces difficultés par Wittgenstein montre qu’il prenait très au sérieux la thèse (1), contrairement à ce que certains ont laissé entendre, comme Putnam, cité dans la note 3 ci-dessus.
-
[64]
Wittgenstein 1980, 428.
-
[65]
Ingham 1932.
-
[66]
Wittgenstein 1980, 367.
-
[67]
Wittgenstein 1980, 408.
-
[68]
Sur ce point, voir Säätelä 2011.
-
[69]
Comme le remarque Wright 1980, 50. Notons que, comme nous le disions, Fermat disait posséder une preuve, mais comme il ne l’a pas donnée, on ne peut pas supposer sans plus qu’elle était valide ; peut-être ne l’était-elle pas.
-
[70]
Il existe plusieurs études qui ne satisfont pas tout à fait, malgré leurs mérites respectifs, ce critère, parce que la particularité du point de vue de Wittgenstein, présentée dans la section 2, n’y est pas pleinement comprise. Voir Ambrose 1966, Wright 1980, 39-56, Diamond 1991 et Säätelä 2011.
-
[71]
Voir, ci-dessus, les critiques de Waismann ; pour un exemple récent, voir Potter 2011, 127-129.
-
[72]
Voir Howard 1980. Cet « isomorphisme » ne peut pas être présenté dans le cadre de ce texte ; pour une présentation en français, voir Coquand 1980, ou celles plus accessibles pour un philosophe de Joinet 2009 et de Wagner 1998, 163-185. Le texte de Joinet peut être vu comme une introduction à la révolution en logique et en philosophie de la logique provoquée par la correspondance de Curry-Howard.
-
[73]
Voir Martin-Löf 1984, 6.
-
[74]
Voir Nederpelt, Geuvers et de Vrijer 1994.
-
[75]
Voir Girard 1971.
-
[76]
Voir Martin-Löf 1973, et l’exposé de Martin-Löf 1984.
-
[77]
Voir Krivine 1996, Krivine 2001, Krivine 2009.
-
[78]
Comme le suggère Pascal Boldini (Boldini 2004, 446).
-
[79]
Krivine 2005, 198.
-
[80]
Nous devons cette suggestion à Jean-Baptiste Joinet (Joinet 2009, 41-42).
-
[81]
Sur cet argument, voir Marion 2011b.
-
[82]
Une première version de ce texte avait été rédigée par Mathieu Marion pour le colloque Wittgenstein’s Philosophy of Mathematics, organisé par Laurence Goldstein, et qui s’est déroulé à l’Université de Kent, Canterbury, le 27 et 28 janvier 2006. Il aimerait remercier Juliet Floyd, Neil Kennedy, Hartley Slater et, surtout, Peter Sullivan pour les commentaires qu’il avait reçus à cette époque. Le travail entrepris depuis en collaboration avec Mitsuhiro Okada a mené à une meilleure compréhension des idées de Wittgenstein, telles qu’exposées dans la section 2, ce qui a mené à une refonte du texte original (dont il ne reste surtout des éléments que dans les sections 1 et 3). Nous devons en outre à une discussion avec Jean-Baptiste Joinet les remarques contenues dans la conclusion. En dernier lieu, nous aimerions remercier Bento Prado Neto et João Vergílio Gallerani Cuter, de nous avoir donné l’occasion de réécrire ce texte, et pour leur patience à notre égard.
Bibliographie
- Ambrose, A. « Proof and the Theorem Proved », dans Essays in Analysis, Londres, Allen & Unwin, 1966, 13-25.
- Boas, R. P. Invitation to Complex Analysis, New York, Random House, 1987.
- Boldini, P. « La priorité de la preuve : le cas de la signification non standard des constantes non logiques », Revue internationale de philosophie, no 230, 2004, 437-447.
- Coquand, T. « Sur l’analogie entre les propositions et les types », dans G. Cousineau, P.-L. Curien et B. Robinet (dir.), Combinators and Functional Programming Languages, Berlin, Springer, 1986, 71-84.
- Diamond, C. « Riddles and Anselm’s Riddle », dans The Realistic Spirit. Wittgenstein, Philosophy, and the Mind, Cambridge MA, MIT Press, 1991, 267-289.
- Dummett, M. A. E. Frege. Philosophy of Language, 2e éd., Londres, Duckworth, 1981.
- Dummett, M. A. E. Philosophie de la logique, Paris, Éditions de Minuit, 1991a.
- Dummett, M. A. E. Frege. Philosophy of Mathematics, Londres, Duckworth, 1991b.
- Fine, B. et G. Rosenberger. The Fundamental Theorem of Algebra, Berlin, Springer, 1997.
- Gandy, R. O. « Church’s Thesis and Principles for Mechanisms », dans The Kleene Symposium, J. Barwise, H. J. Keisler et K. Kunen (dir.), Amsterdam, North Holland, 1980, 123-148.
- Girard, J.-Y. « Une extension de l’interprétation fonctionnelle de Gödel à l’analyse et son application à l’élimination des coupures dans l’analyse et la théorie des types », dans Proceedings of the 2nd Scandinavian Logic Symposium, J. E. Fenstad (dir.), Amsterdam, North-Holland, 1971, 63-92.
- Glock, H.-J. A Wittgenstein Dictionary, Oxford, Blackwell, 1996.
- Goodstein, R. L. « Function Theory in an Axiom-Free Equation Calculus », Proceedings of the London Mathematical Society, vol. 48, 1945, 401-434.
- Goodstein, R. L. Recursive Number Theory, Amsterdam, North-Holland, 1957.
- Goodstein, R. L. « A Constructive Form of the Second Gauss Proof of the Fundamental Theorem of Algebra », dans Constructive Aspects of the Fundamental Theorem of Algebra, B. Dejon et P. Henrici (dir.), London, John Wiley & Sons, 1969, 69-76.
- Hacking, I. « What is Logic ? », Journal of Philosophy, vol. 76, 1976, 296-319.
- Hardy, G. H. « Mathematical Proof », Mind, n.s., vol. 38, 1929, 1-25.
- Howard, W. A. « The Formulae-as-Types Notion of Construction », dans To H. B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism, J. P. Seldin et J. R. Hindley (dir.), Londres, Academic Press, 1980, 479-490.
- Ingham, A. E. The Distribution of Prime Numbers, Cambridge, Cambridge University Press, 1932.
- Joinet, J.-B. « Introduction », dans Ouvrir la logique au monde. Philosophie et mathématique de l’interaction, J.-B. Joinet et S. Tronçon (dir.), Paris, Hermann, 2009, 9-63.
- Krivine, J.-L. « Une preuve formelle et intuitionniste du théorème de complétude de la logique classique », Bulletin of Symbolic Logic, vol. 2, 1996, 405-421.
- Krivine, J.-L. « Typed Lambda Calculus in Classical Zermelo-Fraenkel Set Theory », Archive of Mathematical Logic, vol. 40, 2001, 189-205.
- Krivine, J.-L. « Realizability in Classical Logic », Panoramas et synthèses, vol. 27, 2009, 197-229.
- Marion, M. Quantification and Finitism. A Study in Wittgenstein’s Philosophy of Mathematics, thèse de doctorat, Université d’Oxford, 1991.
- Marion, M. Wittgenstein, Finitism and the Foundations of Mathematics, Oxford, Clarendon Press, 1998.
- Marion, M. « Wittgenstein and Brouwer », Synthese, vol. 137, 2003, 103-127.
- Marion, M. Ludwig Wittgenstein. Introduction au Tractatus logico-philosophicus, Paris, P.U.F., 2004a.
- Marion, M. « Wittgenstein on Mathematics : Constructivism or Constructivity ? », dans Wittgenstein Today, A. Coliva et E. Picardi (dir.), Padoue, Il Poligrafo, 2004b, 201-222.
- Marion, M. « Wittgenstein et le constructivisme », dans Wittgenstein. État des lieux, E. Rigal (dir.), Paris, Vrin, 2008a, 261-273.
- Marion, M. 2008b, « Rationality from a Logical Point of View », dans Action, Attitudes et Décision, D. Fisette et D. Vanderveken (dir.), Londres, College Publications, 2008, 339-359.
- Marion, M. « Brouwer on Hypotheses and the Middle Wittgenstein », dans One Hundred Years of Intuitionism 1907-2007. The Cerisy Conference, M. van Atten, P. Boldini, M. Bourdeau et G. Heinzmann (dir.), Basel, Birkhäuser, 2008c, 96-114.
- Marion, M. « Jogando o bebê junto com a água do banho : Wittgenstein, Goodstein e o cálculo equacional », Revista Dois Pontos, vol. 6, no 1, 2009, 195-246.
- Marion, M. « Wittgenstein et la preuve mathématique comme vérifacteur », Philosophiques, vol. 38, no 1, 2011a, 137-156.
- Marion, M. « Wittgenstein on the Surveyability of Proofs », dans The Oxford Handbook on Wittgenstein, M. McGinn et O. Kuusela (dir.), Oxford, Clarendon Press, 2011b, 138-161.
- Marion, M. et M. Okada. « Wittgenstein and Goodstein on the Equation Calculus and the Uniqueness Rule », à paraître.
- Martin-Löf, P. « An Intuitionistic Theory of Types », dans Logic Colloquium ‘73, H. E. Rose et J. Sheperdson (dir.), Amsterdam, North-Holland, 1973, 73-118.
- Martin-Löf, P. Intuitionistic Type Theory, Naples, Bibliopolis, 1984.
- Nederpelt, R. P., J. H. Geuvers et R. C. de Vrijer (dir.). Selected Papers on Automath, Amsterdam, Elsevier, 1994.
- Okada, M. « On Wittgenstein’s Remarks on Recursive Proofs : A Preliminary Report », dans Essays in the Foundations of Logical and Phenomenological Studies, M. Okada (dir.), Tokyo, Keio University Press, 2007, 121-131.
- Potter, M. « Wittgenstein on Mathematics », dans The Oxford Handbook on Wittgenstein, M. McGinn et O. Kuusela (dir.), Oxford, Clarendon Press, 2011, 122-137.
- Putnam, H. « On Wittgenstein’s Philosophy of Mathematics », Proceedings of the Aristotelian Society. Supplementary Volume LXX, 1996, 243-264.
- Putnam, H. « Was Wittgenstein Really an Anti-realist about Mathematics ? », dans Wittgenstein in America, T. McCarthy et S. C. Stidd (dir.), Oxford, Clarendon Press, 2001, 140-194.
- Putnam, H. « Wittgenstein and the Real Numbers », dans Wittgenstein and the Moral Life. Essays in Honor of Cora Diamond, A. Crary (dir.), Cambridge MA, MIT Press, 2007, 235-250.
- Ribet, K. « On Modular Representations of GAL(Q/Q) Arising from Modular Forms », Inventiones Mathematicae, Vol. 100, 1990, 431-476.
- Säätelä, S. « From Logical Method to ‘Messing about’ : Wittgenstein on ‘Open Problems’ in Mathematics », dans The Oxford Handbook on Wittgenstein, M. McGinn et O. Kuusela (dir.), Oxford, Clarendon Press, 2011, 162-180.
- Skolem, T. « The Foundations of Elementary Arithmetic established by Means of the Recursive Mode of Thought, without Use of Apparent Variables Ranging over Infinite Domains », in From Frege to Gödel. A Sourcebook in Mathematical Logic, 1879-1931, J. van Heijenoort (ed.), Cambridge MA, Harvard University Press, 1967, 303-333.
- Sundholm, G. « Systems of Deduction », dans Handbook of Philosophical Logic, 2e éd., D. M. Gabbay et F. Günther (dir.), Dordrecht, Kluwer, vol. 2, 2001, 1-52.
- Wagner, P. La machine en logique, Paris, P.U.F., 1998.
- Waismann, F. Lectures on the Philosophy of Mathematics, Amsterdam, Rodopi, 1982.
- Wiles, A. « Modular Elliptic Curves and Fermat’s Last Theorem », Annals of Mathematics, vol. 142, 1995, 443-551.
- Wittgenstein, L. Remarques philosophiques, Paris, Gallimard, 1975.
- Wittgenstein, L. Grammaire philosophique, Paris, Gallimard, 1980.
- Wittgenstein, L. Remarques sur les fondements des mathématiques, Paris, Gallimard, 1983.
- Wittgenstein, L. Wittgenstein et le Cercle de Vienne. D’après les notes de Friedrich Waismann, Mauvezin, T. E. R, 1991.
- Wittgenstein, L. Tractatus Logico-Philosophicus, Paris, Gallimard, 1993.
- Wright, C. J. G. Wittgenstein on the Foundations of Mathematics, London, Duckworth, 1980.