Je traîne depuis longtemps l'idée de vulgariser quelques notions de logique linéaire. Du point de vue de la vulgarisation, la logique linéaire a ceci de sympathique que c'est quelque chose mathématiquement à tellement « bas niveau » que je n'ai besoin de présupposer aucune sorte de connaissance mathématique préalable pour en parler : en principe, on peut la considérer comme un pur petit jeu syntactique dont les règles ne sont pas très compliquées — même si, présenté sous cette forme, il risque de ne pas apparaître comme très intéressant, et même s'il est bon d'avoir du recul pour avoir une idée de quelles règles appliquer à quel moment, la compréhension des règles elles-mêmes ne nécessite pas de savoir particulier. Du point de vue personnel, la logique linéaire est quelque chose qui me frustre beaucoup parce que, d'un côté, je la trouve extrêmement élégante et joliment symétrique, de l'autre, à chaque fois qu'elle semble avoir une application ou une interprétation quelque part, on se rend compte qu'il y a une note en bas de page qui fait que ce n'est pas vraiment la logique linéaire (il y a par exemple un axiome en plus, ou un connecteur en moins, ou seulement un fragment du système, ou quelque autre variation), et l'élégance est rompue ; et aussi, pour cette raison, l'intuition qu'on peut se former est brouillée.
De quoi s'agit-il ? D'un système formel inventé par le logicien français Jean-Yves Girard en 1987. J'avoue ne guère avoir d'idée de ce qu'il voulait faire avec, parce que les textes de Girard sont… un peu inhabituels… bourrés de mots qu'il ne définit pas, de références cryptiques, et de blagues dont on se demande si ce sont des blagues (comme l'intervention insistante du brocoli dans beaucoup de ses papiers). Mais depuis, elle a trouvé diverses applications et connexions : en logique, en informatique théorique ou plus appliquée, en algèbre et théorie des catégories, en théorie des jeux et même en physique quantique (sauf qu'à chaque fois, comme je le dis ci-dessus, il y a quelque chose en plus ou en moins) ; mais je ne compte pas essayer de décrire ces applications et connexions, qui sont pourtant sans doute ce qu'il y a de plus intéressant dans l'histoire, parce que je n'ai pas l'espace ni le temps pour ça.
Bref. Avant d'expliquer quelles sont les règles du jeu, il faut
que j'essaye de donner une idée de ce dont il s'agit (en agitant les
mains). On parle de logique
linéaire, et il s'agit
effectivement d'une généralisation de la logique classique, mais ce
terme risque de donner une impression tout à fait fausse, et on
devrait peut-être plutôt s'imaginer que ça s'appelle formalisme
d'échanges
ou synallagologie universelle
ou quelque chose
de ce genre (le seul problème du mot synallagologie
est que
personne ne sait ce qu'il veut dire puisque je viens de l'inventer…
mais à part ça, il est parfait). La différence essentielle est la
suivante : en logique usuelle, si on fait un raisonnement tendant à
démontrer une conclusion X à partir
d'hypothèses A, B et C, disons, on
peut utiliser librement A, B et C
dans le cours du raisonnement, chacune aussi souvent qu'on veut (on
peut aussi, d'ailleurs, ne pas du tout utiliser une hypothèse) ; la
logique linéaire, pour sa part, exige que chacune des « hypothèses »
(qu'il vaut mieux, du coup, ne pas considérer comme des hypothèses)
soit utilisée une et une seule fois : on ne peut ni les
multiplier ni les faire disparaître (évidemment, il y aura des moyens
de marquer des hypothèses spéciales qu'on peut multiplier et/ou faire
disparaître, mais ce n'est pas le cas par défaut) ; dans ces
conditions, il vaut mieux, donc, considérer qu'on n'a pas du tout à
faire à une logique, à des raisonnements et à des hypothèses et
conclusions, mais à des échanges (gestion de ressources
abstraites, transactions économiques, réactions chimiques, que sais-je
encore) qui ont des entrées (réactifs) et des sorties (produits), ou
quelque chose comme ça. Par exemple, la logique linéaire pourrait
concevablement servir à formaliser des contrats financiers
(j'avais déjà évoqué quelque chose
de ce genre), mais il ne faut pas s'imaginer que la logique
linéaire elle-même dira grand-chose d'intéressant : de même
que la logique classique ne fournit que le langage le plus basique
au-dessus duquel on peut bâtir des raisonnements (il faut ajouter des
axiomes intéressants pour obtenir quelque chose d'intéressant), la
logique linéaire n'est qu'un cadre, en lui-même extrêmement
primitif pour possiblement décrire des échanges.
Je digresse un peu (en agitant toujours beaucoup les mains) pour ceux qui savent ce que ces mots veulent dire : la logique linéaire peut surtout servir en informatique, par exemple pour sous-tendre un système de typage d'un langage informatique dans lequel la mémoire, ou une quelconque autre ressource, n'est pas allouée ou libérée automatiquement — le fait que le typage soit linéaire signifie précisément que les données ou ressources ne seront ni dupliquées ni perdues sans un appel explicite à des fonctions d'allocation ou de libération de la mémoire/ressource. (L'utilisation de la logique pour sous-tendre un typage fait appel à la correspondance de Curry-Howard en vertu de laquelle les types d'un langage de programmation et programmes instanciant ces types se comportent de la même manière que, respectivement, les propositions d'un système logique et preuves de ces propositions : les hypothèses et conclusions d'un raisonnement correspondent, côté informatique, aux entrées et sorties d'un programme, et la logique linéaire assure précisément que les entrées ne sont ni reproduites ni jetées.) Mais la logique linéaire peut aussi servir à modéliser le parallélisme en informatique, ou des échanges client-serveur, ou des jeux à deux joueurs, ou encore toutes sortes de choses.
Insistons sur le point suivant : il n'est pas clair (en tout cas pas clair pour moi, sans doute que Girard me dirait de retourner faire pousser des brocolis) que les formules de la logique linéaire aient un « sens » inné (alors que c'est nettement plus clair pour la logique classique) ; selon le genre de choses auxquelles on va appliquer cette logique (formalisation d'échanges, typage informatique, théorie des jeux, algèbre, mécanique quantique), il apparaîtra une sémantique pour la logique linéaire ou peut-être un fragment de la logique linéaire (et peut-être avec des axiomes en plus), mais il n'est pas possible de dire exactement ce que A⅋B signifie de façon générale, juste quelles règles il doit vérifier. Je vais quand même essayer d'en donner une petite idée, mais cette idée sera forcément très grossière, très approximative, très informelle, et ne sert à la limite qu'à permettre de mémoriser un peu quel quantificateur fait quoi.
Tout ceci étant dit de façon extrêmement vague, à quoi ressemblent les formules de la logique linéaire et quels sont ses symboles ? Il y en a tout un paquet : ‘&’, ‘⊕’, ‘⊗’, ‘⅋’ (les quatre connecteurs binaires), ‘⊸’ (l'implication linéaire), ‘⊤’, ‘0’, ‘1’, ‘⊥’ (les quatre neutres), ‘•⊥’ (la dualité, notée par un symbole ‘⊥’ en exposant), ‘!’ et ‘?’ (les exponentielles) ; symboles auxquels on peut encore ajouter ‘⊢’ même s'il n'est pas tant un symbole de la logique qu'un symbole qui sert à en définir les règles. Je vais discuter informellement ces différentes machins avant de définir précisément les règles de la logique : comme je viens de le dire, je vais tenter de proposer un sens intuitif (extrêmement grossier) aux symboles, mais il ne faut pas le prendre trop au sérieux, plutôt l'utiliser comme un vague guide ou moyen mnémotechnique pour retenir ce qui est quoi — ces explications informelles ne sont pas du tout nécessaires, on pourrait les sauter complètement, et on peut les ignorer si on trouve qu'elles rendent les choses plutôt plus confuses. (Néanmoins, comme je vais y mélanger des explications d'ordre syntaxique, par exemple pour dire que ‘&’ est un connecteur prenant deux arguments, qu'on note A&B le résultat de ce connecteur appliqué à ces deux arguments, ou encore que la convention de parenthésage est que A&B⅋C se lit comme A&(B⅋C), il vaut mieux ne pas sauter directement jusqu'aux règles.)
Il faut que j'introduise d'abord les quatre connecteurs, à
savoir & (prononcer avec
), ⊕ (prononcer plus
),
⊗ (prononcer fois
) et ⅋ (prononcer par
; si ce dernier
symbole ne s'affiche pas correctement, sachez que c'est un ‘&’
retourné de 180° : certains, faute de disposer de ce symbole, écrivent
‘℘’ à la place, symbole qui a d'ailleurs lui-même
une histoire
assez compliquée). Du point de vue de la syntaxe, il s'agit de
connecteurs binaires, c'est-à-dire que si A et B
sont des formules (=expressions) de la logique linéaire,
alors A&B, A⊕B, A⊗B
et A⅋B sont quatre nouvelles formules. On dira
que :
- & est conjonctif, additif, négatif ;
- ⊕ est disjonctif, additif, positif ;
- ⊗ est conjonctif, multiplicatif, positif ;
- ⅋ est disjonctif, multiplicatif, négatif.
Ou si on préfère ranger ça en tableau :
Conjonction | Disjonction | |
---|---|---|
Additif | & (avec) | ⊕ (plus) |
Multiplicatif | ⊗ (fois) | ⅋ (par) |
Positif | Négatif | |
---|---|---|
Additif | ⊕ (plus) | & (avec) |
Multiplicatif | ⊗ (fois) | ⅋ (par) |
(Je ne prétends pas avoir expliqué ce que ces termes signifient, ni les connecteurs eux-mêmes. Il s'agit de pure terminologie.) Voici une description intuitive et sommaire de ce que ces connecteurs (je répète encore une fois qu'il ne s'agit pas d'une définition ni même d'une explication, mais juste de donner une idée préalable à laquelle se référer) :
- Le connecteur & (
avec
) marque (intuitivement) le choix entre deux ressources : c'est-à-dire qu'avoir un A&B signifie (intuitivement) qu'on a un A ou un B, mais pas les deux à la fois, et qu'on dispose du choix entre les deux. (Je sais que cette description semble contradictoire à la fois avec la lecture du connecteur commeavec
et avec sa classification comme conjonctif, mais ce n'est pas une erreur de ma part.) Par exemple, si un restaurateur vous proposefromage & dessert-du-jour
, cela signifie qu'il vous propose de choisir entre le fromage et le dessert (mais vous ne pouvez pas avoir les deux, ni deux fois l'un, ni d'ailleurs ne rien avoir du tout). - Le connecteur ⊕ (
plus
) marque (intuitivement) l'absence de choix (ou le choix par l'adversaire, ou par le monde extérieur) entre deux ressources : c'est-à-dire qu'avoir un A⊕B signifie (intuitivement) qu'on a un A ou un B, mais pas les deux à la fois, et qu'on ne dispose pas du choix entre les deux. Par exemple, si le dessert-du-jour estprofiterole ⊕ tarte-tatin
, cela signifie que ce n'est pas vous qui choisissez entre les deux. - Le connecteur ⊗ (
fois
) marque (intuitivement) la présence simultanée de deux ressources : c'est-à-dire qu'avoir un A⊗B signifie (intuitivement) qu'on a un A et un B en même temps (qu'on le veuille ou non). Par exemple, si le plat-du-jour estsaumon ⊗ oseille
, vous aurez les deux (et vous ne pouvez pas avoir moins). - Le connecteur ⅋ (
par
)… ah, c'est là le problème : comme je le disais plus haut, c'est frustrant à quel point chaque interprétation de la logique linéaire semble avoir quelque chose en plus ou en moins, et l'interprétation comme des ressources ne donne pas de sens évident à ce quatrième connecteur. Le mieux que je puisse proposer est que A⅋B signifierait très vaguement quelque chose comme : il y a deux mondes parallèles, l'un dans lequel vous auriez un A et l'autre dans lequel vous auriez un B ; même si c'est très loin d'être satisfaisant, c'est peut-être quelque chose qu'on peut garder à l'esprit.
Ces quatre connecteurs sont tous commutatifs et associatifs, c'est-à-dire que A&B est complètement interchangeable avec B&A, et que A&(B&C) l'est avec (A&B)&C (ce qui permet légitimement d'écrire simplement A&B&C pour l'un quelconque des deux), et de même pour les trois autres connecteurs. (Il y a des définitions de logiques linéaires non-commutatives, dans lesquelles les connecteurs multiplicatifs ⊗ et ⅋ ne sont plus commutatifs, mais je ne vais pas en parler ; et même là, les additifs restent commutatifs.)
À côté de ces quatre connecteurs, il faut mentionner l'opération
notée par le symbole ‘⊸’ (que certains
prononcent sucette
, lollipop
en anglais, à
cause de sa forme ; mais d'autres disent simplement implique
ou
parlent d'implication linéaire
). On peut soit considérer que ⊸
est un connecteur supplémentaire, soit le définir au moyen de
la dualité (dont je vais parler ci-dessous) en décrétant
que A⊸B est un raccourci de langage pour
(A⊥)⅋B (de la même façon que, si on
connaît la logique classique A⇒B peut être un
racourci de langage pour (¬A)∨B). Quoi qu'il en
soit, le sens intuitif de A⊸B est quelque chose
comme une machine qui transforme un A en un B
(mais ne peut servir qu'une seule fois), ou encore un contrat par
lequel on [= celui qui a A⊸B] s'engage à fournir
un A et obtenir un B en échange (ceci peut
éventuellement servir à donner une intuition du ⅋, puisque je viens de
dire que A⊸B est essentiellement synonyme de
(A⊥)⅋B, même si je n'ai pas encore
parlé de A⊥). À la différence des quatre
connecteurs &, ⊕, ⊗ et ⅋, l'implication ⊸ n'est certainement pas
commutative ni associative.
Quand on lit les expressions de logique linéaire, on fait la convention que les connecteurs dits multiplicatifs (c'est-à-dire ⊗ et ⅋) ainsi que l'implication linéaire (⊸) ont la priorité sur les connecteurs dits additifs (& et ⊕) : par exemple, A⊗B⊕C doit se comprendre comme (A⊗B)⊕C ; mais pour le reste, le parenthésage doit être explicitement marqué.
Chacun des quatre connecteurs &, ⊕, ⊗ et ⅋ a un neutre
correspondante (appelé aussi l'unité du connecteur, ou
la constante associée). Ce sont respectivement : ⊤, 0, 1 et
⊥ (on peut les lire comme vrai
, zéro
, un
et faux
respectivement, mais je crois avoir entendu rien
utilisé pour l'un d'entre eux, et pas de façon très cohérente). En
tableau :
Vrai | Faux | |
---|---|---|
Additif | ⊤ (neutre de &) | 0 (neutre de ⊕) |
Multiplicatif | 1 (neutre de ⊗) | ⊥ (neutre de ⅋) |
Positif | Négatif | |
---|---|---|
Additif | 0 (neutre de ⊕) | ⊤ (neutre de &) |
Multiplicatif | 1 (neutre de ⊗) | ⊥ (neutre de ⅋) |
Quand on dit neutre
, pour un connecteur, cela signifie que
connecter avec ce neutre ne change rien : autrement dit, dire que ⊤
est le neutre du connecteur & signifie que A&⊤ est
complètement interchangeable avec A, et de même
pour A⊕0 ou bien A⊗1 ou encore A⅋⊥.
On peut essayer d'en déduire un sens intuitif à ces neutres en se
basant sur le sens intuitif que j'ai proposé aux connecteurs : ainsi,
⊤ serait quelque chose d'épouvantablement mauvais que personne ne veut
avoir à aucun prix (si bien que quand vous avez le
choix A&⊤ entre A et ⊤, vous choisirez
toujours A puisque ⊤ est pire que tout), tandis que 0
serait, au contraire, quelque chose d'infiniment désirable que vous
n'aurez jamais ; quant à 1, c'est « rien du tout » (si bien
qu'avoir A⊗1, un A en même temps que 1, c'est
juste avoir un A), et ⊥, comme d'habitude, n'est pas très
intuitif (mais une interprétation très grossière possible est la mort
ou l'inexistence — la terminaison d'un programme, par exemple —
puisque A⅋⊥ signifie que dans un monde parallèle vous
n'existez pas, ce qui vous fait une belle jambe, tandis que dans
celui-ci vous avez un A).
Une autre opération de la logique linéaire est la dualité
(appelée aussi négation linéaire
) : on la note par un ⊥ en
exposant : le dual de A est noté A⊥
(parfois prononcé nil-A
). En fait, l'implication
linéaire ⊸ et la dualité sont interdéfinissables : on peut soit
considérer que A⊸B est un raccourci de langage
pour (A⊥)⅋B, soit
que A⊥ est un raccourci de langage
pour A⊸⊥ (ce qui justifie plus ou moins l'utilisation du
même symbole ‘⊥’ pour les deux, même si la notation est quand même un
peu malheureuse). Le sens intuitif de A⊥ est
quelque chose comme disparition d'un A
,
ou consommation d'un A
.
Peut-être que je peux glisser ici une explication informatique informelle du fait que A⊸B (que j'ai expliqué comme représentant un appareil pour consommer un A et à produire un B) est équivalent à (A⊥)⅋B (que j'ai vaguement décrit comme deux mondes parallèles, l'un dans lequel on a un B et l'autre dans lequel on a un truc-qui-consomme-un-A-et-fait-disparaître-le-monde) : pour que les choses soient moins floues, disons que ce sont des ressources dans un langage de programmation ; or une façon pour un programme d'accepter un A en entrée et de renvoyer un B est de faire la chose suivante : le programme forke, c'est-à-dire, crée un nouveau fil d'exécution, l'un de ces fils attend/demande qu'on lui fournisse un A, et quand c'est le cas, transmet cette ressource à l'autre programme et termine son exécution, tandis que l'autre fil attend le message de son frère, et produit alors un B ; c'est plus ou moins ça que doit décrire l'équivalence entre A⊸B et (A⊥)⅋B (les deux arguments du ⅋ étant les deux fils dont je viens de parler).
La dualité fournit une symétrie de la logique linéaire : en effet,
- (A⊥)⊥ est (interchangeable avec) A.
- (A&B)⊥ est (interchangeable avec) (A⊥)⊕(B⊥) ; et (A⊕B)⊥ est (interchangeable avec) (A⊥)&(B⊥).
- (A⊗B)⊥ est (interchangeable avec) (A⊥)⅋(B⊥) ; et (A⅋B)⊥ est (interchangeable avec) (A⊥)⊗(B⊥).
- ⊤⊥ est (interchangeable avec) 0 ; et 0⊥ est (interchangeable avec) ⊤.
- 1⊥ est (interchangeable avec) ⊥ ; et ⊥⊥ est (interchangeable avec) 1.
(On comparera avec les lois de De Morgan de la logique classique : en logique classique, la négation échange la conjonction avec la disjonction, et en logique linéaire, la dualité échange les deux connecteurs additifs d'une part, et les deux multiplicatifs d'autre part.)
Quant à (A⊸B)⊥, on peut le réécrire comme A⊗(B⊥).
Enfin, la logique linéaire comporte des exponentielles,
notées !A (qui peut être lu bien sûr
,
ou of course
en anglais) et ?A (qui
peut être lu pourquoi pas
, ou why not
en
anglais), qui servent à permettre à la logique linéaire de traduire la
situation normale en logique classique, c'est-à-dire le fait qu'une
hypothèse est jetable ou multipliable à volonté. Je n'en parlerai
guère plus pour le moment (la logique linéaire sans exponentielles est
déjà assez intéressante et complexe), mais signalons que :
- Le sens de !A ressemble à :
(1&A)⊗(1&A)⊗(1&A)⊗⋯ ;
c'est-à-dire intuitivement :
autant de A que vous voulez (y compris aucun)
. - Le sens de ?A ressemble à :
(⊥⊕A)⅋(⊥⊕A)⅋(⊥⊕A)⅋⋯ ; c'est-à-dire
très grossièrement :
autant de A que vous ne voulez pas (mais dans des univers parallèles (?))
. - Les deux exponentielles sont duales l'une de l'autre, c'est-à-dire que (!A)⊥ est (interchangeable avec) ?(A⊥) ; et (?A)⊥ est (interchangeable avec) !(A⊥).
Pour mieux donner une idée du fonctionnement de toutes ces opérations, je tente une liste d'identités linéaires : cette liste n'est pas exhaustive (il n'est pas possible de dresser une liste exhaustive de telles identités), mais devrait donner au moins les plus fréquemment rencontrées, quitte à répéter certaines que j'ai déjà données ; dans ce qui suit, P≡Q signifie que P et Q sont interchangeables en logique linéaire (et ce, quelles que soient les valeurs des variables A, B, C, etc.) :
- A⊸B ≡ (A⊥)⅋B ; et A⊥ ≡ A⊸⊥
- (A⊥)⊥ ≡ A
- (A&B)⊥ ≡ (A⊥)⊕(B⊥) ; et (A⊕B)⊥ ≡ (A⊥)&(B⊥) ; et ⊤⊥ ≡ 0 ; et 0⊥ ≡ ⊤
- (A⊗B)⊥ ≡ (A⊥)⅋(B⊥) ; et (A⅋B)⊥ ≡ (A⊥)⊗(B⊥) ; et 1⊥ ≡ ⊥ ; et ⊥⊥ ≡ 1
- A&(B&C) ≡ (A&B)&C ; et A&B ≡ B&A ; et A&⊤ ≡ A ; et A&A ≡ A
- A⊕(B⊕C) ≡ (A⊕B)⊕C ; et A⊕B ≡ B⊕A ; et A⊕0 ≡ A ; et A⊕A ≡ A
- A⊗(B⊗C) ≡ (A⊗B)⊗C ; et A⊗B ≡ B⊗A ; et A⊗1 ≡ A ; et A⊗0 ≡ 0
- A⅋(B⅋C) ≡ (A⅋B)⅋C ; et A⅋B ≡ B⅋A ; et A⅋⊥ ≡ A ; et A⅋⊤ ≡ ⊤
- A⊗(B⊕C) ≡ (A⊗B)⊕(A⊗C)
- A⅋(B&C) ≡ (A⅋B)&(A⅋C)
- 1⊸A ≡ A ; et A⊸(B⊸C) ≡ (A⊗B)⊸C ; et A⊸(B&C) ≡ (A⊸B)&(A⊸C) ; et (A⊕B)⊸C ≡ (A⊸C)&(B⊸C)
- (!A)⊥ ≡ ?(A⊥) ; et (?A)⊥ ≡ !(A⊥)
- !!A ≡ !A ; et !A ≡ (!A)⊗(!A) ; et !A ≡ 1&(!A) ; et !A ≡ A&(!A)
- ??A ≡ ?A ; et ?A ≡ (?A)⅋(?A) ; et ?A ≡ ⊤⊕(?A) ; et ?A ≡ A⊕(?A)
- !(A&B) ≡ (!A)⊗(!B) ; et !⊤ ≡ 1
- ?(A⊕B) ≡ (?A)⅋(?B) ; et ?0 ≡ ⊥
(Certains râleurs râleront que mes identités ne sont pas toutes de la même nature, vu que certaines reflètent, en fait, des isomorphismes de structures de preuves alors que certaines sont seulement des implications bidirectionnelles.)
Idéalement, on devrait chercher à se faire une représentation intuitive des opérations de la logique linéaire qui rende évidentes ces identités, mais j'avoue que ça semble vraiment délicat (ou plutôt, ça semble vraiment délicat si elle ne doit pas, par ailleurs, introduire de fausses identités comme laisser penser que A⊗A⊥ serait équivalent à ⊥ ou bien que A⊗(B&C) serait équivalent à (A⊗B)&(A⊗C), choses qu'il est peut-être tentant de penser mais qui ne découlent pas des règles de la logique linéaire).
Tout ce que j'ai raconté jusqu'à présent était censé donner une simple idée préliminaire de la logique linéaire, mais sans rien définir correctemnet. J'en viens maintenant aux explications plus précises.
Pour définir les règles précisément, je vais utiliser un symbole
supplémentaire, qui ne fait pas partie de la logique
elle-même mais sert à la définir : il s'agit du symbole ‘⊢’
(prononcé thèse
ou taquet
). Il s'utilise avec une suite
de formules de la logique linéaire à gauche et à droite, chacune
séparée par des virgules (c'est-à-dire que ça ressemble à
ceci : U,V,W⊢X,Y,Z),
et le tout s'appelle un séquent. Intuitivement, il faut
comprendre un
séquent U,V,W⊢X,Y,Z
comme signifiant à partir
de U,V,W, je peux
obtenir X,Y,Z
(attention, la
virgule n'a pas le même sens à gauche et à droite, comme je vais le
dire ci-dessous) : on dit que les formules à gauche du symbole ‘⊢’
(U,V,W) sont les antécédents
(ou parfois hypothèses) du séquent, et que celles à droite
(X,Y,Z) en sont
les conséquents (ou parfois conclusions). La
logique linéaire se définit par un certain nombre de règles qui
définissent les séquents valables (et ces règles ont la
forme : si ceci et ceci sont des séquents valables alors cela en est
un aussi). Par
exemple, A&B⊢A⊕B est
un séquent valable (dont le contenu intuitif très grossier est quelque
chose comme si j'ai le choix entre A et B, je
peux y renoncer
). Si on écrit
simplement A&B⊢A⊕B
dans une phrase en français, on convient que cela
signifie A&B⊢A⊕B
est un séquent valable
. Un autre exemple de séquent valable (je
le démontrerai plus bas)
est : A⊗(B⅋C)⊢(A⊗B)⅋C
(en revanche, sa « réciproque », c'est-à-dire si on échange
l'antécédent avec le conséquent, n'est pas valable).
Notons qu'un séquent peut très bien avoir zéro formule à gauche du
taquet, ou zéro à droite (ou même les deux, mais il se trouve que ⊢
n'est pas un séquent valable de la logique linéaire). Et de fait, au
bout du compte, on s'intéresse surtout aux formules P
telles que ⊢P [soit un séquent valable] : ce sont elles
qu'on appelle les tautologies ou les théorèmes
de la
logique linéaire. Par exemple, on a
⊢(A&B)⊸(A⊕B),
c'est-à-dire que
(A&B)⊸(A⊕B) est une
tautologie de la logique linéaire. Mais même si on veut, au final,
s'intéresser à des séquents valables de la forme ⊢P, il est
utile, comme étapes intermédiaires, de passer par des sortes plus
générales de séquents.
En fait, dans un séquent comme U,V,W⊢X,Y,Z, les formules séparées par des virgules à gauche du symbole ‘⊢’ (i.e., les antécédents) sont implicitement connectées par ⊗, tandis que celles à droite du symbole ‘⊢’ (i.e., les conséquents) sont implicitement connectées par ⅋ ; c'est-à-dire qu'écrire U,V,W⊢X,Y,Z va être équivalent (même si on n'a pas besoin de le savoir) à écrire U⊗V⊗W⊢X⅋Y⅋Z. Et fort logiquement, l'absence de formule à gauche est implicitement un 1 (écrire ⊢P revient à écrire 1⊢P) et à droite c'est un ⊥. Ce ne sont pas là des choses qu'on doit savoir (ce sont des effets des règles), mais ça explique un petit peu comment les choses fonctionnent.
Voici enfin les règles elles-mêmes : dans tout ce qui suit, les lettres latines majuscules (A,B,C…) sont à remplacer par des formules quelconques de la logique linéaire, et les lettres grecques majuscules (Γ,Δ,Σ,Π) par des suites (finies) quelconques de formules séparées par des virgules (ces formules-là ne seront pas modifiées et portent le nom collectif de contexte d'application de la règle) :
- Coupure : si Γ⊢Δ,A [est un séquent valable] et A,Σ⊢Π [en est un], alors Γ,Σ⊢Δ,Π [en est encore un].
- Identité : on a A⊢A [c'est un séquent valable].
- Échange : si Γ⊢Δ alors Γ′⊢Δ′ où Γ′ et Δ′ s'obtiennent en permutant de façon arbitraire les formules de Γ et Δ respectivement. (Remarque : on peut passer complètement sous silence l'utilisation de la règle d'échange en considérant que les listes à gauche et à droite du symbole taquet, dans un séquent, sont des multiensembles, c'est-à-dire que leur ordre n'est tout simplement pas défini.)
- Introduction du & : si Γ⊢A,Δ et Γ⊢B,Δ, alors Γ⊢A&B,Δ ; élimination du & : si Γ,A⊢Δ ou bien Γ,B⊢Δ alors Γ,A&B⊢Δ.
- Introduction du ⊕ : si Γ⊢A,Δ ou bien Γ⊢B,Δ alors Γ⊢A⊕B,Δ ; élimination du ⊕ : si Γ,A⊢Δ et Γ,B⊢Δ, alors Γ,A⊕B⊢Δ.
- Introduction du ⊗ : si Γ⊢A,Δ et Σ⊢B,Π, alors Γ,Σ⊢A⊗B,Δ,Π ; élimination du ⊗ : si Γ,A,B⊢Δ alors Γ,A⊗B⊢Δ.
- Introduction du ⅋ : si Γ⊢A,B,Δ alors Γ⊢A⅋B,Δ ; élimination du ⅋ : si Γ,A⊢Δ et Σ,B⊢Π, alors Γ,Σ,A⅋B⊢Δ,Π.
- Introduction du ⊤ : [quels que soient Γ et Δ,] on a Γ⊢⊤,Δ. (Il n'y a pas de règle d'élimination du ⊤.)
- Élimination du 0 : [quels que soient Γ et Δ,] on a Γ,0⊢Δ. (Il n'y a pas de règle d'introduction du 0.)
- Introduction du 1 : on a ⊢1 ; élimination du 1 : si Γ⊢Δ alors Γ,1⊢Δ.
- Introduction du ⊥ : si Γ⊢Δ alors Γ⊢⊥,Δ ; élimination du ⊥ : on a ⊥⊢.
- Introduction du ⊸ (=abstraction) : si Γ,A⊢B,Δ alors Γ⊢A⊸B,Δ ; élimination du ⊸ (=application) : si Γ⊢A,Δ et Σ,B⊢Π, alors Γ,Σ,A⊸B⊢Δ,Π.
- Introduction de dualité : si Γ,A⊢Δ alors Γ⊢A⊥,Δ ; élimination de dualité : si Γ⊢A,Δ alors Γ,A⊥⊢Δ.
- Promotion du ! : si !Γ⊢A,?Δ alors !Γ⊢!A,?Δ, où !Γ signifie que chaque formule de la liste est précédée de !, et ?Δ désigne l'hypothèse analogue sur Δ ; élimination du ! : si Γ,A⊢Δ alors Γ,!A⊢Δ ; affaiblissement du ! : si Γ⊢Δ alors Γ,!A⊢Δ ; contraction du ! : si Γ,!A,!A⊢Δ alors Γ,!A⊢Δ.
- Promotion du ? : si !Γ,A⊢?Δ alors !Γ,?A⊢?Δ, où !Γ signifie que chaque formule de la liste est précédée de !, et ?Δ désigne l'hypothèse analogue sur Δ ; introduction du ? : si Γ⊢A,Δ alors Γ⊢?A,Δ ; affaiblissement du ? : si Γ⊢Δ alors Γ⊢?A,Δ ; contraction du ? : si Γ⊢?A,?A,Δ alors Γ⊢?A,Δ.
À titre d'exemple, je vais démontrer le séquent A&B⊢A⊕C (je veux dire, démontrer qu'il est valable). Pour commencer, on a A⊢A par la règle d'identité. On peut ensuite appliquer la règle d'élimination du & (avec pour contexte Γ vide et Δ=A), pour obtenir A&B⊢A. Puis en appliquant la règle d'introduction du ⊕, on en déduit A&B⊢A⊕C, comme annoncé. On pourrait appliquer encore une étape d'introduction du ⊸ pour en réécrire ce séquent en : ⊢ (A&B)⊸(A⊕C), c'est-à-dire que (A&B)⊸(A⊕C) est une tautologie de la logique linéaire. (Par promotion du ! avec un contexte vide, on peut aussi affirmer que !((A&B)⊸(A⊕C)) est une tautologie : toute tautologie P peut toujours être promue en !P, mais on préfère écrire simplement P.)
Comme deuxième exemple, voici un une démonstration du séquent A⊗(B⅋C)⊢(A⊗B)⅋C : pour commencer, on a A⊢A et B⊢B (par la règle d'identité, deux fois), et en appliquant la règle d'introduction du ⊗ (avec Γ=A, Δ vide, Σ=B et Π vide) on en déduit A,B⊢A⊗B ; mais par ailleurs, on a C⊢C (par la règle identité), et en appliquant la règle d'élimination du ⅋ à ces deux derniers séquents on en déduit A,B⅋C⊢A⊗B,C ; la règle d'élimination du ⊗ donne alors A⊗(B⅋C)⊢A⊗B,C, et la règle d'introduction du ⅋ donne enfin A⊗(B⅋C)⊢(A⊗B)⅋C, comme annoncé. Encore une fois, on pourrait appliquer encore une étape d'introduction du ⊸ pour en réécrire ce séquent en : ⊢ (A⊗(B⅋C))⊸((A⊗B)⅋C), c'est-à-dire que (A⊗(B⅋C))⊸((A⊗B)⅋C) est une tautologie de la logique linéaire.
Il faudrait bien sûr motiver l'origine de ces règles. Au niveau purement descriptif et/ou intuitif où je me place, ce n'est pas vraiment possible : je peux évidemment faire remarquer leur grande symétrie, mais la motivation essentielle vient surtout de l'observation des règles analogues pour la logique classique (dont je vais dire un mot plus bas) en retirant les règles dites « structurales » d'affaiblissement et de contraction (qui permettent essentiellement d'abandonner ou de dupliquer les hypothèses d'un raisonnement) et en regardant ce qui surnage.
Quelques remarques néanmoins. En principe, la
règle de coupure n'est pas nécessaire : toute démonstration qui
l'utilise peut
se réécrire sans elle (cela revient, essentiellement, à refaire la
démonstration utilisée dans la coupure à chaque fois qu'on veut
couper). En pratique, elle est bigrement utile : c'est bien elle qui
vous dit que si vous savez démontrer machin à partir de truc, et
bidule à partir de machin, alors vous savez démontrer bidule à partir
de truc (et donc de garder des lemmes sous le coude !). Mais
l'intérêt de savoir qu'on peut éliminer les coupures, c'est que comme
toutes les autres règles ne peuvent qu'ajouter des nouveaux symboles
aux formules, ça simplifie énormément la démonstration du fait que
certains séquents ne sont pas valables : par exemple, on se
convainc facilement que 1⅋1 n'est pas une tautologie linéaire, parce
que la seule façon d'arriver à ⊢1⅋1 serait par ⊢1,1 et la règle
d'introduction du 1 donne juste ⊢1 et pas autre chose. ⁂ Par ailleurs,
si on veut, on peut ne manipuler que des séquents sans rien à gauche
(i.e., sans antécédents, avec seulement des conséquents), quitte à
réécrire la règle de coupure sous la forme si
⊢Δ,A et ⊢A⊥,Π,
alors ⊢Δ,Π
, et la règle d'identité sous la
forme ⊢A,A⊥
; on se passe
alors des règles de dualité et de toutes les règles d'élimination.
On peut s'entraîner à appliquer ces règles en reprenant la liste des identités P≡Q que j'ai données plus haut et, pour chacune d'elles, en montrant P⊢Q et Q⊢P (ce qui permet bien, via la règle de coupure, à remplacer des P par des Q ou vice versa dans un séquent). Par exemple, voici comment on démontre que !⊤⊢1 : on a ⊢1 par introduction du 1 et on en déduit !⊤⊢1 par affaiblissement du ! ; et voici comment on démontre que (réciproquement) 1⊢!⊤ : on a ⊢⊤ par introduction du ⊤, on en déduit ⊢!⊤ par promotion du !, et donc 1⊢!⊤ par élimination du 1.
La logique linéaire est difficile : même si on se limite uniquement aux formules construites avec les connecteurs multiplicatifs (⊗ et ⅋) à partir des neutres multiplicatifs (1 et ⊥), le problème de décider ce qui est une tautologie linéaire (par exemple : (⊥⊗⊥)⅋1⅋1) est algorithmiquement très difficile en général (il a été montré que rien que ce bout-là est NP-complet ; cela passe à PSPACE-complet pour la logique linéaire sans les exponentielles, et c'et tout simplement indécidable si on prend la logique linéaire complète).
La logique linéaire généralise la logique classique. Pour cela, on ajoute les règles (« structurales ») d'affaiblissement et de contraction, la première affirmant que si Γ⊢Δ alors Γ⊢A,Δ (affaiblissement droit, c'est-à-dire affaiblissement des conséquents) et Γ,A⊢Δ (affaiblissement gauche, c'est-à-dire renforcement des antécédents), et la seconde que si Γ⊢A,A,Δ alors Γ⊢A,Δ (contraction droite) et si Γ,A,A⊢Δ alors Γ,A⊢Δ (contraction gauche) ; avec ces règles supplémentaires, les exponentielles deviennent inutiles, et les connecteurs & et ⊗ fusionnent en un seul qu'on peut noter ‘∧’ tandis que ⊕ et ⅋ fusionnent en un seul qu'on peut noter ‘∨’, et on obtient la logique classique. (Si on introduit l'affaiblissement structural mais pas la contraction, on obtient quelque chose qui s'appelle la logique affine, intermédiaire entre la logique classique et la logique linéaire.)
Il y a toutes sortes d'autres choses que la logique linéaire permet de retrouver : notamment, la logique intuitionniste et la structure algébrique de semi-anneau (« anneau sans soustraction »). Je pourrais aussi évoquer la logique MIX, qui ajoute à la logique linéaire la règle « de mélange », laquelle affirme que si Γ⊢Δ et Σ⊢Π alors Γ,Σ⊢Δ,Π et aussi que le séquent trivial ⊢ est valable (ce dernier permet de voir ⊥ comme tautologie, et la règle de mélange permet par exemple de voir 1⅋1 comme tautologie de la logique MIX puique ⊢1 et ⊢1 donnent ⊢1,1 par mélange donc ⊢1⅋1 par introduction du ⅋).
Je n'ai pas vraiment de conclusion à proposer à cette entrée
(disons que je m'arrête là parce que je ne sais pas quoi dire sans
risquer que ça devienne interminablement long), mais je reviens à ce
que je disais plus haut : il n'est pas évident de se faire une
intuition de ce que signifient les formules ou les opérations de la
logique linéaire, parce qu'on a l'impression qu'à chaque fois qu'elle
sert (à chaque fois qu'on en définit une sémantique), il y a
des règles en plus ou des bouts en moins. Par exemple, Andreas Blass
a défini une sémantique de la logique linéaire en termes de jeux à
deux joueurs (en partant principalement de l'idée
que A&B est un choix que j'ai
entre A et B tandis
que A⊕B est un choix qu'a mon adversaire ;
et A⊥ représente l'échange des deux
joueurs), mais cette sémantique apporte des règles
supplémentaires à la logique linéaire (elle n'est
pas complète
), donc elle ne peut pas complètement fonder
l'intuition de cette dernière. Il y a quelque chose de frustrant, et
que je ne comprends pas bien, au fait que la logique linéaire, qui est
pourtant d'apparence si « naturelle », ne semble jamais se manifester
telle quelle, il y a toujours une variation ou une autre.