Colloque "Logique et rationalité", IHPST
Samedi 23 mars 2002

"Modèles épistémiques, omniscience logique et logiques substructurelles"

Mikael Cozic, ENS Ulm

I.	Approche générale du problème

I.1	La monotonie logique des modèles épistémiques
I.2	Le paradoxe de la computation de Savage

II.	Eléments d'analyse du problème de l'omniscience logique

III.	Stratégie de résolution de l'omniscience logique : de van Benthem à Gentzen

III.1	Des vérités logiques aux règles logiques
III.2	Le principe de préservation épistémique

IV.	1ère Proposition : une logique épistémique constructive

IV.1	Motivation conceptuelle : BHK et (RP)
IV.2	Discussion de l'adéquation entre BHK et (RP)
IV.3	Perspectives formelles : directions générales
IV.4	Perspectives formelles : l'exemple de la logique IK de Bozic-Dosen

V.	2nde Proposition : une logique épistémique linéaire

V.1	(RP) et la règle de contraction
V.2	Discussion de la règle de contraction
V.3	Perspectives formelles : directions générales
V.4	Perspectives formelles : l'exemple du système DGR (D'Agostino, Gabbay & Russo) de logique épistémique substructurelle

I. 	Approche générale du problème
I.1	La monotonie logique des modèles épistémiques
Les  modèles formels de connaissance (ou modèles épistémiques) sont des structures mathématiques dont le rôle est de représenter le fonctionnement de certains compartiments de nos activités cognitives ; tombent, selon les cas, dans leurs domaines de compétence des phénomènes comme :
 
•	le fait qu'un agent croit telle chose 
•	le fait que tel agent (et non tel autre) croit que tel agent (et non tel autre) croit telle chose, etc…
•	le fait qu'un agent croit plus ou moins telle chose
•	le fait que tel agent croit plus ou moins que tel agent croit plus ou moins telle chose , etc…
•	le fait qu'un agent soit amené à modifier certaines de ses croyances en fonction de nouvelles informations dont il dispose 
•	le fait un agent soit amené à modifier certaines de ses croyances en fonction de changements dont il est informé

On pourra reconnaître successivement la logique épistémique, son extension multi-épistémique, les espaces probabilisés (dans leur interprétation subjective), leur extension aux espaces de types et la théorie de la révision des croyances, version revising et version updating. Il y aurait beaucoup de choses à dire sur les ressemblances et dissemblances existant entre ces modèles ; la ressemblance la plus frappante, à la fois technique et philosophique, est probablement le fait que les structures de mondes possibles (ou d'espaces d'états) peuvent servir, du point de vue sémantique, de cadre unifiant à tous ces modèles - les connecteurs  de la logique propositionnelle étant uniformément interprétés par les opérations ensemblistes élémentaires. Il existe une ressemblance moins évidente, intimement reliée à la première, et que l'on peut nommer le phénomène de monotonie logique des modèles épistémiques ; voici en quoi il consiste : 

•	Soit M = <S,R,V> une structure de Kripke pour un langage épistémique L ; dans le paradigme de la logique épistémique, les croyances d'un agent sont représentées par une relation R  W  (W) dite relation d'accessibilité. Soient deux formules  et   L ; si M =    alors M = K  K - ce qui s'exprime également de la façon suivante : si [[]]  [[]], alors [[K]]  [[K]] Ceci s'étend trivialement au cas multi-épistémique ; syntaxiquement, ceci correspond au fait que la règle d'inférence (RM) est universellement valide dans les structures de Kripke : 
   
Ki  Ki
•	soit <S, A> un espace mesurable ; dans le paradigme bayésien, les degrés de croyances d'un agent sont représentées par une mesure de probabilité P sur cet espace. Une conséquence immédiate de la -additivité de P est que pour tout A, B  A, si AB, alors P(A)  P(B) Dans ce cadre probabiliste usuel, nulle mention n'est faite d'un langage ; néanmoins si l'on accepte d'interpréter l'inclusion d'événement comme une implication, ce fait signifie que si A implique B, alors la probabilité de A est au moins aussi élevée que celle de B. . Ceci s'étend trivialement au cas multi-agent - les espaces de types – modulo une indexation des mesures de probabilités de chaque joueur sur les états de l'espace. Syntaxiquement, la formalisation du calcul des probabilités pose d'épineux problèmes ; néanmoins, que l'on considère la formalisation finitaire de [Heifetz & Mongin 2001] ou infinitaire de [Meier 2001] on peut toujours dériver la règle d'inférence suivante
  
L  L
où l'opérateur L signifie que la probabilité  au moins est attribuée à la proposition exprimée par 
•	soit <S, [[K]]> une structure de belief set ; dans la version sémantique du paradigme AGM de la révision des croyances, l'ensemble des croyances d'un agent est représenté par [[K]]  (S). Les trois opérations cardinales de modification des croyances (contraction, expansion, révision) prennent comme arguments une proposition, un belief set et ont comme valeur un belief set. Par définition, une proposition [[]] est acceptée par un belief set [[K]] si [[K]]  [[]] ; il s'ensuit immédiatement que si [[]]  [[]], alors si [[]] est accepté par un belief set, [[]] est acceptée par le même belief set. Syntaxiquement – c'est le format initial d'[AGM 1985] – un belief set n'est rien d'autre qu'un ensemble de formules clos sous la relation de conséquence logique classique (et cohérent) ; donc si =   , alors si   K,   K.

Le phénomène de monotonie logique a donc pour caractéristique essentielle que tout modèle épistémique qui le vérifie satisfait une forme de clôture par rapport à la relation de conséquence logique classique ; ce n'est donc rien d'autre que l'appellation générale de ce qui est connu en logique épistémique comme le problème de l'omniscience logique. A ceci près qu'il existe d'autres formes, voisines, d'omniscience logique (que l'on retrouve éventuellement, mais pas nécessairement, dans les autres modèles épistémiques) ; par exemple, en logique épistémique toutes les tautologies classiques sont connues (dans le calcul des probabilités, toute tautologie est connue avec une probabilité égale à 1, en révision des croyances toute tautologie est acceptée par un belief set) Néanmoins le phénomène de monotonie est exemplaire en ce qu'il exhibe de manière particulièrement claire la façon dont ces modèles attribuent "gratuitement" tout raisonnement déductif aux agents qu'ils sont censés représenter : il suffit qu'un agent croit en l'antécédent d'une implication pour automatiquement se voir créditer la croyance en sa conclusion. Une justification courante du principe de monotonie, que l'on trouve par exemple dans [Moore 1988] ou [Gardenfors 1988] est que l'on a affaire au moins problématique et au plus minimal des principes de rationalité, qui plus est passablement innocent en pratique.  A supposer qu'elle soit fondée, le degré de satisfaction que l'on peut tirer d'une telle réponse est inversement proportionnelle à l'ambition et à l'ampleur que l'on assigne aux modèles épistémiques ; en particulier, quand, comme [Stalnaker 1984] on cherche à fonder philosophiquement ces modèles, quand on cherche à montrer que ces modèles épistémiques constituent la base d'une théorie de la connaissance, alors le problème reste entier. 
I.2	Le paradoxe de la computation de Savage
Mais il n'y a pas besoin d'assigner une telle ambition aux modèles épistémiques pour rejeter cette justification car elle est mal fondée ; c'est ce que montre le "paradoxe de la computation" de Savage, qui se présente comme une remarque incidente dans un article où Savage expose ses soucis philosophiques concernant la théorie des probabilités subjectives  : 
"une personne à qui l'on demande de parier sur un chiffre éloigné dans l'expansion décimale de  devrait, afin de respecter strictement la théorie, calculer ce chiffre, bien que cela serait inutile si le coût de calcul excédait le gain en jeu. En effet, les postulats de la théorie impliquent que l'on doit agir en conformité avec toutes les conséquences logiques de ses connaissances. Est-il possible d'améliorer la théorie de ce point de vue, en tenant compte du coût de la pensée, ou bien cela entraînerait-il un paradoxe ?"

Ce qui signifie, pour paraphraser platement Savage : acceptez-vous de parier que x*  est le n-ième chiffre dans l'expansion décimale de  ? La théorie de la décision nous recommande de parier si x* est bien le chiffre correct. Le paradoxe vient de ce que le coût engendré par la computation de x* peut excéder le gain du pari ; la théorie de la décision ne prend en compte que le résultat (attendu) de nos raisonnements et nous fait agir en fonction ; elle ne prend pas en compte le coût induit par le processus de raisonnement lui-même. La prise en compte de la réalité de la connaissance fait donc apparaître une divergence entre ce qui paraît intuitivement raisonnable et ce qui est raisonnable selon la théorie de la décision ; existe-t-il un moyen de résoudre ce paradoxe, comme par exemple la théorie de la décision a pu donner une réponse au paradoxe de Saint-Pétersbourg en distinguant espérance de gain et espérance d'utilité ? 
A vrai dire, Savage ne prend en compte qu'une partie du problème soulevé par ce genre d'exemples ; dans le cas particulier qu'il évoque, on a affaire à une question calculable puisqu'il suffit de développer  jusqu'à la n-ième décimale pour être fixé. Mais il n'est pas sûr que dans le cas général, il soit même possible en un temps fini d'effectuer le raisonnement que l'agent est tenu de faire. En outre, il faudrait distinguer dans la difficulté un

•	un problème computationnel fort = comment intégrer dans le modèle du choix les coûts de calcul ? 
et un
•	un problème computationnel faible = est-il même possible qu'un agent effectue le calcul (le raisonnement) en question ? est-ce possible qu'un agent réel, en pratique, le fasse ? est-il possible qu'un agent réel le fasse dans un temps raisonnable (par exemple, inférieur à son espérance de vie) ? 

Ces difficultés subsistent et même deviennent plus dramatiques : 
(1) quand on passe de la théorie pure aux applications : en Intelligence Artificielle par exemple, ces problèmes computationnels constituent l’obstacle majeur à une application de la théorie de la décision pour la construction d’agents autonomes ; ils empêchent que la théorie de la décision soit aisément implémentable [Shut & Wooldridge 2001]
(2) quand on élargit la théorie aux interactions stratégiques c'est-à-dire quand on passe de la théorie de la décision à la théorie des jeux : l'exemple le plus éloquent en même temps que le plus vénérable est probablement celui des échecs [Rubinstein 1998, pp.130-1]. Si l'on représente les échecs comme un jeu fini, à somme nulle, à information parfaite (ce qui est raisonnable) et si l'on ajoute un clause de non cyclicité (du genre : si trois fois une même configuration apparaît, la partie est déclarée nulle), alors il existe un algorithme (la backward induction) qui donne une solution (un équilibre parfait en sous-jeux) telle que chaque joueur peut forcer la valeur de cette solution. On donne une preuve d'existence de cette solution, on donne un moyen de la construire, mais sa construction effective, dans le cas des échecs, est bien au delà de nos ressources computationnelles ; comme le dit H.Simon, contrairement à tout ce que le bon sens pourrait nous suggérer, la leçon essentielle de la théorie des jeux est que "les échecs sont un jeu trivial"  
(3) quand on passe d'une interprétation descriptive à une interprétation normative de la théorie du choix rationnel : un des points de l'argument de Savage est effectivement que le problème computationnel non seulement invalide partiellement la portée descriptive de la théorie de la décision, mais en plus contrarie sa prétention à nous recommander les choix les plus raisonnables. On va voir que ceci vaut pour le (Pfort) comme pour le (Pfaible). 
Il est clair que ces problèmes, quoique étroitement liés, sont bien distincts : 
-	le (Pfort) est essentiellement un problème métathéorique 
-	le (Pfaible) est essentiellement un problème métanormatif
(1) Problème métathéorique : pour être complète, la théorie de la décision devrait prendre en compte les coûts de computation induits par l'application de la règle de décision ; c'est cela que j'appelle métathéorique. Le "paradoxe" auquel pense Savage est probablement la régression qui menace une telle pente : pour être véritablement complet, il faudrait aussi prendre en compte les coûts de métaraisonnement, et ceux de méta-méta-….raisonnement, etc…Je ne discuterai pas de ce problème complexe ni de la question de savoir si cette régression est vicieuse ou non Cf [Mongin 2000], [Walliser & Mongin 1988] et [Lipman 1991] qui arrivent à des conclusions sensiblement différentes. 
(2) Problème "métanormatif" (R.Ogien): la théorie viole le principe "à l'impossible nul n'est tenu" puisqu'elle peut exiger d'agents des tâches qu'ils peuvent très bien n'avoir aucun moyen de faire. La théorie nous dit ce qu'il faut connaître indépendamment de toute préoccupation sur la manière dont on pourrait être amener à le faire ; c'est ceci que recouvre essentiellement le problème de l'omniscience logique quand on l'aborde du point de vue normatif. 

Idée directrice : il me semble qu'une analyse correcte du problème conduit à penser qu'une voie de résolution féconde consisterait à intégrer à la logique épistémique les avancées de logiques "proof-theoretically motivated", nommément certaines logiques dites substructurelles ; je vais donc successivement exposer : 
-	l'analyse du problème 
-	la composante conceptuelle de l'intégration (a-t-on des bonnes raisons d'aller chercher une solution au problème de l'omniscience logique du côté des logiques substructurelles ?)
-	la composante technique de l'intégration (a-t-on les moyens mathématiques d'aller chercher une solution au problème de l'omniscience logique du côté des logiques substructurelles ?)

II. 	Eléments d'analyse du problème de l'omniscience logique

Voici, rassemblées en quelques propositions, les grandes lignes de l'analyse du problème qui m'a servi de point de départ : 

(Proposition 1) L'hypothèse de faillibilité logique est correcte

Ceci revient, comme le dit Hintikka, à rejeter le principe (PIC) Principe d’Ignorance du Contingent = la condition nécessaire pour qu’un agent puisse ignorer  est que  ne soit pas une proposition nécessaire ; c'est un fait que notre activité déductive n'est pas sans failles

(Proposition 2) La faillibilité logique n'a pas que des raisons purement "accidentelles"

Corollaire 1 : Le couple compétence / performance n'est pas le bon couple pour aborder le problème de l'omniscience logique. Pourquoi ? Parce que les facteurs qui expliquent la distance entre compétence et performance sont des facteurs exogènes et accidentels par rapport à la compétence ; ainsi par exemple [Schick 1991] donne comme exemples de causes de faillibilité déductive la distraction, l’inadvertance, l’alcool… ; mais cela laisse manifestement le principal de côté, c’est-à-dire une véritable théorie des capacités logiques qui nous sont attribuables. Si les mathématiciens ont mis si longtemps pour découvrir une preuve du théorème de Fermat, ce n’est probablement pas, ou pas seulement, parce qu’ils sont distraits ! Il n’est pas envisageable de proposer une théorie de la connaissance complète qui considérerait comme accidentelle toute divergence entre nos capacités déductives et les canons de la logique classique. La représentation de ces capacités entre de plein droit dans celle-là, et des facteurs comme l’alcoolémie ou la fatigue sont les facteurs qui peuvent exprimer l’écart entre notre théorie de la connaissance et les comportements réels des agents. 

Corollaire 2 : ne pas réduire l'omniscience logique à un comportement erratique des connecteurs logiques. C'est un réquisit très important, qui a son origine dans l'examen d'une solution comme celle des mondes possibles impossibles ; il implique que l'on essaiera de garder invariant ce qui détermine la signification des connecteurs ; il n'implique pas, par contre, que l'on ne puisse raffiner les connecteurs classiques. On verra la pertinence du Calcul des Séquents relativement à cette exigence. 

Les deux Propositions suivantes expriment de façon condensée ce que je voulais illustrer avec le paradoxe de Savage. 

(Proposition 3) un modèle épistémique doit résoudre le problème de l'omniscience logique

Comme le remarque [Stalnaker 1991], c’est un pan entier de la connaissance qui s’appauvrit de manière invraisemblable si l’on élimine les prestations déductives des agents : la délibération pratique, le raisonnement à propos de matières empiriques, l’argumentation… C’est, je crois, un point que l’on peut donc accepter sans trop de difficultés : à partir du moment où l’on envisage de donner sinon une théorie du moins un langage pour étudier la cognition humaine, on ne peut tenir pour négligeable la spécificité de nos compétences déductives. A l'opposé, [Moore 1988] soutient-il que le problème de l’omniscience logique est négligeable quand on cherche à rendre compte de notre comportement quotidien, et qu’il ne se pose que dans les cas extraordinaires où la pratique mathématique entre en jeu ; la faillibilité logique des agents est un simple " bruit " dans leur comportement, qui n’a guère de poids à côté de l’incertitude empirique. 

(Proposition 4) :  il existe une connexion intrinsèque entre le problème de l’omniscience logique et la construction d’un modèle de connaissance pour une théorie de l’action.

Il me semble que la réalité est diamétralement opposée à une opinion comme celle de [Moore 1988] : non seulement le problème de l’omniscience logique n’est pas négligeable quand on considère la façon dont un agent agit sur la base de ses connaissances, mais c'est là qu'il devient vraiment incontournable. Comme le remarquent en effet [Fagin & Halpern 1990], [Halpern & ali 199x], il y a des circonstances dans lesquelles l’omniscience logique peut être quelque chose de relativement bénin ; la connaissance que la logique épistémique attribue à un agent peut alors être vue comme une approximation correcte de la part d’un modélisateur. En particulier, si les conséquences logiques des croyances d’un agent n’ont précisément pas de conséquences pragmatiques, on peut considérer que l’approximation est raisonnable ; dans leur terminologie, on peut dire que les imprécisions de cette conception externe de la connaissance ne prêtent pas à conséquences. Mais pour reprendre l'exemple de l'introduction, c'est quand on a la main au début d'une partie d'échecs que cela devient effectivement quelque chose de crucial de pouvoir en pratique effectuer ou non la backward induction ; pour montrer que ce n'est  pas une lubie de logicien, voici le commentaire qu'en font Osborne & Rubinstein dans l'introduction de leur manuel : 
"…the abstract model of chess as described by Zermelo allows us to deduce a significant fact about the game, but at the same time omits the most important determinant of the outcome of an actual play of chess : the "abilities" of the players."
 
(Proposition 5) une solution au problème de l’omniscience logique doit être "substantielle" 

C'est la contrepartie positive de la Proposition 2 : une solution substantielle au problème de l’omniscience logique n’est rien d’autre qu’une solution qui enveloppe une théorie minimale de notre compétence logique ; une solution est donc a priori incomplète quand elle ne nous donne que les moyens de créer de contextes hyperintensionnels : encore faut-il qu’elle nous donne de bonnes raisons de les accepter. Le reproche essentiel, je crois, que l’on peut faire aux solutions existantes est la présence d’un fossé conceptuel entre les moyens qu’elles utilisent pour représenter des agents logiquement limités et les raisons de ces limitations. Une bonne logique épistémique pourrait, pour ainsi dire " à la source ", représenter nos comportements déductifs, et non les surajouter a posteriori comme d’étranges handicaps. Qu’est-ce que cela signifie exactement ? Qu’une logique adéquate pour l’omniscience logique doit être capable, sinon de consigner, du moins de tenir compte des procédures cognitives mises en œuvre par le raisonnement ; elle doit permettre de sélectionner celles qui sont à la portée d'un agent En l'état, la logique épistémique est une logique de la croyance que l’agent devrait entretenir étant donné ses informations, compte non tenu des procédures cognitives exigées pour qu’une information soit réellement possédée et exploitée dans un contexte cognitif plus large. 

(Proposition 6) une logique de la connaissance correcte est une logique dans laquelle l’agent est omniscient

Il y a, dans la littérature qui traite de l’omniscience logique, un certain nombre de malentendus et de confusions autour de cette idée ; telle solution est rejetée parce qu’elle laisse l’agent omniscient dans un certain domaine, dans une certaine logique, à l’égard d’un certain nombre de propositions…Le genre de difficultés que l’on peut entendre par là est à ce point équivoque que c’est presque devenu un automatisme dans la littérature que de qualifier ainsi la plupart des solutions de ses prédécesseurs. Je ne crois pas qu’il y ait beaucoup de sens à chercher une logique où l’agent ne serait pas omniscient " dans l’absolu " ; en particulier, chercher une logique de la conscience ou une logique qui soit capable de tenir compte de nos moindres défaillances n’a guère d’intérêt. Ce que l’on veut, c’est une logique qui soit capable de capturer un ou deux traits structurels propres à nos capacités de raisonnements ; elle contiendra forcément une grande part d’idéalisation. Dans cette logique, l’agent sera omniscient ; on pourra éventuellement paramétrer les capacités logiques sur les agents, sur les différents moments, sur les différents contextes, mais pour un même agent, dans un même contexte et à un même moment, il y aura forcément omniscience. 

III. 	Stratégie de résolution de l'omniscience logique : de van Benthem à Gentzen 
III.1	Des vérités logiques aux règles logiques
Le problème de la sémantique de Kripke, c’est qu’elle traite l’information dont dispose un agent comme déjà " toute faite " et comme complètement cohérente ; aucune des solutions que nous avons envisagées ne modifie véritablement ce point. La sémantique de voisinage traite de l’information éventuellement discordante ; les mondes possibles impossibles donnent un artifice pour représenter l’information logique ; les structures d’awareness nous disent que l’information doit être morphologiquement disponible ; à aucun endroit cependant, la façon dont le traitement syntaxique (l’exploitation déductive) de l’information s’effectue n’est pris en compte. Prendre en compte ce défaut, c'est suivre ce que je propose d'appeler pompeusement le "programme de Van Benthem", qui tient dans le (très vague) mot d'ordre suivant : 
" se déplacer de la réflexion sur la vérité abstraite vers celle sur la structure de l’information et des mécanismes de son traitement " 

Effectuer ce déplacement revient à envisager une modification de la logique épistémique, dont le premier pas consiste à changer de format syntaxique : en logique épistémique, on travaille en général dans un système à la Hilbert – c'est une des raisons pour lesquelles le problème de l’omniscience logique est souvent présenté comme l’attribution scandaleuse aux agents de la " connaissance de toutes les vérités logiques " ; il y a manifestement quelque chose de très artificiel à présenter les choses ainsi. Il n’est pas sûr en effet que les agents réels connaissent certaines (mais pas toutes) de ces vérités logiques ; il n’est pas sûr non plus que les agents connaissent une quelconque vérité logique. Ce que l’on a envie de dire, c’est bien plutôt que les agents raisonnent plus ou moins bien, c’est-à-dire déduisent plus ou moins d’informations, à partir d’informations qu’ils possèdent déjà. De ce point de vue l'opinion de M.Dummett
"the use, before Gentzen, of axiomatic formalizations of logic had other, unfortunate, effects. It was, in the first place, conceptually misleading. It diverted attention from the obvious fact that, whereas in a theory our concern is to establish true statements, and the derivation of statements from others is only a means to this end, in logic the process of derivation is itself the object of study. Axiomatic formalizations, unlike natural deduction, tempt us to regard logic as a search for logical truth." (Dummett 1977, p.168)
est tout à fait justifiée comme préalable heuristique à une résolution de l'omniscience logique. En particulier, quand on présente la logique comme un ensemble de vérités, on a tendance à penser que pour l'action, le problème de l'omniscience logique est relativement non pertinent. Il en va tout autrement quand on considère la logique comme une des façons fondamentales (et clairement pas la seule) que nous avons de rendre fécondes les informations que nous recevons de notre environnement : un ensemble de règles qui permettent de tirer des informations d'hypothèses qui, en elles-mêmes n'ont rien de "logique". 
De ce point de vue, les deux formats inventés par Gentzen, la Déduction Naturelle et le Calcul des Séquents, constituent des points de départ beaucoup plus satisfaisants : ils permettent de ramener la logique à un ensemble de règle de raisonnement, semblables à l'unique règle des systèmes à la Hilbert, le modus ponens. 
Maintenant, il va falloir montrer l'intérêt qu'il y a à adopter, provisoirement au moins, ce point de vue des règles de raisonnement pour avancer dans la résolution du problème de l'omniscience logique ; les règles nous permettent-elles de trouver des contreparties formelles intéressantes à l'idée intuitive à partir de laquelle la Proposition 1 nous recommande de partir :  qu'il y a des choses qui sont logiquement plus ou moins triviales ? La méthode que je propose d'adopter est donc de "tester" la trivialité des règles logiques – si toutefois cette expression a un sens véritable.  
III.2	Le principe de préservation épistémique
Pour préciser quelque peu cette idée de plus ou moins grande trivialité des règles, on peut revenir au principe de monotonie logique : de   inférer Ki  Ki. Si  implique , alors la vérité est préservée quand on passe de  à  ; ce que nous dit le principe, c'est qu'alors l'accès épistémique est également préservée. On peut partir de cette différence entre

•	préserver la vérité = préservation aléthique (ce que l'on attend au minimum d'une règle logique)
 et 
•	préserver la reconnaissance de la vérité = préservation épistémique (ce que l'on attend idéalement d'une logique de la connaissance)

On peut ramener la résolution du problème de l'omniscience logique à l'élimination, (ou à l'amendement, ou encore au contrôle, dans le cas de la logique linéaire) des règles de raisonnement susceptibles de disjoindre préservation aléthique et préservation épistémique ; en particulier, une logique peut être réputée plus ou moins triviale selon qu'elle induit une divergence plus ou moins grande entre préservation aléthique et préservation épistémique. 
C'est la façon dont j'interprète le "programme de van Benthem" ; concrètement, ce que l'on va faire, c'est regarder comment chacun des deux formats inventés par Gentzen peut nous aider à trouver des réalisations plausibles du principe de préservation épistémique. Il faut néanmoins affiner ce principe pour qu'il devienne opératoire ; pour cela, à la suite d'[Usberti ??], on va se servir de la notion de justification pour  par quoi on entend "raison de croire que " ; les règles de raisonnement peuvent être vues comme des principes qui énoncent de (saines) transitions de justifications. Le principe de préservation épistémique s'énonce alors de la manière suivante : 

(PPE) Principe de préservation épistémique : une règle satisfait au principe de préservation épistémique si la justification des prémisses implique celle de la conclusion. 

Le réquisit minimal qui découle de ce principe est que pour qu'une règle satisfasse au principe de préservation épistémique, il faut qu'il soit possible, en principe, de justifier la conclusion à partir des justifications des prémisses ; ce que l'on peut appeler réquisit de préservabilité.
 
(RP) Réquisit de préservabilité : si un agent a des justifications pour les hypothèses A1, …,An, pour lui attribuer nécessairement une justification pour B, il faut au moins qu'il existe une manière possible de construire une justification pour B sur la bases des justifications pour A1, …,An.
Ce qui donne, dans le jargon modal :  J(A1, …,An)  J(B) seulement si (Cons (J(B), J(A1, …,An))

Remarque sur (RP) : Il faut être particulièrement attentif aux modalités (aléthiques bien sûr), ce sont elles qui jouent le rôle clef dans ces questions de motivations conceptuelles ; en particulier, la modalité de la prémisse vaut pour l'ensemble du problème de l'omniscience logique : il s'agit de savoir si on a bien raison – ou plutôt si ce n'est pas une idéalisation excessive - d'attribuer nécessairement telle ou telle compétence déductive à un agent. Si on oublie cette modalité, une bonne partie de la discussion peut s'avérer non pertinente voire carrément absurde  ; pour mettre en question une règle logique, en principe, il suffit donc qu'elle ne soit pas forcément appliquée. 
IV. 	1ère Proposition : une logique épistémique constructive
IV.1	Motivation conceptuelle : BHK et (RP)
Un système de règles satisfait (RP) si à chaque règle il est possible d'associer une construction élémentaire qui assure que l'on peut produire une justification pour la conclusion sur la base d'une justification pour les prémisses ; l'interprétation BHK des constantes logiques peut servir de première approximation pour la satisfaction de ce réquisit, puisqu'elle opère précisément cette association systématique de constructions aux constantes logiques. Typiquement, une preuve d'une proposition AB se construit en formant une paire à partir d'une preuve de A et d'une preuve de B. 
Le format de la DN est particulièrement adapté à l'interprétation BHK : on peut "lire" sur les règles d'introduction la construction associée, et les théorèmes de normalisation garantissent le comportement "harmonieux" des règles d'élimination par rapport aux règles d'introduction. On sait que l'on peut donner un contenu extrêmement fort à cette association, qui tient dans l'isomorphisme de Curry-Howard ; pour notre part, il nous suffit de la composante bijective de cet isomorphisme : à chaque preuve intuitionniste on peut faire correspondre un terme du -calcul qui décrit exactement la construction dont procède la preuve. 
Mais toutes les règles de la Déduction Naturelle Classique (NK) ne passent pas le "test" de l'interprétation constructive : elle nous conduit à restreindre la DN en passant du système classique au système intuitionniste (NJ). Ce que garantit une telle restriction, en retour, c'est que, pour chaque raisonnement reconnu valide, il existe une construction composée de constructions élémentaires (former une paire, projeter, appliquer, abstraire) qui permet de construire des justifications pour la conclusion sur la base de justifications pour les prémisses. 
IV.2	Discussion de l'adéquation entre BHK et (RP)
On peut se demander si l'on ne manque pas le point en considérant finalement l'intuitionnisme comme une première approximation pour avancer dans la résolution de l'omniscience logique ; en particulier, est-il vrai que NK est "moins triviale" que NJ ? 
La question se pose car il est légitime de considérer l'intuitionnisme non comme une logique classique affaiblie mais comme une logique dont la syntaxe exige une autre "qualité" des preuves. On aurait donc pas une logique plus triviale mais une logique plus exigeante ! Pour répondre, il fait d'abord bien prendre en compte le fait que défendre l'adéquation de la logique intuitionniste du point de vue épistémique ne signifie pas que l'on épouse la philosophie intuitionniste. 
Considérons ensuite le cas typique de l'asymétrie entre A et A. 
En termes de construction (= -calcul), on a facilement une justification pour A sur la base d'une justification p pour A : si A  (A), alors q.(p)q représente une justification pour A. Par contre, on n'a pas, en général, une telle construction pour nous faire passer d'une justification de A à une justification de A  ; c'est bien quelque chose de moins trivial que de passer de A à A. Plus concrètement, et pour se référer à notre champ d'application privilégié, c'est bien quelque chose de moins trivial d'avoir une preuve constructive d'un théorème d'existence (Arrow-Debreu, Nash) – ce n'est généralement pas le cas – que d'en avoir une non constructive. Or, ce qui nous intéresse, c'est de restreindre (de manière motivée) les raisonnements réputées triviaux ; passer de A à A est en général une chose moins triviale que de passer de A à A. La logique intuitionniste nous permet donc de faire des différences plus fines que la logique classique et directement exploitables dans notre perspective. 
Dans le cas des théorèmes d'existence en théorie des jeux et en microéconomie, cette différence peut induire des questions techniques et conceptuelles fondamentales : supposons que l'on se place dans le cadre d'une interprétation éductive des équilibres, c'est-à-dire que l'on considère qu'un équilibre est "le résultat d'une réflexion préalable des joueurs" [Binmore 1992] (par opposition à une interprétation évolutive des équilibres comme points de convergence), et supposons que les joueurs disposent d'une justification qu'il existe bien un tel équilibre pour un jeu donné qu'ils vont devoir jouer ; supposons également que l'équilibre est unique. Si les joueurs ont une preuve constructive de cet équilibre, ils disposent d'une méthode pour calculer (du moins en principe) l'équilibre, ce qui est cohérent avec l'hypothèse interprétative – modulo une forte idéalisation comme on l'a vu avec l'exemple des échecs ; par contre, s'ils ne disposent pas d'une preuve constructive, il se peut qu'ils puissent calculer l'équilibre, mais il n'est pas sûr qu'ils le puissent. On retrouve ici la distinction modale constitutive de (RP) ; sous l'interprétation éductive, cela fait clairement une différence : n'est-il pas délicat de prédire un comportement à des joueurs comme résultant d'un raisonnement dont rien ne garantit qu'il leur est possible de l'effectuer ? Une logique épistémique qui peut capturer la différence entre les deux situations, ce qui n'est évidemment pas le cas de la logique épistémique classique, est donc particulièrement recommandée.
IV.3	Perspectives formelles : directions générales
Techniquement, cette proposition prend tout simplement le visage d'une interprétation épistémique d'un champ d'investigation de plus en plus actif : celui des  logiques modales intuitionnistes. Après avoir été pendant longtemps réduit à des contributions sporadiques, il est aujourd'hui en pleine expansion, en raison principalement de ses retombées pour la programmation fonctionnelle (cf notamment [Pfenning-Davies]); à condition d'enrichir le -calcul avec des opérateurs pour la modalité, on peut étendre l'isomorphisme de Curry-Howard à certains systèmes de logique modale. Une des conditions de cette extension est la mise au point de bons systèmes de Déduction Naturelle pour la logique modale, ce que l'on reconnaît comme une difficulté notoire depuis les travaux de Prawitz (1965). 
Pour en rester aux développements élémentaires, l'extension modale de l'intuitionnisme consiste, du point de vue syntaxique, à marier une logique propositionnelle intuitionniste avec les modalités (épistémiques) ; du point de vue sémantique, la façon la plus immédiate de procéder est de profiter de la proximité entre la sémantique de Kripke pour la logique intuitionniste et la sémantique de Kripke pour la logique modale. L'idée, très simple, est de combiner une relation d'accessibilité intuitionniste avec les relations d'accessibilité épistémiques en déterminant les "bonnes" conditions de raccordement des deux types de relation. Qu'entend-on par là ? 
La simple superposition des deux sémantiques ne permet pas de conserver les propriétés qu'on attend d'elles ; par exemple, la propriété d'hérédité des modèles intuitionnistes est perdue dans le cas général. Il faut donc travailler sur les clauses de satisfaction et/ou les contraintes sur les relations d'accessibilité. 
IV.4	Perspectives formelles : l'exemple de la logique IK de Bozic-Dosen
Exemple : IK de Bozic-Dosen est la version intuitionniste de K avec  comme symbole de modalité primitive ; IK a la propriété de la disjonction ; IK est caractérisée par la classe des modèles qui ont une relation d'accessibilité modale R et une relation d'accessibilité intuitionniste I telles que IR  RI. Si l'on représente cette condition par un diagramme, on comprend immédiatement comment elle rend possible l'élargissement de la propriété d'hérédité aux formules modales. [Simpson 1994] note qu'en adoptant l'autre stratégie, c'est-à-dire en modifiant la clause de satisfaction pour l'opérateur modal de manière à l'aligner sur le quantificateur universel intuitionniste, on obtient le même résultat de caractérisation pour IK. La clause est alors la suivante : 
M, s =  ssi s' t.q. sIs' et v t.q. s'Rv, M, v =  
 De la même façon, IK est caractérisé par les modèles modaux intuitionnistes tels que I-1 R  R  I-1 , condition qui garantit à nouveau la propriété de monotonie. Un certain nombre d'auteurs ont adopté une stratégie mixte qui consiste à imposer des conditions de raccordement sur R et I et à modifier les clauses de satisfaction – plus précisément à reproduire pour  et  l'asymétrie de la sémantique intuitionniste du premier ordre entre  et . Néanmoins, du point de vue de la logique épistémique, on peut provisoirement mettre de côté ces questions et se concentrer sur l'exploitation de . 

Exemple : S = {s1, s2}, I = <s1, s2>, R = <s1, s1>, V() = {s2}
s1 =  et s1 
s1= B mais s1= B

Question : extension à la sémantique de voisinage ? L'idée de la sémantique de voisinage, c'est d'attribuer directement les propositions aux agents ; ce qu'il faut modifier, c'est la notion de proposition car l'ensemble des états qui valident une formule n'est plus dans un modèle intuitionniste un simple sous-ensemble de l'espace d'états. Désormais, l'ensemble des états qui satisfont une formule est clos à droite par la relation I. On peut donc définir une sémantique de voisinage qui attribue à chaque agent des ensemble d'états clos à droite par la relation I. Remarque : cette condition n'est pas nécessaire puisque la clause de satisfaction exige seulement que la valeur de la proposition appartienne au voisinage. 
Pour respecter la condition d'hérédité, il suffit d'imposer une clause  parallèle à celle de la valuation atomique, c'est-à-dire que le voisinage épistémique des mondes est cumulatif par rapport à I. Soit  = B et supposons que M, s = B ; alors [[]]  C(s) ; soit s' tq sIs' ; alors clairement s' = B puisque [[]]  C(s). Question : est-ce une condition nécessaire ?  Pas si l'on a défini le voisinage d'une manière classique : il suffit d'exiger que les ensembles clos à droite pour I se cumulent relativement à I. 
Comme la sémantique de voisinage, cette logique ne pourrait pas distinguer entre proposition équivalentes, mais cette fois entre propositions intuitionnistiquement équivalentes – tandis qu'elle pourra évidemment distinguer des propositions classiquement équivalentes. 
Question : conserve-t-on la propriété de la disjonction ? on peut conjecturer que oui, par exemple en adaptant le calcul des séquents pour la sémantique de voisinage de [Lavendhomme & Lucas 2000] qui admet l'élimination des coupures dans le cas classique. Cette adaptation ne doit pas poser de problème puisque dans le cas classique les règles pour l'opérateur modal sont portent sur des séquents dont la partie droite ne comporte qu'une formule.
Question : extension au cadre multi-agent ? C'est une question moins évidente car il faut que les opérateurs collectifs conservent la compatibilité avec l'accessibilité intuitionniste.
Question : quel peut être l'apport des travaux à l'extension de l'isomorphisme de Curry-Howard ? Distinguer les questions de signification générale de l'extension pour la logique épistémique et les éventuelles innovations induites, comme par exemple le calcul des séquents à plusieurs régions
Question : que devient la signification intuitive de la sémantique ? En logique épistémique, on peut considérer les états comme des manières de spécifier (totalement) les paramètres pertinents d'une situation cognitive ; en logique intuitionniste, depuis Kripke, on s'attache à une métaphore (moins robuste) des états comme différents moments dans l'évolution épistémique du sujet connaissant donc comme des états d'information, alors que dans le premier cas les états sont ce qui sert à déterminer des états d'information. Du point de vue interprétatif, la combinaison des deux sémantiques n'est pas triviale – le problème est le même quand on fait usage de situation ou de logique partielle - ; une notion syncrétique comme "support de justifications" est-elle satisfaisante ? Il serait agréable d'avoir une interprétation convaincante car il est possible de construire une sémantique pour les logiques substructurelles épistémiques en partant de tels modèles intuitionnistes mais en contraignant algébriquement l'espace d'états (cf supra et pour un panorama général [van Benthem 1991]).

V. 	2nde Proposition : une logique épistémique linéaire
V.1	(RP) et la règle de contraction
On peut exiger plus de (RP) que le simple critère de constructibilité, qui revient à identifier au couple trivial / non-trivial le couple constructible / non nécessairement constructible : il existe probablement des raisonnements dont la constructibilité n'est que purement principielle et qui sont donc exclus, eux aussi, par (RP). On peut considérer ce pas supplémentaire ou bien comme une étape vers la satisfaction de (PPE) après celle, nécessaire, de (RP), ou bien, plus radicalement comme l'achèvement (philosophiquement) nécessaire de (RP). En effet,  comme le dit [Usberti ??], il est dans la nature de la justification de pouvoir être reconnue comme telle ; aussi, (RP) ne sera réellement satisfait que si la possibilité de la préservation épistémique est une réelle possibilité, et non une pure possibilité de principe. Mais dans le format de la Déduction Naturelle à la Prawitz (non linéarisée), il ne semble pas que l'on ait de prise pour contrôler ce genre de paramètres, à moins de toucher aux règles d'introduction et d'élimination des connecteurs, ce que l'on cherche à éviter en vertu de la Proposition 2. 
Mais quand on passe au Calcul des Séquents, on dispose d'une perspective plus fine sur les règles logiques, dans la mesure où il fait apparaître différentes catégories de règles, là où il y en avait essentiellement une dans la Déduction Naturelle. Pour notre stratégie, qui consiste à tester les règles logiques, c'est évidemment quelque chose de crucial puisque des présuppositions cachées dans la DN deviennent explicites et peuvent être évaluées. Mieux, on peut distinguer les règles qui gouvernent le comportement des connecteurs de celles, dites structurelles, qui n'engagent aucune constante logique mais concernent certaines propriétés générales du raisonnement ; ce qui nous permet de ne pas rabattre la faillibilité logique sur un usage et une compréhension erratiques des connecteurs. 
Les règles structurelles dont la compatibilité avec (PPE) et (RP) est la plus discutable sont la règle de contraction et la règle d'affaiblissement. Voici le genre de motivations que l'on peut trouver pour les remettre en cause  : 

•	Si j'ai la possibilité de construire une justification pour B sur la base notamment de plusieurs justifications pour A, qu'est-ce qui garantit que j'ai la possibilité réelle de me passer de certaines des justifications pour A pour construire une justification pour B ? 

•	Si j'ai la possibilité de construire une justification pour B sur la base de justifications pour A1,...,An, qu'est-ce qui me garantit que j'ai la possibilité réelle d'augmenter indéfiniment mes prémisses tout en menant toujours à bien mon raisonnement ? 
V.2	Discussion de la règle de contraction
Il s'agit là plutôt de questions que d'arguments ; la charge de la preuve appartient à celui qui veut remettre en question ces règles. Il me semble que, de ce point de vue, la contraction a un privilège certain relativement à (PPE) – ce n'est pas vrai en général, puisque la règle structurelle la plus discutée traditionnellement est la règle d'affaiblissement qui relâche toute exigence de connexion conceptuelle entre les prémisses et la conclusion d'un raisonnement ; c'est d'ailleurs la seule que [Gentzen 1935] se sent obligé de discuter 
V.2.1	Un argument a posteriori : règle de contraction et décidabilité
La remise en cause de la règle de contraction a de très solides contreparties formelles ; en étant caricatural, on pourrait dire que la règle de contraction est la responsable de la complexité d'une logique. De manière générale, on ne peut ignorer ce qui reste la contrepartie formelle la plus solide aux exigences de "trivialité" qui sont les nôtres, à savoir la décidabilité ; en particulier, une logique sans règle de contraction (par exemple la logique linéaire) serait un bien décevant candidat au rôle de nouveau sous-bassement propositionnel pour la logique épistémique si elle ne jouissait pas d'une propriété comme la décidabilité de la prouvabilité. 
Ce n'est pas quelque chose d'absolument évident a priori : d'autres logiques substructurelles classiques comme les plus populaires des logiques de la pertinence R, E et T, ne sont pas décidables. Le fragment MALL de la logique linéaire est décidable. On sait cependant que la réintroduction contrôlée des règles structurelles proscrites fait perdre la décidabilité : le fragment complet (avec les exponentielles) de la logique linéaire est indécidable ; bien plus étonnant encore, la restriction de ce fragment aux constantes ne permet pas de recouvrir la décidabilité. Par contre, l'extension au premier ordre de MALL reste décidable – en termes de complexité, on passe de la classe PSPACE-hard, à la classe NEXPTIME-hard. Ces résultats mettent en évidence le rôle essentiel des règles structurelles dans la complexité du problème de la décidabilité ; plus précisément, c'est le rôle de la règle de contraction qui paraît fondamental. Ainsi, l'ajout au fragment MALL du premier ordre de la règle d'affaiblissement fait perdre la décidabilité, mais pas au niveau propositionnel. Par contre, les résultats en logique de la pertinence que la suppression de l'affaiblissement sans celle de la contraction fait perdre la décidabilité dès le niveau propositionnel.
V.2.2	Un argument a priori : l'interprétation GO des constantes logiques

On reprend ici un leitmotiv de la logique linéaire, c'est-à-dire qu'elle est plus apte que les logiques traditionnelles (y compris la logique intuitionniste, dont nous sommes partis) à modéliser le paramètre quantitatif, implicite dans un format comme celui de la Déduction Naturelle. L'intuition de départ consiste à voir les hypothèses d'un raisonnement comme autant de ressources susceptibles de produire la conclusion ; de même que l'on pouvait revoir (et amender) les règles de la DN avec l'interprétation BHK, on peut revoir (et amender) les règles du Calcul des Séquents avec l'inteprétation GO (pour Girard-Okada : Girard a introduit cette idée dans [Girard 1987], [Okada 1999] fait rigoureusement le parallèle avec BHK). Typiquement, on introduit le tenseur en disant que si les ressources  et  permettent d'engendrer  et  (respectivement), alors elles peuvent engendrer conjointement  et  (// si on a une preuve de  et une preuve de  on a une preuve de   ) ; et on rejette la contraction d'une manière évidente en disant que si on peut engendrer  avec les ressources , , on ne peut pas forcément l'engendrer avec  (// on a pas forcément une preuve de  à partir d'une preuve de ).
Touchant donc la "sensibilité aux ressources", il faut cependant  être attentif au déplacement opéré par l'exploitation épistémique que nous en faisons : dans les exemples [Girard 1995] et les applications [Pfenning 2001], ce sont effectivement des ressources (ou des états physiques) qui sont représentés par les formules ; ainsi

H2  H2  O2  H2O  H2O 

mais, 

(H2  O2  H2O  H2O)

alors que nous, ce n'est pas tels ou tels états et transitions que nous voulons représenter mais les contraintes que nos limitations "computationnelles" peuvent faire peser sur une logique plus apte à modéliser nos compétences cognitives. Ici encore, comme dans le cas de la logique intuitionniste, il y a le soupçon que l'on "manque le point", et même que l'on se fourvoie complètement : la logique linéaire ne représente pas une mise en œuvre limitée de nos raisonnements déductifs mais une adaptation de la logique au raisonnement sur des objets différents (changeants, entretenant des relations causales, etc…) A bien y regarder, la situation est encore bien pire que dans le cas intuitionniste : notre objectif, c'est de trouver des contreparties aux phénomènes qui peuvent entraver la facilité des raisonnements ; une étape fondamentale dans la stratégie mise en place pour atteindre ce but, c'est la transition entre idées intuitives et contrepartie formelle. Or, dans le cas intuitionniste, l'interprétation BHK des constantes logiques nous fournissait cette transition ; l'aisance avec laquelle on a pu intégrer l'interprétation BHK est qu'elle est intrinsèquement épistémique. Ce n'est plus le cas avec l'interprétation GO, en termes de ressources, des constantes logiques. 
On peut, je crois, de manière convaincante, écarter cette difficulté : le problème de l'omniscience logique est dû au fait que l'opérateur de connaissance reflète les propriétés de la logique propositionnelle sous-jacente, quelle que soit la façon dont on l'interprète – ce n'est rien d'autre, encore une fois, que le phénomène de monotonie - ; du point de vue de la dichotomie introduite par l'interprétation de la logique linéaire entre les faits stables (pour lesquels les logiques classiques et intuitionnistes seraient adaptées) et les états transitoires (pour lesquels la logique linéaire serait mieux adaptée), la logique épistémique classique reflète une logique adaptée pour les faits stable ; mais cela ne veut pas dire qu'elle ne concerne que les vérités logico-mathématiques (au contraire, ce qu'elle modélise correctement, ce sont les informations empiriques des agents). De même, adopter un sous-bassement propositionnel linéaire ne signifie pas nécessairement que l'on ne représente que des relations épistémiques à des états transitoires ; dans notre cas, il s'agit simplement de tirer leçon du phénomène de monotonie et de constater qu'une logique des états transitoires est mieux adaptée pour représenter la réalité de la connaissance. Il s'agit donc d'une interprétation réflexive de la sensibilité aux ressources : les actions, ce sont nos justifications et les transitions, ce sont nos mises en œuvre des raisonnements logiques ; si l'on donne une certaine consistance philosophique à l'idée que logique classique = logique des objets éternels et logique linéaire = logique des états transitoires, alors cette interprétation réflexive signifie que l'on place la connaissance parmi les autres processus physiques. Ce dernier point est évidemment très spéculatif et on peut le mettre de côté : l'idée est simplement que l'on comble le fossé entre une interprétation épistémique des règles logiques (BHK) et une interprétation en termes de processus physiques (GO) en considérant les processus épistémiques comme des processus physiques parmi d'autres.
V.2.3	Idempotence et règle de contraction

Il y a un autre aspect qui est très séduisant dans la remise en question de la règle de contraction, c'est qu'elle permet une réponse partielle à une difficulté fondamentale qui touche notre façon d'aborder le problème. 
On pourrait en effet considérer que les règles, prises une à une, ne posent pas vraiment de problèmes, mais que c'est leur itération qui est problématique, et qui constitue la difficulté réelle des raisonnements. 
C'est certainement en partie vraie, et cela touche du doigt une limite essentielle de la méthode que nous avons adoptée : quand bien même nous serions-nous restreints au règles triviales, rien n'implique que l'itération du trivial soit elle-même triviale. En bref, la fondamentale idempotence de la relation de conséquence logique est une idéalisation dont il ne semble pas que l'on puisse se défaire par la méthode que nous avons adoptée. 
Mais précisément, l'élimination de la contraction corrige (un peu) cette idéalisation résiduelle puisque l'itération d'une même hypothèse dans un raisonnement n'est plus attribuée nécessairement. Bien que la (nouvelle) relation de conséquence logique soit toujours idempotente, le rôle déductif d'une prémisses ne l'est plus nécessairement. La seule itération qui nous échappe encore, c'est celle des règles qui gouvernent les connecteurs. 
Voici  le genre de raisons qui peut nous convaincre d'adopter une "resource sensitive logic" pour modéliser des "resource bounded agents". 

V.3	Perspectives formelles : directions générales

Techniquement, la mise en place d'un sous-bassement substructurel à la logique épistémique est beaucoup moins évident que dans le cas intuitionniste ; du point de vue syntaxique, la situation est certes comparables. Mais du point de vue sémantique, on ne peut plus simplement marier deux sémantiques a priori fortement homogènes ; par exemple, la sémantique de la prouvabilité "officielle" de la logique linéaire est la sémantique de phase [Girard 1987] qui est une sémantique algébrique. Néanmoins, il est possible, quoique moins usuel, d'une part de donner une sémantique algébrique pour la logique modale (les algèbres de Boole avec opérateurs, cf [BRV 2001], et d'autre part de donner une sémantique relationnelle pour les logiques substructurelles (dans la tradition des logiques de la pertinence, cf [Restall 2000]) 
Il existe donc des façons très différentes de mettre en place l'intégration des modalités aux logiques substructurelles. 
Une proposition qui reflète la démarche que nous avons suivie est celle de [Ono 1993] et [DGR 1996] qui consiste à généraliser la sémantique de Kripke pour la logique intuitionniste (en l'occurrence, combinée avec une relation d'accessibilité pour la modalité épistémique) en la contraignant algébriquement : l'espace des états possibles n'est plus simplement un ensemble (partiellement) ordonné, mais il a une structure algébrique forte qui reflète précisément celle des modèles algébriques usuels pour les logiques substructurelles. 

Question : que devient la signification intuitive de la sémantique ? 
Question : quel genre de phénomène précis cela pourrait nous aider à modéliser ? 
Question : des exemples concrets ? 
Question : est-ce que sa complexité ne la rend pas impraticable ? 

V.4	Perspectives formelles : l'exemple du système DGR (D'Agostino, Gabbay & Russo) de logique épistémique substructurelle

Pour terminer, je voudrais montrer que tout ceci n'est pas purement programmatique en donnant un exemple du genre de logique auquel on pourrait aboutir. Je vais me restreindre ici au fragment implicatif d'une logique modale substructurelle. 
V.4.1.1	Morphologie
Définition 1	l’alphabet d’un langage épistémique propositionnel LB(At) est la donnée 
(i)	d’un ensemble des formules atomiques : At = {p1, p2,…}
(ii)	d’un connecteur propositionnel 
(iii)	d’un opérateur épistémique B 

Définition 2	l’ensemble des formules d’un langage épistémique propositionnel LB(At), noté FORM(LB(At)), est l’ensemble tel que 
(i)	les éléments de At sont des formules de LB(At)
(ii)	si  et  sont des formules, alors est une formule
(iii)	si  est une formule alors B est une formule
(iv)	seules les expressions engendrées par un nombre fini d’applications de (i)-(iii) sont des formules 
V.4.1.2	Sémantique
L'originalité de la sémantique réside pour l'essentiel dans le fait qu'une contrainte algébrique forte pèse sur l'espaces des états possibles ; plus précisément, ces états possibles forment un quantale, les quantales étant aux logiques linéaires ce que les algèbres de Boole sont à la logique classique (Troelstra). 

Définition 1 un cadre informationnel est une structure <IS, , 1, > telle que 
(C1) <IS,  > est un treillis complet c'est-à-dire telle que pour tout X IS, sup(X) et inf(X) existent
(C2)  est une opération binaire sur IS qui est (i) associative et (ii) distributive sur sup ie pour tous X  IS et x IS,  sup (X  x) = sup(X)  x et sup (x  X) = x  sup (X) (iii) a 1 pour élément neutre

Les règles structurelles ont pour contrepartie sémantiques différentes conditions sur l'opération  relativement à . On a ainsi : 
Mélange 	
x  x  x	

Monotonie	
x  x  y	

Contraction	
x  x  x	

Commutativité	
x  y  y  x	

Définition 2 soit IS un cadre informationnel et FORM(L) l'ensemble des formules d'un langage L ; une valuation sur IS est une fonction V : FORM(L)  IS  {0, 1} telle que 
(C3) Condition d'hérédité : pour toute   FORM(L),  V (, x) = 1 implique que pour tout y tel que x  y, V(,y) = 1
(C4) Condition de continuité : pour tout   FORM(L) et X  IS, (i) V (, sup(X)) = sup  {V(,x) ; x  X} (ii) V (, inf (X)) = inf {V(, x) ; x  X}
Définition 3 un cadre informationnel modal est une paire < IS, B > où IS  est un cadre informationnel et
(C5) B est une relation sur IS telle que (1a) si X  IS, pour tout y  X, xBy implique x B sup(X) (1b) et x B inf (X) (2a) si x  y et xBz alors il existe z' tel que yBz' et z  z' (2b) si x  y et  yB z alors il existe z'  tel que x B z' et z'  z
Définition 4 une structure informationnelle modale est un triplet < IS, B, V > où <IS, B > est un cadre informationnel modal et V est une valuation telle que 
(1)	V(  , x) = 1 ssi pour tout y, si V(,y) = 1 alors V(, x  y) = 1
(2)	V (B, x) = 1 ssi pour tout y tel que xBy, V(, y) = 1
(3)	V (P, x) = 1 ssi il existe y tel que xBy et V(, y) = 1  

Sémantique pour (DGR)

Il faut commencer par l'essentiel ie l'assouplissement du sous-bassement propositionnel de la logique.  
Définition 3	un cadre informationnel est une structure <IS, , 1, > telle que 
(C1) <IS,  > est un treillis complet c'est-à-dire telle que pour tout X IS, sup(X) et inf(X) existent
(C2)  est une opération binaire sur IS qui est (i) associative et (ii) distributive sur sup ie pour tous X  IS et x IS,  sup (X  x) = sup(X)  x et sup (x  X) = x  sup (X) (iii) a 1 pour élément neutre
Les règles structurelles ont pour contrepartie sémantiques différentes conditions sur l'opération  relativement à . On a ainsi : 
Mélange 	x  x  x	
Monotonie	x  x  y	
Contraction	x  x  x	
Commutativité	x  y  y  x	

Commentaires : 
(1) la signification intuitive de cette sémantique qui est une simple généralisation de la sémantique opérationnelle de Urquhart pour la logique R est : les éléments de IS sont des token d'information, x  y si y contient au moins l'information contenue dans x, x  y est la combinaison de l'information contenue dans x et de celle contenue dans y  [Dunn 1983] 

(2) Si l'on suit cette interprétation, on retrouve des intuitions tout à fait compatibles avec la réflexion que l'on avait menée sur les règles déductives :  refuser la validité inconditionnelle de la règle de contraction correspond à l'acceptation que deux tokens d'une même information puisse représenter plus de ressource informationnelle qu'un seul token de cette même information. 
(3) 1 correspond à l'état d'information minimal : celui qui n'ajoute rien quelle que soit l'état informationnel avec lequel on le combine. 
Définition 4	soit IS un cadre informationnel et FORM(L) l'ensemble des formules d'un langage L ; une valuation sur IS est une fonction V : FORM(L)  IS  {0, 1} telle que 
(C3) Condition d'hérédité : pour toute   FORM(L),  V (, x) = 1 implique que pour tout y tel que x  y, V(,y) = 1
(C4) Condition de continuité : pour tout   FORM(L) et X  IS, (i) V (, sup(X)) = sup  {V(,x) ; x  X} (ii) V (, inf (X)) = inf {V(, x) ; x  X}
Définition 5	un cadre informationnel modal est une paire < IS, B > où IS  est un cadre informationnel et
(C5) B est une relation sur IS telle que (1a) si X  IS, pour tout y  X, xBy implique x B sup(X) (1b) et x B inf (X) (2a) si x  y et xBz alors il existe z' tel que yBz' et z  z' (2b) si x  y et  yB z alors il existe z'  tel que x B z' et z'  z
Définition 6	une structure informationnelle modale est un triplet < IS, B, V > où <IS, B > est un cadre informationnel modal et V est une valuation telle que 
(1)	V(  , x) = 1 ssi pour tout y, si V(,y) = 1 alors V(, x  y) = 1
(2)	V (B, x) = 1 ssi pour tout y tel que xBy, V(, y) = 1
(3)	V (P, x) = 1 ssi il existe y tel que xBy et V(, y) = 1  
Les conditions (1a) et (1b) ont chacune pour conséquence que les cadres informationnels modaux ont la propriété d'êtres sériels : pour chaque token d'information, il existe un token d'information accessible depuis lui. 
Les conditions (2a) et (2b) sont un import direct des recherches précédentes en logique modale intuitionniste où l'on s'est aperçu qu'il fallait imposer de telles conditions pour résoudre le problème principal à savoir la préservation de la propriété d'hérédité malgré l'implantation d'une relation d'accessibilité. Il est en effet aisé de voir que (2a) est une condition suffisante pour que si V(P, x) = 1 alors pour tout y t.q. x  y, V(P, y) = 1 ; et (2b) une condition suffisante pour que si V(B, x) = 1, alors pour tout y t.q. x  y, V(B, y) = 1. Notons que grâce à des conditions similaires, on peut rendre compatible avec  différentes sortes de relations d'accessibilités ([Restall 2000], pp.240 et sq.) 
V.4.1.3	Syntaxe

Définition 7	Soit un langage L ; un séquent    est une paire ordonnée formée de d'une suite finie de formules, l’antécédent  = <1,…,n> et d'une formule, , le cédent
Définition 8	Un séquent  est prouvable , noté -  , s’il est le nœud terminal d’un arbre dont les nœuds initiaux sont les règles-axiomes et dont tout passage d’un nœud de niveau n à un nœud de niveau n+1 se fait selon les règles d’inférence
Définition 9	Un séquent  avec  = <A1, …, An> est vérifié dans une SIMS ssi la formule A1  (A2…(An)…) est vérifiée dans SIMS 
Définition 10	calcul des séquents MSSeq pour la logique épistémique monotone et sérielle est le suivant :

Règles structurelles	
Permutation	 , ,   
, , ,   
	
Coupure	       ’,, ’ 
, ’, ’ 	
Identité	  	
Règles propositionnelles	
	,   
   	    
,   	
Règles modales	
Monotonie modale I	       
B  B	
Monotonie modale II	       
P  P	
Axiome D	B  P
	
Système de déduction pour (DGR)