Lindström Maximality for Fitting's Finite Heyting-Valued Modal Logic with Exact Truth Tests

Sintesi Tecnica: Massimalità di Lindström per la Logica Modale di Fitting con Test di Verità Esatti su un'Algebra di Heyting Finita

Enunciato del Problema
Il saggio affronta la caratterizzazione del potere espressivo delle logiche modali multivalenti, nello specifico la logica modale di Fitting su un'algebra di Heyting finita fissata ($L$). Mentre esistono teoremi di massimalità in stile Lindström per la logica modale classica e per le logiche multivalenti su catene finite di MTL (algebre linearmente ordinate), un corrispondente risultato mancava per il caso non lineare. Il lavoro precedente di Badia e Olkhovikov ha stabilito la massimalità sulle catene MTL finite utilizzando l'unico predecessore immediato dell'elemento superiore (1) per separare i valori designati da quelli non designati. Questo approccio fallisce per arbitrarie algebre di Heyting finite, che possono mancare di linearità e di un singolo coatomo sotto 1. Il problema centrale è determinare se la presentazione della logica di Fitting di Maruyama — che utilizza test di verità unari esatti ($T_\ell$) invece di costanti di verità primitive per tutti i valori — mantenga la massimalità tra le sue estensioni astratte senza assumere che l'algebra sia una catena.

Metodologia
L'autore impiega un approccio modello-teoretico adattato dai teoremi di Lindström classici e multivalenti. La metodologia prevede:

1. Definizione della Logica di Base: Utilizzando la versione di Maruyama della logica di Fitting ($FML_L$) su frame di Kripke "crisp", dove le formule assumono valori in un'algebra di Heyting finita $L$. Il linguaggio include test di verità esatti $T_\ell$ tali che $T_\ell \phi$ valuta a 1 se e solo se $\phi$ valuta a $\ell$.
2. Introduzione di Operatori Booleani Derivati: Per sostituire il meccanismo di separazione dipendente dalla catena, l'autore definisce i test a valore Booleano:
   • $D\phi := T_1\phi$ (Vero se $\phi$ è designato/uguale a 1).
   • $N\phi := T_0(T_1\phi)$ (Vero se $\phi$ è non designato/non uguale a 1).
   • Una modalità esistenziale derivata $\Diamond_1 \phi := T_0(\Box N\phi)$, che esprime l'esistenza di uno stato accessibile in cui $\phi$ ha valore 1.
3. Estensioni Astratte: Il saggio considera estensioni astratte $\mathcal{L}$ di $FML_L$ che soddisfano tre proprietà modello-teoretiche: Compattezza, la Proprietà di Unione di Tarski e la forte invarianza sotto bisimulazione.
4. Saturazione e Srotolamento (Unravelling): La dimostrazione costruisce estensioni elementari saturate utilizzando tecniche di srotolamento. Essa sfrutta la modalità derivata $\Diamond_1$ per definire "tipi successori" e utilizza la Compattezza e la Proprietà di Unione di Tarski per costruire modelli in cui tali tipi siano realizzati.
5. Il Lemma Decisionale: Un passaggio critico coinvolge un "Lemma Decisionale" che utilizza la coppia $(D\psi, N\psi)$ per separare qualsiasi nuova formula dalla logica di base. Questo sostituisce l'argomento del "predecessore immediato di 1" utilizzato nelle dimostrazioni basate su catene.

Contributi Chiave e Risultati

• Teorema di Massimalità di Lindström: Il risultato primario (Teorema 1) afferma che, per ogni data algebra di Heyting finita $L$, la versione di Maruyama della logica di Fitting è massimale rispetto al potere espressivo 1 tra tutte le sue estensioni astratte che sono compatte, possiedono la Proprietà di Unione di Tarski e sono fortemente invarianti sotto bisimulazione.
• Rimozione dell'Assunzione di Linearità: Il saggio riesce a generalizzare il risultato di massimalità dalle algebre linearmente ordinate (catene MTL) alle arbitrarie algebre di Heyting finite. La dimostrazione mostra che i test di verità esatti forniscono un potere di separazione sufficiente senza richiedere un ordine lineare o un coatomo distinto.
• Definibilità del Valore Esatto: Come conseguenza del teorema di massimalità (Corollario 1), il saggio dimostra che per ogni formula $\phi$ in un'estensione $\mathcal{L}$ e per ogni valore $\ell \in L$, l'insieme dei modelli puntati in cui $\phi$ assume il valore esatto $\ell$ è definibile tramite una formula nella logica di base $FML_L$. Nello specifico, la "fibra del valore esatto" è definibile, sebbene il saggio noti che ciò non implica necessariamente l'esistenza di una singola formula in $FML_L$ capace di riprodurre la piena semantica di $\phi$.
• Proprietà di Hennessy-Milner per Modelli Saturi: Il saggio stabilisce che per i modelli saturi di $FML_L$, l'equivalenza modale implica la bisimulazione, estendendo i normali fenomeni di Hennessy-Milner a questo contesto multivalente.

Significatività e Rivendicazioni
Il saggio sostiene di aver risolto una lacuna nella letteratura riguardante i limiti espressivi delle logiche modali multivalenti su algebre non lineari. Dimostrando che i test di verità esatti ($T_\ell$) producono coppie decisionali booleane ($D\phi, N\phi$) capaci di separare i valori designati da quelli non designati, l'autore mostra che i vincoli strutturali dell'algebra sottostante (specificamente la linearità) non sono necessari per la massimalità di Lindström.

La significatività risiede in:

1. Generalizzazione: Estendere l'ambito dei teoremi di Lindström oltre l'impostazione restrittiva delle catene finite verso la classe più ampia delle algebre di Heyting finite.
2. Identificazione del Meccanismo: Identificare i test a valore Booleano derivati dai test di verità esatti come il meccanismo cruciale per la separazione dei valori e gli argomenti di saturazione in contesti non lineari.
3. Definibilità: Stabilire che la logica di base è sufficientemente espressiva da definire le fibre dei valori esatti di qualsiasi formula in un'estensione "ragionevole", rafforzando la robustezza della presentazione di Maruyama.

L'autore rimane modesto riguardo alle direzioni future, menzionando questioni aperte quali se la Proprietà di Unione di Tarski possa essere indebolita, come gestire le relazioni di accessibilità $L$-valutate (fuzzy) e se le definizioni separate dei valori esatti possano essere unificate in una singola formula che riproduca la piena semantica.