La logique linéaire
Tant qu'on y est, je veux dire sur Girard (J.Y.) autant y passer.
Qu'est ce que LL (la logique linéaire)?
D'abord, c'est l'une des 3. Il n'y en a pas cinquante, en fait, et le mot "logique" désigne la méthode de raisonnement que tout un chacun applique quand il raisonne. Foin des "systèmes formels" et autre arithmétiques, en nombre indéfini, tous instances d'axiomatiques variées, créateurs de mondes dotés de significations variées ou pas.
Là on est dans le dur, dans l'universel, quasiment dans le langage: qu'est ce donc qu'on dit quand on déduit?
On a abordé dans divers articles précédents, les séquents, Gentzen, son nazisme etc. Il nous faut passer à Girard, et à ses inventions.
On se réfère à http://baptiste.meles.free.fr/site/B.Meles-Logique_lineaire.pdf
D'abord le language qui raisonne et qui se fixe une rigueur, des règles, la question étant le choix de celles ci, sachant qu'on a de l'esthétique là dedans: il faut, et oui, de la symétrie dans les principes.
Bon au départ, il y a deux logiques. D'abord celle d'Aristote, de Hilbert, la logique classique. Ca fait deux mille ans que ca dure (plus en fait) et on a fondé une civilisation là dessus, dite occidentale vue sa position mais tout est relatif. On a d'abord "et, ou, non" avec une belle symétrie, celle de Morgan: non (a et b) == (non a) ou (non b).
On a aussi le "donc": ((non a) ou b) matérialise l'implication et toutes les conséquences qui s'en suivent (...) dont le fait, bien rappelé par Duns Scot, que du faux on peut déduire n'importe quoi...
Car la logique a un coté utilitaire: non seulement on exprime des propositions (avec les connecteurs en question) mais on les relie entre elles. Il se trouve en effet, et c'est cela le raisonnement, que de la considération comme vraie d'une proposition, il est possible d'en déduire, sur la base de considérations sur la structure composite de cette proposition, une autre proposition. Ces considérations sont basées sur le bon sens acceptable de celui qui invente la logique, l'acceptation par la société de ce bon sens là étant motivé par l'évidence, il y a des choses qu'on ne peut pas refuser.
Une "logique" ou "la" logique se définit ainsi une formalisation du raisonnement. Un raisonnement est le passage d'une proposition à une autre. La formalisation est la liste de toutes les sortes de raisonnement possibles, basées chacune sur des formes de proposition exprimées comme des "séquents".
Qu'est ce que ces "propositions" ? Il faut bien comprendre qu'elle ne sont pas qu'atomiques et que le fait, asserté faux ou vrai ne prête pas à discussion. Ce qui choque, fâche et irrite ce sont les conclusions qu'on en tire, connectées à d'autres propositions simultanées ou non. Conclusions qui font le langage, et dont on doit décider si elles sont fausses ou non, correctes "logiquement" ou non. C'est cela le raisonnement: raisonner sur des raisonnement. Cette activité dédoublée est souvent mal vue, elle est l'essentiel de la chose: le "bien raisonner" c'est d'abord l'application d'un nombre très réduit de principes, indépendants des vérités factuelles, et c'est le fantasme philosophique par excellence vrai par dessus tout, vrai absolument...
La formalisation de ce raisonnement c'est la technique de démonstration, fait à la fin du XIXème siècle et proclamée comme un programme en 1900 par David Hilbert à Paris: les questions furent posées, c'est sur.
Sur le tard on introduisit une logique dit "intuitionniste", basée sur l'idée du refus de la règle du "tiers exclus". L'idée était de refuser de construire des objets magiquement par simple négation de leur non existence: il fallait que l'objet déduit soit construit explicitement pour accéder à l'être. Au passage, on rendait la logique capable d'exprimer un calcul véritable, on la rendait opérationnelle.
Hélas, au passage, on rendait le raisonnement asymétrique. Débarrassé des multiples conséquents (un séquent intuitionniste n'a qu'un seul énoncé en partie droite), des règles de négation, le système de Brouwer est très laid.
Cette histoire d'une seule formule en partie droite rend impossible le tiers exclu. En effet, si on ne peut pas avoir un "ou" en partie droite, on ne peut pas faire |- A v non A , c'est à dire précisément le tiers exclu...
Cette asymétrie et cette laideur avait pourtant été combattue avec succès par un immense génie, nazi au demeurant, le fameux Gerhard Gentzen (GG). Le calcul des séquents a transformé la "logique" en un splendide alignement minimal, initialement appelé "déduction naturelle", incontournable description absolument claire de la pensée en marche.
Mieux, cet exposé de la marche du raisonnement le rend propre à la mécanisation. L'âge de l'informatique peut commencer.
Mais revenons au tiers exclu et à la négation. Exprimée par Gentzen en logique classique, la négation bien loin d'être diabolique ou expression du non vrai, le vrai restant à définir, elle est essentiellement (...) géométrique et traduit en fait le passage (de part et d'autre du "|-") du "ou" au "et" et du "E "au "A" (retournez moi ces lettres) et réciproquement. Là je fais mon Girard anti réaliste...
En gros, Gentzen rend symétrique et splendide la logique classique LK, alors que LJ la logique intuitionnisme constructiviste permet justement l'informatique, bloquée par les états permanents et les créations monstrueuses d'entités incontrôlées par le tiers exclu, autorisé par LK et interdit par LJ.
Confronté au débat insoluble entre un beauté inopérante et une laideur utile, Girard (J.Y.) se trouva alors investi (par lui même) du soin de construire la logique des logiques, celle qui fusionne élégance et utilité, responsable du vrai passage en douceur et en beauté à l'âge de l'informatique, l'âge de l'action, qui succède à l'âge de l'état (je me lâche).
Pour cela, il faut de nouveaux opérateurs et un système plus riche, mais plus puissant, avec des interprétations un peu alambiquées, mais qui ont le mérite d'être pensées, cohérentes et qui fonctionnent. Et puis, tout se ramène aux systèmes bien connus modulo des conventions. On ne fait donc qu'y gagner en pouvoir d'expression, le bain englobant étant un peu baroque, mais enrichissant et assez rigolo à interpréter.
L'idée de base est d'abord qu'on a des objets qui se transforment et des disjonctions qui sont exclusives. On matérialise des objets en transformation, des objets vivants. Cela concerne l'interprétation des nouveaux symboles introduits par LL (il y en a plein) mais aussi l'interprétation du "|-" de chaque séquent.
La vérité
Il faut cependant dire la vérité: les trucs bizarres de la logique linéaire viennent d'une procédure: on fait tourner l'isomorphisme de Curry Howard à l'envers en partant de l'informatique: toutes ses bizarreries viennent de là, elle est une interprétation du calcul fonctionnel, voilà le fond de l'affaire. Pardon de rajouter ce paragraphe après coup, mais cela est trop important.
Implication
A --o B signifie que A est "consommé" pour produire B. A est une "ressource" et ne peut servir qu'une fois. Le symbole "--o" est ainsi l'expression d'une causalité.
Pour pallier le caractère évanescent de l'hypothèse en LL, on définit un opérateur "exponentiel" qui caractérise la ressource qui se renouvelle: "!A" ne se consomme pas. On peut alors exprimer l'implication traditionnelle comme:
!A --o B <=> A =>B
"!" c'est l'infini, ce qui ne s'use pas quand on s'en sert...
Il a son pendant "?" qui est un infini aussi mais dans le sens des lectures (en partie droite, donc).
Tenseur
L'opérateur "tenseur" "X" est une sorte de "^", mais non involutive: alors que A^A se réduit en A, ce n'est pas le cas pour X: "AXA" est une juxtaposition. Quand on a une pièce de 1 euro ET une pièce de un euro, ça fait DEUX euros...
Un truc marrant: AXA --o A . Il y a bien un A qui disparait, on ne sait pas lequel.
Choix
L'opérateur "avec" "&" est lui aussi une conjonction, mais là il y a le choix.
Plus et PAR
+ et "par" (noté comme un "&" à l'envers) sont les duaux de "X" et "&".
"+" est une disjonction additive
"par" est spécialement abscon et désigne un échange intriqué entre deux réservoirs en communication...
2 conjonctions et 2 disjonctions
On a donc le titre... De fait chaque onction a une version additive et une version multiplicative.
Pour illustrer l'humour ravageur du soixantehuitard Girard, comment modélise-t-on l'achat d'un paquet de Camels ET d'un paquet de Malboros en logique classique ?
A|-C A|-M
____________
A |- C,M
La ruine de l'économie libérale: on peut acheter les deux ! Alors que le gauchiste, plus inventif impose :
A|-C A|-M
______________
A,A |- C X M
Là on DEUX A nécessaires pour obtenir une ressource composite incluant les DEUX paquets de clopes.
La négation
On en vient alors à la négation.
D'abord elle noté "A nil" avec "nil" noté "_|_" ...
Bien sur elle exprime l'implication linéaire:
"A nil par B" est "A --o B "
Mais aussi qu'elle est détruite ponctuellement, et non pas (comme en classique) perpétuellement niée.
Pour exprimer que j'ai bien destruction d'un A "compensé" par la création d'un B, c'est l'interprétation de --o.
Le tiers exclu
Et là on résoud l'antinomie classique/intuitionniste
"A nil nil --o A" se déduit très bien, exactement comme en classique, par contre
A + A nil n'est pas possible, on refuse le tiers exclu dans ce cas, il faut choisir, c'était ce que voulaient dire les intuitionnistes.
On a donc le beurre et l'argent du beurre, le bon sens constructiviste avec toute les symétries possibles. Une merveille.
Les délires
Bien sur le politiquement correct est donné en plus,
A nil nil = A exprime que ce que je donne est reçu
Les séquents suivant sont équivalents et expriment que A est donné puis reçu
A |- A
|- Anil, A
|- A --o A
On a ainsi, en permanence, une logique de l'action et de la transmission...
Les programmes
Au sens de Curry Howard, la logique linéaire s'identifie à la programmation, une proposition étant un type et l'implication un type de fonction de A vers B, avec consommation de l'argument A en entrée.
Par contre, l'interprétation est facile et sans convolution ou autre tortillis cervical: c'est fait "pour"...
Par exemple, et c'est un chef d'oeuvre, (A nil) est le type d'une fonction qui prend un A en entrée !!!
La négation est donc interprétée comme un "input", la double négation comme le retour à l'output, ce qui exprime parfaitement l'involutivité de la chose, seule réalité qui compte...
