The Varieties of Ought-Implies-Can and Deontic STIT Logic

1. O Problema

O princípio filosófico "O que deve ser feito, pode ser feito" (Ought-implies-Can ou OiC) é central na ética e na lógica deôntica, postulando que um agente só pode ter obrigações sobre ações que ele é capaz de realizar. No entanto, a literatura filosófica apresenta uma vasta gama de interpretações desse princípio, variando desde versões fracas (como a mera consistência lógica) até versões fortes (como o controle total do agente sobre a situação).

O problema abordado pelos autores é a falta de uma estrutura formal unificada e modular que permita:

1. Analisar e comparar sistematicamente essas diferentes interpretações de OiC dentro do mesmo quadro lógico.
2. Determinar as relações lógicas precisas (dependências, independências e hierarquias) entre essas interpretações.
3. Superar as limitações da abordagem tradicional de STIT (Seeing To It That) baseada em utilitarismo, que muitas vezes não consegue acomodar a multiplicidade de nuances do princípio OiC sem modificações complexas.

2. Metodologia

Os autores empregam uma abordagem baseada em Lógica STIT Deôntica (lógica da ação de agentes) combinada com Cálculos de Sequente Rotulados (Labelled Sequent Calculi).

• Semântica Modular: Em vez de usar a semântica tradicional de tempo ramificado baseada em utilidades, os autores adotam uma semântica relacional modular. Eles definem quadros (frames) de STIT deôntica ($DS_n$) compostos por mundos, relações de equivalência para "momentos" ($R_2$) e escolhas dos agentes ($R_{[i]}$), além de relações deônticas ($R_{\otimes i}$).
• Propriedades de Quadros: Para capturar as diferentes versões de OiC, são introduzidas quatro propriedades adicionais de quadros ($D2$ a $D5$) que restringem o comportamento dos operadores deônticos (exigindo, por exemplo, que o mundo ideal seja acessível, que esteja contido no momento atual, ou que corresponda a uma escolha do agente).
• Cálculos de Sequente: Os autores desenvolvem sistemas de prova (cálculos de sequente) $G3DS_nX$ que são corretos e completos para cada lógica resultante. Esses cálculos incorporam explicitamente informações semânticas nas regras de inferência, permitindo não apenas provar teoremas, mas também extrair contra-modelos quando uma prova falha.
• Formalização de Princípios: Dez princípios distintos de OiC são formalizados na linguagem da lógica STIT, utilizando operadores modais para "possibilidade", "capacidade", "contingência" e "controle".

3. Principais Contribuições

O artigo oferece três contribuições fundamentais:

1. Taxonomia Formal de Dez Princípios OiC:
   Os autores identificam e formalizam dez leituras do princípio OiC encontradas na literatura, incluindo:

   • OiLP: Ode implica Possibilidade Lógica.
   • OiAP: Ode implica Possibilidade Real (Atual).
   • OiA: Ode implica Capacidade (o agente pode garantir o resultado).
   • OiV: Ode implica Violabilidade (a obrigação pode ser violada).
   • OiR: Ode implica Possibilidade de Abster-se (o agente pode escolher não cumprir).
   • OiO: Ode implica Oportunidade (o estado de coisas é contingente).
   • OiA+O: Ode implica Capacidade e Oportunidade.
   • OiCtrl: Ode implica Controle (o agente pode realizar e pode violar).
   • OiNC/OiNA: Versões normativas ("Deveria ser possível que...").

2. Desenvolvimento de Cálculos de Sequente Completos:
   São apresentados cálculos de sequente rotulados para todas as classes de lógicas STIT deônticas geradas pelas combinações das propriedades de quadros. Estes cálculos permitem a verificação automática (em teoria) da validade de princípios e a construção de contra-modelos para provar independência.

3. Princípio de Endosso (Endorsement Principle):
   Através da análise das relações entre os cálculos, os autores estabelecem um "princípio de endosso". Este princípio descreve quais leituras de OiC, ao serem adotadas, comprometem logicamente o agente a adotar outras leituras mais fracas. Isso cria uma hierarquia lógica clara.

4. Resultados

A análise dos cálculos e dos quadros resultou nos seguintes achados técnicos:

• Hierarquia de Força: Os autores construíram um reticulado (lattice) que ordena as 16 lógicas STIT deônticas possíveis (baseadas nas combinações de propriedades $D2-D5$) de acordo com sua força expressiva.
• Dependências e Independências:
  • Foi demonstrado que princípios fortes (como OiCtrl ou OiA+O) implicam logicamente princípios mais fracos (como OiLP ou OiAP).
  • Identificou-se que certas leituras são mutuamente independentes. Por exemplo, o princípio normativo OiNA ("Ode implica que deveria ser possível") é estritamente independente de princípios baseados na capacidade factual do agente (OiA), o que só pôde ser provado através da construção de contra-modelos específicos gerados pelos cálculos de sequente.
• Relação com a STIT Tradicional: O artigo mostra que a lógica STIT deôntica tradicional (baseada em utilitarismo, conforme [23, 32]) corresponde a uma lógica específica no reticulado (gerada por $D2, D3, D4$), que valida uma versão específica de OiC (OiA), mas não as versões deliberativas mais fortes sem a adição de propriedades adicionais.
• Distinção entre "Ode" e "Ode a ver que": A análise clarifica a distinção lógica entre "é obrigatório para o agente i que $\phi$" ($\otimes_i \phi$) e "o agente i deve ver que $\phi$" ($\otimes_i [i]\phi$), mostrando que a equivalência entre eles depende de propriedades específicas do quadro (como $D4$).

5. Significado e Impacto

Este trabalho é significativo por várias razões:

• Precisão Filosófica: Transforma debates filosóficos vagos sobre "o que significa poder fazer algo" em estruturas lógicas rigorosas e comparáveis. Permite que filósofos e cientistas da computação discutam exatamente qual versão de OiC estão adotando.
• Ferramentas Computacionais: Ao fornecer cálculos de sequente corretos e completos, o trabalho habilita a automação do raciocínio deôntico. As ferramentas podem ser usadas para verificação de modelos, busca de provas e extração de contra-exemplos, o que é crucial para aplicações em IA, sistemas multiagentes e direito computacional.
• Fundação para Futuras Pesquisas: Estabelece uma base para investigar princípios éticos mais complexos e para expandir a lógica STIT para contextos temporais e epistêmicos, mantendo a modularidade necessária para analisar diferentes interpretações normativas.

Em resumo, o artigo oferece a primeira taxonomia lógica completa e formalizada das variações do princípio "Ode implica Pode" dentro do paradigma STIT, utilizando métodos de teoria da prova para mapear as implicações lógicas de cada escolha filosófica.