Ok

En poursuivant votre navigation sur ce site, vous acceptez l'utilisation de cookies. Ces derniers assurent le bon fonctionnement de nos services. En savoir plus.

12/09/2015

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. 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. 

 

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é ! 

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. 

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). 

 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 

A, B, ou C sont des expressions quelconques, quantifiées ou non. 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 !

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 à partir de plusieurs autres. 

La déduction naturelle la plus simple n'a pas d'hypothèses: 

____________

   X, A  |-   A 

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 / par exemple, s'écrit: 

       X   |-   A 

______________

   X   |-   A /  B 

 

L'élimination droite du ET : 

   X   |-   A / 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.

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 ?

GG se lança alors dans le "calcul des séquents", un "vrai" séquent pouvant cette fois avoir PLUSIEURS formules à droite, mais adjointes par des OU (/). Un tel système est magnifiquement symétrique, la négation étant la transformation miroir entre les parties droites et gauches d'un séquent. 

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". 

 

 

Les commentaires sont fermés.