Formalizing Kantian Ethics: Formula of the Universal Law Logic (FULL)

1. Problema

O campo da ética de máquinas visa construir Agentes Morais Artificiais (AMAs) para tornar a IA mais segura e compreensível. As abordagens atuais geralmente codificam intuições morais humanas como um conjunto de axiomas prescritivos (ex: "não cause danos", "não minta"). O artigo identifica três limitações críticas nessas abordagens:

1. Foco no Agente vs. Ação: Os axiomas atuais avaliam apenas a ação em si (foco na ação), ignorando o propósito do agente ao realizá-la. Isso impede a distinção entre ações feitas por dever e aquelas feitas por interesse (ex: reduzir poluição por dever vs. por relações públicas).
2. Dependência de Intuição Enumerada: Assumem que os humanos podem enumerar a priori toda a intuição moral necessária para resolver conflitos e exceções futuras (problema do alinhamento de valores).
3. Falta de Autonomia Moral: Como os AMAs não podem criticar os próprios axiomas morais, eles não participam ativamente do discurso moral.

O objetivo do artigo é superar essas limitações formalizando um procedimento moral que não dependa de uma lista pré-definida de regras, mas sim de princípios racionais de agência.

2. Metodologia

O autor propõe a formalização da Ética Kantiana, especificamente a primeira formulação do Imperativo Categórico, conhecida como Fórmula da Lei Universal (FUL - Formula of the Universal Law).

• Lógica Proposta: O artigo introduz a Lógica da Fórmula da Lei Universal (FULL), uma lógica modal quantificada multi-sorteada.
• Interpretação Utilizada: A FULL baseia-se na Interpretação da Contradição Prática (PCI), defendida por filósofos como O'Neill e Korsgaard. Diferente de interpretações puramente lógicas (que falham em ações naturais como assassinato) ou teleológicas, a PCI avalia se a ação permanece um meio eficaz para atingir o propósito do agente em um "Mundo da Lei Universal" (WUL).
• Componentes da FULL:
  • Sortes (S): Objetos, Agentes e Ações.
  • Operadores Modais:
    • Does(a, b): O agente a realiza a ação b.
    • Wills(a, ϕ): O agente a quer que ϕ seja verdade.
    • For(ϕ1, ϕ2): Formaliza uma Máxima (agir ϕ1 para o propósito ϕ2).
    • Causes(ϕ1, ϕ2): Lei causal onde a ação causa o estado de fato.
  • Lei Universal (UL): Um processo de transformação sintática que substitui constantes específicas por variáveis quantificadas universalmente (para agentes e propósitos) e existencialmente (para objetos da ação), criando uma lei universal a partir de uma máxima individual.
  • Teste de Permissibilidade: Uma máxima é permissível se, e somente se, o agente puder querer simultaneamente sua própria máxima e a lei universal derivada dela, sem gerar uma contradição lógica no sistema.

3. Principais Contribuições

1. Formalização da FUL: A primeira formalização completa e rigorosa da primeira formulação do Imperativo Categórico de Kant em uma lógica modal quantificada, superando trabalhos anteriores que focaram na segunda formulação (Humanidade).
2. Abordagem Centrada no Agente: A FULL avalia ações baseadas nos propósitos do agente, permitindo distinguir entre ações moralmente idênticas fisicamente, mas diferentes intencionalmente (ex: cirurgia vs. assassinato).
3. Redução da Intuição Humana: O sistema não requer axiomas morais pré-carregados (como "não mate"). Em vez disso, deriva normas morais a partir de princípios formais de racionalidade, causalidade e agência, exigindo apenas conhecimento de fundo não normativo (fatos sobre o mundo).
4. Distinção de Deveres: O sistema consegue diferenciar formalmente entre:
   • Contradições na Concepção: Levam a deveres perfeitos (obrigações estritas, ex: não mentir, não matar).
   • Contradições na Vontade: Levam a deveres imperfeitos (obrigações amplas, ex: ajudar os outros).

4. Resultados

O artigo demonstra a eficácia da FULL através de três casos de teste formais, provando teoremas de impermissibilidade:

• Exemplo 1: Promessa Falsa (Karli):
  • Cenário: Karli promete falsamente dinheiro para viajar.
  • Resultado: A universalização da máxima cria um mundo onde ninguém acredita em promessas. Consequentemente, a promessa falsa deixa de ser um meio eficaz para obter dinheiro. Isso gera uma contradição na concepção (a ação anula o próprio propósito). O sistema conclui que a ação é impermissível.
• Exemplo 2: Assassinato (Karli):
  • Cenário: Karli planeja matar um concorrente para conseguir um emprego.
  • Resultado: Na lei universal, todos matariam concorrentes. Isso implica que Karli também seria morta por outros. Se Karli for morta, sua ação de matar não a levará ao emprego. A ação torna-se ineficaz para seu propósito. Contradição prática. O sistema conclui que é impermissível.
  • Contraste: O sistema diferencia isso de uma cirurgia, onde o propósito é salvar a vida. Na lei universal, a cirurgia continua sendo um meio eficaz, portanto, é permissível.
• Exemplo 3: Não Ajudar Ninguém:
  • Cenário: Karli decide nunca ajudar ninguém para ter tempo de lazer.
  • Resultado: Na lei universal, ninguém ajudaria Karli. Como a vida de agentes racionais depende de ajuda (ex: bebês, doentes), Karli estaria querendo um mundo onde ela não está viva. Isso gera uma contradição na vontade (querer viver e querer não viver). O sistema conclui que é impermissível não ajudar, derivando um dever imperfeito de ajudar.

5. Significado e Impacto

A FULL representa um avanço significativo para a ética de máquinas e a IA:

• Robustez e Autonomia: Ao basear a moralidade em princípios formais de racionalidade e causalidade em vez de regras estáticas, os AMAs tornam-se mais robustos e capazes de lidar com novos cenários sem reprogramação humana constante.
• Compreensão Formal da Ética Kantiana: Oferece uma interpretação computacional clara de conceitos kantianos abstratos, como contradições na concepção vs. na vontade, validando a aplicabilidade prática da filosofia de Kant na IA.
• Futuro: O trabalho abre caminho para AMAs que não apenas "seguem regras", mas que podem participar de discursos morais, justificando suas ações com base em princípios racionais universais, reduzindo a necessidade de alinhamento de valores baseado em intuições humanas enumeradas.

Em resumo, o artigo demonstra que a lógica formal pode capturar a essência da ética deontológica kantiana, permitindo que agentes de IA derivem normas morais complexas a partir de princípios fundamentais de agência racional.