March 3, 2026Open Access

Finite tree-like model property for multi-modal logic in Isabelle/HOLZF

Key Points

The finite tree-like model property is established, ensuring structures of satisfiable formulas are restricted.
Key findings show this property applies to families of modal operators, emphasizing structural constraints.
Formalization was achieved through Isabelle/HOL's HOLZF extension, ensuring the model property is type-independent.
These findings may enable further investigations into multi-modal logic applications across various fields.

Abstract

We describe an Isabelle formalization of the finite tree-like model property of multi-modal logic, which considers families of modal operators. This property can be used to restrict structures that are models of satisfiable formulas to be "finite tree-like". We use Isabelle/HOL's HOLZF extension to prove the theorem independently of the type underlying the structures.

Finite tree-like model property for multi-modal logic in Isabelle/HOLZF

Key Points

Abstract

Cite This Study