Most Properties are Undecidable for Transitive Tense Logics

Technische Samenvatting: De meeste eigenschappen zijn onbeslisbaar voor transitieve tense logica

Probleemstelling
Het artikel behandelt de algoritmische beslisbaarheid van logische eigenschappen binnen het rooster van transitieve tense logica, aangeduid als $NExtK4t$. Hoewel de beslisbaarheid van eigenschappen (zoals Kripke-volledigheid, de eindige modeleigenschap en beslisbaarheid zelf) goed bestudeerd is voor unimodale logica en lineaire tense logica, blijft de status van deze eigenschappen in de intermediaire klasse van transitieve tense logica een kritieke open vraag. Specifiek onderzoeken de auteurs of de natuurlijke interactie tussen de toekomstige ($\Box$) en verleden ($\blacksquare$) modaliteiten in transitieve frames de beslisbaarheid van het probleem voor deze eigenschappen onbeslisbaar maakt. Voorgaand werk door Chagrov en Shehtman stelde de onbeslisbaarheid van tabulariteit en consistentie in $NExtK4t$ vast, maar de beslisbaarheid van Kripke-volledigheid, de eindige modeleigenschap (FMP) en algemene beslisbaarheid bleef onopgelost.

Methodologie
De auteurs passen een reductietechniek aan die oorspronkelijk door Chagrov voor unimodale logica werd ontwikkeld, en breiden deze uit naar de bimodale setting van tense logica. De kernmethode houdt het construeren van een berekenbare reductie in van het bereikbaarheidsprobleem van Minsky-machines (een bekend onbeslisbaar probleem dat equivalent is aan het haltingprobleem voor Turingmachines) naar het beslissingsprobleem voor specifieke logische eigenschappen.

1. Minsky Machine Codering: De auteurs maken gebruik van een Minsky-machine $M$ met twee registers en een specifieke configuratie $c_0 = \langle s, n, m \rangle$ zodanig dat de verzameling bereikbare configuraties onbeslisbaar is.
2. Generale Frame Constructie: Een specifieke generale frame $\mathcal{F} = (W, R, A)$ wordt geconstrueerd. Het domein $W$ codeert de bereikbare configuraties van $M$ samen met hulppunten ($a_i, b_i, c_i$) die de registerwaarden en een "teller"-structuur representeren. De toegankelijkheidsrelatie $R$ wordt gedefinieerd om de transities van de Minsky-machine en de increment/decrement operaties op de registers te simuleren.
3. Formule Constructie: De auteurs definiëren een verzameling variabellevrije formules ($\phi_{c_n}, \phi_{a_n}, \phi_{b_n}$) die specifieke punten in het frame $\mathcal{F}$ uniek identificeren. Verder definiëren zij formules $\psi_A, \psi_B$ en hun opvolgers om de $+1$ en $-1$ operaties op de registers te simuleren.
4. Logica Constructie: Voor elke configuratie $c = \langle t, k, l \rangle$ wordt een logica $L(c)$ gedefinieerd als een uitbreiding van $K4t$. Deze logica bevat:
   • Axioma's ($Ax_M$) die de transitie-regels van de Minsky-machine coderen.
   • Een conditioneel axioma dat de initiële configuratie verbindt met de doelconfiguratie $c$.
   • Een specifieke formule $\alpha$ (afgeleid van een tabulaire logica) en een "trap"-formule $\phi_0$, ontworpen om te garanderen dat als de doelconfiguratie niet bereikbaar is, de resulterende logica Kripke-onvolledig en onbeslisbaar is.

Belangrijkste Bijdragen en Resultaten
Het artikel stelt een algemeen criterium vast (Stelling 3.5) voor de onbeslisbaarheid van eigenschappen in $NExtK4t$. De stelling stelt dat indien een eigenschap $P$ deel uitmaakt van de vereniging van Kripke-volledigheid ($KC$) en beslisbaarheid ($DEC$), en er een formule $\alpha$ bestaat zodanig dat $K4t \oplus \alpha \in P$ maar de geconstrueerde frame $\mathcal{F}$ $\alpha$ niet valideert, dan is $P$ onbeslisbaar.

Door deze stelling toe te passen, bewijzen de auteurs de volgende resultaten (Corollary 3.13):

• De volgende verzamelingen formules zijn onbeslisbaar in $NExtK4t$:
  1. Kripke-volledigheid.
  2. Canoniciteit.
  3. Eerstelijns definieerbaarheid.
  4. De eindige modeleigenschap (FMP).
  5. Lokale tabulariteit.
  6. Tabulariteit.
  7. Beslisbaarheid (van de logica zelf).
  8. Coïncidentie met een vaste tabulaire logica.
  9. Consistentie (specifiek, het complement, inconsistentie, is onbeslisbaar).

Verder merken de auteurs via Propositie 2.2 op dat, aangezien $K4t$ een uitbreiding is van $Kt$ (de minimale tense logica), deze onbeslisbaarheidsresultaten zich uitstrekken tot het rooster $NExtKt$.

Betekenis en Claims
Het artikel beweert de beslisbaarheidsstatus van belangrijke logische eigenschappen voor transitieve tense logica te hebben opgelost, waarmee wordt aangetoond dat "de meeste eigenschappen onbeslisbaar zijn" in deze klasse. De betekenis ligt in het verhelderen van hoe de interactie van modaliteiten de beslisbaarheid beïnvloedt:

• Contrast met Lineaire Tijd: Terwijl eigenschappen beslisbaar zijn in het rooster van lineaire tijdsstromen ($NExtLint$), leidt de introductie van transitiviteit zonder lineariteit ($NExtK4t$) tot onbeslisbaarheid.
• Contrast met Unimodale Logica: De resultaten benadrukken dat de minimale tense extensie-afbeelding eigenschappen zoals Kripke-volledigheid of FMP niet behoudt, waardoor de bimodale casus fundamenteel anders en complexer is dan de unimodale casus ($NExtK4$).
• Algemeen Schema: Het artikel biedt een algemeen bewijs-schema voor het vaststellen van onbeslisbaarheid in tense logica door de bereikbaarheid van Minsky-machines te reduceren naar logische eigenschappen, waarmee het gat vult dat achtergelaten is door voorgaande werken die de onbeslisbaarheid van unimodale logica niet direct konden overbrengen naar de tense setting vanwege de niet-injectiviteit van de tense extensie-afbeelding.

De auteurs concluderen dat de interacties van modaliteiten in transitieve tense logica het beslissingsprobleem voor eigenschappen strikter moeilijker maken dan in lineaire tense logica, en suggereren dat voor eigenschappen zoals Kripke-volledigheid, onbeslisbaarheid in een unimodale lattice waarschijnlijk onbeslisbaarheid in de minimale tense extensie daarvan impliceert, hoewel dit een vermoeden blijft voor toekomstig werk.