Version classiqueVersion mobile
OpenEdition Books

Logique, dynamique et cognition

 | 
Jean-Baptiste Joinet

Première partie. La logique à la croisée des chemins

Sur le temps logique

Jean-Baptiste Joinet

Texte intégral

1Il est assez traditionnel de concevoir la logique comme étant en somme « la théorie des lois de la pensée rationnelle considérée dans sa simple forme in dépendamment de ses contenus possibles ». Au regard de cette tradition, largement prédominante dans les cercles institutionnels de la Philosophie et dont une dénomination aussi courante que « logique formelle » tend à accréditer l’importance, l’expression qui donne leur titre aux présentes réflexions − le temps logique − résonne comme un oxymore. La conjonction du temps et du logique, en effet, n’a de sens ou d’intérêt qu’à partir du moment où le logique s’inscrit effectivement en quelque manière dans la temporalité (autrement dit, s’il y a bien un « temps logique » et que ce temps n’est pas l’éternité) ou si, au moins, la temporalité s’inscrit en lui. Or si, comme le défend cette tradition, les « lois de la pensée » rationnelle sont formes apriori, elles sont alors à la fois intemporelles (se tenant hors du temps, le logique est immuable, sans histoire) et atemporelles (le temps, expulsé en même temps que les « contenus » de la pensée vivante, est maintenu hors du logique).

  • 1 Cette métaphore très usitée du « contenu » de signification relève à mon avis surtout du poncif ; s (...)

2À partir du « tournant linguistique » pris au XIXe siècle par les logiciens (qui cherchaient à réaliser ce rêve déjà ancien d’une objectivation complète de la rationalité dans les formes de la discursivité), cette idée de « validité formelle indépendante des contenus » trouva rapidement sa contrepartie « technique », éclatante et fameuse, dans la notion bien connue de tautologie ou loi logique : énoncé vrai quelle que soit l’interprétation du langage dont il est composé, indépendamment donc de tout « contenu1de signification » (dont le rôle dans ce contexte est joué, au plan technique, par la notion d’interprétation d’un langage dans le cadre ensembliste). Les modalités sous lesquelles cette notion classique d’interprétation consacre le divorce du logique et du temporel relèvent en fait de plans multiples et hétérogènes.

  • 2 Comme il est plus ou moins traditionnel en théorie de la démonstration, le terme morpho logie renvo (...)
  • 3 Le cas des « logiques modales temporelles » visant à modéliser des adverbes temporels par des axiom (...)
  • 4 Le dédoublement terminologique proposé par de nombreuses langues (ainsi de l’anglais, qui distingue (...)

3Tout d’abord, les langages formels relativement auxquels cette notion d’interprétation fut initialement élaborée (langage du calcul des prédicats du premier ordre) sont des langages dont la morphologie2est proportionnée à leur visée avant tout mathématique (ce qu’avère leur postérité dans le contexte fondationnel qui a mobilisé la plus grande part de l’activité logique au XXe siècle). Or les théorèmes mathématiques se rédigent au présent de l’indicatif − un temps qui, dans ce contexte, n’est pas celui de l’actuel, mais celui de l’actualité quelconque, indéfiniment réitérée, l’autre nom donc de l’intemporel. En particulier, contrairement à ce qui prévaut pour les langages naturels, les composants lexicaux « temporels » sont ici inexistants3, ce qui semble signer l’absence en ce contexte de toute temporalité grammaticale4.

4Par ailleurs, la définition logicienne de la notion d’interprétation réalisant un énoncé intervient dans le contexte déjà évoqué du « tournant linguistique » qui, dans le temps même où il promeut le langage comme instance objective, maintient la psychologie à distance de la logique, la subjectivité à distance du logique. Ainsi, avec l’évacuation du sujet, toute la dimension temporelle de l’appréhension subjective de la signification s’évanouit. D’une manière générale, toute référence au classique temps subjectif disparaît.

5Enfin, parce que cette notion de réalisation d’un énoncé (dans la théorie des ensembles où l’extensionalité est décrétée) ne relativise pas la détermination de la vérité à l’utilisation d’une technologie démonstrative (fût-elle désincarnée, indépendante d’un sujet-démonstrateur particulier), elle écarte aussi toute intrusion de la temporalité pratique.

  • 5 Subsidiairement, observons que toute dimension temporelle qui aurait pu éventuellement subsister da (...)

6En première approximation, une rencontre du temps et du logique, ainsi envisagée à travers cette notion de loi logique, apparaît donc effectivement comme radicalement impossible, car contredisant le geste inaugural de la logique : l’expulsion du temps − grammatical, subjectif ou pratique5.

1. À la recherche du temps perdu

  • 6 Des « prémices », pourrait-on écrire, vers la conclusion.
  • 7 L’expression imagée « flèche du temps » n’a pas ici la valeur déterminée qu’elle prend dans le cont (...)

7En réalité, cet apparent positionnement du logique hors du temps n’est pas tant corrélatif du tournant linguistique en tant que tel, que d’une attention trop exclusivement concentrée, dans le champ ouvert par le tournant linguistique, sur cette notion de « loi logique ». Si, au centre de la discipline, on substitue à cette dernière notion celle de « règle logique » − si donc l’attention se porte à présent vers les moyens démonstratifs concrètement utilisés dans le contexte rationnel ou mathématique − une certaine forme de temporalité semble en tout cas réapparaître. Les « règles logiques » (et c’est déjà le cas des figures de la syllogistique aristotélicienne) se présentent en effet comme des règles de transition du discours vers le discours, munies d’une orientation − des prémisses vers la conclusion6− et lorsqu’elles sont enchaînées au sein d’une démonstration selon un ordre, une chronologie déterminés, elles communiquent cette orientation au texte qu’elles composent − la preuve −, des hypothèses jusqu’au théorème prouvé. Ordonné et dirigé, le texte argumentatif comprend-il pour autant une flèche du temps7 ?

  • 8 Typiquement, preuves représentées par des « arbres » (dont les nœuds sont des formules et les embra (...)

8En premier lieu, on peut observer que l’orientation évoquée détermine avant toutes choses l’émergence d’une temporalité pratique (à l’envergure certes encore très modeste). De cette temporalité relèvent tant le déroulement de la rédaction du texte mathématique (l’agencement ordonné des règles), que celui de sa lecture. Cette dernière, se réalisant au travers des occasions saisies par le lecteur d’une circulation disconnexe dans l’espace du texte au gré d’une libre actualisation de l’information mémorisée, mais toujours dans le cadre des contraintes posées par l’ordonnancement singulier des règles, s’exerce de façon variable en fonction du format de représentation des preuves adopté, et dépend en particulier du profit tiré de la bidimensionalité de la feuille ou du tableau (de l’espace donc) pour représenter simultanément de multiples déroulés chronologiques possibles de l’ « intrigue » argumentative8.

9En second lieu, les parcours actualisés lors d’un investissement pratique du texte rationnel dépendent du recours à des procédés linguistiques standard de gestion de la temporalité du récit, qui, altérations normées et régulières du « signifiant » textuel au sens saussurien, relèvent à proprement parler du temps grammatical.

10On pourrait d’abord citer ici les formes grammaticales ordinaires propres à la narration, utiles et utilisées dès lors que les démonstrations sont rédigées dans une langue historique ( « langage naturel » ). Divers adverbes, conjonctions ou conjugaisons viennent alors soutenir, surtout à l’oral, l’organisation chronologique et structurelle complexe d’une « intrigue » argumentative bien trop à l’étroit dans l’axe uni-dimensionnel de la parole déroulée (on pense par exemple au conditionnel dans un raisonnement par l’absurde, aux usages des temps du passé dans le rappel d’une hypothèse courante posée en début de démonstration ou plus généralement d’une conclusion antérieurement acquise, etc).

  • 9 La « déduction naturelle » fut élaborée avec l’intention explicite de figurer, d’imiter, dans le ca (...)

11Au-delà de ces instances de la temporalité grammaticale qui pourraient sembler relever de la simple stylistique ou de la « mise en scène » et ne sont pas spécifiques du discours rationnel, il convient d’évoquer l’existence de composants grammaticaux (dévolus à la gestion des aspects temporels) propres au texte argumentatif. Un format de représentation des preuves formelles où se manifeste bien, proprement marqué au coin de la syntaxe, un premier type de prise en compte de cette temporalité grammaticale des textes démonstratifs est celui des systèmes dits « à la Hilbert » ou plus encore des systèmes de « déduction naturelle » 9. Dans ces formalismes de représentation des preuves, interviennent des « renvois » internes au texte, qui sont autant de procédés notationnels gérant explicitement sur le mode anaphorique la chronologie du texte (c’est typiquement le cas des « désactivations d’hypothèses » en déduction naturelle, qui déterminent, à chaque instant de la construction d’une preuve, quel est l’ensemble des hypothèses qui, à cet instant, ont cessé d’être des hypo thèses courantes).

  • 10 Cf. l’article de J.-Y. Girard dans ce volume.
  • 11 Cf. dans la typologie des conjugaisons, et plus précisément des « aspects » verbaux, la distinction (...)
  • 12 Les langages de la logique formelle étant des langages idéographiques (i.e. sans le premier niveau (...)
  • 13 On pourrait être tenté de considérer que ce rapprochement de la distinction opérée par la Logique L (...)

12Plus décisive encore est la démarcation instaurée par la Logique Linéaire entre prédication perfective (l’énoncé éphémère, l’hypothèse définitivement consommée dès sa première utilisation) et prédication imperfective (l’énoncé durable, l’hypothèse réutilisable) 10qui reprend littéralement la distinction grammaticale standard correspondante11. Présentée en termes de « temps grammatical », cette distinction correspond à une décomposition de l’ « indicatif pré sent » du texte mathématique (celui-là même que le début du présent article identifiait comme un « présent d’éternité » ), dorénavant dédoublé en sa part perfective (le présent instantané, éphémère) et sa part imperfective (le présent durable, le présent d’éternité). Contrairement aux procédés anaphoriques de gestion de la chronologie dans les preuves évoqués il y a un instant, la distinction grammaticale instaurée par la Logique Linéaire est cette fois réalisée au niveau morphologique lui-même (comme c’est le cas dans les langues « naturelles » 12) via une modalité spécifique.13

  • 14 Souvent seulement nominale sans doute, cette identification, ce manque de distinction, n’en demeure (...)

13Ce temps apparemment retrouvé dès que l’attention se déplace de la « loi logique » vers la « règle logique » (temps grammatical du texte argumenta tif, temps pratique de sa construction et de sa fréquentation), l’usage commun s’empresse ordinairement d’y déceler un écho du temps psychologique lui-même. Emblématique de cette tendance est l’identification très commune de la « règle logique » (règle d’inférence discursive) et de la « règle de raisonnement », identification14qui repose à mots couverts sur le présupposé représentationaliste d’une isomorphie entre la temporalité de l’enchaînement du texte démonstratif et celle du déroulement de la pensée rationnelle : la règle logique redoublerait en quelque sorte, dans l’ordre formel du discours, les pas accomplis par la pensée.

  • 15 Pour une discussion plus approfondie de l’opposition démonstration-raisonnement, voir J.-B. Joinet, (...)

14Le temps logique non seulement grammatical et pratique, mais aussi rationnel, psychologique serait-il donc à son tour retrouvé ? Processus mental seulement partiellement conscient, rétif à l’introspection (et pour une éventuelle description duquel manque en tout état de cause, en raison de sa nature dynamique, processuelle, un langage adapté), le raisonnement humain se dérobe à une approche directe et, au mieux, n’est que malaisément constitué comme phénomène par les disciplines scientifiques (comme la psychologie ex périmentale ou la neuro-physiologie) qui l’abordent indirectement à travers ses objectivations mesurables. Ces quelques éléments suffisent cependant à dévaluer cette identification simpliste de l’enchaînement des règles logiques et de la conduite du raisonnement, dont la dynamique et la temporalité, sous le regard de ces disciplines, apparaissent incommensurablement plus complexes. On retiendra donc sur ce point que si, comme on l’a souligné, l’orientation communiquée au texte démonstratif par les règles logiques du fait de leur caractère « dirigé » semble y inscrire une « flèche du temps », il convient de ne pas y projeter, par une transition factice, indue, la temporalité de la pensée elle-même15. Le temps psychologique est-il cependant le seul à quitter, à peine arrivé, la scène de notre temps temporairement retrouvé ?

  • 16 Cf. J.-Y. Girard, « Linear Logic », Theoretical Computer Science, 50 :1-102,1987 et l’abondante lit (...)

15On se souvient en effet que la modeste « temporalité pratique » dégagée dans les analyses qui précèdent dépendait de façon essentielle d’une part de l’orientation des règles logiques, d’autre part de leur « convergence » (vers une conclusion déterminée), enfin de l’ordonnancement essentiellement séquentiel de ces règles composant le texte démonstratif. Or un trait marquant des formalismes de représentation des preuves élaborés dans la période récente (réseaux de preuves16) est précisément la triple disparition de cette orientation, de son caractère dirigé et de cette « chronologie » de l’agencement des règles.

16En effet, le fait que, dans une preuve jouissant des symétries de la logique classique, le genre de manipulations auxquelles les prémisses des règles sont soumises s’avère identique (à une symétrie miroir près) à celui dont les conclusions des règles font l’objet, a été repéré par la Théorie de la démonstration comme consistant en une sorte de bégaiement inutile, bégaiement supprimé sans perte d’information essentielle, dans ces nouveaux formalismes, par un simple « repliement » du monde des hypothèses sur celui des conclusions (ce qu’on pourrait décrire, avec les mots qui nous occupent, comme un repliement du commencement sur la fin).

  • 17 Ceci ne vaut certes pas dans le cadre non symétrique de logiques sans dualité (comme la logique int (...)

17Dans ce contexte, il n’y a plus de commencements (plus d’hypothèses), il y a plusieurs fins, autrement dit plusieurs conclusions « simultanées », parallèles : parmi ces fins (ces conclusions) possibles, aucune ne se distingue pour « donner la direction » 17. Par ailleurs (et indépendamment de ce qui précède), dans les formalismes de types « réseaux », la notion d’un ordre d’application des règles logiques, sans complètement disparaître, est également affectée. Un réseau de preuve est en effet un objet géométrique compact qui rassemble simultanément, comme repliés dans un même espace, divers scénarios, diverses chronologies démonstratives. Le critère discriminant de la preuve n’est plus ici l’enchaînement ordonné (ordonnancement successif, chronologique) de règles localement correctes, mais un ensemble de propriétés géométriques globales garantissant la possibilité endroit d’un « dépliement » de la structure de ré seau en les diverses chronologies qu’elle contient en puissance.

18Doit-on en conclure qu’avec l’identification des réseaux comme objets profonds sous-jacents aux textes démonstratifs, et donc avec l’abandon corollaire du « paradigme des preuves-comme-textes », les temporalités « pratique » et « grammaticale » que nous avions cru pouvoir repérer dans la construction du texte argumentatif, sont altérées au point de disparaître à leur tour, à la suite du « temps psychologique », de la scène de ce temps que nous pensions retrouvé ?

2. Le temps introuvable ?

19Commençons par observer ici qu’en réalité, lors de la double abstraction présentée à l’instant (celle qui nous amené en deux étapes des preuves comme textes séquentiels aux objets foncièrement géométriques que sont les réseaux), ni le « temps pratique » lié à l’ordre d’application de certaines règles, ni le « temps grammatical » n’ont totalement disparu.

20Concernant en particulier ce dernier (sur lequel nous allons nous arrêter longuement), la distinction entre une « conjugaison » perfective et une « conjugaison » imperfective incarnée par les modalités de la logique linéaire (les « exponentielles » ) a survécu à la quotientation. Bien entendu, le dépassement du paradigme des preuves-comme-textes ayant été proclamé, on pourrait s’étonner qu’une grammaticalité soit imputée à des objets auxquels la textualité est par ailleurs déniée. En quel sens en effet peut-on encore parler de temps grammatical, s’il n’y a plus de texte, si donc a disparu l’analogie formelle qui fondait l’idée qu’un « récit » argumentatif soit à l’œuvre dans le discours démonstratif ? Si cette dimension narrative (voire même tout simplement cette nature discursive) a disparu, n’est-il pas artificiel, spécieux, de convoquer une terminologie grammaticale relevant d’une typologie linguistique des conjugaisons dont le critère classificatoire paraît précisément lié à une fonction narrative ?

  • 18 La diégèse est « l’univers spatio-temporel auquel se rattache l’histoire narrée par un récit ». Est (...)

21Au prix d’un long détour (au terme duquel nous identifierons la temporalité diégétique18à laquelle ces preuves non textuelles que sont les réseaux réfèrent), nous allons voir qu’il n’en est rien. Il est crucial pour commencer d’observer que la narration peut s’accomplir sous deux modalités extrêmement diverses, apriori hétérogènes.

  • 19 Ordre linéaire, cursif, dans les langues naturelles, mais il s’agit là d’une caractéristique contin (...)

22Selon une première modalité, la plus standard, la narration est la présentation (linguistique, discursive) d’une succession d’ensembles d’événements (la trame, l’action, l’intrigue) proposant un « découpage » et un « montage » particuliers (potentiellement complexe : événements simultanés, flash-back ou anticipations, densité variable du nombre d’événements etc), notamment grâce à divers outils lexicaux et grammaticaux explicites (conjugaison, adverbes, conjonctions etc) ou implicites (la succession des énoncés disposés dans le texte selon un ordre déterminé) 19et telle que la temporalité de cette succession soit reconstructible à partir de ce discours.

23Cette esquisse de définition, évidemment très partielle et approximative, trop simpliste pour prétendre rendre compte de la complexité de la narration littéraire, vise ici simplement à mettre en relief l’arrière-fond représentationaliste de la conception ordinaire de la narration. Mais la narration existe également sous une autre modalité, non représentationnelle, qu’incarnent de manière paradigmatique ces textes particuliers que sont les programmes informatiques. Bien que les programmes informatiques se présentent généralement littérale ment comme des textes (rédigés en quelque langage de programmation, ces langages artificiels élaborés par l’ingénierie logicielle), il est plutôt inhabituel de les considérer comme des discours à part entière, encore moins comme des discours narratifs.

  • 20 En partie aussi, certes, en raison de la faiblesse de leur valeur littéraire ! On est loin de la Re (...)

24Cela est dû pour partie au préjugé répandu selon lequel le caractère « formel » du langage dans lequel ils sont rédigés interdirait qu’on les identifiât aux discours ordinaires (comme si nos langues historiques n’étaient pas elles-mêmes des systèmes formels opérant sur des signes !) 20, mais aussi sans doute, et surtout, à l’obstacle épistémologique que constitue la prééminence quasi exclusive de la conception représentationaliste en matière sémantique à tous les niveaux d’articulation du langage : le niveau lexical (morphème / idéo gramme logique), le niveau morphologique (phrase grammaticale / proposition logique), enfin, celui qui nous intéresse ici, le niveau textologique (récit/ texte démonstratif).

  • 21 John L. Austin, Quand dire c’est faire, 1962 (traduc. française, Coll. Points, Seuil, 1979). Appliq (...)

25En écho à la terminologie popularisée par les travaux d’Austin21, on pourrait qualifier de performatif, le régime narratif non représentationnel dont relève ce texte particulier qu’est le programme informatique : celui d’un texte qui fait ce qu’il dit faire. Pour défendre ce choix terminologique, remarquons que, de même qu’un énoncé performatif au sens d’Austin ( « la séance est ouverte ! » ) n’est doué de performativité qu’au moment où il est prononcé, qui plus est dans un certain type d’environnement, de même ce n’est que dans le contexte où il est à même de produire ses effets, le contexte donc de l’évaluation en acte, que le faire/ dire d’un programme se dévoile véritablement.

26La diégèse associée à un programme, autrement dit le déroulé effectif des événements calculatoires (y compris les « effets de bord » ) que le programme est susceptible de provoquer, dépend d’une part, dynamiquement, du contexte, autrement dit des environnements avec lesquels, séquentiellement ou non, il interagit (ces données et programmes avec lesquels il est amené à échanger des informations, des requêtes et des résultats, au furet à mesure que le processus d’évaluation s’effectue), mais aussi, bien sûr, de l’effet opérationnel concret que produisent ces interactions (qui dépend de la manière dont l’implémentation de ce langage est concrètement réalisée). Le programme informatique est donc un texte qui dit non pas tant ce qu’il fait, que ce qu’il fait en puissance : ce qu’il ferait, s’il était dans un contexte idoine.

  • 22 Mais nous verrons bientôt que cela vaut aussi bien pour ces autres textes que sont les preuves, et (...)

27Ce point de vue sémantique non représentationaliste sur les textes informatiques (les programmes), nous permet de reformuler à leur propos, la question que nous avions laissée un instant en suspens22, à savoir : « Que veut dire, dans le cadre d’une sémantique performative, qu’un sème grammatical donné assume une fonction grammaticale « temporelle » analogue à celle jouée par le couple grammatical traditionnel conjugaison perfective / conjugaison imperfective, dont la pertinence est ordinairement liée au point de vue représentationnel sur la narration ? ».

  • 23 Soit encore, pour utiliser la terminologie technique des linguistes : le « sémème » performatif.

28Dans le cas d’un programme informatique, l’unité syntaxique de base dotée d’une fonction sémantique performative23, c’est, idéalement du moins, l’instruction de programmation, une petite unité de texte, dont la sémantique per formative (autrement dit le genre d’évaluation/interaction élémentaire qu’elle est susceptible de produire opérationnellement, dans un environnement donné) est définie. Sans qu’il soit besoin d’entrer dans le détail fastidieux de syntaxes au demeurant très variables, souvent difficilement comparables et qualitative ment inégales d’un langage de programmation à l’autre, on retiendra simple ment que certaines instructions de programmation (séparées ou non, selon le degré de perfection analytique du langage considéré) fonctionnent comme des « sèmes » de conjugaison performative implémentant cette distinction perfectif /imperfectif − typiquement sous la forme d’une déclaration d’itérabilité ou non d’une procédure, de duplicabilité ou non d’une donnée, procédure ou don née dont la permanence ou la fugacité est alors effectivement réalisée comme propriété opérationnelle au long de leur destinée calculatoire.

29En définitive, la difficulté que semblait poser l’attribution d’une grammaticalité à des objets (les réseaux de preuve) ne jouissant plus du statut de textes apparaît sous ce nouveau jour surmontable. En effet, la textualité des pro grammes (suites d’instructions séquentiellement ordonnées d’un langage de programmation donné) apparaît comme un trait contingent, non nécessaire à leur narrativité (puisqu’une narration performative sera aussi bien actualisée dans tout dispositif non séquentiel évoluant globalement en raison des capacités d’interaction locale de ses composants).

30Arrivés au terme de ce long détour qui nous a conduit jusqu’à cette idée d’une grammaire de la temporalité calculatoire, il nous reste donc à comprendre comment projeter sur la logique, sur les preuves (et en particulier, sur ces composants des preuves évoqués plus haut auxquels une fonction grammaticale temporelle a été imputée) les enseignements tirés de l’analyse de la narrativité calculatoire.

3. Temps logique et temps calculatoire : l’heuristique

  • 24 La temporalité de la construction de preuves est celle du processus de réponse à la question « tel (...)

31Pour peu que l’attention accordée aux processus pratiques dont relèvent les preuves − attention qui, plus haut, était restée focalisée sur la temporalité de la « construction » de ces dernières, sur celle de leur « rédaction » −, soit désormais étendue aux processus plus généraux de leur découverte, à la dynamique de la recherche de preuves24, un premier pont entre logique et calcul, entre processus d’heuristique démonstrative et processus d’évaluation calculatoire, peut être aisément dressé.

  • 25 Sous réserve de cohérence de l’arithmétique.

32Pour illustrer ce point tout à fait classique, observons qu’un problème calculatoire typique comme « combien font deux et deux ? » (2+2 = ?) et le problème logique de démontrer l’énoncé 2+2 =4, sont deux problèmes équisolvables : une solution apportée à l’un, apporte une solution à l’autre25. Ici donc, une stratégie de recherche de preuve coïncide littéralement avec une stratégie d’évaluation numérique − en d’autres termes, elle n’est autre qu’un calcul, au sens le plus ordinaire de ce mot.

  • 26 Ce constat, intervenu très tôt dans l’histoire de la logique (dès Leibniz sans doute, qui don nant (...)

33Tôt repérée26, cette connivence de l’heuristique logique et de l’évaluation calculatoire a de longue date nourri le dialogue entre logiciens et théoriciens du calcul, conviant à une « traduction » des concepts de l’un des deux champs à l’aide des concepts de l’autre. Pour ce qui nous occupe ici, elle invite à tenter de réaffecter à la temporalité de l’heuristique, les conclusions tirées ci-dessus quant à la grammaire de la temporalité calculatoire, autrement dit à tenter d’appréhender l’effet opératoire (dans la dynamique de la recherche de preuves) des modalités « exponentielles » (ces composants du langage de la Logique Linéaire évoqués plus haut, et dont le statut de « sèmes grammaticaux imperfectifs » restait à défendre) en termes d’une fonction narrative temporelle. Observées sous cet angle, les modalités exponentielles présentes dans l’énoncé dont une preuve est recherchée, viennent signer la continue restaurabilité, à chaque étape de la recherche, des sous-énoncés qu’elles viennent préfixer parmi les données du problème à résoudre. Cette « permanence », cette « durabilité » qu’instaure la modalisation « exponentielle » d’un énoncé relève sans conteste de la temporalité bien identifiée de l’épopée heuristique : elle concerne les événements qui la composent.

  • 27 On a vu plus haut que la textualité des preuves n’est qu’épiphénoménale. En vue d’aborder en propre (...)
  • 28 L’énoncé n’est ici envisagé comme producteur d’effets calculatoires que relativement à des stratégi (...)

34Aussi éclairante (pour la problématique générale de ces investigations) que soit l’articulation précise entre énoncé logique et temps logique qui vient d’être dégagée, il convient d’observer qu’elle ne contribue toutefois pas, au moins au premier abord, à l’élucidation des questions précises que nous poursuivions, à savoir : est-ce que les preuves elles-mêmes – à l’instar des programmes − peuvent être vues sous l’angle sémantique performatif comme sources de récit ? Et, si oui, les modalités exponentielles présentes dans le texte démonstratif remplissent-elles ce rôle grammatical temporel sur la scène de cette narration que ce texte est susceptible de produire performativement ?Pour cerner la difficulté ici, il importe de prémunir le lecteur contre l’éventuel malentendu au quel conduirait, dans la lecture de ce qui précède, un involontaire glissement métonymique confondant l’épopée heuristique (l’expérience processuelle de la recherche de la preuve) et l’éventuel récit de cette épopée (récit dont le texte démonstratif27, la preuve, pourrait apriori jouer le rôle). En effet, la « traduction » entre processus de calcul et processus heuristique qui nous a permis de projeter la temporalité diégétique du « récit calculatoire » (la temporalité du processus d’évaluation calculatoire) sur la temporalité du processus heuristique, ne met pas en relation le texte du programme informatique (côté calcul) avec le texte de la preuve (côté logique), mais avec « l’épilogue » de la future preuve, à savoir l’énoncé à prouver28.

35Si donc la temporalité heuristique est bien elle-même diégétique (comme on pouvait s’y attendre puisqu’elle est l’image, à travers cette traduction, d’une temporalité diégétique), elle ne peut être la temporalité diégétique imputée au récit du texte démonstratif − la preuve − puisque, en passe d’être découverte, la preuve n’existe pas encore. L’idée de narrativité performative, si limpide dans le cas du programme informatique, semble donc passablement altérée par la « traduction » (du langage de la théorie du calcul vers celui de l’heuristique logique) présentée, qui s’avère a posteriori peu exploitable, du moins à cette étape intermédiaire de l’analyse, pour progresser vers une réponse à la question posée. On peut cependant tenter un nouveau départ en reconsidérant, obstinément, l’inscription des preuves dans la temporalité.

4. Temps logique et temps calculatoire : l’analytisation

36Eu égard à la dynamique heuristique, le statut de la preuve est simplement celui de produit terminal du processus de recherche. Résultat du processus, elle est donc seconde relativement à lui, postérieure pour ainsi dire, donc extérieure à lui. Mais l’inscription d’une preuve dans la temporalité, ne se réduit pas à ce statut d’être émergent, seulement relatif à ce passé que constitue pour lui son engendrement heuristique, sa rédaction ou sa construction. Dans l’économie démonstrative, en effet, les preuves ont également un devenir. Elles sont d’une part sujettes à divers types de manipulations qui signent leur modularité : elles sont utilisées comme autant de briques pour construire de nouvelles preuves, les règles logiques apparaissant, en tout cas dans cette perspective, comme formant simplement divers modes possibles donnés d’agencement de ces « briques ». Elles font d’autre part l’objet de compositions, une opération relevant d’un tout autre plan et qu’il importe de bien distinguer du précédent.

  • 29 Une façon alternative de se représenter plus directement et exactement la composition des programme (...)

37Comme l’expérience le montre, appliquée au cas des preuves, l’idée de composition s’avère délicate à présenter à un public non averti, et commencer par l’illustrer dans le cas de programmes informatiques, n’est pas sans vertus. Schématiquement dit, composer un programme implémentant une fonction de A dans B d’une part et une donnée de type A d’autre part, c’est simple ment « appliquer » le premier à la seconde (autrement dit fournir cette donnée comme « entrée » au programme en question). Bien sûr, la « composition » décrite n’est rien en elle même : pour lui donner sens, encore faut-il déclencher l’évaluation, pour produire, le cas échéant, le résultat de type B escompté29.

38De même que la composition des programmes n’a de sens que relativement à la dynamique des programmes au long de l’évaluation calculatoire (dynamique qui dans sa réalisation effective dépend bien sûr des singularités opérationnelles propres au langage de programmation utilisé et à son implémentation), cette composition des preuves (dont la présentation est en cours) prend seulement sens en fonction d’une dynamique des preuves − qu’il nous faut donc commencer par aborder.

  • 30 L’existence et la réalisabilité de telles conversions (autrement dit la convertibilité des preuves (...)
  • 31 Systèmes dont les règles formalisées imitent celles de la culture logique commune.

39La dynamique des preuves ici en question peut être décrite comme celle de la conversion des preuves en preuves analytiques (l’analytisation des preuves), c’est-à-dire, dans le cas des preuves envisagées comme textes, en preuves dont les étapes intermédiaires (tous ces énoncés qui pavent le chemin qui mène à la conclusion) s’obtiennent par une analyse de l’énoncé prouvé, autrement dit, sont tous des sous-énoncés du théorème prouvé30. Schématiquement, composer des preuves, c’est donc créer l’occasion d’un déclenchement du processus d’analytisation, autrement dit leur faire subir une opération telle que la preuve ce faisant produite ait « perdu en analyticité ». Si l’on s’en tient aux systèmes logiques « naturels » 31, l’application d’une banale règle de modus ponens (de l’énoncé « A implique B » et de l’énoncé « A », déduire l’énoncé « B » ) fournit généralement l’occasion (et pour nous une illustration simple) d’un tel accroissement du défaut d’analyticité des preuves (en effet, une preuve de l’énoncé B, ayant pour dernière règle un tel modus ponens, n’est pas en général analytique puisque l’énoncé « A implique B » − ou même l’énoncé « A » lui-même, sauf cas particulier − n’est pas sous-énoncé de l’énoncé « B » ).

  • 32 À la formulation « alternative » de la composition des programmes sous forme de « branchement » don (...)

40Un trait remarquable (et d’ailleurs très tôt remarqué) de cette forme prise par la composition des preuves dans les systèmes logiques de ce type est son analogie formelle avec la composition des programmes évoquée plus haut (analogie de « la composition d’une preuve de « A implique B » avec une preuve de « A » », avec « l’application d’une fonction de A dans B à un argument de type A » ) 32.

  • 33 Cette identité est connue depuis 1969 sous le nom de « correspondance de Curry-Howard » : l’analyti (...)

41Comme cela fut remarqué vers 1969, si la dynamique des programmes considérée est celle associée au lambda-calcul (un langage de programmation sommaire mais complet issu des premières théories de la calculabilité), c’est non d’une simple analogie, mais d’une pure et simple identité qu’il s’agit : l’analytisation des preuves et l’évaluation des programmes ne font qu’un33.

42Observée de ce belvédère, l’idée d’une narrativité performative à l’œuvre dans les preuves (dont on a vu qu’elle demeurait obscure lorsqu’on s’en tenait à une modélisation de l’évaluation calculatoire en termes de dynamique heuristique) rejoint naturellement en limpidité l’idée de narrativité performative des programmes informatiques exposée plus haut. En particulier, la temporalité diégétique à laquelle la fonction grammaticale des connecteurs exponentiels est relative peut être à présent clairement identifiée comme étant celle du processus d’analytisation des preuves (alias l’évaluation, dans le vocabulaire informatique). C’est en somme relativement à cette temporalité, que la modalité imperfective ( « exponentielle » ) réalise performativement (sous la forme d’une réplication) la permanence des sous-preuves qui lui font face au cours du processus d’analytisation logique.

43Seulement relative à la temporalité de l’analytisation, la distinction grammaticale entre « aspect perfectif » et « aspect imperfectif » n’est pas spécfiquement liée à l’appréhension des preuves comme textes : elle vaut encore relativement au processus d’analytisation des réseaux de preuves (autrement dit, pour reprendre les termes utilisés plus haut : elle survit à cette quotientation des textes démonstratifs que constitue le passage aux réseaux). Voici donc l’objectif que nous nous étions fixé (à savoir comprendre la fonction grammaticale temporelle des exponentielles dans ces preuves non textuelles que sont les réseaux, en identifiant la temporalité diégétique à laquelle celle-ci est relative) atteint.

44À ce stade, on peut observer que cette temporalité grammaticale retrouvée et comprise, éclaire en retour la temporalité pratique de la construction des preuves (dont ne subsiste dans les réseaux qu’une part résiduelle en comparai son de celle identifiée plus haut à propos des preuves textuelles), puisque c’est cette dernière qui détermine les formes particulières que prend le processus d’analytisation à chaque étape.

45Dans le cas des réseaux, le fait que les preuves soient dégagées de divers aspects contingents liés à la textualité que nous avions repérés (orientation de la preuve d’un début vers une fin, centrage de cette orientation vers une conclusion, exclusives équentialité de sa construction – tous ces traits qu’on avait pu prendre comme autant d’indices d’une temporalité pratique propre à la construction du texte démonstratif, comme autant de traces d’une flèche du temps inscrite au cœur du texte démonstratif, mais qui précisément n’existent plus dans les réseaux de preuves), rend par contraste plus visible la structure véritable de la temporalité du processus d’analytisation logique.

46Tout d’abord en effet, nombre d’étapes vaines dues aux contraintes inessentielles de séquentialité dans l’organisation des textes démonstratifs n’ont plus de correspondant dans les processus d’analytisation des réseaux, ce qui par contraste met en relief les étapes véritables de la dynamique, celles qui précisément survivent à la quotientation.

47Par ailleurs, dans la mesure où la preuve sous sa forme réticulaire apparaît comme un objet ouvert sur l’environnement via ses multiples conclusions (au tant de ports d’entrées-sorties potentiellement ouverts à une composition avec d’autres preuves / processus), objet dont la composition n’est plus singulière et séquentielle, mais plurielle et parallèle, la temporalité du processus d’analytisation correspondant, libérée, gagne en structure et en élasticité : la temporalité simple d’un déroulé narratif singulier laisse la place à une temporalité plurielle, associant en parallèle des déroulés multiples aux rythmes indépendants.

  • 34 Cf. le vaste corpus de recherche autour des contraintes de « focalisation » (Jean-Marc Andreoli) al (...)
  • 35 Comme objet statique (texte ou réseau), la preuve peut être conçue comme un moment, un arrêt-sur-im (...)

48Enfin, la disparition des étapes inessentielles conjuguée à la possibilité de pouvoir abstraire l’un de ces « déroulés » des interférences apparentes avec ses congénères en réalité indépendants, permet de repérer derrière le morcelle ment et la succession superficiellement désordonnée des étapes ayant subsisté, un tempo, une pulsation plus fondamentale, scansion dialectique de l’inter action logique : l’alternance de phases « polarisées » (dites « positives » et « négatives » ) où « la main », alternativement, revient au processus courant ou à son opposant, l’environnement34. La preuve, ainsi dégagée, est donc un être processuel en interaction avec son environnement et dont la structure interne s’identifie à la définition de ses capacités d’interaction35.

5. Le temps retrouvé

49Sous ce nouveau jour, loin d’être cette théorie de lois logiques hors du temps qu’elle pouvait sembler être, la logique apparaît proprement comme la théorie fondamentale de l’interaction calculatoire et communicationnelle entre processus, théorie de la dynamique informationnelle traversée de part en part par la question du temps.

  • 36 Disqualifié (au profit du discours) comme point de départ (tant historique que technique) de la log (...)
  • 37 Cf. les analyses de l’article de F. Bailly et G. Longo dans le présent volume.
  • 38 Deux dynamiques dont la Ludique permet déjà de rendre compte de manière unifiée pour un fragment im (...)
  • 39 Y compris sa fameuse élasticité : problématique lorsqu’on se représente l’évaluation chez un indivi (...)
  • 40 Mais pour mettre en relief la spécificité méthodologique de cette approche du raisonnement et lever (...)

50Ce renversement copernicien du point de vue logique sur le temps opéré par la logique contemporaine conduit naturellement à interroger en de nouveaux termes la relation entre cette dynamique de l’interaction logico-calculatoire et celle du raisonnement (bien distingué cette fois de la démonstration) et à avancer la thèse philosophique de leur éventuelle identité36. La question ici n’est plus celle longuement débattue au long du XXe siècle, et devenue banale, de la réductibilité de la pensée rationnelle au calcul (posée peu ou prou en les termes, inadéquats, de la simulabilité du cerveau humain par une machine de Turing ou l’un de ses avatars37), mais celle de l’isomorphie éventuelle entre dynamique de l’heuristique et dynamique de l’analytisation38. Une telle issue donnerait à l’approche phénoménologique de l’expérience mathématique un nouvel outil (dégagé de tout présupposé sémantique représentationaliste) et, à la suite du temps grammatical et du temps pratique, le temps psychologique lui-même39 (du moins le temps retrouvé de la rationalité), enfin objectivé, finirait à son tour par recouvrer un statut logique − ce que le divorce inaugural de la Logique avec la Psychologie semblait apriori interdire40.

51En défaveur de cette « thèse », on pourrait être tenté d’objecter que les traits les plus saillants de la dynamique rationnelle humaine sont ses erreurs, ses er rances, ses confusions, ses abandons, et estimer par conséquent qu’identifier la dynamique des preuves structurée par les « règles logiques » au raisonnement, serait à la fois sombrer dans le dogmatisme normatif imputé au positivisme logique et passer à côté de la véritable rationalité.

52Une telle argumentation est toutefois renversée ou plutôt retournée par le fait que la dynamique des preuves mise à jour est en réalité identifiée par la théorie de la démonstration comme ne formant que le cas particularisé d’une dynamique plus générale où ces caractères « débridés » de la rationalité ont justement leur place.

  • 41 Sans doute conviendrait-il cependant de rendre ici justice aux vues pénétrantes d’Aristote sur la c (...)
  • 42 Une contradiction permet de typer des termes du lambda-calcul non normalisant et non résolubles : e (...)

53En effet, tandis que la tradition logique, au long de l’histoire de la discipline, ne s’intéressa guère aux inférences « fautives » que pour mieux les oublier de l’autre côté de la ligne de démarcation les excluant41, le recul panoramique qu’offre le point de vue dynamique, permet d’envisager de façon homogène preuves et non-preuves, autrement dit reconnaît également à ces dernières une existence bien déterminée en tant que processus rationnels. Le statut dynamique des paradoxes est emblématique à cet égard : ils apparaissent comme le paradigme des processus « divergents » (absence de terminaison, mais aussi absence de productivité informationnelle42).

  • 43 Complexité dite « implicite ».
  • 44 C’est l’idée même de « typage » d’un calcul.

54En outre, ainsi envisagée, la ligne de démarcation entre inférences correctes et incorrectes n’est plus le fait d’un décret promulgué ex machina au nom d’une raison normative, mais émerge au contraire a posteriori : dans l’univers infini et sans lois préalables des processus sauvages, c’est parce que leur dynamique leur confère des propriétés particulières (typiquement : la finitude ou encore la terminaison dans des limites déterminées de complexité43, la confluence etc) que certaines constructions inférentielles (qu’on peut voir comme autant d’outils de discipline ou de domestication de cette dynamique44) survivent.

55Du haut du nouveau belvédère, non seulement, comme on l’a déjà dit, la logique n’est pas cette théorie indifférente au temps qu’elle a longtemps pu sembler être, mais elle apparaît en fait tout au contraire comme la théorie même de l’apprivoisement du temps rationnel.

Notes

1 Cette métaphore très usitée du « contenu » de signification relève à mon avis surtout du poncif ; son effet principal me semble être trop souvent de brouiller les pistes.

2 Comme il est plus ou moins traditionnel en théorie de la démonstration, le terme morpho logie renvoie ici au premier « niveau d’articulation » (pour reprendre la terminologie issue de la linguistique), à savoir l’articulation des « idéogrammes » composant le texte formalisé (le niveau de la définition des formules) − le second « niveau d’articulation » (celui de la définition du texte argumentatif ou démonstration ou preuve) étant désigné par le mot syntaxe.

3 Le cas des « logiques modales temporelles » visant à modéliser des adverbes temporels par des axiomatisations idoines, fait bien sûr ici exception. On verra toutefois plus loin que la temporalité en question n’a ici rien à voir avec la temporalité logique, celle du raisonnement.

4 Le dédoublement terminologique proposé par de nombreuses langues (ainsi de l’anglais, qui distingue Time et Tense) attise le soupçon d’un apparentement purement nominal ou superficiel entre le « temps » grammatical − la conjugaison − et les diverses instances du « temps » processuel. Expliquer la nature complexe du lien entre ces deux notions est indirectement l’objet de cette étude.

5 Subsidiairement, observons que toute dimension temporelle qui aurait pu éventuellement subsister dans la notion d’ » interprétation » adoptée (cf. notamment la glose des interprétations de Kripke pour la logique intuitionniste en termes d’évolutions temporelles des connaissances) aurait été en tout état de cause neutralisée (dans cette approche de la notion de « loi logique » ) par la quantification universelle sur les interprétations qu’elle comporte − l’universelle validité, pourrait-on dire, englobant l’intemporelle validité.

6 Des « prémices », pourrait-on écrire, vers la conclusion.

7 L’expression imagée « flèche du temps » n’a pas ici la valeur déterminée qu’elle prend dans le contexte des théories physiques du temps où elle vient désigner l’irréversibilité des phénomènes (cf. Étienne Klein, Les tactiques de Chronos, Coll. Champs, Flammarion, Paris, 2004)

8 Typiquement, preuves représentées par des « arbres » (dont les nœuds sont des formules et les embranchements des règles logiques).

9 La « déduction naturelle » fut élaborée avec l’intention explicite de figurer, d’imiter, dans le cadre du langage de la logique des prédicats, la manière dont les mathématiciens rédigent leurs démonstrations (cf. G. Gentzen, « Untersuchungen über das logische Schliessen », in Mathematische Zeitschrift, 39 :176-210,405-431, 1935).

10 Cf. l’article de J.-Y. Girard dans ce volume.

11 Cf. dans la typologie des conjugaisons, et plus précisément des « aspects » verbaux, la distinction de l’imparfait et du parfait.

12 Les langages de la logique formelle étant des langages idéographiques (i.e. sans le premier niveau d’articulation propre aux langues alphabétiques), le premier niveau d’articulation du langage y est d’emblée celui des énoncés (ceci dit au prix d’une légère approximation).

13 On pourrait être tenté de considérer que ce rapprochement de la distinction opérée par la Logique Linéaire avec la distinction grammaticale traditionnelle, n’a d’autre valeur que celle d’une analogie vague et superficielle. En particulier, on pourrait estimer que la classification grammaticale des types de conjugaisons (aspects perfectifs versus imperfectifs) correspond à une classification des modalités temporelles du référent (actes éphémères versus actions durables) extérieur au discours et relatif à une interprétation donnée du langage (à la manière des sémantiques à la Kripke pour la logique temporelle ou encore, moins formellement, eu égard à un cours du récit narré), tandis que la distinction propre à la logique linéaire renverrait plus prosaïquement à une temporalité interne et pratique de l’activité démonstrative discursive (typiquement « réutilisation d’une hypothèse » etc). On observera tout d’abord qu’au sein même de la « textologie » (le chapitre de la linguistique ayant pour objet l’unité textuelle elle-même − celle où, en particulier, une grammaire spécifique du récit prend ses marques) la thèse selon laquelle les « temps grammaticaux » ont avant tout une fonction de gestion de la chronologie interne de construction du texte a ses défenseurs (cf. H. Weinrich, Tempus,1964 ; éd. consultée : Le temps, traduc. Lacoste, éd. Le Seuil, 1973, Paris). Les présentes investigations tentent de dé montrer que ce dernier point de vue n’interdit pas l’identification d’une référentialité narrative afférente non représentationaliste.

14 Souvent seulement nominale sans doute, cette identification, ce manque de distinction, n’en demeure pas moins symptomatique d’une certaine confusion.

15 Pour une discussion plus approfondie de l’opposition démonstration-raisonnement, voir J.-B. Joinet, « Proofs, reasoning and the metamorphosis of logic », texte d’un exposé donné dans le cadre de la conférence Natural Deduction, Pontifícia Universida de Católica do Rio de Janeiro, 2001 (actes en cours de publication sous la direction de Luiz Carlos Pereira).

16 Cf. J.-Y. Girard, « Linear Logic », Theoretical Computer Science, 50 :1-102,1987 et l’abondante littérature associée.

17 Ceci ne vaut certes pas dans le cadre non symétrique de logiques sans dualité (comme la logique intuitionniste)

18 La diégèse est « l’univers spatio-temporel auquel se rattache l’histoire narrée par un récit ». Est « diégétique » ce qui se rapporte ou appartient à l’histoire narrée, à la trame du récit. Cette terminologie a été popularisée et précisée par Gérard Genette dans ses analyses « narra tologiques » des problèmes du récit (cf. « Discours du récit », in Figures III, Paris, Seuil, et en 1983, dans « Nouveau discours du récit » ).

19 Ordre linéaire, cursif, dans les langues naturelles, mais il s’agit là d’une caractéristique contingente.

20 En partie aussi, certes, en raison de la faiblesse de leur valeur littéraire ! On est loin de la Recherche du temps perdu...

21 John L. Austin, Quand dire c’est faire, 1962 (traduc. française, Coll. Points, Seuil, 1979). Appliqué au cas des programmes informatiques et des preuves, le terme est déjà présent dans la thèse de Vincent Danos (Thèse de doctorat, spécialité mathématiques, La logique linéaire appliquée à l’étude de divers processus de normalisation, soutenue le 20 juin 1990 à l’Université Paris 7).

22 Mais nous verrons bientôt que cela vaut aussi bien pour ces autres textes que sont les preuves, et en fait même que, les concernant, la textualité n’étant ici qu’épiphénoménale, le point de vue performatif sur la narration reste pertinent une fois le paradigme des preuves comme-textes dépassé.

23 Soit encore, pour utiliser la terminologie technique des linguistes : le « sémème » performatif.

24 La temporalité de la construction de preuves est celle du processus de réponse à la question « tel texte est-il une preuve correcte de cet énoncé ? », la temporalité de la recherche de preuves est la temporalité du processus de réponse à la question « existe-t-il une preuve correcte de cet énoncé ? ».

25 Sous réserve de cohérence de l’arithmétique.

26 Ce constat, intervenu très tôt dans l’histoire de la logique (dès Leibniz sans doute, qui don nant dans ses Nouveaux essais sur l’entendement humain la première preuve, en fait incomplète comme on sait, de » deux et deux font quatre » pose le cadre du dialogue entre théorie de la recherche de preuves et théorie du calcul) a été le point de départ, dès le début du xxe siècle, de nombreux travaux de logique et de théorie de la calculabilité, trop connus pour qu’il soit besoin ici d’insister.

27 On a vu plus haut que la textualité des preuves n’est qu’épiphénoménale. En vue d’aborder en propre la question du récit et de la diégèse (plus communément abordée dans le contexte de l’analyse de textes), il fait cependant sens, pédagogiquement parlant, de revenir provisoirement aux preuves comme textes.

28 L’énoncé n’est ici envisagé comme producteur d’effets calculatoires que relativement à des stratégies heuristiques fixées. Le langage de programmation PROLOG (pour PROgrammation LOGique) est une réalisation exacte, dans un cadre restreint, de cette approche.

29 Une façon alternative de se représenter plus directement et exactement la composition des programmes (ici, pour simplifier, au travers d’une métaphore), consiste à se représenter le branchement de deux prises duales, l’une apportant un flux de type A en sortie l’autre recevant un flux entrant de type A.

30 L’existence et la réalisabilité de telles conversions (autrement dit la convertibilité des preuves − en un mot leur « analytisabilité » ) ne va pas de soi, et le fait que les preuves et donc leurs composants, les règles logiques, se prêtent à cette conversion, constitue en fait un critère (à tout le moins nécessaire) de la logicité des règles.

31 Systèmes dont les règles formalisées imitent celles de la culture logique commune.

32 À la formulation « alternative » de la composition des programmes sous forme de « branchement » donnée plus haut (note 29) correspond, du côté de la composition des preuves, l’usage d’une règle spécifique d ite de » coupure ». L’introduction d’une telle règle dans di vers formalismes (comme le « calcul des séquents » ou les « réseaux de preuves » évoqués plus haut) vient corriger l’illusion d’optique faisant apparaître la « composition des preuves » dans le cadre des systèmes de « déduction naturelle » comme étant non pas une opération spécifique initiatrice de dynamique, mais un simple effet collatéral de certains agencements de règles logiques.

33 Cette identité est connue depuis 1969 sous le nom de « correspondance de Curry-Howard » : l’analytisation des preuves en déduction naturelle intuitionniste implicative d’une part, l’évaluation des programmes en lambda-calcul simplement typé d’autre part, s’avèrent simplement être deux notations distinctes pour un même phénomène. Il s’agit en fait d’une simple remarque : son importance ne provient pas de sa complexité, mais de la richesse de ses conséquences. En contre coup du constat de cette identité entre les preuves (et leur analytisation) et les programmes (et leur évaluation), le processus d’analytisation des preuves (abordé en pionnier par G. Gentzen qui, dans les années 1930, visait par ses investigations à élaborer un outil en vue de démonstrations de cohérence pour l’arithmétique du premier ordre) sous les noms de « normalisation » et d’ » élimination des coupures » est devenu, à partir des années 1970, l’objet d’étude central de la théorie de la démonstration... et l’interface principal du dialogue entre logique et informatique théorique. À défaut de pouvoir présenter ici ce « dialogue », on peut du moins rappeler l’inter-traduction des éléments principaux du lexique concerné : preuves =programmes, règle =instruction de programmation, formule = spécification du programme (type), analytisation =évaluation.

34 Cf. le vaste corpus de recherche autour des contraintes de « focalisation » (Jean-Marc Andreoli) alias les « η-contraintes » (Vincent Danos, Jean-Baptiste Joinet et Harold Schellinx) et de « polarisation » (Jean-Yves Girard, Olivier Laurent...), et aux modèles de l’évaluation en termes de jeux (Martin Hyland et al.) y compris la Ludique (J.-Y. Girard).

35 Comme objet statique (texte ou réseau), la preuve peut être conçue comme un moment, un arrêt-sur-image du processus.

36 Disqualifié (au profit du discours) comme point de départ (tant historique que technique) de la logique scientifique, le raisonnement serait en somme aujourd’hui restauré comme objet possible de science à son point d’arrivée.

37 Cf. les analyses de l’article de F. Bailly et G. Longo dans le présent volume.

38 Deux dynamiques dont la Ludique permet déjà de rendre compte de manière unifiée pour un fragment important de la logique.

39 Y compris sa fameuse élasticité : problématique lorsqu’on se représente l’évaluation chez un individu comme séquentielle (car l’élasticité peut seulement alors prendre le sens d’une accélération-décélération du temps, idée paradoxale ou confuse), cette élasticité cesse de l’être dans le contexte d’une évaluation « répartie ».

40 Mais pour mettre en relief la spécificité méthodologique de cette approche du raisonnement et lever d’éventuels malentendus peut-être serait-il judicieux, plutôt que d’évoquer « le temps psychologique », terminologie profondément marquée par une longue tradition philosophique, de parler ici plutôt de « temps cognitif » ou de « temps rationnel ».

41 Sans doute conviendrait-il cependant de rendre ici justice aux vues pénétrantes d’Aristote sur la contradiction comme déréliction de l’interaction dialogique (Aristote, Métaphysique Gamma).

42 Une contradiction permet de typer des termes du lambda-calcul non normalisant et non résolubles : en termes de narration, comme l’avait bien vu Aristote, ils parlent infiniment, mais ne disent jamais rien. Sur le « sens » calculatoire de la contradiction, voir aussi la « Ludique » de J.-Y. Girard.

43 Complexité dite « implicite ».

44 C’est l’idée même de « typage » d’un calcul.

© Éditions de la Sorbonne, 2007

Conditions d’utilisation : http://www.openedition.org/6540