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

1. Il Problema

Il campo dell'etica delle macchine mira a costruire Agenti Morali Artificiali (AMA) capaci di ragionare su obblighi e divieti morali per rendere l'IA più sicura. Gli approcci attuali si basano prevalentemente su un'encoding "bottom-up" o su assiomi morali fissi (es. "non fare del male", "aiuta gli altri"). Olson identifica tre limitazioni critiche in questi metodi:

1. Mancanza di focalizzazione sull'agente: Gli approcci attuali valutano solo l'azione in sé (action-centric), ignorando lo scopo o l'intenzione dell'agente (agent-centric). Non riescono quindi a distinguere tra un'azione fatta per dovere e la stessa azione fatta per calcolo strategico (es. ridurre l'inquinamento per dovere vs. per pubbliche relazioni).
2. Dipendenza dall'intuizione umana: Assumono che gli esseri umani possano elencare a priori tutte le intuizioni morali necessarie. Questo non risolve il problema dell'allineamento dei valori in situazioni nuove o conflittuali (es. un chirurgo che "fa male" tagliando un paziente, ma per salvarlo).
3. Mancanza di autonomia morale: Gli AMA non possono criticare gli assiomi morali su cui sono programmati, impedendo loro di partecipare al discorso morale.

L'obiettivo del paper è superare queste limitazioni formalizzando un procedimento morale che non richieda un elenco predefinito di intuizioni, ma che derivi norme morali da principi formali di razionalità.

2. Metodologia

L'autore propone di fondare gli AMA sulla etica kantiana, in particolare sulla prima formulazione dell'Imperativo Categorico: la Formula della Legge Universale (FUL).
La FUL afferma: "Agisci solo secondo quella massima che puoi volere al tempo stesso che diventi una legge universale".

Per formalizzare questo concetto, Olson introduce la Formula of the Universal Law Logic (FULL), una logica modale quantificata a più sortite (multi-sorted quantified modal logic). La metodologia si basa su tre pilastri concettuali:

• Interpretazione della Contraddizione Pratica (PCI): Invece di cercare contraddizioni logiche (impossibilità di concepire l'azione) o teleologiche, la FULL adotta l'interpretazione della contraddizione pratica. Un'azione è moralmente impermissibile se, nel "Mondo della Legge Universale" (WUL), l'azione cessa di essere un mezzo efficace per raggiungere lo scopo dell'agente.
• Struttura della Logica (FULL):
  • Sorti: Definisce entità come Agenti, Azioni e Oggetti.
  • Predicati: Usa Does(a, b) per le azioni, Wills(a, ϕ) per la volontà (l'agente vuole che ϕ sia vero), e Causes per le leggi causali.
  • Massime: Formalizzate come For(ϕ1, ϕ2), dove ϕ1 è l'azione e ϕ2 lo scopo.
  • Legge Universale (UL): Una funzione che trasforma una massima specifica in una legge universale quantificando l'agente e i costanti dello scopo, e quantificando esistenzialmente i costanti dell'azione.
• Procedimento di Verifica: La logica esegue un test negativo in tre passaggi:
  1. L'agente immagina un mondo dove la Legge Universale della sua massima è vera (Wills(a, UL(M))).
  2. L'agente vuole agire secondo la sua massima in quel mondo (Wills(a, M)).
  3. Si verifica se questi due desideri generano una contraddizione logica (⊢ ⊥). Se sì, l'azione è impermissibile.

3. Contributi Chiave

1. Formalizzazione della FUL: È uno dei primi tentativi completi di formalizzare la prima formulazione dell'Imperativo Categorico (precedentemente considerata un problema aperto), distinguendosi dalla formalizzazione della seconda formulazione (Formula dell'Umanità).
2. Approccio Agent-Centric: La logica valuta le azioni in base allo scopo dell'agente. Questo permette di differenziare moralmente azioni fisicamente identiche ma con intenzioni diverse (es. chirurgia vs. omicidio).
3. Riduzione dell'Intuizione Morale: Il sistema non richiede che gli umani codifichino regole morali specifiche (es. "non mentire"). Richiede solo conoscenze di base non normative (fatti causali, leggi fisiche, necessità di sopravvivenza) e principi di razionalità.
4. Distinzione tra Doveri: La logica è in grado di derivare formalmente la distinzione kantiana tra:
   • Contraddizioni di Concezione (CC): Portano a doveri perfetti (assoluti, es. non mentire, non uccidere).
   • Contraddizioni di Volontà (CW): Portano a doveri imperfetti (ampi, es. dovere di aiutare gli altri).

4. Risultati (Dimostrazioni)

L'autore dimostra l'efficacia della FULL attraverso tre casi di studio classici, fornendo prove formali che derivano l'impermissibilità delle azioni:

• Esempio 1: La Falsa Promessa.
  • Scenario: Karli promette di restituire denaro senza intenzione di farlo per ottenere soldi per viaggiare.
  • Risultato: Nel mondo universale, se tutti facessero false promesse, nessuno crederebbe alle promesse. Di conseguenza, la promessa falsa di Karli non sarebbe più un mezzo efficace per ottenere denaro. Si crea una contraddizione tra il volere la massima (ottenere denaro) e il volere la legge universale (dove la promessa è inefficace). L'azione è impermissibile.
• Esempio 2: Omicidio (per ottenere un lavoro).
  • Scenario: Karli uccide un candidato per ottenere un lavoro.
  • Risultato: Nel mondo universale, tutti ucciderebbero i rivali. Karli, volendo la legge universale, deve volere di essere uccisa a sua volta. Se Karli è uccisa, non può ottenere il lavoro. L'azione diventa inefficace per il suo scopo. Contraddizione pratica. L'azione è impermissibile.
  • Nota: La logica distingue questo caso da un chirurgo che "taglia" un paziente: nel caso del chirurgo, l'azione è un mezzo efficace per salvare la vita anche nel mondo universale, quindi non c'è contraddizione.
• Esempio 3: Non aiutare mai gli altri.
  • Scenario: Karli decide di non aiutare nessuno per avere più tempo libero.
  • Risultato: Nel mondo universale, nessuno aiuta nessuno. Poiché gli agenti razionali hanno bisogno di aiuto per sopravvivere (es. infanzia, malattia), Karli, volendo la legge universale, vuole di non essere aiutata e quindi di non sopravvivere. Tuttavia, per volere qualsiasi cosa (inclusa la massima), Karli deve essere viva. Contraddizione tra il volere di vivere (necessario per la volontà) e il volere di non vivere (conseguenza della massima universalizzata). L'azione è impermissibile, generando un dovere imperfetto di aiutare.

5. Significatività e Implicazioni

Il paper rappresenta un passo fondamentale verso AMA più robusti e autonomi:

• Autonomia Morale: Gli agenti non agiscono ciecamente su regole preimpostate, ma derivano norme morali attraverso il ragionamento logico su principi di razionalità e causalità.
• Flessibilità: Il sistema può gestire nuovi scenari senza bisogno di aggiornare il database di regole, purché l'agente possieda le conoscenze causali pertinenti.
• Comprensione Formale dell'Etica: Offre una base matematica rigorosa per l'etica kantiana, permettendo di analizzare la struttura logica dei doveri morali.
• Sfide Future: L'autore riconosce che la formalizzazione presuppone che le massime siano già formulate correttamente (il problema della descrizione dell'azione), il che potrebbe richiedere ancora un certo grado di intuizione umana o giudizio contestuale. Il lavoro futuro includerà l'espansione della logica per gestire quantificatori generalizzati e concetti intenzionali più complessi.

In sintesi, la FULL dimostra che è possibile costruire un sistema di etica artificiale che non si basa su un elenco statico di "regole", ma su un processo dinamico di verifica della coerenza razionale tra le intenzioni dell'agente e un mondo ipotetico di universalità.