A Gödel Modal Logic Over Witnessed Models

Sintesi Tecnica: Una Logica Modale di Gödel su Modelli Testimoniati

Problema
Le logiche modali di Gödel (GK) forniscono un quadro per ragionare su nozioni graduate di incompletezza e vaghezza utilizzando gli operatori di necessità ($\Box$) e possibilità ($\Diamond$) valutati sull'intervallo reale unitario $[0,1]$. La semantica standard per queste logiche si basa su modelli di Gödel-Kripke (modelli G), dove il valore di verità di una formula modale è definito dall'infimo o dal supremo dei valori di verità su mondi accessibili. Questa limitazione critica della semantica standard è che tali limiti non devono necessariamente essere raggiunti da un mondo specifico accessibile. Questo fenomeno "basato sul limite" conduce a significative patologie logiche: la logica non possiede la Proprietà del Modello Finito (FMP), e certe validità in modelli finiti (ad esempio $\Box\neg\neg\phi \to \neg\Box\phi$) falliscono in modelli infiniti. Di conseguenza, gli argomenti semantici richiedono spesso comportamenti genuinamente infinitari, complicando il ragionamento automatizzato e l'analisi proof-teoretica.

Metodologia
Gli autori introducono GW, una logica modale di Gödel basata su modelli testimoniati (witnessed models). In un modello GW, la semantica degli operatori modali è vincolata in modo che l'infimo e il supremo che definiscono i valori di verità di $\Box\phi$ e $\Diamond\phi$ debbano essere raggiunti da almeno un mondo accessibile (un "testimone"). Ciò assicura che il valore di verità di una formula modale sia determinato da mondi concreti piuttosto che da approssimazioni asintotiche.

Per analizzare GW, gli autori sviluppano un calcolo di confutazione basato su vincoli chiamato CGW. La metodologia prevede:

1. Linguaggio di Vincoli: Le formule sono tradotte in vincoli su un insieme numerabile di etichette che rappresentano i mondi. Questi vincoli coinvolgono termini atomici (mondi, relazioni di accessibilità $R$, e valutazioni proposizionali) e relazioni ($<, \le, >, \ge$) su numeri razionali in $[0,1]$.
2. Calcolo di Confutazione: CGW è progettato per certificare che una formula non sia valida in alcun modello GW. Esso impiega regole proposizionali, regole modali (che introducono nuove etichette per i testimoni) e regole per la relazione di accessibilità (regole $R$).
3. Ricerca di Prove e Generazione di Contromodelli: Gli autori progettano una procedura di ricerca di prove backward-search terminante. Se la ricerca fallisce nel derivare una contraddizione, la procedura traccia il computo per costruire un contromodello finito (specificamente, un modello GW discreto) per la formula di input.
4. Analisi della Complessità: Viene abbozzata una procedura decisionale PSPACE, che utilizza una ricerca ricorsiva che gestisce le assegnazioni di valori di verità ai sottoformule senza costruire esplicitamente l'intero modello in memoria.

Contributi Chiave

• Definizione di GW: La formalizzazione della logica modale di Gödel su modelli di Kripke testimoniati, distinguendola dalla standard GK e dalla variante "crisp" $GW^c$.
• Calcolo CGW: La presentazione di un calcolo di confutazione sound e completo per GW. Il calcolo gestisce i vincoli specifici della semantica testimoniata, in particolare il requisito che i limiti siano raggiunti.
• Proprietà del Modello Finito (FMP): Gli autori dimostrano che GW gode della FMP come conseguenza diretta della procedura di ricerca di prove terminante. Se una formula non è valida, esiste un contromodello finito. Questo contrasta con la standard GK, che manca della FMP.
• Embedding e Non-Interdefinibilità:
  • Il documento dimostra che la logica modale classica K può essere incorporata in GW (e logiche correlate) tramite una traduzione che coinvolge la doppia negazione.
  • Dimostra che $\Box$ e $\Diamond$ non sono interdefinibili in alcuna logica modale contenuta in $GW^c$, estendendo i risultati precedentemente noti per i modelli crisp.
• Risultati di Complessità: La validità del problema per GW è stabilita come PSPACE-completa. Il limite inferiore segue dall'embedding di K, e il limite superiore è derivato dalla procedura PSPACE per l'esistenza di contromodelli.
• Implementazione: Un prototipo di prover chiamato gwref è implementato, utilizzando il motore JTabWb e il solver Choco per i controlli di consistenza dei vincoli.

Risultati

• Soundness e Completezza: CGW è dimostrato sound e completo rispetto ai modelli GW. Una formula $\phi$ è valida in GW se e solo se l'insieme di vincoli $\{w : \phi < 1\}$ non è provabile in CGW.
• Terminazione: Il calcolo è fortemente terminante. Una relazione ben fondata su multisetti di vincoli assicura che qualsiasi ricerca di prova backward-search termini.
• Estrazione del Contromodello: Quando la ricerca di prova fallisce, la procedura costruisce un contromodello discreto con una dimensione limitata da $O(|\phi|^{| \phi |})$.
• Gerarchia Logica: Il documento chiarisce le relazioni tra varie logiche: $GK \subset G^c \subset GW^c$ e $GK \subset GW \subset GW^c$. Mostra che l'assioma "Crisp" (valido in $G^c$) non è valido in $GW$, e l'assioma "Witnessed" ($\Box\neg\neg\alpha \to \neg\neg\Box\alpha$) è valido in $GW$ ma non in $G^c$.

Significatività
Il documento sostiene che la semantica testimoniata fornisce un modo principato per superare le difficoltà associate ai fenomeni basati sul limite nei logiche modali fuzzy. Assicurando che i comportamenti esistenziali ed esistenziali siano supportati da testimoni espliciti, la semantica di GW riflette più da vicino la quantificazione guardata nella logica del primo ordine e ripristina una lettura costruttiva.

La significatività di questo lavoro risiede nel fatto che:

1. Ripristinare le Proprietà Costruttive: La FMP e i risultati di decidibilità rendono GW adatto al ragionamento automatizzato, permettendo agli argomenti semantici infinitari di essere sostituiti da argomenti combinatori finiti.
2. Allineamento Proof-Teoretico: La semantica testimoniata si allinea più da vicino ai calcoli sintattici, facilitando le costruzioni di modelli canonici e le prove di completezza standard.
3. Connessioni con le Logiche Intermedie: I risultati sono posizionati come rilevanti per lo studio delle logiche predicate intermedie, suggerendo profonde connessioni con proprietà come il Teorema di Herbrand e l'interpolazione nei frammenti a una variabile delle logiche predicative intuitionistiche.
4. Applicabilità Pratica: Lo sviluppo di una procedura di ricerca di prove terminante con generazione di contromodelli offre uno strumento pratico per verificare le proprietà in sistemi che coinvolgono l'incertezza graduata, la rappresentazione della conoscenza e i sistemi multi-agente.

Gli autori osservano che, sebbene l'approccio funzioni bene per i modelli testimoniati, trattare le logiche modali di Gödel con modelli non testimiati rimane un problema aperto significativamente più complesso. Il lavoro futuro include l'estensione della procedura ad altre logiche testimoniate con vincoli di frame aggiuntivi (riflessività, transitività) e lo sviluppo di una semantica Kripke birelazionale per GW.