Labelled Sequents for Inquisitive First-Order Modal Logic

Problema
Il documento affronta una lacuna nello sviluppo proof-teoretico della logica modale primo-ordine inquisitiva, nello specifico il sistema $\text{InqQML}^{-}_{\Box}$ proposto da Ciardelli [5]. Questa logica estende la logica debole primo-ordine inquisitiva ($\text{InqWQ}$) con una modalità di tipo Kripke $\Box$ per ragionare sulle relazioni di dipendenza modale, in particolare sulla supervenienza globale. Sebbene la ricorsiva enumerabilità di $\text{InqQML}^{-}_{\Box}$ sia stata dimostrata tramite traduzione in logica del primo ordine a due sortite, non esisteva un sistema di derivazione dedicato per essa. I sistemi di derivazione esistenti per i frammenti proposizionali o non modali (ad esempio, la deduzione naturale di Conti [10] o i sequenti etichettati di Litak e Sano [22]) si basano sulla proprietà di coerenza finita, ma l'estensione al caso modale richiedeva nuove regole strutturali per gestire l'interazione tra la modalità e la disgiunzione inquisitiva.

Metodologia
Gli autori sviluppano un calcolo dei sequenti etichettati chiamato IWMC (Inquisitive Weak Modal Calculus). La metodologia si basa sul framework dei sequenti etichettati di Litak e Sano [22] per $\text{InqWQ}$, adattandolo all'ambito modale.

• Etichette e Semantica: Le etichette sono insiemi finiti non vuoti di numeri naturali (indici), che rappresentano stati informativi finiti. Una formula etichettata $s : \phi$ afferma intuitivamente che lo stato rappresentato da $s$ supporta $\phi$. Gli atomi relazionali $wRv$ codificano la relazione di accessibilità.
• Coerenza Finita: Uno strumento tecnico centrale è la proprietà di coerenza finita di $\text{InqQML}^{-}_{\Box}$. Ogni formula $\phi$ è $n_\phi$-coerente, il che significa che il suo supporto in uno stato dipende solo da sottostati di cardinalità al massimo $n_\phi$. Questo numero è computabile a partire dalla formula.
• Regole Modali: Il calcolo introduce regole specifiche per la modalità $\Box$:
  • $(\Rightarrow \Box)$: Per provare $s : \Box \phi$, la regola introduce $n_\phi$ nuovi indici $t$ (che rappresentano un insieme di successori) e richiede di provare $t : \phi$ per tutti i $w \in s$ tali che $wRt$. Questa regola sfrutta la coerenza finita per ridurre la condizione semantica (supporto da parte di tutti i successori) al supporto da parte di finiti insiemi di successori di dimensione limitata.
  • $(\Box \Rightarrow)$: Per utilizzare $s : \Box \phi$ nell'antecedente, la regola permette di derivare conseguenze da $t : \phi$ per qualsiasi insieme finito di successori $t$ di un mondo $w \in s$ già presenti nella derivazione.
• Gestione dell'Identità: Gli autori estendono il calcolo a IWMC= per gestire le firme con il predicato di identità, aggiungendo regole per riflessività, simmetria, transitività e sostituzione, trattando l'identità come un predicato binario con estensioni dipendenti dal mondo soggette a vincoli di congruenza.

Contributi Chiave e Risultati

1. Correttezza e Completezza: Gli autori dimostrano che IWMC è corretto e fortemente completo per $\text{InqQML}^{-}_{\Box}$.
   • La correttezza è stabilita per induzione sulle derivazioni, mostrando che i sequenti derivabili sono validi sotto la standard semantica inquisitiva.
   • La completezza è provata tramite la costruzione di un modello canonico. Gli autori definiscono sequenti generalizzati "saturi" (potenzialmente infiniti) e mostrano che ogni sequente non derivabile può essere esteso in uno saturo. Un modello canonico viene poi costruito da questo sequente saturo, che funge da controesempio, dimostrando così che se un sequente è valido, deve essere derivabile.
2. Proprietà Strutturali: Il calcolo gode di desiderabili proprietà proof-teoretiche:
   • Invertibilità: Tutte le regole di inferenza sono invertibili (preservando l'altezza).
   • Ammissibilità: Le regole di indebolimento, contrazione e taglio sono ammissibili.
   • Analiticità: Il sistema soddisfa la proprietà del sottofomula (estesa per includere le sostituzioni), garantendo che le prove contengano solo sottoforme della conclusione.
3. Estensione all'Identità: Il documento dimostra come generalizzare l'approccio per includere il predicato di identità, mantenendo le proprietà strutturali e la completezza del sistema.

Significato
Il documento sostiene che IWMC rappresenti il primo sistema di derivazione per una logica modale primo-ordine inquisitiva. La sua importanza è duplice:

1. Utilità Pratica: Fornisce uno strumento formale per stabilire la validità delle inferenze riguardanti le dipendenze modali e la supervenienza globale, permettendo l'analisi rigorosa di tesi filosofiche come la supervenienza di Hume all'interno di questo framework logico.
2. Modello Teorico: Gli autori suggeriscono che il loro approccio, in particolare l'integrazione della coerenza finita nelle regole dei sequenti etichettati per le modalità, possa servire da modello per la costruzione di sistemi di derivazione per altre logiche modali primo-ordine inquisitive.

Il documento conclude osservando che, sebbene il sistema sia completo, è necessario ulteriore lavoro per esplorare le estensioni a firme con simboli di funzione, investigare risultati metateoretici come l'interpolazione e adattare il calcolo a modalità basate su vicinato (neighborhood-based modalities).