Biprofile Deviation Logic: Report-Replacement Frames and Audit Witnesses

Resumo Técnico: Lógica de Desvio Biperfil: Quadros de Substituição de Relatórios e Testemunhas de Auditoria

Declaração do Problema
O artigo aborda a formalização da escolha social estratégica, especificamente a distinção entre um perfil de preferência "verdadeiro" ($R$) que determina comparações de bem-estar e um perfil de relatório "apresentado" ($P$) que determina o resultado de uma regra de escolha social. Abordagens tradicionais de lógica modal frequentemente tratam o desvio como uma aresta genérica de grafo ou recorrem à teoria geral de correspondência (por exemplo, teoremas de Sahlqvist) sem modelar explicitamente a estrutura algébrica das substituições de relatórios baseadas em coalizões. Os autores identificam uma lacuna na provisão de uma lógica que trate o estado como um par $(R, P)$, onde as modalidades correspondem estritamente à mudança das coordenadas de relatório de uma coalizão específica $C$ enquanto deixam o perfil verdadeiro $R$ invariante. Além disso, há uma necessidade de uma "camada de auditoria" para verificar como as propriedades estratégicas (como a prova de estratégia) se comportam quando o domínio dos relatórios admissíveis é alterado (por exemplo, restrito, estendido ou publicamente excluído) sem reprovvar teoremas clássicos de impossibilidade.

Metodologia
Os autores desenvolvem a Lógica de Desvio Biperfil, uma lógica multimodal onde os estados são pares $(R, P)$.

1. Semântica: A lógica utiliza uma classe de quadros $\text{Dev}(N)$ definida por um conjunto de agentes $N$. As relações de acessibilidade $E_C$ para uma coalizão $C$ representam a substituição das coordenadas de relatório para os agentes em $C$. A restrição semântica central é a lei exata de composição de união: $E_C \circ E_D = E_{C \cup D}$. Isso captura a intuição de que mudanças independentes de relatório por coalizões disjuntas compõem-se em uma mudança por sua união.
2. Teoria da Prova: Um sistema de Hilbert $H_{bp}$ é definido com axiomas para comportamento S5 (reflexividade, transitividade, propriedade euclidiana) para cada coalizão, um axioma de identidade para a coalizão vazia, axiomas de inclusão para subconjuntos de coalizões e um axioma de redução para a união de coalizões.
3. Prova de Completude: O artigo fornece uma prova direta de completude canônica para $H_{bp}$. Um passo técnico chave envolve a construção de um "ponto médio" no modelo canônico para provar a inclusão reversa do axioma de composição ($R_{C \cup D} \subseteq R_C \circ R_D$), garantindo que o quadro canônico satisfaça a lei exata de composição de união sem pressupor uma estrutura de produto.
4. Separação de Representação: Os autores distinguem entre quadros abstratos que satisfazem as equações $\text{Dev}(N)$ e produtos concretos de coordenadas de relatório. Eles provam que uma condição adicional de separação de coordenadas é necessária para recuperar uma estrutura de produto genuína a partir da álgebra abstrata.
5. Estrutura de Auditoria: O artigo traduz conceitos clássicos de escolha social (prova de estratégia, Gibbard–Satterthwaite, preferência de pico único) em fórmulas modais. Em seguida, introduz "teoremas de auditoria" que diagnosticam como essas propriedades mudam quando a representação do domínio muda (por exemplo, extensões fora do domínio ou exclusões públicas).

Principais Contribuições

• Núcleo Modal (Teorema 1): O artigo prova a correção e completude de $H_{bp}$ para a classe de quadros abstratos $\text{Dev}(N)$. Isola e prova explicitamente o passo do "ponto médio" necessário para o axioma de composição reversa, que é a parte não rotineira da construção canônica para esta tabela específica de semilattice.
• Limite de Representação (Proposição 1): Os autores demonstram que satisfazer as equações abstratas $\text{Dev}(N)$ é insuficiente para garantir uma estrutura de produto de coordenadas. Eles identificam a separação de coordenadas como a condição necessária e suficiente para recuperar um produto concreto de coordenadas de relatório a partir de um quadro de desvio abstrato.
• Teoremas de Auditoria:
  • Teorema 4 (Critério de Linha de Fronteira): Estabelece que estender uma regra para um domínio de relatório maior cria novas testemunhas de manipulação apenas na "fronteira" (ou seja, usando relatórios que eram anteriormente inadmissíveis). Isso permite a verificação incremental da prova de estratégia sem reexaminar todo o domínio.
  • Proposição 6 (Critério de Fechamento de Fator): Fornece uma condição necessária e suficiente para que uma exclusão pública (submodelo) preserve a estrutura algébrica $\text{Dev}(N)$. A condição exige que os estados sobreviventes devem ser "fechados por fator", significando que qualquer aresta sobrevivente $E_{C \cup D}$ deve ser fatorável através de um estado intermediário sobrevivente.
• Mecanismos de Auditoria Finita: O artigo introduz um formato de certificado tipado e verificadores executáveis (em Python, Lean e Alloy) para verificar instâncias finitas dessas propriedades lógicas. Isso inclui um mecanismo de "reprodução de testemunha" que classifica falhas como aresta-excluída, testemunhas de fronteira ou atualizações inseguras com base em qual campo do registro da testemunha mudou.

Resultados

• Completude: O sistema $H_{bp}$ é provado completo para $\text{Dev}(N)$. A prova depende de uma construção de modelo canônico que realiza explicitamente a lei de composição de união.
• Tradução de Teoremas Clássicos: O teorema de Gibbard–Satterthwaite e o teorema do eleitor mediano de Moulin são traduzidos com sucesso para a linguagem biperfil. O artigo não reprova esses teoremas, mas usa a nova linguagem para analisar seu comportamento sob mudanças de domínio.
• Estudo de Caso: Um exemplo de mediana de pico único com cinco agentes é usado para demonstrar a camada de auditoria. O estudo mostra como uma única tupla de testemunha de manipulação $(R, P, C, Q, x, y)$ é interpretada diferentemente sob três cenários:
  1. Domínio Restrito: A testemunha é "aresta-excluída" porque o relatório desviado $Q$ não é gerado pelo gerador de domínio restrito.
  2. Extensão Fora do Domínio: A testemunha é uma falha de "linha de fronteira", criada exclusivamente pelo novo relatório admissível $Q$.
  3. Exclusão Pública: A testemunha pode sobreviver (extremidades permanecem), mas a atualização é "insegura" porque a exclusão de um ponto médio misto quebra o fechamento por fator requerido para a álgebra $\text{Dev}(N)$.
• Complexidade de Verificação: A Proposição 7 estabelece que verificar um certificado tipado finito submetido é polinomial no tamanho do certificado para um conjunto fixo de agentes $N$.

Significância e Alegações
O artigo alega significância principalmente como uma estrutura formal de auditoria e não como um novo teorema de impossibilidade.

• Separação de Preocupações: Separa a espinha dorsal da teoria da prova (completude da álgebra abstrata) do limite de representação (recuperação de coordenadas) e da camada de aplicação (auditoria de mudanças de domínio).
• Valor Operacional: Os autores argumentam que sua "camada de auditoria" fornece uma interface de diagnóstico para mecanismos de escolha social. Em vez de reexecutar provas complexas de impossibilidade quando um domínio é modificado, verificadores podem usar o teorema da linha de fronteira para verificar apenas novas linhas e o critério de fechamento por fator para verificar se uma exclusão preserva a estrutura algébrica necessária.
• Modéstia: Os autores afirmam explicitamente que não fornecem um algoritmo geral de satisfatibilidade para $\text{Dev}(N)$ ou um novo limite de complexidade para regras representadas de forma sucinta. O resultado de completude é para a classe de quadros abstratos, e as verificações finitas são para certificados fornecidos explicitamente. O trabalho é apresentado como um "cenário de auditoria pequeno, mas completo" que esclarece onde e por que uma mudança de representação afeta propriedades estratégicas, em vez de oferecer uma nova solução para os problemas fundamentais da escolha social.