Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses

Résumé Technique : Logique de Déviation Biprofile : Cadres de Remplacement de Rapports et Témoins d'Audit

Énoncé du Problème
L'article traite de la formalisation du choix social stratégique, en particulier la distinction entre un profil de préférences « vrai » ($R$) qui détermine les comparaisons de bien-être et un profil de rapports « soumis » ($P$) qui détermine le résultat d'une règle de choix social. Les approches traditionnelles de la logique modale traitent souvent la déviation comme une arête générique de graphe ou s'appuient sur la théorie générale de la correspondance (par exemple, les théorèmes de Sahlqvist) sans modéliser explicitement la structure algébrique des remplacements de rapports basés sur des coalitions. Les auteurs identifient un manque dans la fourniture d'une logique traitant l'état comme une paire $(R, P)$, où les modalités correspondent strictement au changement des coordonnées de rapport d'une coalition spécifique $C$ tout en laissant le profil vrai $R$ invariant. De plus, il existe un besoin d'une « couche d'audit » pour vérifier comment les propriétés stratégiques (comme l'immunité à la manipulation) se comportent lorsque le domaine des rapports admissibles est modifié (par exemple, restreint, étendu ou supprimé publiquement) sans devoir re-démontrer les théorèmes d'impossibilité classiques.

Méthodologie
Les auteurs développent la Logique de Déviation Biprofile, une logique multimodale où les états sont des paires $(R, P)$.

1. Sémantique : La logique utilise une classe de cadres $\text{Dev}(N)$ définie par un ensemble d'agents $N$. Les relations d'accessibilité $E_C$ pour une coalition $C$ représentent le remplacement des coordonnées de rapport pour les agents de $C$. La contrainte sémantique centrale est la loi exacte de composition par union : $E_C \circ E_D = E_{C \cup D}$. Cela capture l'intuition que les changements de rapports indépendants par des coalitions disjointes se composent en un changement par leur union.
2. Théorie de la Preuve : Un système de Hilbert $H_{bp}$ est défini avec des axiomes pour un comportement S5 (réflexivité, transitivité, propriété euclidienne) pour chaque coalition, un axiome d'identité pour la coalition vide, des axiomes d'inclusion pour les sous-ensembles de coalitions, et un axiome de réduction pour l'union des coalitions.
3. Preuve de Complétude : L'article fournit une preuve directe de complétude canonique pour $H_{bp}$. Une étape technique clé consiste à construire un « point milieu » dans le modèle canonique pour prouver l'inclusion inverse de l'axiome de composition ($R_{C \cup D} \subseteq R_C \circ R_D$), garantissant ainsi que le cadre canonique satisfait la loi exacte de composition par union sans présupposer une structure de produit.
4. Séparation de la Représentation : Les auteurs distinguent entre les cadres abstraits satisfaisant les équations $\text{Dev}(N)$ et les produits concrets de coordonnées de rapport. Ils prouvent qu'une condition supplémentaire de séparation des coordonnées est nécessaire pour retrouver une structure de produit véritable à partir de l'algèbre abstraite.
5. Cadre d'Audit : L'article traduit les concepts classiques du choix social (immunité à la manipulation, théorème de Gibbard–Satterthwaite, préférence unimodale) en formules modales. Il introduit ensuite des « théorèmes d'audit » qui diagnostiquent comment ces propriétés changent lorsque la représentation du domaine change (par exemple, extensions hors domaine ou suppressions publiques).

Contributions Clés

• Cœur Modale (Théorème 1) : L'article prouve la correction et la complétude de $H_{bp}$ pour la classe de cadres abstraits $\text{Dev}(N)$. Il isole et prouve explicitement l'étape du « point milieu » requise pour l'axiome de composition inverse, qui est la partie non routinière de la construction canonique pour ce tableau de demi-réseau spécifique.
• Frontière de Représentation (Proposition 1) : Les auteurs démontrent que satisfaire les équations abstraites $\text{Dev}(N)$ est insuffisant pour garantir une structure de produit de coordonnées. Ils identifient la séparation des coordonnées comme la condition nécessaire et suffisante pour retrouver un produit concret de coordonnées de rapport à partir d'un cadre de déviation abstrait.
• Théorèmes d'Audit :
  • Théorème 4 (Critère de Ligne Frontière) : Établit que l'extension d'une règle à un plus grand domaine de rapports crée de nouveaux témoins de manipulation uniquement à la « frontière » (c'est-à-dire en utilisant des rapports qui étaient précédemment inadmissibles). Cela permet une vérification incrémentielle de l'immunité à la manipulation sans re-vérifier l'ensemble du domaine.
  • Proposition 6 (Critère de Clôture par Facteur) : Fournit une condition nécessaire et suffisante pour qu'une suppression publique (sous-modèle) préserve la structure algébrique $\text{Dev}(N)$. La condition exige que les états survivants soient « clos par facteur », ce qui signifie que toute arête survivante $E_{C \cup D}$ doit être factorisable à travers un état intermédiaire survivant.
• Mécanismes d'Audit Finis : L'article introduit un format de certificat typé et des vérificateurs exécutables (en Python, Lean et Alloy) pour vérifier des instances finies de ces propriétés logiques. Cela inclut un mécanisme de « rejeu de témoin » qui classe les échecs comme arêtes supprimées, témoins de ligne frontière, ou mises à jour non sécurisées, en fonction du champ du dossier du témoin qui a changé.

Résultats

• Complétude : Le système $H_{bp}$ est prouvé complet pour $\text{Dev}(N)$. La preuve repose sur une construction de modèle canonique qui réalise explicitement la loi de composition par union.
• Traduction des Théorèmes Classiques : Le théorème de Gibbard–Satterthwaite et le théorème du médian de Moulin sont traduits avec succès dans le langage biprofile. L'article ne re-démontre pas ces théorèmes mais utilise le nouveau langage pour analyser leur comportement sous des changements de domaine.
• Étude de Cas : Un exemple de médiane unimodale à cinq agents est utilisé pour démontrer la couche d'audit. L'étude montre comment un seul tuple de témoin de manipulation $(R, P, C, Q, x, y)$ est interprété différemment dans trois scénarios :
  1. Domaine Restreint : Le témoin est « arête-supprimée » car le rapport dévié $Q$ n'est pas généré par le générateur du domaine restreint.
  2. Extension Hors Domaine : Le témoin est un échec de « ligne frontière », créé uniquement par le nouveau rapport admissible $Q$.
  3. Suppression Publique : Le témoin peut survivre (les extrémités restent), mais la mise à jour est « non sécurisée » car la suppression d'un point milieu mixte brise la clôture par facteur requise pour l'algèbre $\text{Dev}(N)$.
• Complexité de Vérification : La Proposition 7 établit que la vérification d'un certificat fini typé soumis est polynomiale par rapport à la taille du certificat pour un ensemble fixe d'agents $N$.

Signification et Revendications
L'article revendique sa signification principalement comme un cadre formel d'audit plutôt que comme un nouveau théorème d'impossibilité.

• Séparation des Préoccupations : Il sépare l'épine dorsale de la théorie de la preuve (complétude de l'algèbre abstraite) de la frontière de représentation (récupération des coordonnées) et de la couche d'application (audit des changements de domaine).
• Valeur Opérationnelle : Les auteurs soutiennent que leur « couche d'audit » fournit une interface de diagnostic pour les mécanismes de choix social. Au lieu de relancer des preuves d'impossibilité complexes lorsqu'un domaine est modifié, les vérificateurs peuvent utiliser le théorème de la ligne frontière pour vérifier uniquement les nouvelles lignes et le critère de clôture par facteur pour vérifier si une suppression préserve la structure algébrique nécessaire.
• Modestie : Les auteurs déclarent explicitement qu'ils ne fournissent pas d'algorithme général de satisfaisabilité pour $\text{Dev}(N)$ ni de nouvelle borne de complexité pour les règles représentées succinctement. Le résultat de complétude concerne la classe de cadres abstraits, et les vérifications finies s'appliquent aux certificats fournis explicitement. Le travail est présenté comme un « scénario d'audit petit mais complet » qui clarifie où et pourquoi un changement de représentation affecte les propriétés stratégiques, plutôt que d'offrir une nouvelle solution aux problèmes fondamentaux du choix social.