Je continue ma série sur la logique tout en sachant que peu de lecteurs iront spontanément me suivre. Il faudrait pour cela que je sois plus convaincant dans mes explications que la logique peut intéresser tout le monde. « Ouvrir la logique au monde » tel était le titre d’un livre dirigé par Samuel Tronçon et Jean-Baptiste Joinet en 2009 (d’après un colloque de Cerisy portant ce titre). Ce livre contenait des interventions de Jean-Yves Girard, Giuseppe Longo et quelques autres (Michel Bitbol, Pierre Livet, Bernard Teissier…) qui tentaient de réfléchir à l’apport de la logique contemporaine à notre connaissance du monde au travers notamment de la notion de calculabilité (par exemple : la thèse de Church physique, celle selon laquelle l’univers calcule et les fonctions qui s’y révèlent sont donc « calculables », est-elle valide ?). Si j’en crois l’horizon actuel, post-pandémie et en plein dans la crise climatique liée au réchauffement de la planète, une nouvelle pensée serait requise, au sens d’une nouvelle manière de penser le monde (parce qu’on ne va pas brutalement, sans transition, installer une nouvelle pensée comme si on transplantait un nouveau cerveau à la place de l’ancien chez toute personne qui se mettrait en devoir de réfléchir). Ils disaient « Nouveau monde » mais il fallait dire « nouvelle manière de penser le monde », or qui ne voit que pour cela, il faudrait d’abord opérer une critique de nos instruments anciens de pensée, et donc en premier lieu de la logique qui est à la base de nos raisonnements ? Je viens de découvrir le livre « Bifurquer », écrit par un collectif (« les amis de la génération Greta Thunberg ») qui comprend, entre autres Bernard Stiegler, Jean-Marie Le Clézio et le sus-nommé Giuseppe Longo, autrement dit des anthropologues, des écrivains, des mathématiciens, des philosophes et même des artistes et des designers. Cela semble être une entreprise salutaire de repenser notre monde, que je salue, et c’est en tout cas une belle initiative interdisciplinaire visant à réviser les fondements de nos savoirs. Pas de logicien dans cette assemblée (Girard et Longo ont dû se fâcher)… Dommage.


Pourquoi votre fille est muette ? L’égalité et les individus etc.
Dans mon précédent billet, je faisais part d’un premier étonnement : comment tirer de l’existant à partir de rien ? D’autres étonnements sont possibles. Ainsi figurera toujours comme axiome la formule A => A, ou, ce qui revient au même, la règle selon laquelle de A on peut toujours déduire A, qualifiée en général de règle d’identité. Quoi de plus naturel qu’admettre en effet que si A est vrai, alors… A est vrai ! Oui, mais alors pourquoi a-t-on besoin d’un axiome pour le dire ? De fait, dans la logique « réelle », nous ne déduisons jamais A d’un A que nous savons déjà être vrai, ou alors cela s’appelle une pétition de principe : si votre fille ne parle pas, madame, c’est qu’elle est muette. Une manière de prouver que A => A est vraie (dans un système dit « de la déduction naturelle ») consiste à poser A comme hypothèse puis, par simple réitération de l’hypothèse, à réécrire A (tour de passe-passe qui ne convainc pas), après quoi, on « décharge » l’hypothèse A et on dit : vous voyez, A « implique » A… Une autre formule semblable est A => (B => A) que l’on démontre ainsi : se plaçant sous l’hypothèse que l’on a A, on fait n’importe quelle autre hypothèse B et, comme dans la précédente, on réinscrit en dessous A par réitération de l’hypothèse. Formule extraordinaire qui vous permet de dire :
du fait que l’on puisse guérir de la covid 19, je peux déduire sans problème que si la chloroquine est administrée alors on peut guérir de la covid 19… (mais aussi bien en administrant de l’oscillococcinum ou de la poudre de perlimpimpin).
Autre bizarrerie, contrairement à ce que l’on pourrait croire, en prenant trois propositions arbitraires, il se trouve que nécessairement deux au moins d’entre elles sont équivalentes, on peut en effet prouver :
(A <=> B) ∨ (A <=> C) ∨ (B <=> C)
ce qui, on en conviendra, laisse bien peu de place pour exprimer des propositions nuancées !
Et que dire des « individus » qui peuplent notre univers, ceux dont le nominalisme voudrait reconnaître comme seules entités « existantes » ? (voir la querelle des universaux). Outre que nous avons du mal à délimiter pratiquement ce que nous entendons par « individus » (cela dépend vraiment du regard adopté, suis-je un individu moi-même ? Ou bien ne faut-il pas plutôt considérer que ce sont les cellules qui sont des individus. Les micro-organismes ? Les virus?), il est très difficile théoriquement de dire quand nous sommes en présence de deux individus identiques ou différents. Ici intervient l’enjeu délicat de l’égalité. Quoi de plus simple et de plus répandu que le signe « = » ? et pourtant, est-il seulement défini ? Une relation d’équivalence comme une autre, appris-je en classe, oui mais alors comment la distinguer ? Leibniz eut la bonne idée de dire que deux individus sont égaux si et seulement s’ils ont exactement les mêmes propriétés (ce qui implique de nouvelles entités : les propriétés, et nécessiterait que l’on quantifie sur elles avec toutes les difficultés que cela comporte etc.).
t = u si et seulement si toute propriété de t est propriété de u et réciproquement
ah bon, mais immédiatement saute aux yeux une propriété de t qui n’est pas celle de u… la localisation spatiale (t est à gauche de u). De la délicatesse des individus et de leurs propriétés…
Tout ceci (et d’autres choses encore…) fait dire à Jean-Yves Girard que, décidément, non, la logique classique n’est pas la logique…
En passant, soulignons les aberrations d’une pensée totalement centrée sur ces vieilles querelles qui tournent autour de ce qui existe vraiment, les individus ou les propriétés (ou les concepts etc.). W. V. O. Quine a régi le monde de la philosophie américaine pendant presque un siècle, il s’inscrit dans la continuation de Russell et a donné, certes, quelques œuvres qui méritent d’être lues attentivement, mais il avait décidé une bonne fois pour toutes que seule la logique des prédicats du premier ordre était la véritable logique, allez savoir pourquoi… au nom d’un nominalisme enraciné. Il avait un solide mépris pour le second ordre (et aussi pour les logiques modales, qui, il est vrai, n’apportent guère à nos efforts, quoiqu’on en dise). D’où cette maxime célèbre : « être, c’est être la valeur d’une variable » (seul existe ce sur quoi peut porter un quantificateur). Une telle restriction de l’existence est typiquement ce qui peut sembler dangereux en ce monde qui demande à ce que l’on réfléchisse à bien d’autres entités que les individus… (l’idée quinienne est la même que celle jadis affirmée par les économistes néo-libéraux à la Hayek ou les politiciens à la Thatcher selon qui il n’y aurait rien de tel qu’une « société » – no such thing as society – puisqu’il n’y aurait que des individus !).

et les mathématiques dans tout ça ?
Pourtant, on notera que la logique dite classique fut bien utile quand il s’agissait de garantir la justesse des démonstrations mathématiques (justesse bien approximative avant Frege, du temps de Gauss et de Cauchy…), mais c’est que, du strict point de vue des mathématiques, tous ces défauts ne sont pas si importants. Lorsque l’on accepte de n’envisager une proposition mathématique que sous l’angle de sa bivalence (être fausse ou être vraie), il ne faut pas s’étonner que l’on ait beaucoup de propositions équivalentes ! Ou bien, il n’est pas grave d’avoir des règles de déduction un tantinet absurdes : on ne les utilise pas car elles sont inutiles, le mathématicien peut se permettre de les ignorer, la règle d’identité ne va pas ajouter des conclusions fâcheuses puisqu’il s’agit de répéter la même assertion… Quant à l’idée qu’un univers se doive d’être non vide, on s’en accommode sans difficulté (tant mieux même puisque cela peut éviter des sources d’ennui!). D’où il vient finalement que les mathématiques telles qu’elles sont ne sauraient être remises en cause pour autant. Bien sûr, comme dit plus haut en regard du théorème d’incomplétude de Gödel, on ne parviendra jamais à prouver leur cohérence. Peut-être viendra un mathématicien de l’an 3000 qui détectera une contradiction au cœur de l’édifice causant ainsi son effondrement, mais s’il est assez fort pour cela, sans doute aura-t-il dans sa manche une martingale pour reconstruire une super-mathématique…
Il nous faut nous résigner à notre condition humaine dans tous les domaines, même celui-là, ne sommes-nous pas dans l’impermanence ?
Tout ceci en tout cas semble légitimer le parti pris par Girard d’admettre comme support suffisant à ses travaux la bonne vieille théorie des ensembles, dite théorie ZF (pour Zermelo-Fraenkel). C’est donc sans aucun scrupule qu’on s’autorisera à parler d’ensemble de preuves, d’orthogonal ou de filtre ensembliste. (NB : c’est bien là le seul point commun que l’on peut trouver entre Jean-Yves Girard et Alain Badiou).
La vérité dans les preuves… et les réseaux de preuve
Il reste que ce n’est pas parce que la logique classique sert de bon outil technique (un bon marteau, une bonne clé anglaise, mais on ne demande pas à un marteau de faire plus que ce qu’il lui est possible de faire) qu’il faut l’admettre comme expression pure de la logique au sens où nous l’avons caractérisée précédemment comme soubassement du langage et même de notre monde.
Mais alors où saisir cette insaisissable logique ?
Ailleurs sans doute que dans les formules, les variables et les constantes « individuelles ».
Qu’est-ce qui peut être « vrai » ? des formules ? Mais comment vérifierions-nous leur vérité si ce n’est en nous référant à des modèles qui, par essence, ne sont que des transpositions du même sur un autre plan (car les logiciens des modèles ne font jamais que mettre en relation des langages les uns avec les autres, ils ne mettent jamais en relation un langage avec « la réalité » puisque celle-ci s’échappe à tout jamais…) ?
Une preuve, en revanche, peut être qualifiée de « vraie », elle le sera en effet si nous avons vérifié à chaque étape la correction d’une règle appliquée. Ici, nous répondons à la première question d’Ange Scalpel : 1. Comment la logique peut-elle être féconde, si ses inférences sont triviales (paradoxe de Mill) ? À laquelle lui-même répond par : « [Ce] problème peut être résolu si l’on caractérise le domaine de la logique non seulement comme celui de la vérité, mais aussi comme celui de la preuve et de l’inférence ». A quoi nous ajoutons que ce n’est pas seulement « aussi » qu’il faut dire, mais « avant tout », voire « seulement »… et que, autre façon de voir les choses, une preuve pourra aussi être qualifiée de « vraie » si nous avons pu vérifier un critère qui s’avèrerait être un critère de correction infaillible. C’est cela qui nous conduit aux derniers travaux sur « une logique sans système ».
Vérifier la validité d’une preuve en procédant pas à pas suppose que nous soyons au sein d’un système formel, avec ses règles et ses axiomes, reproduction de l’éternel achoppement, celui de notre pensée avec un cadre rigide dont les axiomes ont toujours une part d’arbitraire. La pensée est enrégimentée, corsetée au sein d’une axiomatique, celle-ci fût-elle « non classique » (c’est-à-dire intuitionniste, partielle, libre, dialogique ou… linéaire – au sens de la première version de la logique linéaire, exprimée en calcul des séquents, où l’on voit apparaître des êtres rendus nécessaires par le formalisme mais auxquels on a du mal à conférer un sens, comme des éléments neutres bizarres par exemple). La logique linéaire née en 1987 aura permis au moins de mettre à jour ces entités nouvelles et remarquables que sont les réseaux de preuve. Un réseau de preuve est un graphe (définition : un ensemble de points et d’arêtes, chaque arête reliant deux points) associé à une preuve. La logique multiplicative, celle qui possède comme connecteurs le « par » et le tenseur (℘ et ⊗) (« par » dénommé ainsi pour une lointaine référence au parallélisme, le tenseur étant un « et » multiplicatif, autrement dit une opération de cumuler une ressource avec une autre) et qui possède une négation, ou orthogonalité (interprétable comme changement de point de vue quand on se place dans une perspective dialogique), et qui permet de définir une implication particulière, dite « linéaire », A –o B par A –o B = A┴ ℘ B, c’est-à-dire « contre A je peux avoir B », permet de définir une notion de réseau assez facile : les connecteurs sont représentés par des liens de types différents – un lien est un mini-graphe avec deux arêtes chacune reliant la formule de départ à ses deux constituants reliés soit par un ℘ soit par un ⊗. On admet que les liens de type « par » sont en pointillés et les liens de type « tenseur » en traits continus. Un lien « axiome » est une arête qui unit un atome (formule sans connecteurs) à son orthogonal (soit A à A┴). On démontre (critère dit de Danos-Régnier) que la suite de formules à laquelle est associé le graphe est une preuve si et seulement si le graphe possède une propriété remarquable : toute sélection pour chaque lien « par » d’une des deux arêtes possibles (donc en pointillé) conduit à un graphe connexe et sans cycle.




Ayant vu cela, on se pose la question évidente : mais pourquoi s’en tenir à des preuves données séquentiellement et leur associer ensuite un graphe ? Pourquoi ne pas prendre pour premier objet le graphe lui-même ? Quitte à ce que d’autres construisent une preuve associée dans un système convenable ou… quitte à se passer complètement de « système convenable » ! Alors cela en sera fini de l’idée selon laquelle toute justification de loi logique serait arbitraire et circulaire, deuxième problème d’Ange Scalpel qu’il « résout » en affirmant péremptoirement que toute justification des lois logiques est nécessairement circulaire : car des lois logiques peuvent être justifiées par de simples contraintes objectives de l’espace de nos dires (nous y reviendrons), un peu comme nos déplacements spatiaux sont régis par des contraintes de géométrie.
Une logique sans système est-elle possible ? Comportements et autres desseins
Une logique sans système, c’est ce que propose Jean-Yves Girard dans sa série d’articles « Transcendantal Syntax » et dans son dernier « tract », « Le monstre de Gila »(*). Qu’on n’attende pas de moi ici que j’en donne une présentation claire et fidèle, ni que j’entre dans les détails techniques, ce dont je suis bien incapable, étant peut-être trop paresseux, ou trop ignorant des méandres d’une démarche dont les débuts remontent aux années 1970 (et au fameux système F, plusieurs fois pris en référence). Disons que Girard s’appuie sur quelques résultats essentiels comme le théorème de Herbrand (de Jacques Herbrand, logicien français des années vingt mort en montagne à l’âge de 23 ans, et qui fait partie des rares logiciens admirés par l’auteur), théorème permettant de ramener la preuve d’une formule de logique des prédicats du premier ordre à celle d’un ensemble fini de propositions, et qu’il reprend l’idée, déjà présente dans la ludique, que les preuves ne sont que les exemplaires d’un ensemble plus général de processus (les desseins, en ludique).
Pourquoi, à côté de preuves authentiques (dites visibles), faut-il des preuves invisibles ? L’un des arguments est que, pour éviter les simplifications outrancières du genre de celle mentionnée plus haut avec les trois propositions A, B, C dont toujours deux parmi les trois sont équivalentes, et qui dépend du principe du tiers-exclu (autre manière d’exprimer la bivalence), il est nécessaire de se garder… du vide ! Les intuitionnistes avaient déjà eu l’idée qu’une proposition consiste en l’ensemble de ses preuves (un peu comme si, dans le discours ordinaire, on disait qu’une assertion a pour contenu l’ensemble de tous les arguments qui la soutiennent), en ce cas, une proposition P est fausse si… elle est vide ! (elle n’a pas de preuve). Mais si nous gardons cette même idée, nous arrivons à ceci : étant donné que la négation en logique classique ou intuitionniste peut s’exprimer par A => ⊥, où ⊥ désigne l’absurde et est bien sûr représenté par l’ensemble vide, et que, selon la conception de Brouwer (et Kolmogorov), une preuve de A => B est toujours une fonction qui, à une preuve de A associe une preuve de B, une preuve de la négation de A est une fonction qui associe à une preuve de A… un élément du vide. Or l’ensemble des fonctions de A dans le vide n’est non vide que si A est vide ! (auquel cas, il y a une seule fonction, vide elle-même). Autrement dit, non-A n’est vrai que si A est faux, et si A est vrai, bien sûr non-A est faux, d’où le tiers-exclu… On échappera à cette trappe si toute proposition est un ensemble de desseins, dont certains seulement sont des preuves. En ce cas, P sera vrai si et seulement si P contient, parmi ses desseins, une preuve visible.
Mais entre temps, on n’aura plus parlé de propositions, mais de comportements, ce sera l’objet de mon prochain billet.

(*) En grand cinéphile, Girard fait souvent référence à des films, ici « Le trésor de la Sierra Madre » de John Houston dans lequel figure un monstre qui a la particularité de continuer à mordre même mort. Ce monstre est ici utilisé comme métaphore du scientisme attribué à Hilbert, Russell, Tarski et quelques autres et qui continue à occuper les esprits alors que Gödel l’a mis à mort depuis longtemps.



























