Langage et signification : le cas des mathématiques constructives
Apparues au début du siècle précédent avec l’intuitionnisme de Brouwer, les mathématiques constructives n’ont été longtemps qu’un courant très minoritaire dans les mathématiques modernes ; courant qui s’est scindé de plus en différentes écoles - l’intuitionnisme proprement dit, les mathématiques constructives dans le style de Bishop, l’école de Markov etc - dont chacune défend sa propre conception de la constructivité. Les mathématiques qui en résultent à chaque fois sont parfois incompatibles, non seulement avec les mathématiques classiques, mais aussi entre elles. Un accord minimal règne malgré tout autour du refus de certaines règles d’inférence communément admises, à commencer par celles qui expriment le tiers exclu, et de l’adoption d’une logique dite intuitionniste, celle-ci étant tenue pour une condition nécessaire, mais non suffisante, pour s’assurer de la constructivité des démonstrations. L’on attend d’une démonstration constructive dans le cas d’une proposition existentielle comme "il existe des x ayant la propriété A" qu’elle donne une méthode permettant de produire un individu a ayant la propriété A ; l’on ne se contente pas alors d’une ???pure’ preuve d’existence assurant seulement qu’il serait absurde qu’il n’en existe pas. Par delà le fait que la seconde preuve est moins informative que la première, ce qui est difficilement contestable, ce refus se justifie traditionnellement par des considérations ontologiques : la preuve non constructive présupposerait que l’individu a existe indépendamment des moyens dont on dispose pour s’en assurer. Pour le dire autrement, la vérité dans le cas classique peut relever d’un simple constat d’existence d’entités qui restent, en quelque sorte, cachées ou inconnues, dans le cas constructif elle dépend toujours d’un acte de construction de ces entités qui en donne, au moins en principe, une connaissance directe.
Brouwer, pour des raisons complexes, a développé une ???contre-mathématique’ permettant de prouver des théorèmes classiquement inadmissibles. Ce qui explique qu’elle ait rencontré au mieux l’indifférence de la quasi-totalité de la communauté des mathématiciens, au pire l’hostilité affichée de certains ; la seule exception notable étant celle de Weyl qui lui fut un temps favorable. Bishop a proposé par la suite une reconstruction constructive des mathématiques restant dans les limites de ce qui est classiquement acceptable ; ce qui contribua à assurer à son entreprise une audience un peu plus étendue. Assez paradoxalement, compte tenu des préventions de Brouwer et de l’indifférence de Bishop vis à vis de toute (méta)mathématique et de l’axiomatique formelle, les mathématiques constructives auront surtout retenu l’attention des logiciens, plus précisément des théoriciens de la démonstration et de la calculabilité et ceci pour deux raisons.
Tout d’abord, l’échec du programme de Hilbert, qui demandait de n’employer que des moyens extrêmement restreints, finitistes, dans l’étude (méta)mathématique des axiomatiques formelles, indiqua clairement qu’une extension de ces moyens était nécessaire ; or, justement, certains de ceux admis par les constructivistes se révélèrent être exactement les outils voulus.
Ensuite, on en vint à découvrir que les preuves formelles constructives possèdent des propriétés structurelles qui permettent, non seulement de comprendre pourquoi elles sont constructives, mais aussi d’établir un lien direct avec la théorie de la calculabilité formelle. C’est la correspondance de Curry-Howard qui montre qu’une preuve constructive a toutes les propriétés d’un programme ; plus précisément que les règles de démonstration permettent d’écrire des programmes corrects, i.e. satisfaisant leur spécification donnée à chaque fois par le théorème démontré, et que des règles spécifiques de transformation de ces preuves sont des règles de calcul de l’algorithme obtenu. Ce qui répondait justement aux attentes des informaticiens dont certains, comme par exemple Hoare, avaient assez vite compris que seuls des outils théoriques empruntés à la logique mathématique permettraient de contrôler systématiquement la correction des programmes employés en pratique.
Bishop en son temps avait largement pressenti la possibilité d’interpréter au moinspartiellement ses mathématiques en leur donnant une ???signification en terme de calcul’["computational meaning"] afin de relier la Science des mathématiques et l’Art de laprogrammation des machines. Les résultats obtenus sont venus dépasser ses attentes puisquetoutes les mathématiques constructives peuvent désormais faire l’objet d’une interprétationinformatique ; bien mieux, la correspondance de Curry-Howard a été étendue auxmathématiques classiques. En se restreignant au cas des seules mathématiques constructives,il est possible aujourd’hui de s’interroger sur la pertinence de leur interprétation informatiqueau regard des conceptions philosophiques qui sont invoquées traditionnellement en leur faveur: que ce soit chez Brouwer, Bishop ou, plus récemment, chez Dummett et Martin-Löf, l’idéedominante est que les ???véritables’ mathématiques résultent d’une activité mentale dépendantdes significations qu’un sujet peut conférer au langage qu’il emploie ; le rôle et l’importancede ce dernier étant diversement appréciés selon les auteurs. Cette conception est à tout lemoins très éloignée des considérations informatiques qui précèdent, au point que l’on peuts’interroger sur la nécessité même de les prendre en compte dans un travail consacré auxrapports qu’entretiennent langage et signification dans le cas des mathématiques constructives. Une comparaison avec les mathématiques classiques permet sans doute demieux comprendre pourquoi on doit au contraire prendre cette interprétation très au sérieux.
Dans le cas des mathématiques classiques, une des approches (méta)mathématiquesdes axiomatiques formelles, à bien des égards la plus fertile mathématiquement, est celle de lathéorie des modèles. A un langage formalisé L, c’est-à-dire un langage dépourvu de toutesignification mathématique, correspond la classe des L-modèles définie dans le(méta)langage ; chacun de ces modèles permettant d’interpréter les symboles de L par desentités mathématiques de type approprié. Une axiomatique formelle T est alors un ensemblede formules de L et la définition de la satisfiabilité d’une formule dans un modèle, due pourune bonne part à Tarski, joue alors un double rôle : elle permet d’interpréter les axiomes de Tdans chacune de ces structures, donc de leur donner une signification, tout en leur attribuantune valeur de vérité. Ces structures étant des structures ensemblistes, cette valeur de vérité estelle-même une entité mathématiquement définie : c’est un élément de l’ensemble de based’une algèbre de Boole et des opérations définies sur cet ensemble permettent de donner uneinterprétation mathématique aux constantes logiques du langage L. La validité d’une formuleclose de L est alors définie comme sa vérité dans tout L- modèle. Dès lors que T prétend êtreune axiomatisation formelle d’un fragment du langage contentuel des mathématiquesclassiques, plusieurs questions devraient se poser. En quoi sommes nous assurés que
(i) parmi ses L-modèles s’en trouvent certains qui sont la, ou les, interprétation(s)
attendue(s), intuitive(s), de ce fragment ?
(ii) les éléments de l’ensemble de base d’une algèbre de Boole sont des valeurs de
vérité, au sens intuitif du mot "vérité" ?
(iii) la validité mathématiquement définie est bien la notion intuitive de vérité logique
ou nécessaire ?
En un sens, la réponse à chacune de ces questions est immédiate et elle est négative.Aucune de ces définitions ne prétend ???être’ la notion intuitive correspondante ; l’on en attendtout au plus qu’elle en soit une représentation mathématique suffisamment adéquate pour quel’approche "model theoretic" puisse prétendre avoir une pertinence quant aux mathématiquesclassiques. Dès lors que les questions (i)-(iii) sont ainsi reformulées, l’accord est à peu prèsgénéral sur les réponses à leur donner : elle est à chaque fois positive. On peut invoquer en (i)le fait qu’un modèle, au sens de la théorie classique des modèles, est purement et simplementune structure ensembliste, qu’il en va de même des entités mathématiques prises dans cettestructure afin d’interpréter les symboles d’un langage formalisé L et, enfin, que les structuresmathématiques peuvent (au moins en principe) être décrites dans un langage ensembliste. Lathéorie des ensembles permet alors de prouver qu’il existe une relation étroite entre les Lmodèlesd’une axiomatique T et les algèbres de Boole qui lui sont associées et, de plus,personne ne doute de l’adéquation de ces dernières à la notion intuitive de vérité bivalente, cequi justifie la réponse donnée en (ii). Enfin, il semble immédiat que celle apportée à (iii)découle de la précédente.
Si l’on se tourne par contre vers les mathématiques constructives, force est deconstater que le paysage que l’on y découvre est complètement différent. En effet, il existealors une pluralité de théories mathématiques dont chacune vise à être une théorie de lasignification, une sémantique, des axiomatisations formelles qui en ont été proposées.
I S’il existe des structures algébriques, les algèbres dites de Heyting, et des modèles,dus à Scott, Beth ou Kripke, qui sont techniquement des analogues des algèbres de Boole etdes modèles ensemblistes dans le cas classique, par contre leur adéquation, au sens de (i)-(iii),est douteuse. Toute la première partie de ce travail est consacrée à montrer pourquoi
(i) ces modèles ne permettent pas de retrouver la, ou les, interprétation(s) attendue(s), intuitive(s), d’un fragment du langage contentuel des mathématiques constructives,
(ii) les éléments de l’ensemble de base d’une algèbre de Heyting ne représentent pas de façon adéquate la notion intuitive de vérité ou d’absurdité constructive,
(iii) aucune des définitions mathématiques de la validité que ces modèles proposent ne peut être prouvée de façon constructive adéquate à la notion intuitive de validité constructive.
II Dans la deuxième partie, deux autres approches sont considérées que l’on peutprésenter, au moins a posteriori, comme des tentatives de donner des théories mathématiquesde l’explication informelle qui accompagne, depuis Heyting et Kolmogorov, lesformalisations de la logique intuitionniste. Cette explication informelle forme l’interprétationdite de Brouwer, Heyting et Kolmogorov (BHK) qui est censée justifier la constructivité desrègles formelles adoptées en décrivant la forme que doit prendre une construction a pour nousassurer d’une proposition A. On montre dans la deuxième partie de ce travail quel’interprétation BHK permet de caractériser deux notions intuitives de vérité constructive.Décrivons les très brièvement en supposant que A est de la forme : pour tout entier x, il existeun entier y tel que R(x, y).
(a)La première est de considérer qu’un sujet X a fait l’expérience de la vérité de A dès lors qu’il sait, par exemple au moyen d’une démonstration d, qu’une méthode effective r lui permet de faire l’expérience de celle de R(n, r(n)) pour chaque entier n. Pour le dire autrement, l’on attend de r qu’elle produise, pour chaque n, un entier r(n) tel que R(n, r(n)) et une preuve dn de R(n, r(n)). C’est là une notion de vérité constructive qui est clairement épistémique : la vérité d’une proposition dépend d’un sujet connaissant. Une option ambitieuse est d’essayer de rendre compte mathématiquement de ces conditions de vérité épistémiques au moyen d’une théorie axiomatisée des constructions, i.e. des démonstrations, qui se veut alors, peu ou prou, l’analogue constructif de la théorie axiomatisée des ensembles.
C’est là l’approche privilégiée par Kreisel et Goodman. Force est de reconnaître qu’elle ne parvient guère à donner une représentation mathématique adéquate à la notion intuitive de démonstration constructive.
(b) La seconde est d’oublier ce qui fait de la précédente une notion de vérité épistémique en posant que A est constructivement vérifiée, pour ne pas dire vraie, dès lors qu’il existe une méthode r donnant, pour chaque n, un entier r(n) tel que R(n, r(n)). Ici on ne fait intervenir aucun sujet X supposé savoir que r est une méthode ayant cette propriété : r est une méthode de vérification non épistémique à laquelle on demande seulement d’être constructive et de donner, pour chaque entier n, un entier r(n) et une méthode de vérification non épistémique de R(n, r(n)). On obtient alors une caractérisation informelle d’une notion de vérité constructive non épistémique. A posteriori, il apparaît qu’il ne manque à cette caractérisation qu’une définition mathématique précisant ce que l’on entend par "moyen de vérification" pour qu’elle devienne une véritable interprétation mathématique.
L’on doit à Kleene l’idée d’employer à cette fin la définition des fonctions récursives ;les interprétations mathématiques obtenues sont dites alors des interprétations par réalisabilitérécursive. Le choix de la définition des fonctions récursives n’est pas évident et demande àêtre justifié. D’un point de vue constructif l’adéquation de cette définition à la notion intuitivede calculabilité mécanique n’est pas douteuse. Par contre, la réalisabilité récursive repose surl’hypothèse que les moyens de vérification d’une proposition, du fait qu’ils sont justementnon épistémiques, sont nécessairement exécutables par une machine idéalisée. Ce qui est trèsloin d’être immédiat. En quoi sommes nous assurés que la constructivité qui les caractérise nemet pas en jeu une notion d’effectivité humaine qui ne se laisserait pas réduire à unedéfinition mathématique de la calculabilité mécanique ? Il faut alors donner, à tout le moins,quelques raisons de se convaincre de la correction d’une thèse d’adéquation selon laquelle
(iv) il existe une définition mathématique de la réalisabilité récursive qui rend compte fidèlement de la notion de vérité constructive non épistémique.
Il faudrait alors s’assurer que toute proposition récursivement réalisable ou vérifiableest constructivement vraie ; la notion de vérité ici étant celle de vérité non épistémique. Oraucune des définitions proposées par Kleene ne satisfait à cette condition minimale. Est-ce àdire que son programme aurait complètement échoué ? Loin de là. Car Kleene est parvenu àmontrer qu’en un sens une des versions au moins de la réalisabilité récursive était bel et bienla théorie mathématique voulue. Ce qui peut sembler hautement paradoxal au regard de ce quiprécède. Le paradoxe n’est qu’apparent et se dissipe immédiatement si l’on tient compte dufait suivant. Ce que l’on attendait d’une sémantique ambitieuse, comme la théorie desconstructions, c’est qu’elle rende compte de la vérité épistémique justifiée des axiomes et decelle démontrée des théorèmes. Mais si l’on parvenait à prouver que les axiomes, tenus pourconstructivement vrais, d’une théorie contentuelle sont vérifiés par des moyens seulementmécaniques, disons récursifs, et que les règles constructives de démonstration conservent cettepropriété, alors, dans le cas d’une proposition de la forme "à chaque entier x correspond unentier y tel que R(x, y)", la méthode r donnée par la démonstration et telle que, pour tout entierx, on a R(x,r(x)), serait récursive. Et l’on en tirerait un argument en faveur d’une autre thèsed’adéquation selon laquelle
(v) toute méthode de vérification donnée par une démonstration constructive est
récursive.
A une réserve près. Parler de démonstration ici est équivoque. Du fait qu’il n’existepas de définition mathématique de la notion générale de démonstration constructive, que peutonvouloir dire par "toute" et "démonstration" dans "toute démonstration constructive d’unthéorème de l’analyse intuitionniste", par exemple ? En toute rigueur, cette totalité dedémonstrations n’est pas une classe d’objets mathématiques dont on pourrait prouver qu’ilsont, ou qu’ils n’ont pas, telle ou telle propriété. L’objection est justifiée et il convient depréciser que ce sont en fait toutes les dérivations dans des théories formellement axiomatiséessur lesquelles portent les (méta)démonstrations en question. Ce qui mène à envisager dans latroisième partie une dernière thèse d’adéquation selon laquelle
(vi) l’axiomatique formelle serait adéquate à son objet intuitif qui est, ni plus, ni
moins, la pratique des mathématiques constructives.
III L’opinion communément défendue par les logiciens est qu’il n’y aurait pas au fond desolution de continuité entre langage ordinaire et langages formalisés. Ce qui en un sens estdéfendable : indéniablement l’axiomatique formelle peut être vue comme une conséquence duprocessus d’amélioration du langage employé en mathématiques et tous deux ont été desfacteurs de progrès en mathématique favorisant leur intelligibilité. Mais on ne peut pourautant prétendre qu’un langage formalisé sert directement à faciliter et à préciser lacommunication entre mathématiciens. Ce qui peut contribuer ici à l’équivoque est qu’enthéorie des modèles les axiomes formels ressemblent parfois beaucoup à des axiomescontentuels du fait des échanges fréquents entre le langage ordinaire et le lexique formel.Mais, si l’on se tourne vers la théorie de la démonstration et que l’on considère unedémonstration entièrement formalisée, force est de constater qu’il est impossible de lacomprendre quand bien même on en connaîtrait la version informelle ; l’on peut au mieuxvérifier mécaniquement qu’elle est une preuve formelle. Il convient donc de distinguer nonpas deux termes en présence, le raisonnement linguistique et le raisonnement mental, maisbien trois. Les démonstrations formalisées, c’est-à-dire les dérivations, les démonstrationsdonnées dans le langage ordinaire des mathématiques et les démonstrations proprement dites,si l’on ose dire, dont les précédentes sont les traces écrites. Les troisièmes mettent en jeu unecompréhension, un acte ou une construction mental(e), et l’on accordera qu’elles sont, aumoins, des mixtes : ni purement linguistiques, ni purement mentales puisque communicablesvia un langage qui ne peut pas être en pratique un langage formalisé. De même qu’unenotation ensembliste comme "{ , }" n’est pas la collection composée de l’ensemble vide etde l’ensemble des entiers naturels mais désigne, fait référence ou dénote, comme on voudra,cette collection, de même une démonstration linguistique, ou une dérivation, peut au mieuxprétendre désigner, faire référence ou dénoter la démonstration correspondante. Et c’estseulement dans le cas de la première que l’on peut soutenir que la référence est effective pourun sujet humain doué de compétences mathématiques en la lisant et en la comprenant ; pasdans celui de la seconde car les preuves formelles ne relèvent pas de capacités humaines, maisseulement mécaniques.
Une question se pose alors. Le langage ordinaire des mathématiciens, éventuellementamélioré par les progrès de l’axiomatique, peut-il être tenu pour un outil de communicationsûr et efficace ? Elle peut sembler naïve ; pourtant l’accord sur ce point n’est pas universel.Les mathématiques constructives, surtout dans leur version intuitionniste, sont apparues dansun climat de suspicion et de méfiance, non seulement vis à vis de la formalisation desmathématiques, mais même vis à vis des pouvoirs expressifs du langage ordinaire desmathématiques. Pour Brouwer, par exemple, les mathématiques étaient une activité totalementindépendante du langage. Quant à la formalisation, elle était tenue alors pour une entreprisedouteuse visant à remplacer une activité créatrice, propre à l’esprit humain ou, si l’on préfère,à des agents intelligents, par de pures manipulations de symboles dénués de signification,relevant de l’activité d’un chien convenablement dressé ou d’un automate. L’axiomatiqueformelle était alors suspectée d’être liée indissolublement à une idéologie formaliste, cellegénéralement attribuée à Hilbert ; pour le dire crûment, à une conception purementbureaucratique des mathématiques privilégiant la lettre contre l’esprit. Ces préventions sontd’ailleurs toujours d’actualité chez bon nombre d’auteurs. Ceci étant dit, chez Brouwer luimêmeces convictions cohabitaient, plus ou moins harmonieusement d’ailleurs, avec uneconception beaucoup plus modérée de la logique et du rôle du langage en mathématique et quifut d’ailleurs celle adoptée par ses héritiers, à commencer par Heyting lui-même. Pourquoichercher alors à faire renaître des discussions anciennes opposant formalisme etintuitionnisme, aujourd’hui largement oubliées, et qui ne prirent un tour polémique que dansle contexte d’un conflit personnel entre Hilbert et Brouwer ?
Pour mieux le comprendre, il faut accepter d’adopter momentanément les préventionsde ce dernier à l’encontre de la formalisation. Dans cette perspective, les résultats de Kleenene prouvent nullement ce qu’ils prétendent démontrer. Que l’on puisse faire correspondre uneméthode purement mécanique de vérification à chaque dérivation menée dans un systèmeformel constructif n’est guère surprenant puisque les secondes résultent déjà d’une réductiond’un acte créateur de significations nouvelles, la démonstration proprement dite, à unesuccession d’opérations qui sont déjà des opérations de calcul formel donc évidemmentmécaniques. Or c’est là l’hypothèse implicite sur laquelle repose l’entreprise de Kleene.Selon lui, la formalisation ne s’accompagne d’aucune réduction : les dérivations et lesmécanismes qui permettent de les produire, les règles formelles, représentent fidèlement lesdémonstrations contentuelles et les moyens mis en oeuvre par les mathématiciens de chair etde sang. On aura reconnu là la thèse (vi).
L’on essaye alors de donner un argument en faveur de cette thèse (vi). Il repose sur lesanalyses proposées par Dummett et Prawitz : selon eux la signification du langage ordinairedes mathématiques constructives découle de certaines propriétés des règles de démonstration,logiques et mathématiques, qui y sont admises. Ces propriétés n’apparaissent explicitementque si l’on adopte un style bien particulier de formalisation, dû essentiellement à Gentzen,celui des systèmes de déduction naturelle. S’inspirant des indications de Gentzen tout en lesapprofondissant, Prawitz a donné une analyse de la notion intuitive de conséquence logiqueconstructive. La conclusion essentielle à laquelle elle nous mène est que toute démonstrationconstructive peut, en principe tout au moins, être mise sous forme d’une déduction formelledans un système de déduction naturelle. Ce qui suffit à nous assurer de la correction de lathèse (vi) donc, indirectement, de celle de la thèse (iv). Car démontrer constructivement unthéorème et montrer qu’il est une conséquence logique nécessaire des hypothèses employéesdans la démonstration, cela revient au même. Ce qui est déjà un résultat considérable. Mais cen’est pas tout.
Une des propriétés importantes des systèmes de déduction naturelle est qu’ils mettenten évidence le lien existant entre la théorie de la démonstration et celle de la calculabilitéformelle via la correspondance de Curry-Howard qui, on l’a vu, rend manifeste que les règlesformelles de déduction sont aussi des règles indiquant comment définir pas-à-pas desalgorithmes. Le lien entre informatique théorique et mathématiques constructives apparaîtimmédiatement dès lors que l’on précise que la procédure récursive donnée par une déductionest justement un moyen de vérification de la formule déduite. Les axiomes mathématiquessont vus alors comme des règles auxquelles sont associées des instructions élémentaires, aumême titre que les règles logiques. L’importance de cette correspondance entre les preuves etles algorithmes ne saurait être sous-estimée. Elle permet de s’assurer directement de lacorrection de la thèse (vi) et surtout de comprendre pourquoi elle est correcte ; elle montreaussi, contre Brouwer, en quoi la formalisation contribue à l’intelligibilité des mathématiques.Quant aux significations constructives des constantes formelles, elles sont justement données,à en croire Dummett et Prawitz, par les règles formelles qui permettent de les utiliser. C’estparce que ces règles satisfont à des propriétés spécifiques qu’elles confèrent à ces constantesleurs significations constructives. Mais ce sont aussi ces propriétés qui rendent possible demanifester explicitement dans les systèmes de déduction naturelle la correspondance entre lapreuve constructive d’un théorème et l’algorithme qui le vérifie.
La correspondance de Curry-Howard est ainsi à l’origine depuis une trentained’années d’une rencontre entre les théories de la calculabilité formelle et de la démonstration,d’une part, et l’informatique théorique, d’autre part. Dans cette perspective, une théoriemathématique formalisée est vue comme un langage de programmation très sophistiquépermettant de faire de l’art de la programmation une discipline aussi rigoureuse que lesmathématiques. Par ailleurs, les systèmes de déduction naturelle peuvent être vus comme dessystèmes formels interprétés : les significations des constantes logiques et mathématiques deleur langage étant implicitement déterminées, selon Dummett, par les règles qui en régissentl’emploi. C’est donc en fait à une rencontre mettant en jeu trois disciplines que l’on assiste :l’informatique théorique, les mathématiques constructives et la théorie de la signification.C’est dans cette triple perspective que nous présentons la théorie des types de Martin-Löf quise veut à la fois une théorie fondatrice des mathématiques constructives contenant sa propresémantique et un langage de programmation permettant de générer automatiquement desalgorithmes prouvés corrects. Elle rend manifeste une conséquence implicite de la thèse (vi) :il n’y aurait pas à distinguer entre informatique et mathématiques constructives.
L’enquête sur la signification du langage des mathématiques constructives trouveraitainsi son aboutissement dans l’adoption d’une conception mécaniste des mathématiquesconstructives. Le fait que la correspondance de Curry-Howard ait pu être étendue auxmathématiques classiques prend alors un relief tout particulier puisqu’il resterait à expliquercette coïncidence miraculeuse entre des mathématiques et une logique non constructives etdes algorithmes de calcul. Cette question n’est qu’abordée dans la conclusion de la thèse tantil est clair que la traiter comme il le conviendrait mènerait à sortir des limites que son titreimposait de respecter.
