💻 computer science

The Dynamic Turn in Paraconsistency

Cet article introduit un cadre dynamique pour la paraconsistance en définissant des logiques d'action et d'annonce publique (AMLFI1 et PALFI1) qui étendent les systèmes épistémiques paraconsistants existants, permettant la formalisation de l'obtention et de la résolution de contradictions provisoires tout en prouvant leur correction et leur complétude.

Auteurs originaux : Rafael Ongaratto, Hans van Ditmarsch

Publié 2026-07-23

📖 8 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Rafael Ongaratto, Hans van Ditmarsch

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous soyez un détective tentant de résoudre un mystère, mais que votre carnet de notes soit un peu défectueux. Parfois, deux témoins différents racontent des choses opposées sur un même indice. Dans la vieille logique, si vous entendiez « Le suspect est au parc » et « Le suspect n'est PAS au parc », votre carnet entier exploserait. Le système planterait, et vous seriez contraint de conclure que tout est vrai et que rien n'est vrai, rendant votre enquête inutile. C'est ce qu'on appelle le « principe d'explosion ». Mais la vraie vie n'est pas comme ça. Nous traitons des contradictions tout le temps sans perdre la tête. Nous disons simplement : « D'accord, il y a un conflit ici, cherchons à savoir qui ment ou qui a fait une erreur. »

C'est là que la paraconsistance entre en jeu. C'est une branche de la logique conçue pour gérer ces situations contradictoires et désordonnées sans faire planter le système. Elle permet de porter deux idées opposées en tête simultanément, en les traitant comme un bug temporaire plutôt que comme un désastre total. La logique dynamique, quant à elle, est comme si l'on ajoutait un bouton « retour en arrière » et « avance rapide » à votre histoire de détective. Elle ne se contente pas de regarder une image statique du monde ; elle suit l'évolution de vos croyances lorsque vous recevez de nouvelles informations, comme lorsqu'un témoin change de version ou que vous trouvez un nouvel indice.

La grande question que cet article aborde est la suivante : que se passe-t-il lorsque l'on combine ces deux approches ? Comment construire un système logique capable non seulement de gérer les contradictions, mais aussi de montrer comment ces contradictions apparaissent, évoluent et finissent par être résolues à mesure que l'on apprend de nouvelles choses ? Les auteurs, Rafael Ongaratto et Hans van Ditmarsch, soutiennent que nous avons besoin d'un « tournant dynamique » dans la paraconsistance. Ils veulent passer de l'observation d'une image contradictoire figée à la création d'un film où l'on peut voir la contradiction naître, puis se résoudre.

L'idée centrale de l'article : L'histoire de détective « à l'épreuve des bugs »

Dans cet article, les auteurs introduisent un nouvel ensemble d'outils logiques appelés AMLFI1 et UMLFI1. Considérez cela comme un système d'exploitation super-puissant et résistant aux bugs pour une équipe de détectives (ou d'agents) qui tentent de résoudre une affaire ensemble.

La configuration : La base de données défectueuse

Imaginez une base de données numérique partagée où différents agents (appelons-les Anne, Bill et Cath) échangent des informations. Dans le monde réel, les bases de données deviennent parfois désordonnées. Peut-être qu'Anne pense qu'un fichier est « Bleu », mais que Bill pense qu'il est « Rouge ». Dans un système logique normal et strict, ce conflit briserait toute la base de données. Mais dans le monde de la LFI1 (la logique de base sur laquelle les auteurs s'appuient), la base de données peut gérer cela. Elle possède un commutateur d'incohérence spécial (un symbole comme •) qui dit : « Hé, cette donnée est contradictoire, mais ne paniquez pas. Nous pouvons encore travailler avec elle. »

Les auteurs prennent cette idée statique et y ajoutent des Modèles d'Action. Imaginez que ce soient de petites « cartes d'événements » que les agents jouent. Lorsqu'un agent joue une carte, cela met à jour la base de données.

AMLFI1 est la première version de ce système. Elle permet aux agents de jouer des cartes qui changent ce qu'ils savent. Par exemple, si Cath dit : « J'ai la carte des Trèfles », le système met à jour la connaissance d'Anne. Même si Cath ment et possède en réalité la carte des Piques, le système ne plante pas. Il enregistre simplement qu'Anne croit maintenant à « Trèfle » alors que la réalité pourrait être « Pique », créant ainsi une contradiction temporaire et gérable.
UMLFI1 est la version améliorée. Elle ajoute le Changement Factuel. C'est la « baguette magique » qui ne se contente pas de changer ce que les gens pensent, mais change les faits eux-mêmes. Si Cath mentait et qu'elle est ensuite démasquée, elle peut montrer sa carte. Le système ne met pas seulement à jour la croyance d'Anne ; il réécrit réellement l'entrée de la base de données pour correspondre à la vérité. La contradiction est résolue, et le système revient à la normale.

Le problème du « menteur » et l'agent « byzantin »

L'article utilise un jeu appelé Coup pour expliquer pourquoi cela est intéressant. Dans Coup, les joueurs détiennent des cartes et peuvent mentir sur ce qu'ils possèdent pour gagner. Si vous mentez, vous créez une contradiction entre ce que vous dites et ce que vous détenez.

Ancienne Logique : Si vous essayez de modéliser un menteur, le système casse généralement parce qu'il ne peut pas gérer le mensonge sans supposer que le menteur est « fou » (connaissant tout et rien à la fois).
La Logique de cet Article : Les auteurs montrent que l'on peut modéliser un menteur parfaitement. Le système peut dire : « Cath prétend avoir le Trèfle, mais elle a en fait le Pique. » Il conserve ces deux informations dans un « état contradictoire » (marqué comme 1/2 ou « peut-être/les deux ») sans exploser.
Le Twist : L'article distingue un Menteur (quelqu'un qui connaît la vérité mais dit le contraire) d'un Agent Byzantin (quelqu'un qui est simplement cassé, confus ou défaillant). Dans leur système, un agent défectueux pourrait sincèrement croire qu'il possède les deux cartes à la fois. La logique gère ce « dysfonctionnement » avec élégance, en laissant le reste du système fonctionner pendant que l'agent défectueux est réparé ou ignoré.

Le mécanisme de « Résolution »

La partie la plus excitante de l'article est la façon dont ils montrent les contradictions se faisant réparer.

Le Conflit : Anne entend Cath dire « J'ai le Trèfle », puis Cath dit « J'ai le Pique ». Anne est maintenant confuse. Sa base de données contient une contradiction.
La Réparation : Cath est mise au défi de montrer sa carte. Elle révèle qu'elle a le Pique.
La Mise à jour : Dans le système UMLFI1, il ne s'agit pas seulement d'Anne qui change d'avis. Le système effectue un « changement factuel ». Il met à jour la réalité de la carte. La contradiction disparaît car le fait « Pique » écrase le mensonge « Trèfle ». Le système prouve mathématiquement que ce processus est sain (il ne mène jamais à l'absurde) et complet (il peut prouver tout ce qui est vrai dans ce système).

Ce qu'ils ont prouvé

Les auteurs n'ont pas seulement supposé que cela fonctionnerait ; ils ont construit une preuve mathématique rigoureuse.

Ils ont montré que leurs nouvelles logiques (AMLFI1 et UMLFI1) sont saines : si vous suivez les règles, vous ne finirez pas avec une conclusion erronée.
Ils ont montré qu'elles sont complètes : si quelque chose est vrai dans le système, vous pouvez le prouver en utilisant leurs règles.
Ils ont montré qu'elles sont décidables : il existe une recette étape par étape (un algorithme) qui peut vous dire, en un temps fini, si une proposition spécifique est vraie ou fausse dans ce système.
Ils ont également montré que leur version de la « Logique d'Annonce Publique » (un type spécifique de mise à jour où tout le monde entend la même chose) est mathématiquement équivalente à une autre version récente, simplement écrite avec des règles légèrement différentes.

Ce qu'ils ne prétendent pas

Il est important de noter ce que cet article ne fait pas. Ils ne prétendent pas avoir résolu le problème du mensonge dans toutes les interactions humaines, ni prétendent avoir construit une IA fonctionnelle capable de mentir et de s'en remettre. Ils n'ont pas testé cela sur une base de données réelle ou un jeu de Coup en direct. Ils ont construit le plan et le moteur mathématique qui disent : « Oui, c'est une manière valide de penser aux contradictions et aux mises à jour. » Ils laissent le travail lourd consistant à appliquer cela à des systèmes distribués complexes (comme de massives bases de données internet) à la charge de futurs chercheurs.

La conclusion à retenir

En termes simples, cet article nous donne une nouvelle façon d'écrire les règles d'un monde où les choses tournent mal. Il montre que nous n'avons pas à choisir entre un monde parfaitement cohérent (et donc fragile) et un monde chaotique. Nous pouvons avoir un monde qui accepte les contradictions comme des bugs temporaires, suit leur apparition et offre une voie logique pour les résoudre. C'est comme donner à un détective un carnet qui ne se déchire pas lorsqu'on écrit deux choses différentes sur la même page, mais qui souligne plutôt le conflit et attend le prochain indice pour le résoudre.

Résumé Technique : Le Tournant Dynamique de la Paraconsistance

Énoncé du Problème
L'article traite d'une limitation fondamentale de l'état actuel de la logique paraconsistante : sa nature statique. Bien que les logiques paraconsistantes (telles que LFI1) modélisent avec succès des états inconsistants mais non triviaux, elles n'offrent généralement qu'une « image statique » de la contradiction. Dans l'approche épistémique de la paraconsistance, les contradictions sont souvent considérées comme « provisoires » — émergeant de limitations cognitives, d'erreurs de mesure ou d'étapes dans le développement d'une théorie — et sont censées être résolues au fil du temps. Cependant, les logiques paraconsistantes standards ne peuvent pas représenter le processus de changement de modèle (mise à jour de l'information) au sein même du langage logique. Au lieu de cela, ces mises à jour doivent être décrites dans le métalangage (par exemple, « à l'instant $t_1$ le modèle est $M_1$ , et après l'action $k$ , il devient $M_2$ »). Les auteurs soutiennent qu'un « tournant dynamique » est nécessaire pour formaliser l'obtention et la résolution des contradictions provisoires, de manière similaire au « tournant dynamique » réalisé dans la logique épistémique classique via la Logique Épistémique Dynamique (DEL).

Méthodologie
Les auteurs étendent la logique paraconsistante à trois valeurs LFI1 (Logique de l'Inconsistance Formelle) avec des modalités dynamiques dérivées de l'école hollandaise des logiques dynamiques. La méthodologie implique :

Fondation Logique : Utilisation de LFI1, qui étend la Logique du Paradoxe (LP) avec un opérateur de consistance ( $\circ$ ) et un opérateur d'inconsistance ( $\bullet$ ). LFI1 est une logique à trois valeurs (valeurs : 1, 1/2, 0) où 1 et 1/2 sont des valeurs désignées. Crucialement, LFI1 possède une « équivalence forte » ( $\equiv$ ) qui fonctionne comme une relation de congruence, une propriété absente d'autres logiques à plusieurs valeurs comme LP ou K3.
Extension Dynamique (AMLFI1) : Les auteurs introduisent AMLFI1 (Action Model LFI1), une logique épistémique dynamique étendant S5LFI1. Elle incorpore des modèles d'action où les actions ont des préconditions mais pas de postconditions (changements factuels). La sémantique est définie via un produit modal restreint de modèles de Kripke et de modèles d'action.
Extension de Changement Factuel (UMLFI1) : Les auteurs introduisent ensuite UMLFI1 (Update Model LFI1), qui étend AMLFI1 en permettant aux actions d'avoir des postconditions. Cela permet le « changement ontique » (changer la valeur de vérité des faits atomiques), ce qui est essentiel pour modéliser la résolution des contradictions.
Axiomatisation et Réduction : L'approche technique centrale implique la définition d'axiomes de réduction. Contrairement aux DEL standards où les axiomes de réduction sont souvent des équivalences, les auteurs utilisent des équivalences fortes (basées sur la congruence de $\equiv$ ) pour réduire les formules contenant des modalités dynamiques en formules du langage épistémique statique (LK). Cette stratégie de réduction est utilisée pour prouver la complétude.
Analyse Comparative : L'article compare la PALFI1 (Public Announcement LFI1) proposée (un cas particulier de AMLFI1) à une axiomatisation alternative récemment publiée, PALFI1C.

Contributions Clés

Formalisation de la Paraconsistance Dynamique : L'article propose AMLFI1 et UMLFI1, les premières logiques épistémiques dynamiques spécifiquement conçues pour la logique paraconsistante à trois valeurs LFI1.
Gestion des Contradictions Provisoires : En intégrant des modèles d'action avec préconditions et postconditions, le cadre permet la représentation formelle d'agents recevant des informations conflictuelles (entrant dans un état d'inconsistance) et les résolvant par la suite (retour à la consistance) par des changements factuels.
Équivalence des Axiomatisations : Les auteurs démontrent que leur logique d'annonce publique (PALFI1), qui utilise une règle de remplacement des équivalents (RE) et manque d'un axiome de composition, est logiquement équivalente à la récemment publiée PALFI1C, qui utilise un axiome de composition mais manque de RE. Ils prouvent l'admissibilité de RE dans PALFI1C et de l'axiome de composition dans PALFI1.
Nouveauté Technique de la Réduction : Les axiomes de réduction sont formulés comme des équivalences fortes plutôt que de simples équivalences. C'est une adaptation nécessaire pour le cadre à trois valeurs de LFI1, où l'équivalence standard n'induit pas une congruence.

Résultats
L'article établit les propriétés métathéoriques suivantes pour les logiques introduites (AMLFI1, PALF1 et UMLFI1) :

Correction (Soundness) : Les axiomes et les règles sont corrects par rapport à la sémantique de Kripke définie.
Complétude Forte : Les logiques sont fortement complètes par rapport à leurs sémantiques. Ceci est prouvé via la stratégie de réduction, montrant que toute formule dans le langage dynamique est prouvablement équivalente à une formule dans le langage statique, lequel est déjà connu pour être complet.
Compacité : Les logiques satisfont la propriété de compacité.
Décidabilité : Les logiques sont décidables, suivant de la décidabilité de la logique statique sous-jacente (S5LFI1) et de la nature terminante de la procédure de réduction.
Relations de Sous-systèmes : Les logiques dynamiques étendent proprement les logiques paraconsistantes épistémiques statiques KLFI1, KB4LFI1 et S5LFI1.

Signification et Revendications
Les auteurs affirment que leur travail fournit un « tournant dynamique » pour la paraconsistance, passant de modèles statiques de la contradiction à un cadre où les contradictions sont traitées comme des états transitoires qui peuvent être mis à jour et résolus.

Application au Mensonge et au Comportement Byzantin : L'article applique ces logiques à l'analyse du mensonge, des erreurs et des comportements « byzantins » (par exemple, dans le contexte du jeu Coup). Il soutient que la paraconsistance dynamique offre une vision plus nuancée que la logique épistémique dynamique classique, où le mensonge mène souvent à l'« explosion » ou à la trivialité. Dans le cadre proposé, les agents peuvent détenir des informations contradictoires sans devenir « fous » (triviaux), et les changements factuels (postconditions) permettent de se rétablir de ces inconsistances.
Systèmes Distribués : Les auteurs suggèrent que ces résultats sont transférables à la gestion de bases de données distribuées, particulièrement pour gérer les inconsistances locales où différents agents peuvent détenir des vues conflictuelles qui sont ultérieurement résolues.
Modestie : L'article cadre modestement sa contribution comme une étape fondamentale. Il reconnaît que modéliser pleinement la distinction entre le mensonge (intentionnel) et l'erreur (non intentionnelle) ou gérer la révision complexe des croyances (ajout de flèches d'accessibilité) nécessite des recherches supplémentaires et des encodages plus complexes, qui sont laissés pour des travaux futurs. Les auteurs soulignent que la beauté de leur approche réside dans la fourniture d'encodages « économiques » pour les inconsistances locales par rapport aux cadres de révision des croyances plus complexes.