A Gödel Modal Logic Over Witnessed Models

Technische Samenvatting: Een Gödel Modale Logica over Gewitnessed Modellen

Probleemstelling
Gödel modale logica's (GKs) bieden een raamwerk voor het redeneren over gegradeerde concepten van incompletheid en vaagheid met behulp van noodzakelijkheid ($\Box$) en mogelijkheid ($\Diamond$) operatoren, geëvalueerd over het reële eenheidsinterval $[0,1]$. De standaardsemantiek voor deze logica's berust op Gödel Kripke-modellen (G-modellen), waarbij de waarheidswaarde van een modale formule wordt gedefinieerd door het infimum of supremum van de waarheidswaarden over toegankelijke werelden. Een kritieke beperking van deze standaardsemantiek is dat deze grenzen niet noodzakelijkerwijs bereikt worden door een specifieke toegankelijke wereld. Dit "limiet-gebaseerde" fenomeen leidt tot significante logische pathologieën: de logica bezit geen Eindige Model Eigenschap (FMP), en bepaalde validiteiten in eindige modellen (bijv. $\Box\neg\neg\phi \to \neg\Box\phi$) falen in oneindige modellen. Bijgevolg vereisen semantische argumenten vaak werkelijk infinitaire processen, wat automatische redeneren en bewijs-theoretische analyse bemoeilijkt.

Methodologie
De auteurs introduceren GW, een Gödel modale logica gebaseerd op gewitnessed modellen (getuige-modellen). In een GW-model wordt de semantiek van modale operatoren zodanig beperkt dat het infimum en supremum dat de waarheidswaarden van $\Box\phi$ en $\Diamond\phi$ definiëren, door ten minste één toegankelijke wereld (een "getuige" of "witness") moet worden bereikt. Dit zorgt ervoor dat de waarheidswaarde van een modale formule wordt bepaald door concrete werelden in plaats van asymptotische benaderingen.

Om GW te analyseren, ontwikkelen de auteurs een constraint-gebaseerde weerleggingscalculus genaamd CGW. De methodologie omvat:

1. Constraint Taal: Formula's worden vertaald naar constraints over een aftelbare verzameling labels die werelden representeren. Deze constraints omvatten atomaire termen (werelden, toegankelijkheidsrelaties $R$, en propositionele evaluaties) en relaties ($<, \le, >, \ge$) over rationale getallen in $[0,1]$.
2. Weerleggingscalculus: CGW is ontworpen om te certificeren dat een formule niet geldig is in enig GW-model. Het maakt gebruik van propositionele regels, modale regels (die nieuwe labels introduceren voor getuigen) en regels voor de toegankelijkheidsrelatie ($R$-regels).
3. Bewijszoeking en Tegenmodelgeneratie: De auteurs ontwerpen een terminerende backward proof-search procedure. Als de zoekopdracht faalt in het afleiden van een contradictie, volgt de procedure de berekening om een eindig tegenmodel (specifiek, een discrete GW-model) voor de invoerformule te construeren.
4. Complexiteitsanalyse: Een PSPACE beslissingsprocedure wordt geschetst, waarbij een recursieve zoekopdracht wordt gebruikt die de toewijzing van waarheidswaarden aan subformula's beheert zonder het volledige model expliciet in het geheugen op te slaan.

Kernbijdragen

• Definitie van GW: De formalisering van Gödel modale logica over witnessed Kripke-modellen, waarbij onderscheid wordt gemaakt met de standaard GK en de crisp variant $GW^c$.
• Calculus CGW: De presentatie van een sound en complete weerleggingscalculus voor GW. De calculus behandelt de specifieke constraints van witnessed semantiek, met name de vereiste dat grenzen bereikt moeten worden.
• Eindige Model Eigenschap (FMP): De auteurs bewijzen dat GW de FMP bezit als een direct gevolg van de terminerende proof-search procedure. Indien een formule niet geldig is, bestaat er een eindig tegenmodel. Dit staat in contrast met de standaard GK, die de FMP mist.
• Inbedding en Niet-interdefinieerbaarheid:
  • Het artikel toont aan dat klassieke modale logica K ingebed kan worden in GW (en gerelateerde logica's) via een vertaling die gebruikmaakt van dubbele negatie.
  • Het bewijst dat $\Box$ en $\Diamond$ niet interdefinieerbaar zijn in enige modale logica die binnen $GW^c$ valt, waarmee eerdere resultaten bekend van crisp modellen worden uitgebreid.
• Complexiteitsresultaten: De validiteit van GW wordt vastgesteld als PSPACE-compleet. De ondergrens volgt uit de inbedding van K, en de bovengrens wordt afgeleid van de PSPACE-procedure voor tegenmodel-existentie.
• Implementatie: Een prototype prover genaamd gwref is geïmplementeerd, gebruikmakend van de JTabWb engine en de Choco-solver voor constraint consistentie-checks.

Resultaten

• Soundness en Compleetheid: CGW is bewezen sound en compleet met betrekking tot GW-modellen. Een formule $\phi$ is geldig in GW dan en slechts dan als de constraint set $\{w : \phi < 1\}$ niet bewijsbaar is in CGW.
• Terminatie: De calculus is sterk terminerend. Een well-founded relatie op multisets van constraints garandeert dat elke backward proof search stopt.
• Extractie van Tegenmodellen: Wanneer de proof search faalt, construeert de procedure een discreet tegenmodel met een grootte begrensd door $O(|\phi|^{| \phi |})$.
• Logische Hiërarchie: Het artikel verheldert de relaties tussen diverse logica's: $GK \subset G^c \subset GW^c$ en $GK \subset GW \subset GW^c$. Het toont aan dat de "Crisp" axioma (geldig in $G^c$) niet geldig is in $GW$, en dat het "Witnessed" axioma ($\Box\neg\neg\alpha \to \neg\neg\Box\alpha$) wel geldig is in $GW$ maar niet in $G^c$.

Significantie
Het artikel betoogt dat witnessed semantiek een principiële manier biedt om de problemen geassocieerd met limiet-gebaseerde fenomenen in fuzzy modale logica's te overwinnen. Door te garanderen dat existentiële en universele gedragingen worden ondersteund door expliciete getuigen, weerspiegelt de semantiek van GW de guarded kwantificatie in de eerste-orde logica nauwer en herstelt het een constructieve interpretatie.

De significantie van dit werk ligt in:

1. Herstel van Constructieve Eigenschappen: De FMP en de decidability resultaten maken GW geschikt voor automatisch redeneren, waardoor infinitaire semantische argumenten vervangen kunnen worden door eindige combinatorische argumenten.
2. Bewijs-theoretische Uitlijning: De witnessed semantiek sluit nauwer aan bij syntactische calculi, wat de constructie van canonieke modellen en standaard volledigheidsproeven vergemakkelijkt.
3. Verbindingen met Intermediaire Logica's: De resultaten zijn relevant voor de studie van intermediaire predicatenlogica's, wat wijst op diepe verbanden met eigenschappen zoals de Stelling van Herbrand en interpolatie in een-variabele fragmenten van intuïtionistische predicatenlogica's.
4. Praktische Toepasbaarheid: De ontwikkeling van een terminerende proof-search procedure met tegenmodelgeneratie biedt een praktisch instrument voor het verifiëren van eigenschappen in systemen die betrokken zijn bij gegradeerde onzekerheid, kennisrepresentatie en multi-agent systemen.

De auteurs merken op dat hoewel de aanpak goed werkt voor witnessed modellen, het behandelen van Gödel modale logica's met niet-witnessed modellen een aanzienlijk uitdagender openstaand probleem blijft. Toekomstig werk omvat het uitbreiden van de procedure naar andere witnessed logica's met aanvullende frame-constraints (reflexiviteit, transitiviteit) en het ontwikkelen van een birelationele Kripke-semantiek voor GW.