Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses

Resumen Técnico: Lógica de Desviación de Biperfiles: Marcos de Reemplazo de Informes y Testigos de Auditoría

Enunciado del Problema
El artículo aborda la formalización de la elección social estratégica, específicamente la distinción entre un perfil de preferencias "verdadero" ($R$) que determina las comparaciones de bienestar y un perfil de informe "presentado" ($P$) que determina el resultado de una regla de elección social. Los enfoques tradicionales de lógica modal a menudo tratan la desviación como una arista genérica de grafo o se basan en la teoría general de correspondencia (por ejemplo, teoremas de Sahlqvist) sin modelar explícitamente la estructura algebraica de los reemplazos de informes basados en coaliciones. Los autores identifican una brecha en la provisión de una lógica que trate al estado como un par $(R, P)$, donde las modalidades corresponden estrictamente al cambio de las coordenadas de informe de una coalición específica $C$ mientras se deja invariante el perfil verdadero $R$. Además, existe la necesidad de una "capa de auditoría" para verificar cómo se comportan las propiedades estratégicas (como la inmunidad a la manipulación) cuando se altera el dominio de informes admisibles (por ejemplo, restringido, extendido o eliminado públicamente) sin volver a demostrar los teoremas de imposibilidad clásicos.

Metodología
Los autores desarrollan la Lógica de Desviación de Biperfiles, una lógica multimodal donde los estados son pares $(R, P)$.

1. Semántica: La lógica utiliza una clase de marcos $\text{Dev}(N)$ definida por un conjunto de agentes $N$. Las relaciones de accesibilidad $E_C$ para una coalición $C$ representan el reemplazo de las coordenadas de informe para los agentes en $C$. La restricción semántica central es la ley exacta de composición de uniones: $E_C \circ E_D = E_{C \cup D}$. Esto captura la intuición de que los cambios de informes independientes realizados por coaliciones disjuntas se componen en un cambio realizado por su unión.
2. Teoría de la Demostración: Se define un sistema de Hilbert $H_{bp}$ con axiomas para el comportamiento S5 (reflexividad, transitividad, propiedad euclidiana) para cada coalición, un axioma de identidad para la coalición vacía, axiomas de inclusión para subconjuntos de coaliciones y un axioma de reducción para la unión de coaliciones.
3. Demostración de Completitud: El artículo proporciona una demostración directa de completitud canónica para $H_{bp}$. Un paso técnico clave implica la construcción de un "punto medio" en el modelo canónico para probar la inclusión inversa del axioma de composición ($R_{C \cup D} \subseteq R_C \circ R_D$), asegurando que el marco canónico satisfaga la ley exacta de composición de uniones sin presuponer una estructura de producto.
4. Separación de Representación: Los autores distinguen entre marcos abstractos que satisfacen las ecuaciones $\text{Dev}(N)$ y productos concretos de coordenadas de informe. Demuestran que se requiere una condición adicional de separación de coordenadas para recuperar una estructura de producto genuina a partir del álgebra abstracta.
5. Marco de Auditoría: El artículo traduce conceptos clásicos de elección social (inmunidad a la manipulación, teorema de Gibbard–Satterthwaite, preferencias de pico único) a fórmulas modales. Luego introduce "teoremas de auditoría" que diagnostican cómo cambian estas propiedades cuando cambia la representación del dominio (por ejemplo, extensiones fuera del dominio o eliminaciones públicas).

Contribuciones Clave

• Núcleo Modal (Teorema 1): El artículo demuestra la solidez y completitud de $H_{bp}$ para la clase de marcos abstractos $\text{Dev}(N)$. Aísla y demuestra explícitamente el paso del "punto medio" requerido para el axioma de composición inversa, que es la parte no rutinaria de la construcción canónica para esta tabla semilatice específica.
• Límite de Representación (Proposición 1): Los autores demuestran que satisfacer las ecuaciones abstractas $\text{Dev}(N)$ es insuficiente para garantizar una estructura de producto de coordenadas. Identifican la separación de coordenadas como la condición necesaria y suficiente para recuperar un producto concreto de coordenadas de informe a partir de un marco de desviación abstracto.
• Teoremas de Auditoría:
  • Teorema 4 (Criterio de Fila Límite): Establece que extender una regla a un dominio de informes más grande crea nuevos testigos de manipulación solo en la "frontera" (es decir, utilizando informes que previamente eran inadmisibles). Esto permite una verificación incremental de la inmunidad a la manipulación sin volver a verificar todo el dominio.
  • Proposición 6 (Criterio de Cierre de Factores): Proporciona una condición necesaria y suficiente para que una eliminación pública (submodelo) preserve la estructura algebraica $\text{Dev}(N)$. La condición requiere que los estados supervivientes sean "cerrados por factores", lo que significa que cualquier arista superviviente $E_{C \cup D}$ debe ser factorizable a través de un estado intermedio superviviente.
• Mecanismos de Auditoría Finita: El artículo introduce un formato de certificado tipado y verificadores ejecutables (en Python, Lean y Alloy) para verificar instancias finitas de estas propiedades lógicas. Esto incluye un mecanismo de "reproducción de testigos" que clasifica los fallos como aristas eliminadas, testigos de fila límite o actualizaciones inseguras, basándose en qué campo del registro del testigo cambió.

Resultados

• Completitud: El sistema $H_{bp}$ se demuestra completo para $\text{Dev}(N)$. La demostración se basa en una construcción de modelo canónico que realiza explícitamente la ley de composición de uniones.
• Traducción de Teoremas Clásicos: El teorema de Gibbard–Satterthwaite y el teorema del votante mediano de Moulin se traducen exitosamente al lenguaje de biperfiles. El artículo no vuelve a demostrar estos teoremas, sino que utiliza el nuevo lenguaje para analizar su comportamiento bajo cambios de dominio.
• Estudio de Caso: Se utiliza un ejemplo de mediana de pico único con cinco agentes para demostrar la capa de auditoría. El estudio muestra cómo una tupla de testigo de manipulación única $(R, P, C, Q, x, y)$ se interpreta de manera diferente bajo tres escenarios:
  1. Dominio Restringido: El testigo es "borde eliminado" porque el informe desviado $Q$ no es generado por el generador del dominio restringido.
  2. Extensión Fuera del Dominio: El testigo es un fallo de "fila límite", creado únicamente por el nuevo informe admisible $Q$.
  3. Eliminación Pública: El testigo puede sobrevivir (los extremos permanecen), pero la actualización es "insegura" porque la eliminación de un punto medio mixto rompe el cierre de factores requerido para el álgebra $\text{Dev}(N)$.
• Complejidad de Verificación: La Proposición 7 establece que verificar un certificado tipado finito presentado es polinomial en el tamaño del certificado para un conjunto fijo de agentes $N$.

Significado y Afirmaciones
El artículo afirma su importancia principalmente como un marco formal de auditoría en lugar de un nuevo teorema de imposibilidad.

• Separación de Preocupaciones: Separa la columna vertebral de la teoría de la demostración (completitud del álgebra abstracta) del límite de representación (recuperación de coordenadas) y de la capa de aplicación (auditoría de cambios de dominio).
• Valor Operativo: Los autores argumentan que su "capa de auditoría" proporciona una interfaz de diagnóstico para mecanismos de elección social. En lugar de volver a ejecutar demostraciones complejas de imposibilidad cuando se modifica un dominio, los verificadores pueden utilizar el teorema de la fila límite para verificar solo las nuevas filas y el criterio de cierre de factores para verificar si una eliminación preserva la estructura algebraica necesaria.
• Modestia: Los autores declaran explícitamente que no proporcionan un algoritmo general de satisfacibilidad para $\text{Dev}(N)$ ni un nuevo límite de complejidad para reglas representadas de forma concisa. El resultado de completitud es para la clase de marcos abstractos, y las verificaciones finitas son para certificados suministrados explícitamente. El trabajo se presenta como un "escenario de auditoría pequeño pero completo" que aclara dónde y por qué un cambio de representación afecta las propiedades estratégicas, en lugar de ofrecer una nueva solución a los problemas fundamentales de la elección social.