Girard, Jean Yves

On trouve un article ancien (les années 2000) et aussi les vidéos associées, qui fleurent bon un passé désigné par un type d'ordinateur portable. 

https://www.canal-u.tv/video/universite_de_tous_les_savoirs/les_fondements_des_mathematiques.1021

 

sérieux: http://recherche.ircam.fr/equipes/repmus/mamux/hermann.pdf

Jean Yves Girard est sans doute, et cela est peu connu, l'équivalent actuel de Cantor ou de Gödel lui même. 

Auteur de la logique "linéaire", il est l'homme de la compréhension la plus aboutie, à l'heure actuelle, de la nature de la logique et des mathématiques, rien que ça. 

Né en 1947, c'est un soixante huitard typique dans le sens le plus fort du terme: incroyablement arrogant et fulgurant, il dénonce, approxime, accuse et plaisante avec toute la verve possible. Ses articles et vidéos de 2000 sont incroyablement puissantes, rapides et ... personnelles. 

Que dit il  ? Et bien le comprendre c'est sans doute comprendre le monde plus qu'on n'a jamais pu le faire depuis l'antiquité, et les revues "secondaires" sont pleines des plaintes des semi intellectuels qui feraient mieux de finaliser cette compréhension. 

La diagonale de Cantor

D'abord le premier élément du basculement du monde: sa formalisation nous explose à la figure.

Il y a un infini non dénombrable. Ca commence comme ça avec l'argument de Cantor (1891) prouvant la non dénombrabilité des parties de l'ensemble des entiers naturels. 

Si les ensembles possibles d'entiers sont décrits par une matrice N(i,j) de 1 et de 0, suivant que l'entier i appartient à la partie de numéro j, et bien l'ensemble d'entiers défini par les entiers k tels que N(k,k) = 0, n'est pas répertorié. Cet ensemble est réel, non vide mais invisible. Où qu'il est ? 

Une autre forme de l'argument consiste à mettre en bijection les entiers et les ensembles d'entiers (les parties d'entiers), puis définir l'ensemble D(iagonal) qui contient les entiers qui ne sont pas contenus dans leur image par la bijection. Et bien D n'est pas l'image par la bijection d'un entier et ce par définition. Ou qu'il est?  

Cet argument, dit diagonal, extrêmement simple, est considéré, par exemple par Girard lui même, comme la même chose que tous les paradoxes diagonaux, Gödel compris, ce qui sonne le glas de l'impossible formalisation du monde. En effet, ils se présentent tous avec la structure du "point fixe paradoxal": une fonction f(x,y), une fonction g(z), et à partir de là l'expression h(x) = g(f(x,x)) plus l'exhibition d'un a tel que h(x) = f(x,a). On a alors h(a) = g(f(a,a)) = f(a,a).  Ce point fixe est dans pas mal de cas similaires, paradoxal.

Par exemple, dans le cas de Cantor, f(x,y) est la matrice N, et g est la fonction qui échange 0 et 1. h va définir la fameuse partie invisible de numéro a, dont les éléments sont les entiers x tels h(x) = f(x,a). Comme h(a)=f(a,a)=g(f(a,a)) et que g n'a PAS de point fixe, cette partie invisible ne peut pas exister. 

Le "monstre" de Gödel est construit exactement de cette manière. Juste un point au sujet du monstre: il est défini par un encodage, qui suppose des manipulations à base de "lemme du chinois" qui impose, pour identifier des suites de termes de longueur arbitraire, qu'on ait la multiplication: c'est pour cela que l'arithmétique de Pressburger, sans elle, est décidable, elle. 

Notons que le paradoxe de Jules Richard (1905, c'est un français) qui parle du plus petit entier non définissable en moins de douze mots, conduit directement au monstre et en est l'équivalent strict. 

Löwenheim Skolem 

La question de l'existence démontrée par Löwenheim et Skolem d'un modèle dénombrable pour toute théorie du premier ordre pose alors le problème de l'argument diagonal qui prouve la non dénombrabilité. Et bien cette preuve est une illusion, la chose non dénombrable construit par diagonale n'étant pas un objet du modèle dénombrable prouvé par L.S.

Plus exactement, l'interprétation exacte étant difficile et piégeuse, l'ensemble des parties de N n'a pas la même extension dans tous les modèles de ZF, alors que c'est le cas de N lui même... 

Ainsi il est faux de dire que dans certains modèles de ZF, tous les ensembles infinis sont dénombrables ! En gros, le théorème de Cantor est bien absolu. Ouf. 

 

Le vrai, le faux et le prouvable

 Mis à part la construction du monstre, c'est la dernière partie de la démonstration du théorème de Gödel qui est rigolote. Le monstre est un énoncé qui dit "moi, énoncé, je ne suis pas prouvable". 

On ne sait pas si cet énoncé est vrai, mais on peut le démontrer facilement. Si il était démontrable (prouvable), il serait, comme énoncé, "vrai", ceci car la théorie est cohérente, donc non contradictoire, c'est à dire que tout ce qu'on y démontre est vrai. Si il était vrai, le fait qu'il n'est pas démontrable serait vrai, or on a supposé le contraire. L'hypothèse est donc fausse, et il n'est pas démontrable, c'est à dire que ce qu'il énonce est vrai. Un énoncé dont le contenu est vrai est vrai, il est donc "vrai". 

Ce petit jeu qui produit le vrai par une démonstration qui joue sur le vrai et le prouvable est en soi une pure merveille autonome. Le vrai surgit du néant, littéralement. 

Le théorème de Gödel: irréfragable

Le premier théorème de Gödel montre qu'il existe (au moins une) vérité non démontrable dans tout système formel assez expressif. Le second théorème reformule le premier en affirmant qu'une théorie assez expressive cohérente ne peut démontrer sa propre cohérence (cohérent=non contradictoire="consistant"). 

Plus exactement, le premier théorème est une réflexion sur la contemplation d'une proposition monstrueuse de l'arithmétique obtenue après force codage, et qui se trouve ainsi vraie. Cette proposition affirme qu'elle n'est pas démontrable. L'arithmétique étant cohérente, on a donc le vrai monstre: vrai mais pas démontrable.  

Les deux concepts fondamentaux de la pensée humaine, vérité et démontrabilité ne s'identifient pas. Boum. 

Girard fait remarquer que Gödel est absolument irréfragable: si il était réfuté, alors que les preuves mathématiques de sa véracité existent (on l'a vérifié par ordinateur), les mathématiques seraient alors contradictoires (il y aurait un théorème démontré qui serait faux), et donc le théorème de Gödel serait vrai, ex falso quodlibet (du contradictoire on déduit ce qu'on veut). Irréfragable, c'est le mot. Pardon de méditer encore une telle merveille, mais il faut bien réaliser la beauté de la chose: il est d'autant plus vrai que sa réfutation implique sa vérité ! 

Un mot au sujet du DEUXIEME théorème de Gödel. Il est basé sur l'ENCODAGE du raisonnement ayant mené au premier. Le premier affirme donc que toute théorie cohérente T contient des énoncés non décidables. Cette affirmation encodée DANS T, signifie donc que T contient l'implication (Cohérence => G ).

Et là champagne ! Comme G n'est pas prouvable (premier théorème), la cohérence de T ne l'est pas non plus: une théorie ne peut contenir de preuve de sa cohérence, Hilbert est réfuté... 

L'isomorphisme de Curry Howard

La grande découverte du XXème siècle c'est aussi cette mystérieuse correspondance qui relie la logique et le calcul. Une interprétation de la logique même, celle qui préside à la véracité des constructions du langage qui s'identifie à l'application des fonctions à leurs arguments, comme le font tous les jours les braves ordinateurs.

Le raisonnement c'est donc le calcul, tout simplement. 

Si on y a va dans le détail, un type c'est une proposition, et une valeur typée une preuve du type, c'est à dire une preuve existentielle  que dans un cas la proposition est vraie. Un type de fonction d'un type vers un autre est un raisonnement de la déduction d'une proposition par une autre, et une fonction de ce type est une preuve de ce raisonnement, l'application de la fonction étant la règle de coupure, le "calcul" consistant à éliminer ces coupures. 

Girard et tout le monde, maintenant, construisent leurs logiques sur la base de cette identification, cherchant, au delà des intuitionnismes à penser la logique nue d'une façon qui rompt tout à fait avec les idéologies variées du début du XXème siècle. C'est là que Girard se lance dans ses articles dans des dénonciations variées qui font justice aussi bien des ultra formels des débuts que des bouddhistes de la fin. 

Girard philosophe

Girard prononce alors toute une série de fatwas, dénonçant aussi bien l'essentialisme (contre l'existentialisme), et le popperisme (c'est là où il est le plus virulent). 

Au sujet de Popper, j'avoue être perturbé: faut il choisir entre papa et maman ? Je crois en fait que les propositions "popperriennes" (récessives, ou généralisations (AxB)) s'opposant aux propositions expansives (ExB), et identifiant la vérité à l'attente indéfinie d'un bus, identifiant le faux à l'inexistence, sont en fait des métaphores d'après diner, faites pour distraire, et que hélas Girard n'est pas philosophe. 

Car Popper ne prendrait pas en compte le caractère irréfragable du théorème de Gödel, qui se trouvant donc non falsifiable, serait donc non scientifique d'après Popper. Il est clair là que maman se moque de papa et qu'on est bien dans l'irrévérencieux, rien de plus. Ouf: Popper n'applique pas la falsifiabilté aux axiomes d'une théorie formelle, et le déductif n'a pas à être falsifié, quoique,  et c'est la question. 

Et puis, là où Girard est particulièrement injuste, c'est qu'on ne peut que qualifier de "scientifique" le programme de Hilbert lui même !  Il pose des conjectures dans le domaine mathématique, et celles ci se trouvent réfutées, les unes après les autres. Le théorème de Gödel et son irréfragabilité est bien un élément de preuve, absolument distinct et asymétrique de la prétention à la super cohérence, parfaitement scientifique, mais ... fausse, parce que falsifiée.

Deux remarques en passant: il me semble que le mot "falsification" a un coté bien trop "filosof" pour ne pas être à la base d'une "philosophie" des sciences, ah le jeu de mot signifiant ! Voilà que je fais mon heildeguerre... La deuxième remarque est que mot "endlösung" (solution finale) était utilisé par Hilbert... 

 

Les différents problèmes

Il y a deux sortes de problèmes, les Pi1 et les Sigma1. Pi1 c'est ce sont les généralisations (AxB) et Sigma1 se sont les exemples (ExB), comme on a dit, Girard parle des récessifs et des expansifs. 
L'énoncé de Gödel est typiquement une généralisation (il n'existe pas de démonstration qui me prouve). 

Notons qu'un exemple est en principe semi-décidable: en essayant toutes les combinaisons de variables, on peut chercher à rendre l'exemple vrai,(à condition bien sur que la formule soit décidable en temps fini, bien sur, ce qui est le cas quand elle ne contient que des quantificateurs bornés). Il faut bien comprendre la chose: le "il existe" affirme, mais sans montrer. Pour s'en convaincre absolument, pour décider "finalement", il faut donc trouver UN exemple, on dit qu'il "suffit" de le trouver, puisque la décision se réduira à un seul évènement, obtenu en essayant tour à tour toutes les combinaisons, et en appliquant les tables de vérités à l'application des fonctions propositionnelles. En principe cette démarche "peut" marcher: au bout d'un certain temps, nécessairement fini, on peut, au moins en principe trouver un exemple qui marche. Ce n'est que SI l'affirmation est fausse que cet heureux évènement ne se produira jamais. Mais pour en être sur, il faudra attendre infiniment, ce qui est là, absolument hors de portée.

Notons qu'on considère évidemment les "B" comme ne contenant eux mêmes que des quantificateurs bornés, (Ex<p, Ax<q), pour ne pas partir à l'infini immédiatement. Par contre, il y a bien asymétrie entre les deux types d'énoncés: la généralisation n'est PAS prouvable elle par simple vérification. 

 Gentzen et la déduction naturelle

(en lisant http://baptiste.meles.free.fr/site/B.Meles-Logique_lineaire.pdf)

Gerhard Gentzen (GG), ex assistant de Hilbert, inventa la "déduction naturelle", une classification nécessaire des règles de déduction exprimée proprement sous forme de "séquents". 

Un séquent, atome de la démonstration est de la forme :  A , B   |-  C 

Il est très précisément l'équivalent d'une sorte d'implication: nonA ou nonB ou C

Plus précisément encore, il est affirmation d'une vérité décomposée en disjonctions.

Bien sur et le "bien" sur a deux titres, on a bien les lois de morgan et la logique de base que chacun connait, bien sur. Simplement cette logique là, elle est celle de la "métamathématique", celle du raisonneur lambda de haut niveau. Bien sur formée suivant les principes habituels, mais aussi, "bien sur", applicable uniquement au sommet de la pyramide, et servant à raisonner sur les autres logiques, celles qu'on va pouvoir inventer et dont on exprimera ainsi la cohérence. 

A, B, ou C sont des expressions quelconques, quantifiées ou non dont on affirme la vérité. Un séquent exprime une implication élémentaire, prouvant une expression vraie sous certaines hypothèses. En fait il ne s'agit pas d'une implication au sens logique mais d'un "modus ponens", le deuxième sens de la chose, bien plus riche: c'est Gentzen qui le matérialisa: au cas où X serait considéré comme vrai, ben Y le sera aussi, tiens. Ecrire le séquent signifie en fait qu'on a une preuve de ce qu'il énonce. 

La déduction "naturelle" sous sa forme la plus générale consiste à dessiner des arbres avec de belles lignes horizontales désignant la production possible d'un séquent ou preuve à partir de plusieurs autres. Chaque arbre est une "règle", atome d'un système de déduction. 

Un séquent en lui même est donc une preuve de quelque chose, et la "déduction" consiste à expliquer comment on l'obtient à partir d'autres preuves. La déduction n'est pas un simple modus ponens ou  un raisonnement basique (nonA ou B, écrit  A |- B), mais une "déduction" de cette preuve à partir d'autres preuves. On a donc une machine permettant d'obtenir toutes les preuves possible d'un système. 

Revenons sur la granule, le séquent, la preuve élementaire. Il n'est pas la simple assertion de quelque chose qui serait "vrai", il est l'affirmation que quelque chose est prouvé, et que ce quelque chose est intelligible, car décomposé sur un monde, doté de signification. Bon, ça fait rêver, quoi. 

Notons ce qui caractérise la déduction dite "naturelle" inventée par GG: il y a toujours UNE SEULE conclusion. Le système se compose donc de règles avec UN seul axiome, qui est  la règle sans prémisses:

____________

   X, A  |-   A 

Ainsi, il est "licite" de se débarrasser dans une preuve, des hypothèses supplémentaires. TOUT le reste sont des règles d'introduction 

De manière systématique, on (GG en fait, qui prêta serment à Hitler en 39) a des règles d'introduction et d'élimination basiques pour chaque symbole logique, qui apparaissent comme autant d'opérations de bases dans la conduite des preuves.

 L'introduction du "v" (le "ou") par exemple, s'écrit: 

       X   |-   A 

______________

   X   |-   A ou B 

 

L'élimination droite du ET : 

   X   |-   A et B 

_______________

      X   |-   A 

On a encore 2 ou 3 règles générales de ce type pour finir de décrire la "déduction naturelle". Ce qui permet de décrire absolument une démonstration comme un arbre d'application de règles.

GG est un génie: il invente une représentation du raisonnement qui rend complètement mécanisable, par exploration d'un arbre de preuves, les raisonnements logiques en général. La porte de la démonstration automatique, devant vos yeux ébahis, vient d'être ouverte. 

Hélas, la symétrie du système est cassée par la règle du tiers exclus, la négation ne pouvant être proprement éliminée et introduite. Cette question du statut spécial de la négation qui occupa beaucoup GG, demande à être comprise, et je n'en suis pas encore là. Et vous ?

Simplement, les "preuves" ne s'expriment pas de manière symétriques (il n'y a qu'une seule conclusion). En étendant la notion de séquent: (Ai |- Bi), le système est rendu complètement symétrique, les et et les ou se trouvant complètement équivalents, la négation servant de passage d'une formule à l'autre, le shéma étant bien sur celui des fameuses lois de Morgan. Le calcul des séquents représente proprement le raisonnement automatique.

Cependant, la distinction logique classique/logique intuitioniste reste, le refus du tiers exclus, propre à l'intuitionnisme, cassant cette belle symétrie.

Tout ça pour dire que la logique linéaire de Girard (mot vide de sens pour moi jusqu'à aujourd'hui), a pour objet de compléter le travail de GG et de refonder la logique autrement, tout simplement.

De nouveaux opérateurs (x, &), une nouvelle implication (--o), qui serait capable, selon Girard sans les épicycles de ptolémée, de rendre compte de toutes les formes de logiques variées qu'on a pu inventer entre temps. Du diable si je comprends les détails. Encore des trucs à lire.

 

Encore, Encore

Une conférence plus récente est en https://www.youtube.com/watch?v=Nc3pgZxU-Cg 

Le portable est un Apple, bien plus moderne. Encore plus sarcastique et drôle: il veut tuer le réalisme et n'est ni objectiviste, ni subjectiviste et il cite: le sens c'est l'usage (Wittgenstein), la négation c'est le format (Hégel), il est existentialiste et non pas réaliste ou essentialiste et surtout: il n'y a pas de preuve que "non". 

 

Un article sur l'état présent de la logique, avec l'introduction des 3 mondes, la logique linéaire étant au niveau 3 (bien sur) est bien sur un must.  http://iml.univ-mrs.fr/~girard/roma2004.pdf

On y trouve une critique de la logique de Guantanamo: un sujet est un objet qu'on n'a pas torturé suffisamment.