A Gödel Modal Logic Over Witnessed Models

Mauro Ferrari; Camillo Fiorentini; Paolo Giardini; Ricardo Oscar Rodriguez

doi:10.4204/EPTCS.447.20

A Gödel Modal Logic Over Witnessed Models

Logic in Computer Science 2026-06-30 v1

Authors: Mauro Ferrari , Camillo Fiorentini , Paolo Giardini , Ricardo Oscar Rodriguez

View on arXiv ↗ PDF ↗ DOI ↗

Abstract

We introduce GW, a G\"odel modal logic based on Kripke models in which the value of each modal formula is witnessed by an accessible world. This witnessed semantics eliminates the limit-based phenomena that preclude the finite model property in the usual Kripke semantics for G\"odel modal logics, thereby yielding a more constructive semantic framework. We present a sound and complete refutation calculus for GW and design a terminating backward proof-search procedure with countermodel generation. As a direct consequence of this procedure, GW enjoys the finite model property.

Keywords

Gödel modal logic witnessed semantics Kripke models refutation calculus proof search finite model property

Cite

@article{arxiv.2606.31906,
  title  = {A Gödel Modal Logic Over Witnessed Models},
  author = {Mauro Ferrari and Camillo Fiorentini and Paolo Giardini and Ricardo Oscar Rodriguez},
  journal= {arXiv preprint arXiv:2606.31906},
  year   = {2026}
}

Comments

In Proceedings AiML 2026, arXiv:2606.29444