Understanding Privacy by Formalizing It

Resumo Técnico: Compreendendo a Privacidade através de sua Formalização

Problema
O artigo aborda o desafio de traduzir o conceito de privacidade para um formato adequado à análise e implementação algorítmica, particularmente no contexto da Inteligência Artificial (IA) e da digitalização. Embora haja um consenso amplo sobre a necessidade de proteger a privacidade, o conceito em si carece de uma definição unificada e está sujeito a diversas interpretações no direito, nas ciências sociais e na ciência da computação. As capacidades atuais da IA, como o reconhecimento de padrões em dados, podem erodir a privacidade ao inferir informações não compartilhadas explicitamente, embora os marcos regulatórios existentes frequentemente dependam de conceitualizações vagas ou conflitantes. Os autores argumentam que, para impor restrições algorítmicas significativas ou mecanismos de autorregulação, o direito à privacidade deve ser formalmente especificado. Sem tal precisão, é impossível comparar diferentes conceitualizações de privacidade ou determinar se elas se referem às mesmas ideias subjacentes.

Metodologia
Os autores empregam uma abordagem lógica formal para caracterizar diferentes teorias da privacidade. A metodologia consiste em três componentes principais:

1. Estrutura Teórica: O artigo utiliza a Teoria das Posições Normativas, fundamentada na análise de direitos de W.N. Hoheld. Este framework distingue quatro tipos atômicos de direitos e seus correlatos: direitos de pretensão (claim-rights e deveres), privilégios (e ausência de pretensões), poderes (e responsabilidades/liabilities) e imunidades (e incapacidades/disabilities). Os autores estendem isso para direitos multital (direitos mantidos contra todos) e direitos moleculares (combinações complexas de posições atômicas). Eles focam especificamente em direitos epistêmicos, definidos como direitos relativos à distribuição e acessibilidade de bens epistêmicos (conhecimento/informação).
2. Formalismo Lógico: Uma lógica multimodal é construída para representar esses direitos. A linguagem $L$ estende a lógica proposicional com quatro modalidades:
   • Agência ($E_a$): "O agente $a$ providencia que..." (modelado via semântica de vizinhança).
   • Obrigação Direcionada ($O_{a \to b}$): "O agente $a$ tem um dever para com $b$ de que..." (lógica deontica padrão, axioma D).
   • Conhecimento Epistêmico ($K_a$): "O agente $a$ sabe que..." (lógica de conhecimento S5 padrão).
   • Necessidade Alética ($\Box$): "É necessário que..." (S5).
     A lógica evita suposições fortes sobre ação (usando lógica de ação fraca) para permitir uma interpretação ampla de "ações", mantendo propriedades padrão para conhecimento e necessidade.
3. Processo de Formalização: Os autores mapeiam definições e teorias específicas de privacidade para esta linguagem lógica. Eles traduzem conceitos como "o direito de ser deixado em paz", "controle sobre a informação" e "integridade contextual" em fórmulas envolvendo combinações das modalidades acima.

Principais Contribuições e Resultados
O artigo fornece representações formais iniciais de várias abordagens proeminentes de privacidade, demonstrando como elas se traduzem em distintas posições normativas:

• Direito de Ser Deixado em Paz / Controle: Os autores formalizam o "direito de ser deixado em paz" (Warren e Brandeis) e a definição de "controle" de Westin. Eles distinguem entre:
  • Fórmulas de dever-ser (ex: $O\Diamond E_a \neg K_b \phi$), que declaram um estado de coisas desejado.
  • Fórmulas de dever-fazer envolvendo agentes específicos (ex: o estado $s$ impondo um dever a uma empresa $c$ para permitir que o agente $a$ impeça $b$ de saber $\phi$).
  • Eles formalizam liberdades multital (a ausência de uma obrigação de divulgar) e imunidades (a incapacidade de outros alterarem essa liberdade), mostrando como a privacidade pode ser um direito molecular complexo em vez de um único direito atômico de pretensão.
• Integridade Contextual e Privacidade Inalcançável: Abordando a crítica de Nissenbaum de que o controle absoluto é impossível, o artigo formaliza cenários onde o acesso é inevitável. Nestes casos, a privacidade é redefinida como o direito de controlar a disseminação adicional ou o direito de impedir que aqueles que necessariamente conhecem a informação possam escrutinar ou comentar sobre ela (ex: $E_a O_{b \to a} \neg E_b K_a \phi$).
• Transparência: O artigo formaliza o "direito à transparência" (saber se outros têm acesso) usando um operador de "saber se" para evitar paradoxos lógicos, garantindo que o detentor do dever informe o detentor do direito sobre o status de acesso.
• Execução (Enforcement): Os autores incluem formalizações para o poder de executar direitos. Eles modelam a transição de uma violação de um dever de privacidade para uma nova pretensão contra o judiciário para executar o dever original ou fornecer compensação.

Significância e Alegações
O artigo alega que sua principal contribuição é o uso de especificações lógicas tanto como um objetivo quanto como um método para esclarecer as distinções entre diferentes conceitos de privacidade. Ao formalizar esses conceitos dentro da Teoria das Posições Normativas, os autores visam:

1. Tornar as especificações de privacidade acessíveis para análise algorítmica, permitindo a construção de algoritmos que possam detectar violações de privacidade.
2. Prover um terreno comum para comparar diferentes conceitualizações de privacidade (ex: no direito vs. na ciência da computação) para determinar se são equivalentes ou distintas.
3. Estabelecer as bases para especificações implementáveis de direitos de privacidade, servindo como base para iniciativas de "política-como-código" (policy-as-code) e "lei-como-código" (law-as-code) em IA e Sistemas Multiagentes (MAS).

Os autores declaram explicitamente que não fornecem resultados metalógicos (como provas de completude ou decidibilidade), mas sim focam na análise conceitual formal de como diferentes teorias da privacidade mapeiam para posições normativas. Eles reconhecem que este é um passo inicial, com trabalhos futuros planejados para abordar a defeatibilidade desses direitos e para testar esses formalismos usando frameworks como o LogiKEy.