Intuitionistic modal logic shown to have finite model property
Fine Selection for Intuitionistic Modal Logic
Logic in Computer Science
Summary
The paper deals with a complex type of logic called intuitionistic modal logic, which combines reasoning about truth and possibility in a certain constructive way. The authors extended a method originally developed by Fine to this type of logic. Using this extension, they provide a mathematical proof that a specific form of this logic called Fischer Servi-style intuitionistic K4 always has a finite model that fits it, which is important for understanding its behavior and how it can be computed or checked. This kind of finite model property is a desirable feature for logical systems.
What this means in practice
- •For logic system designers: Design formal systems and verification tools knowing that Fischer Servi-style intuitionistic K4 logic models are finitely representable.
- •For program verification engineers: Use the finite model property in reasoning engines for programs based on constructive modal logics to improve model checking efficiency.
A theory result. No direct application yet.
Authors
David Fernández-Duque
Abstract
We extend Fine's selection method to the setting of intuitionistic modal logic and use it to provide a model-theoretic proof that Fischer Servi-style intuitionistic $\sf K4$ has the finite model property.