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

Technische Samenvatting: Lindström-maximaliteit voor de eindige Heyting-gewaardeerde modale logica van Fitting met exacte waarheidstesten

Probleemstelling
Het artikel behandelt de karakterisering van de expressieve kracht van meerwaardige modale logica's, specifiek de modale logica van Fitting over een vaste eindige Heyting-algebra ($L$). Terwijl Lindström-stijl maximaliteitsstellingen bestaan voor klassieke modale logica en voor meerwaardige logica over eindige MTL-ketens (lineair geordende algebra's), ontbrak een overeenkomend resultaat voor het niet-lineaire geval. Vorig werk door Badia en Olkhovikov stelde maximaliteit vast over eindige MTL-ketens door gebruik te maken van de unieke directe voorganger van het bovenste element (1) om gedesignerde waarden van niet-gedesignerde waarden te scheiden. Deze benadering faalt voor willekeurige eindige Heyting-algebra's, die mogelijk geen lineariteit of een enkele coatoom onder 1 bezitten. Het centrale probleem is om te bepalen of Maruyama's presentatie van Fitting's logica — die unary exacte waarheidstesten ($T_\ell$) gebruikt in plaats van primitieve waarheid constanten voor alle waarden — zijn maximaliteit behoudt onder abstracte uitbreidingen zonder een algebra als keten te veronderstellen.

Methodologie
De auteur hanteert een modeltheoretische benadering, aangepast van klassieke en meerwaardige Lindström-stellingen. De methodologie omvat:

1. Definiëren van de basislogica: Gebruikmaken van Maruyama's versie van Fitting's logica ($FML_L$) over crisp Kripke-frames, waarbij formules waarden aannemen in een eindige Heyting-algebra $L$. De taal bevat exacte waarheidstesten $T_\ell$ zodanig dat $T_\ell \phi$ de waarde 1 aanneemt indien en slechts indien $\phi$ de waarde $\ell$ aanneemt.
2. Introductie van afgeleide Booleaanse operatoren: Om de keten-afhankelijke scheidingsmechanisme te vervangen, definieert de auteur Booleaanse-gewaardeerde testen:
   • $D\phi := T_1\phi$ (Waar indien $\phi$ gedesigneerd/gelijk aan 1 is).
   • $N\phi := T_0(T_1\phi)$ (Waar indien $\phi$ niet-gedesigneerd/niet gelijk aan 1 is).
   • Een afgeleide existentiële modaliteit $\Diamond_1 \phi := T_0(\Box N\phi)$, die het bestaan uitdrukt van een toegankelijke toestand waar $\phi$ de waarde 1 heeft.
3. Abstracte uitbreidingen: Het artikel beschouwt abstracte uitbreidingen $\mathcal{L}$ van $FML_L$ die drie modeltheoretische eigenschappen bevredigen: Compactheid, de Tarski-unie-eigenschap en sterke invariantie onder bisimulatie.
4. Verzadiging en Unravelling: Het bewijs construeert verzadigde elementaire uitbreidingen met behulp van unravelling-technieken. Het maakt gebruik van de afgeleide modaliteit $\Diamond_1$ om "opvolgerstypen" te definiëren en gebruikt de Compactheid en de Tarski-unie-eigenschappen om modellen te bouwen waarin deze typen gerealiseerd worden.
5. De Beslissingslemma: Een cruciale stap is een "Beslissingslemma" dat het paar $(D\psi, N\psi)$ gebruikt om elke hypothetische nieuwe formule van de basislogica te scheiden. Dit vervangt het argument van de "directe voorganger van 1" dat gebruikt wordt in keten-gebaseerde bewijzen.

Belangrijkste Bijdragen en Resultaten

• Lindström-maximaliteitsstelling: Het primaire resultaat (Stelling 1) stelt dat voor elke vaste eindige Heyting-algebra $L$, Maruyama's versie van Fitting's modale logica maximaal is met betrekking tot 1-expressieve kracht onder al haar abstracte uitbreidingen die compact zijn, de Tarski-unie-eigenschap bezitten en sterk invariant zijn onder bisimulatie.
• Verwijdering van de Lineariteitsveronderstelling: Het artikel generaliseert het maximaliteitsresultaat succesvol van de beperkende setting van eindige ketens naar de bredere klasse van willekeurige eindige Heyting-algebra's. Het bewijs toont aan dat de exacte waarheidstesten voldoende scheidingskracht bieden zonder een lineaire ordening of een onderscheiden coatoom te vereisen.
• Exact-waarde Definieerbaarheid: Als gevolg van de maximaliteitsstelling (Corollary 1) bewijst het artikel dat voor elke formule $\phi$ in een uitbreiding $\mathcal{L}$ en elke waarde $\ell \in L$, de verzameling gepunteerde modellen waar $\phi$ de exacte waarde $\ell$ aanneemt, definieerbaar is door een formule in de basislogica $FML_L$. Specifiek is de "exact-waarde vezel" definieerbaar, hoewel het artikel opmerkt dat dit niet noodzakelijkerwijs de existentie impliceert van een enkele formule in $FML_L$ die de volledige $L$-gewaardeerde semantiek van $\phi$ reproduceert.
• Hennessy-Milner Eigenschap voor Verzadigde Modellen: Het artikel stelt vast dat voor $FML_L$-verzadigde modellen modale equivalentie bisimulatie impliceert, waarmee het standaard Hennessy-Milner fenomenen uitbreidt naar deze meerwaardige setting.

Betekenis en Claims
Het artikel claimt de kloof in de literatuur over de expressieve grenzen van meerwaardige modale logica's over niet-lineaire algebra's te hebben opgelost. Door aan te tonen dat de exacte waarheidstesten ($T_\ell$) Booleaanse beslissingsparen ($D\phi, N\phi$) opleveren die in staat zijn gedesignerde van niet-gedesignerde waarden te scheiden, laat de auteur zien dat de structurele beperkingen van de onderliggende algebra (specifiek lineariteit) niet noodzakelijk zijn voor Lindström-maximaliteit.

De betekenis ligt in:

1. Generalisatie: Het uitbreiden van de reikwijdte van Lindström-stellingen voorbij de restrictieve setting van eindige ketens naar de bredere klasse van eindige Heyting-algebra's.
2. Mechanisme Identificatie: Het identificeren van de Booleaanse-gewaardeerde testen afgeleid van de exacte waarheidstesten als het cruciale mechanisme voor waarde-scheiding en verzadigingsargumenten in niet-lineaire settings.
3. Definieerbaarheid: Het vaststellen dat de basislogica voldoende expressief is om de exacte-waarde vezels van elke formule in een "redelijke" uitbreiding te definiëren, wat de robuustheid van Maruyama's presentatie versterkt.

De auteur blijft bescheiden over toekomstige richtingen en merkt openstaande vragen op, zoals of de Tarski-unie-eigenschap kan worden verzwakt, hoe men $L$-gewaardeerde (fuzzy) toegankelijkheidsrelaties kan behandelen, en of de afzonderlijke exacte-waarde definities kunnen worden verenigd in een enkele formule die de volledige semantiek reproduceert.