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

1. Il Problema

Il principio filosofico "Ought-implies-Can" (OiC), ovvero "ciò che un agente deve fare, l'agente è in grado di fare", è un pilastro della filosofia morale e della logica deontica. Tuttavia, la letteratura filosofica propone numerose interpretazioni di questo principio, che variano per forza logica e significato (es. possibilità logica, possibilità attuale, abilità, controllabilità, opportunità).

Il problema centrale affrontato dagli autori è la mancanza di un quadro formale unificato all'interno della logica STIT (Seeing To It That) che possa:

1. Accogliere e formalizzare simultaneamente queste diverse interpretazioni dell'OiC.
2. Analizzare rigorosamente le relazioni logiche (dipendenze, indipendenze, gerarchie) tra queste diverse letture.
3. Superare le limitazioni delle caratterizzazioni tradizionali della logica deontica STIT, che si basano su un approccio utilitaristico e faticoso da adattare a una molteplicità di principi.

2. Metodologia

Gli autori adottano un approccio modulare basato sulla logica STIT deontica e sulla teoria della dimostrazione (proof theory).

• Semantica Modulare: Invece di utilizzare la semantica classica basata sul tempo ramificato e sulle funzioni di scelta, gli autori adottano una semantica relazionale modulare. Definiscono un quadro di base ($DS_n$) e introducono quattro proprietà aggiuntive per i frame ($D2, D3, D4, D5$) che modificano il comportamento degli operatori deontici ($\otimes_i$) per catturare diverse sfumature di "potere" e "contingenza".
• Calcoli di Sequenza Etichettati (Labelled Sequent Calculi): Per ogni combinazione di proprietà del frame, gli autori costruiscono un calcolo di sequenza etichettato ($G3DSnX$). Questi calcoli incorporano esplicitamente le informazioni semantiche (relazioni tra mondi possibili) nelle regole di inferenza.
• Formalizzazione dei Principi: Vengono formalizzate dieci diverse letture dell'OiC, utilizzando operatori STIT standard ($[i]$ per l'azione, $\Box$ per la verità stabilita) e operatori deontici ($\otimes_i$). Per le letture "deliberative" (che richiedono che un'obbligazione sia violabile), vengono introdotti operatori derivati ($\otimes^d_i$ e $\otimes^c_i$).

3. Contributi Chiave

1. Tassonomia dei Principi OiC: Il paper identifica e formalizza dieci principi OiC distinti tratti dalla letteratura filosofica, tra cui:
   • OiLP: Ought implies Logical Possibility.
   • OiAP: Ought implies Actually Possible.
   • OiA: Ought implies Ability.
   • OiV/OiR: Ought implies Violability/Refrainability.
   • OiO: Ought implies Opportunity.
   • OiA+O: Ought implies Ability and Opportunity.
   • OiCtrl: Ought implies Control.
   • OiNC/OiNA: Letture normative ("Ought implies Normatively Can/Able").
2. Sistemi di Calcolo Completi e Corretti: Vengono forniti calcoli di sequenza corretti e completi (sound and complete) per tutte le classi di logiche STIT deontiche generate dalle diverse combinazioni di proprietà dei frame. Questo permette di trattare formalmente ogni variante dell'OiC.
3. Principio di "Endorsement" (Sostegno): Gli autori introducono un principio filosofico-logico che descrive come l'adozione di una certa lettura dell'OiC impegni logicamente l'agente ad accettare altre letture più deboli. Questo crea una gerarchia logica precisa.

4. Risultati Principali

• Gerarchia Logica: Attraverso l'analisi dei calcoli, gli autori costruiscono un reticolo (lattice) che ordina le logiche STIT deontiche in base alla loro forza espressiva.
  • La logica più debole ($G3DSn$) valida solo principi molto basilari come OiLP e OiNC.
  • La logica più forte (che include le proprietà $D2, D3, D4$) corrisponde alla logica STIT deontica tradizionale e valida principi più forti come OiA (Abilità) e OiA+O.
• Indipendenza Logica: L'approccio proof-theoretic permette di dimostrare l'indipendenza tra certi principi. Ad esempio, viene mostrato che il principio normativo OiNA (Ought implies Normatively Able) è logicamente indipendente da OiA (Ought implies Ability) e da OiLP.
• Costruzione di Contro-modelli: Quando una derivazione fallisce nel calcolo (proof-search fallito), gli autori mostrano come estrarre automaticamente un contro-modello semantico. Questo dimostra formalmente che un principio non implica un altro (es. OiLP non implica OiNA).
• Risoluzione di Dibattiti Filosofici: Il lavoro chiarisce che la logica STIT tradizionale (basata su $D3$ e $D5$) è sufficiente per validare la lettura classica dell'OiC (Abilità), ma che per ottenere la lettura di "Dominance Ought" (Horty) è necessaria l'aggiunta della proprietà $D4$.

5. Significato e Implicazioni

• Unificazione Teorica: Il paper fornisce il primo quadro formale capace di gestire sistematicamente la varietà delle interpretazioni dell'OiC, risolvendo ambiguità che in precedenza richiedevano analisi filosofiche qualitative.
• Strumento per la Ragionamento Normativo: L'uso di calcoli di sequenza etichettati non solo garantisce la correttezza teorica, ma rende i sistemi adatti per applicazioni computazionali, come la ricerca di prove automatizzata e l'estrazione di contro-esempi.
• Fondamento per Futuri Studi: La tassonomia logica proposta serve come base per investigare ulteriormente i dilemmi morali, la responsabilità agente-dipendente e le interazioni tra obblighi e capacità in contesti multi-agente.
• Chiarezza Concettuale: Dimostra che molte dispute filosofiche sull'OiC sono in realtà dispute su quale logica sottostante (quale combinazione di proprietà del frame) sia appropriata per il contesto specifico, offrendo una mappa precisa delle implicazioni logiche di ogni scelta.

In sintesi, van Berkel e Lyon trasformano un dibattito filosofico complesso in una struttura logica rigorosa e computabile, dimostrando come la scelta di un principio "Ought-implies-Can" vincoli necessariamente l'adozione di altri principi all'interno del sistema logico STIT.