Compliqué? La preuve

Puisque la foule en délire demande des détails sur le contenu de mon périple tout frais de Paname, je vais m'essayer à un résumé plus ou moins condensé des interventions de vendredi après-midi.

Le décor: l'Université Paris-Diderot, Paris 7 pour les intimes, par un temps bien ensoleillé et sec comme j'aime le sentir dans ma bonne Lorraine et ... mais je m'égare et la militante dissidente ne va pas aimer. Allons au fait, donc.

Première conférence: Dag Prawitz, de l'Université de Stockholm. Intitulé du sujet: "The validity of inference". Problème posé: comment garantir qu'une inférence est valide, c'est-à-dire qu'elle est menée correctement depuis sa ou ses prémisses jusqu'à sa conclusion et préserve la vérité de l'un à l'autre? Précision: Prawitz appartient à l'école de Stockholm ou suédoise, de tendance intuitionniste ou plutôt constructive et dont les réquisits pour décrire le processus d'une preuve sont plus contraignants que ceux des logiciens ou mathématiciens que l'on appelle "classiques".
Avant que tout le monde ne tombe dans le ravin de mes explications, je précise que le classique est à l'intuitionniste ce que le classicisme est à l'expressionnisme dans les beaux-arts. Ou à peu de choses près: les premiers recherchent la simplicité, l'harmonie et l'efficacité dans la conduite des travaux, tandis que les seconds veulent que la structure d'ensemble prenne en compte les conditions de travail de l'architecte, que celui-ci soit affairé à la construction d'une preuve ou d'un bâtiment.
"Et la vérité, dans tout ça?", me direz-vous naïvement et, donc, à juste titre? Prawitz ne conteste pas la validité de certaines inférences classiques, il admet à dire (vrai) la grande majorité d'entre elles. Alors pourquoi venir à Paris tailler le bout de gras sur des pécadilles ... c'est que la notion de vérité en jeu dépend plus ou moins du sujet constructeur, chez les partisans dont Prawitz est un membre attitré.
... prenons une inférence et sa forme générale, de type: A, donc B. Pour économiser le temps, l'encre ou les touches du clavier, on réduit ceci symboliquement sous la forme: A |- B, ou le "|-" s'appelle "turnstile" (ou "tourniquet") et représente la transformation d'une formule de départ en une formule d'arrivée qui est sa conclusion. Or classiques et intuitionnistes ne s'entendent pas tout à fait sur l'ensemble des valeurs de B partant de A. Exemples hyper-connu dans le milieu et sans cesse rebattus depuis le mathématicien pionnier de l'intuitionnisme, Luitzen Egbertus Jan Brouwer: le principe du tiers exclu, la réduction par l'absurde qui en découle, puis d'autres discussions fondamentales sur le rôle de l'axiome du choix dans le calcul des preuves dans un contexte d'informations de longueur indéfinie voire infinie. On en revient à Aristote et sa discussion centrale sur la nature de l'infini (réel? potentiel?) ...
... question de Prawitz: que doit-il se passer lorsque l'on passe de A à B, afin que la transformation lors de l'inférence soit considérée comme valable? Précision: l'inférence est l'ensemble de l'opération effectuée par celui qui prouve que B résulte de A, ou que de A il s'ensuit B. Retour à la case Lewis Carroll et son Paradoxe de la Tortue. Je parle bien ici du Carroll d'Alice au Pays des Merveilles car, pour ceux qui ne le savent pas, Charles Dodgson de son vrai nom était passionné de mathématiques et de logique. L'intéressé écrivit dans la revue "Mind" ce très fameux paradoxe dans lequel la tortue demande au lapin ce qui permet d'obtenir la conclusion dans un Modus Ponens. Référence: "What the Tortoise Said to Achilles, Mind 4, n°14 (April 1895), pp. 278-280. Désolé pour les barbarismes de circonstances ... Modus Ponens = si j'ai A, alors j'ai B; or j'ai A; donc j'ai B. Opération si simple qu'on se demande presque pour quelle raison la discuter. La tortue insiste: comment parviens-je de A à B, ici? Le lapin: si tu as A, et si tu sais que de A tu peux déduire B, alors tu sais que tu as B. La tortue: certes; mais comment sais-tu lorsque de A tu peux déduire B. Le lapin, légèrement gonflé par l'animal à carapace persistante: si tu sais que de A tu peux déduire B, alors si tu sais que tu as A et que de A tu peux déduire B, alors ... total: régression à l'infini, c'est-à-dire une chaîne sans fin d'étapes intermédiaires pour passer du simple A au simple B. Symboliquement, l'ensemble de la procédure apparemment si simple donne à peu près ceci:


A
--- (Inférence niveau 1)
B

A, A|-B (Inférence niveau 2)
----------
B

A, A|-B, (A,(A|-B))|- B (Inférence niveau 3)
--------------------------
B

............ ...............

A, A ... (A|-B)n (Inférence niveau n)
------------------
B


Pour des précisions sur Carroll et sa discussion sur l'inférence distincte du conditionnel, voir l'ami philosophard Amirouche Moktefi puisque celui-ci est devenu un spécialiste de l'oeuvre logique de Lewis Carroll (cf. billet précédent parmi mes "Coup de pub").

Conscient de la difficulté, Prawitz prétend qu'une reconstruction ou, plutôt, une reformulation symbolique du processus de la preuve doit être effectuée afin d'expliquer dans les détails les conditions dans lesquelles le passage de A à B est effectivement garanti. On obtient une logique dans laquelle le sujet qui opère a sa place au sein du symbolisme, contrairement à la logique classique ou non-constructive dans laquelle la construction ne se montre pas elle-même dans le symbolisme.
Clair? Un sujet assez subtil, qui demande plus de finesse et d'esprit que dans ce billet (désolé) et dont la problématique a été nettement traitée dans le Tractatus Logico-Philosophicus de Wittgenstein. Pour celui-ci: certaines choses se montrent et ne se disent pas, parmi nos opérations permanentes de la pensée. Traduction: impossible pour lui de décrire ce qui se passe lors d'une opération déductive, preuve ou inférence. La chose se fait, et c'est la reproduction inlassable de la même dérivation qui donne à l'ensemble de l'inférence sa certitude et sa garantie.
Transition intéressante puisque c'est de la certitude de ce qui rend une inférence vraie que le second conférencier a parlé après Prawitz. Mon big boss du moment, sur lequel je revendrai avec son accord très tacite.

Mais revenons et terminons avec Prawitz: le Suédois propose donc une autre symbolisation, un autre langage logique plus fourni afin de "montrer" les étapes de construction d'une preuve. Une relation R de forme R(P,I) s'effectue entre une personne P qui prouve et une inférence I à prouver; plus précisément, l'inférence réalisée par P consiste à effectuer une opération "Phi" (pas de lettre grecque dispo ici, on fera avec les abréviations) qui fait passer d'une première étape de la preuve G1 à une n-ième étape Gn: l'opération d'une inférence correspond donc au schéma général de forme Phi(G1,Gn), et le rôle du constructiviste est de mettre à jour toutes les caractéristiques qui, dans cette opération, garantissent la validité de l'ensemble. Ne rien laisser au hasard et entrer dans les détails, donc. Complications supposées nécessaires pour expliquer la véritable nature d'une connaissance mathématique, à l'opposé des classiques plus soucieux de simplicité dans les formes. Dans les beaux-arts comme dans les preuves formelles, s'entend.

Pour conclure, Prawitz propose un ensemble de règles de déduction naturelle, c'est-à-dire des symbolismes formels dans lesquels une preuve est détaillée sous ses multiples facettes, selon le A de départ et le B attendu à l'arrivée. D'autres scandinaves le suivent sur cette voie, parmi lesquels Per Martin-Löf et Göran Sundholm.
Ma question, avant de retourner dans mes bulles internes: qu'apprend-on réellement de plus lorsque l'on passe par la méthode constructiviste, et a-t-on besoin de ces détails supplémentaires pour saisir l'essentiel d'une preuve logique ou mathématique (la différence m'échappe encore et toujours dans ses détails)? Les constructivistes proposent d'autres manières de définir le passage de A à (AouB), le passage de (AetB) à A ... mais y gagne-t-on réellement en compréhension du processus de preuve? C'est là que le bât blesse, selon que l'on répond oui ou non à cette question méthodologique. En gros: pourquoi se fouler et compliquer la tâche si seul le résultat compte, c'est-à-dire le passage d'un point à un autre quel que soit le chemin emprunté?
C'est un problème qu'on dira "philosophique": est-il plus important de connaître le chemin menant de A à B, ou d'arpenter ce chemin par soi-même et dans des conditions qu'il faut prendre en compte afin de comprendre B? Morphéus, quand tu nous tiens, le ciné n'est plus très loin des spéculos ... mieux: le choix dans le chemin traversé pour aller de A à B peut-il modifier la nature de B? On aurait tendance à dire que non, puisqu'il très possible d'arriver à un même endroit par deux chemins distincts. Mais l'analogie a des vertus limitées: peut-on comparer des lieux spatio-temporels A et B à des arguments de preuve?

Je m'arrête là, insuffisamment instruit que je suis sur les travaux de Prawitz mais suffisamment intéressé pour avoir troué la tête de la militante dissidente à ce stade du billet. Du moins le crois-je. J'ai mes propres réticences face à l'approche constructiviste, concernant l'intérêt véritable de ces complications symboliques ou le rôle épistémologique qu'il prétend tenir pour ce qui est de mieux expliquer la nature d'une preuve en termes d'inférence (une preuve faite par quelqu'un sans qui preuve il n'y a pas). Mais il y a réticence et résistance, et sans doute ma résistance n'est-elle rien de plus que ce que Bachelard appelait un "obstacle épistémologique": une incapacité à comprendre la façon dont un autre fonctionne dans son raisonnement en raison de présupposés divergents et inaperçus. J'ai tenté de les mettre à jour dans une section de ma thèse, mais j'y reviens en vitesse plus bas.
Frege a dit que ce n'est pas le promeneur qui fait le chemin, car celui-ci existerait encore et déjà si le promeneur était resté chez lui boire une bière et mater Téléfoot. C'est ce qu'il a voulu faire comprendre à peu de choses près. C'est là une intuition profondément enracinée en nous mais que tout un courant réduit à un jeu de tiroirs rejetter sous l'appellation d'antiréalisme: l'idée selon laquelle la réalité est dépendante de ceux qui l'appréhendent sous quelque manière que ce soit (l'observation pour les preuves informelles de la vérité d'un fait, la démonstration pour le versant formel de cette vérité).
Je n'ai rien à redire contre ce fossé réalisme vs. antiréalisme; j'ai eu plus à dire dans la seconde partie de ma thèse, concernant les moyens proposés par les constructivites afin de donner une meilleure explication de la preuve: qu'est-ce que ce "Phi" dont on a parlé tout à l'heure, sinon un autre symbole que l'opérateur K de Hintikka mais dont les effets seraient les mêmes? Je m'explique: K signifie "je sais", donc le rôle essentiel de l'agent dans la conduite de la preuve dépend d'un agent dont la présence était manifesté dans la logique épistémique de Hintikka, autre scandinave (mais finlandais et non constructiviste, pour sa part). Peut-on remplacer Phi par K, et même le tourniquet "|-" par ce même K? Dans ce cas, quelle différence substantielle entre le formalisme des constructivistes et la logique modale, cette extension de la logique classique dans laquelle sont introduits de nouveaux opérateurs? Je ne saisis pas bien la fécondité et l'apport essentiel du formalisme constructiviste, face à la logique modale et ses constructions de type Kripke plus simples ... affaire à suivre, et pour plusieurs années parce que le sujet est si profond qu'il vaut la peine de prendre le casque de spéléo et s'engouffrer dans ces problèmes vite complexifiés. J'en connais d'autres qui parlent de faisabilité ou de limitations des ressources déductives pour décrire le champ des preuves garanties ou pas. Mais ces partisans de l'affaiblissement des logiques en vue de leur meilleure explication étaient absents pour des raisons de principe, ou plutôt de concurrence universitaire. Pas convaincu du rôle explicatif des logiques substructurelles dans la description de la preuve et des procédures déductives, mais c'est une autre histoire trop longue pour être revue en détail ici.

Passons aux souvenirs plus personnels d'une fin de rédaction de thèse, au cours desquels j'achevai la journée stressante par des tours de Pépinière (parc nancéien) et m'endormai comme une masse essoufflée plein de Korn à l'oreille. Des bons moments de stress et d'incertitude enrobés par de gros riffs salvateurs et purificateurs. Car le métal me sert de catharsis par temps de pensées brumeuses. Pour la bonne peine, voici le morceau que j'écoutai en boucle afin de poursuivre mes pseudo-méditations modales et constructivistes mêleées. "Twisted Transistor", dont le clip sans intérêt m'a donné une raison valable de préférer une autre adaptation:



Première piste d'un album qui, nouvelle coïncidence du genre, p
ortait comme titre "See You on the Other Side" et faisait référence au miroir à deux faces d'Alice au pays des merveilles. Comme quoi la tortue de Lewis Carroll et son Alice ont fait équipe bon grè mal gré durant ma fin de rédaction universitaire. Hasard? Avouez qu'il se passe des choses bizarres par ici.
Prochain billet possible: sur la controverse méthodologique entre Dedekind et Kronecker concernant la conduite d'une preuve. Même combat mais en termes différents et sur des thèmes plus mathématiques. J'hésite à m'aventurer sur ce terrain qui m'est très mal connu. Mais la dissidente niçoise en jugera ... heureuse?!!!


F&H