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

Yiming Xu, Jasmin Blanchette, Sophie Tourret

<figure><img src="image_1.png" /></figure>

► To cite this version:

Yiming Xu, Jasmin Blanchette, Sophie Tourret. Finite tree-like model property for multi-modal logic in Isabelle/HOLZF. 2026. hal-05494076v2

HAL Id: hal-05494076

https://hal.science/hal-05494076v2

Preprint submitted on 5 Feb 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
FINITE TREE-LIKE MODEL PROPERTY FOR MULTI-MODAL LOGIC
IN ISABELLE/HOLZF

YIMING XU<sup>a</sup>, JASMIN BLANCHETTE<sup>a</sup>, AND SOPHIE TOURRET<sup>b</sup>

<sup>a</sup> Ludwig-Maximilians-Universität München
*e-mail address:* yiming.xu@lmu.de, jasmin.blanchette@ifi.lmu.de

<sup>b</sup> Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
*e-mail address:* sophie.tourret@loria.fr

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.

INTRODUCTION

As a well-established framework for talking about relational structures, propositional modal
logic has been used and investigated for decades [BRV01, Sid10, NHPD23]. Clearly, modal
logic deserves the attention of the formalization community. There are two angles to approach
this challenge. The first is through the prism of syntax, by investigating logic calculi [Fro18].
The second is through the prism of semantics, by investigating the model theory associated
with the logic of interest [XN20].

Here we follow the semantics angle by formalizing propositional modal model theory.
We carry out the work using Isabelle/HOLZF, an extension of Isabelle's higher-order logic
(HOL) with the Zermelo-Fraenkel (ZF) set theory axioms. We chose Isabelle for several
reasons. First, Isabelle/HOL is a trustworthy proof assistant that offers a good balance
between expressiveness and proof automation. Second, the Isabelle community has already
built IsaFoL, a large library on the formalization of logic [Bla19] and an even larger library
of third-party contributions, the *Archive of Formal Proofs* (AFP) [BHMN15], that we want
to contribute to so that this work is easy to reuse.¹ Finally, Isabelle offers the structured
Isar proof language [Wen07], improving the human readability of proofs over proof scripts,
and includes advanced automation that saves time and effort [BBN11a].

The final milestone in our development is the rather complex proof of the finite tree-like
model property. Informally, this property states that if a modal formula is satisfiable, then
it is satisfied in a finite tree-like structure. This property is valuable because if a modal logic
has the finite model property and is finitely axiomatizable, then it is decidable [BRV01].

Key words and phrases: optional comma separated list of keywords.

¹Our formalization is available as anonymous supplementary material. We will submit it to the AFP following the reviewing process. The archive includes a README file that connects the code to the paper.
Our formal development loosely follows the sketches presented in the textbook by Blackburn et al. [BRV01] and generalizes parts of a HOL4 formalization by Xu and Norrish [XN20]. Briefly, our main contributions are as follows:

* We formalize the syntax and semantics of the general theory of multi-modal logic, considering any propositional modal language and any family of relations for arbitrary arities. Our formalization is the first step toward a reusable library for modal model theory.

* We provide a formal proof of the finiteness of modal formulas in a finite signature of degree at most $k$.

* We formalize a central result in modal model theory—the finite tree-like model property in a general form—demonstrating the usability of our definitions.

* By using ZF axioms, we restrict our interest to the class of models with an underlying ZF set, and hence avoid the unpleasant change of types that arises in the construction of the finite structure.

The part of our work that uses ZF is built on top of, and kept separated from, the rest of our formulation of modal model theory in HOL. Our formalization code is available from

https://github.com/u5943321/Tree-Like-Model-Property

For formalizations to be broadly applicable, generic approaches are desirable. Thus, instead of treating the modal language for only one binary relation, we reserve a parameter for the modal signature and allow the syntax to reason about any number of modal operators corresponding to relations of any finite arity. Such modal operators correspond to multi-relational structures. In this way, our result is applicable to most propositional modal logics.

This paper is organized as follows. In Section 1, we formally define the syntax and semantics of propositional modal logic, explaining our choices. In Section 2, we discuss formula equivalence and prove two related theorems. In Section 3, we formalize the notion of tree-like frames. In Section 4, we formalize the construction of the finite tree-like model. In Section 5, we explain HOLZF and use it to avoid a type issue. In Section 6, we discuss related work. Finally, we summarize the paper and suggest directions for future research.

# 1. SYNTAX AND SEMANTICS

This section recapitulates the syntax and semantics of propositional modal logic; we refer to Blackburn et al. [BRV01] for more details. In propositional modal logic, a formula can be false (denoted by $\perp$), a propositional letter, a disjunction, a negation, or a *triangle formula*, i.e., a modal operator $\Delta_m$, where $m: 'm$, applied to a list $fl$ of formulas:

$$ ( 'm, 'p ) \text{ form } = \perp \mid \text{Var } 'p \mid ( 'm, 'p ) \text{ form } \lor ( 'm, 'p ) \text{ form } \mid \neg ( 'm, 'p ) \text{ form } \mid \Delta_{ 'm} ( 'm, 'p ) \text{ form list} $$

The type parameters are '$p$' for propositional variables and '$m$' for modal operators. In basic modal logic, '$m$' would be the unit type, with its unique term indexing the only modal operator $\diamond$. The *dual* of this modal operator is defined by $\Box\phi := \neg\diamond\neg\phi$ for each modal formula $\phi$. We can also have multiple modal operators indexed by a non-trivial type '$m$, a binary modal operator indexed by a natural number, say 0, applied on two modal formulas $\phi$ and $\psi$, is formalised as a term in our datatype as $\Delta_0[\phi, \psi]$. Using a type parameter for modal operators rather than indexing them with natural numbers gives more freedom to
specify them as needed. For instance, in PDL, one may want to construct an inductive type for modal operators [BRV01, Example 1.15].

We write ('m, 'p) sig to abbreviate a tuple $\tau = (O, \rho, \Pi)$, called a *signature*, where $O$ is an 'm set of modal operators, $\rho: 'm \Rightarrow N$ gives the arity of each operator, and $\Pi$ is a 'p set of propositional letters. The three components of $\tau$ are written ops $\tau$, arity $\tau$, and props $\tau$. We collect all modal operators and propositional letters occurring in a formula as sets using the functions **operators** and **pletters**.

**Definition 1.1.** A *well-formed* $\tau$-formula $\phi$ is defined as an inductive predicate wff. For $\tau = (O, \rho, \Pi)$

$$
\begin{align*}
\text{wff } \tau \perp &\leftrightarrow \text{True} \\
\text{wff } \tau (\text{Var } p) &\leftrightarrow p \in \Pi \\
\text{wff } \tau (\neg \phi) &\leftrightarrow \text{wff } \tau \phi \\
\text{wff } \tau (\phi \lor \psi) &\leftrightarrow \text{wff } \tau \phi \land \text{wff } \tau \psi \\
\text{wff } \tau (\Delta_m \text{fl}) &\leftrightarrow m \in O \land \text{length fl} = \rho m \land \forall \psi \in \text{set fl. wff } \tau \psi
\end{align*}
$$

The type ('m, 'p, 'a) **structure** of **structures** consists of tuples (*W*, *R*, *β*). The set *W* :: 'a set contains all possible worlds. It serves as our domain of discourse. We encode a family of relations using the term *R* :: 'm ⇒ 'a list ⇒ **bool**. We have *R* m *wl* if the relation *R* m holds on the list of worlds *wl* :: 'a list. The valuation function *β* :: 'p ⇒ 'a ⇒ **bool** is such that *β* p w holds if p is true on w. Given a structure *M*, we refer to its three components as world *M*, rel *M*, and valt *M*. When 'm and 'p are irrelevant or can be understood from the context, we call an ('m, 'p, 'a) structure an 'a-structure.

A structure *M* is a *τ*-structure if rel *M* m *wl* implies *m* ∈ *O*, set *wl* ⊆ *W*, and length *wl* = *ρ* m + 1, and if valt *M* p w implies *p* ∈ Π and *w* ∈ *W*. The predicate struct_on enforces this property in Isabelle. This means *R* and *β* provide no information about terms outside the world set or the signature. We define the satisfaction of a formula as follows.

**Definition 1.2.** Given a *τ*-structure *M*, a world *w*, a (not necessarily well-formed) formula *φ* is satisfied at *w* by *M*, denoted *M*, *w* ⊩<sub>*τ*</sub> *φ* in the following cases depending on the shape of *φ*:

$$
\begin{align*}
M, w \Vdash_{\tau} \perp &\leftrightarrow \text{False} \\
M, w \Vdash_{\tau} \text{Var } p &\leftrightarrow \text{valt } M p w \\
M, w \Vdash_{\tau} \neg \phi &\leftrightarrow w \in \text{world } M \wedge M, w, \Vdash_{\tau} \phi \\
M, w \Vdash_{\tau} \phi \lor \psi &\leftrightarrow M, w, \Vdash_{\tau} \phi \lor M, w, \Vdash_{\tau} \psi \\
M, w \Vdash_{\tau} \Delta_m \text{fl} &\leftrightarrow \exists \text{wl. } \begin{aligned}[t]
&\text{length } \text{wl} = \text{length } \text{fl} \wedge \\
&\text{rel } M m (w\#\text{wl}) \wedge \\
&\quad (\forall w' \phi. (w', \psi) \in \text{set } (\text{zip } \text{wl fl}). M, w' \Vdash_{\tau} \psi)
\end{aligned}
\end{align*}
$$

where $w\#wl$ denotes a list with $w$ as its head and $wl$ as its tail while **zip** is the usual zipping function on lists. The last condition corresponds to the one for diamonds in basic modal logic, while boxes can be obtained as the dual of diamonds. Definition 1.2 ensures that $M, w \Vdash_{\tau} \phi$ implies $w \in \text{world } M$ as long as $M$ is a $\tau$-structure. This is the *structure assumption*. Under this assumption, we can write formalized definitions and theorems without assuming $w \in \text{world } M$, that would clutter them and is generally implicit in Blackburn et al. [BRV01].

In practice, it is not necessary to explicitly introduce a signature when investigating
satisfaction. Every formula can simply be associated with the signature determined by the
symbols it contains. In practice, we usually prefer an equivalent definition of satisfaction presented below (that generalizes the one by Xu and Norrish [XN20]), denoted using $|-τ$ instead of $|-τ$ by extending Definition 1.2 for propositional letters and triangle formulas as follows, where the unchanged parts of the definition are grayed out:

$$ 
\begin{array}{l}
M, w \Vdash \text{Var } p \leftrightarrow w \in \text{world } M \wedge \text{valt } M pw \\
M, w \Vdash \Delta_m fl \leftrightarrow w \in \text{world } M \wedge m \in \text{ops } \tau \wedge \\
\quad \text{length } fl = \text{arity } \tau m \wedge \\
\quad \exists vl. \text{ length } vl = \text{length } fl \wedge \text{rel } M m (w \# vl) \wedge \\
\quad \forall x y. (x, y) \in \text{set}(\text{zip } vl fl) \rightarrow M, x \Vdash_{\tau} y
\end{array}
$$

Such a definition enables us to state theorems in a cleaner and more concise form by omitting assumptions on the signature and well-formedness.

We proved that the two definitions are interchangeable when $M$ is a $\tau$-structure:

**Lemma 1.3.** Given a signature $\tau$, a structure $M$ such that $\text{struct_on } \tau M$, a world $w$, and a formula $\phi$, we have that $M, w \Vdash_{\tau} \phi$ is equivalent to $M, w \Vdash \phi$.

Note that in Definition 1.2 as well as in its extension, it is necessary to check the membership condition for formulas of the form $\neg\phi$. Otherwise, $\neg p$ would be satisfied at any world $w$ with $\neg\text{valt } M pw$, even outside the world set $W$, and even for any propositional letter $p$ outside of the signature.

We use one or the other definition according to the situation. $M, w \Vdash_{\tau} \phi$ implies that $\phi$ is well formed in $\tau$ whereas $M, w \Vdash \phi$ does not. In practice, if we are verifying a statement made under the structure assumption, we use $|-\tau$ to reduce the number of conditions that must be checked in the proof. In other situations, using $|-\tau$ is generally preferable.

## 2. FORMULA EQUIVALENCE

The proof of the finite tree-like model property relies on two critical theorems concerning equivalence between modal formulas, introduced in Sections 2.1 and 2.2, respectively. The first of these is not present in Blackburn et al. [BRV01], whereas the second one is a generalization of their Theorem 2.29.

There are many ways to define “the formula $\phi_1$ is equivalent to $\phi_2$.” Possible formal definitions that would correspond to Blackburn et al. [BRV01] include

$$ 
\begin{array}{l}
\text{wff } \tau \phi_1 \wedge \text{wff } \tau \phi_2 \wedge (\forall M w. \text{struct_on } \tau M \rightarrow (M, w \Vdash_{\tau} \phi_1 \leftrightarrow M, w \Vdash_{\tau} \phi_2)) \\
\text{wff } \tau \phi_1 \wedge \text{wff } \tau \phi_2 \wedge (\forall M w. M, w \Vdash \phi_1 \leftrightarrow M, w \Vdash \phi_2) \\
\text{struct_on } \tau M \rightarrow (M, w \Vdash \phi_1 \leftrightarrow M, w \Vdash \phi_2) \\
M, w \Vdash_{\tau} \phi_1 \leftrightarrow M, w \Vdash_{\tau} \phi_2
\end{array}
$$

We choose the simplest approach:

**Definition 2.1.** Two modal formulas $\phi_1, \phi_2 :: ('m, 'p)$ form are equivalent over type 'a if, for every

$M :: ('m, 'p, 'a)$ structure and every $w$, we have $M, w \Vdash \phi_1 \leftrightarrow M, w \Vdash \phi_2$. In this case, we write $\phi_1 \equiv'a \phi_2$.
As noted by Xu and Norrish, higher-order logic does not allow quantification over the type $'a$, so the type parameter cannot be omitted in HOL4. This is also true in Isabelle/HOL. Although our definition works with multi-modal logics, it is superficially identical to theirs.

Given $A :: \text{'a}$ set and $\sim$, an equivalence relation on the entire universe of $'a$, we write $A/\sim$ to denote the partition of $A$ with respect to $\sim$. Thus we can write $A/\equiv_{\text{'a}}$ and $B/\equiv_{\text{'a}}$ for different sets of formulas without having to restrict $\equiv_{\text{'a}}$ to $A$ or $B$.

**2.1. Congruence condition for triangle formulas.** It is tempting to prove that two triangle formulas, $\Delta_m \fl$ and $\Delta_{m'} \gl$, are equivalent if and only if $m = m'$, the lengths of $\fl$ and $\gl$ are equal and for each $i < \text{length } \fl$, the formulas $\fl \! i$ (the $(i+1)$st element of $\fl$) and $\gl \! i$ are equivalent. In fact, this statement holds most of the time, but there are two exceptions:

* If any formula in the lists $\fl$ or $\gl$ is unsatisfiable (i.e., equivalent to $\bot$), then regardless of $m, m'$, and other formulas in the lists, the entire formula is equivalent to $\bot$.

* The result does not necessarily hold when the underlying type of the structures is finite.

We first focus on the second point. Consider the modal language with two distinct unary operators $\Delta_1$ and $\Delta_2$. Consider the formulas $\Delta_1\Delta_2\top$ and $\Delta_2\Delta_1\top$, and examine the structures $(W, R, \beta)$ where $W$ is a singleton of type Unit. The only possible relations $R$ on $W$ are the empty relation and the reflexive relation. Moreover, both formulas hold in such a structure if and only if the relation is reflexive. Hence we have $\Delta_1\Delta_2\top \equiv_{\text{Unit}} \Delta_2\Delta_1\top$, serving as a counterexample.

Assuming that the type universe of the structures is infinite eliminates this issue.

**Lemma 2.2.**

$$
\begin{array}{l}
\text{assumes infinite } (\mathit{UNIV} :: \text{'a} \text{ set}) \\
\quad \text{and } \bigwedge f. f \in \mathit{set} \ \mathit{fl} \implies \exists M (w :: \text{'a}). M, w \Vdash f \\
\quad \text{and } \Delta_m \ \mathit{fl} \equiv_{\text{'a}} \Delta_{m'} \ \mathit{gl} \\
\text{shows } m = m'
\end{array}
$$

*Proof.* Assume $m \neq m'$. We show $\Delta_m \fl \not\equiv_{\text{'a}} \Delta_{m'} \gl$ by constructing an '$a$-structure that witnesses this non-equivalence. We take a family of '$a$-structures and worlds such that $M_i, w_i \Vdash \fl \! i$ for all $i < n$, where $n = \text{length } \fl$. We embed such a family of structures into their *disjoint union*. Intuitively, the disjoint union puts the structures $M_i$ side by side and regards them as a large structure. Therefore, if a formula is satisfied at a world in a structure, then it is satisfied at its copy in the disjoint union. Here we index the family of structures to be taken as a disjoint union with a set of natural numbers. Consequently, the disjoint union $\cup_i M_i = (W, R, \beta)$ is a $(\mathbb{N} \times \text{'a})$-structure, and the embedding is given by $w_i \mapsto (i+1, w_i)$. We construct a structure $M' = (W', R', \beta')$ by defining $W' = \{(0, \text{undefined})\} \cup \{(i+1, w_i) \mid 0 \le i < n\}$, $\beta' = \beta$, and $R'$ such that $R' \text{ o } \text{vl}$ holds if and only if either $R \text{ o } \text{vl}$ holds or both $o = m$ and $\text{vl} = [(0, \text{undefined}), (1, w_0), \dots, (n, w_{n-1})]$. The structure $M'$ is as shown in Figure 1. We have

$M', (0, \text{undefined}) \Vdash \Delta_m \fl$ but, because there is no relation indexed by $m'$ from $(0, \text{undefined})$, we have

$M', (0, \text{undefined}) \Vdash \Delta_{m'} \gl$. The final step in the proof uses the infiniteness of '$a$: we have an injection $\mathbb{N} \times \text{'a} \to \text{'a}$, so we can inject $M'$ back to an '$a$-structure, serving as the witness of the required type. $\square$
<figure><img src="image_3.png" /><figcaption>Figure 1: The structure $M'$ constructed from the disjoint union. For all $i$ in $0...n-1$, $fl ! i$ is satisfied at $(i+1, w_i)$ in the copy of $M_i$ present in the disjoint union, which is injected to $M'$. The dashed lines denote the element added to the relation $R$ to obtain $R'$. This element connects all worlds in the list $[(0, undefined), (1, w_0), ..., (n, w_{n-1})]$.</figcaption></figure>

We now prove the congruence theorem in an “if-and-only-if” form, with merely one assumption:

**Theorem 2.3.**

assumes infinite (UNIV :: 'a set)

$$
\text{shows } \begin{array}{l} \triangle_m \mathit{fl} \equiv_{\prime a} \triangle_{m'} \mathit{gl} \longleftrightarrow \\ \qquad (m = m' \land \mathit{length} \ \mathit{fl} = \mathit{length} \ \mathit{gl} \land (\forall i.i < \mathit{length} \ \mathit{fl} \longrightarrow \mathit{fl} ! i \equiv_{\prime a} \mathit{gl} ! i)) \lor \\ \qquad (\triangle_m \mathit{fl} \equiv_{\prime a} \perp \land \triangle_{m'} \mathit{gl} \equiv_{\prime a} \perp) \end{array}
$$

Using a similar strategy of selecting suitable families to construct a counterexample and
then injecting them back into the original type, we can prove the difficult direction: namely,
if fl and gl are lists of satisfiable formulas of equal length and Δ<sub>m</sub> fl ≡<sub>la</sub> Δ<sub>m'</sub> gl, then for
every pair (fl ! i, gl ! i) of formulas in corresponding position i in fl and gl we have f ≡<sub>la</sub> g.
The same strategy also eliminates the assumption on length.

The infiniteness assumption is not used in the right-to-left direction of Theorem 2.3.
Using HOLZF, we can omit this assumption also in the left-to-right direction. We do not do
so because the ZF counterpart of Theorem 2.3 is not required to prove the finite tree-like
model property.

**2.2. Finiteness of equivalence classes of degree-bounded formulas.** The satisfaction of modal formulas is intrinsically *local*. A single modal formula can capture information only about worlds that are reachable within finitely many steps from the current state. The number of steps that a modal formula can “see” is called its *degree*. For a modal formula *φ*, represented as an abstract syntax tree, deg *φ* is defined as the maximum number of modal operators appearing along any branch of the tree.

We are interested in the set of well-formed τ-formulas with degree no more than *k*, denoted by degwffs *k* τ. More precisely, we are interested in the equivalence classes of degwffs *k* τ with respect to ≡<sub>a</sub>.
$$ \frac{\begin{array}{c} \phi \in A \\ \mathbf{boolcomb} A \phi \end{array}}{\mathbf{boolcomb} A \phi} \quad \frac{\begin{array}{c} \mathbf{boolcomb} A \phi \\ \mathbf{boolcomb} A \neg\phi \end{array}}{\mathbf{boolcomb} A \neg\phi} \quad \frac{\begin{array}{c} \mathbf{boolcomb} A \phi_1 \\ \mathbf{boolcomb} A \phi_2 \end{array}}{\mathbf{boolcomb} A (\phi_1 \lor \phi_2)} $$

<caption>Figure 2: Rules for the inductive definition of the boolean combination function</caption>

**Theorem 2.4.**

assumes finite $O \wedge$ finite $\Pi$
shows finite $(\deg wffs k (O, \rho, \Pi)) / \equiv_a$

Theorem 2.4 states that if the signature $\tau = (O, \rho, \Pi)$ has only finitely many modal operators and propositional letters then for each $k \in \mathbb{N}$ there are only finitely many distinct modal formulas up to degree $k$ modulo formula equivalence. This corresponds to Blackburn et al.'s [BRV01] Proposition 2.29(i).

The pen-and-paper proof proceeds by induction on $k$. For the base case, a modal formula has degree 0 if and only if it is purely propositional. If a propositional formula contains propositional letters in a '$p$ set, then we only need a propositional valuation $\sigma : '$$p \Rightarrow \mathbf{bool}$ to obtain its truth value, which we denote **peval** $\sigma \phi$. Two propositional formulas are equivalent if and only if they have the same truth table, i.e., the set of valuation functions that satisfy them is the same. Moreover, when evaluating a propositional formula $\phi$, only the truth values on the propositional letters that may appear in the formula matter. If the set of propositional letters $\Pi$ is finite, then there is an injection sending each equivalence class of propositional formulas to the set of valuations that validates them. Since the codomain is finite, this proves the finiteness of the propositional formulas up to equivalence. Notice that instead of evaluating propositional formulas with truth functions, we are evaluating them on structures. We link the two notions of propositional truth by proving that for a propositional formula $\phi$, a structure $M$ and a world $w$ in $M$, we have

$$ M, w \Vdash \phi \leftrightarrow \mathbf{peval} (\lambda p. \ valt M p w) \phi. \qquad (2.1) $$

This link is sufficient to prove the base case.

For the induction step, assuming the lemma holds up to degree $k$, we show that there are finitely many non-equivalent modal formulas up to degree $k+1$ using the same idea as in the base case. As outlined in Blackburn et al. [BRV01], the key observation is that each formula of degree at most $k+1$ in the signature $\tau$ is a boolean combination of propositional letters in $\Pi$ and formulas of the form $\Delta_m \mathfrak{fl}$, where $m \in O$ and all the formulas in $\mathfrak{fl}$ have a degree at most $k$. Then we define an inductive predicate **boolcomb** $A \phi$, which states that $\phi$ is a boolean combination of formulas from the set $A$, according to the rules in Figure 2.

Effectively, a boolean combination of formulas in $A$ can itself be regarded as a propositional formula built from the formulas in $A$, which act as propositional letters. We aim to characterize the satisfaction of modal formulas, specifically those obtained as boolean combinations, in terms of propositional formulas. The following lemma demonstrates that this is possible by associating each such modal formula with a corresponding propositional formula.
**Lemma 2.5.**

assumes finite A

shows $∃σ. ∀φ. boolcomb A φ →$

$∃φ_0. prop φ_0 ∧ pletters φ_0 ⊆ \{n. n < card A\} ∧ subst σ φ_0 = φ$

In the above, **prop** is a predicate that takes a modal formula as argument and that returns true if the formula is propositional. The lemma states that each boolean combination $\phi$ from A has a propositional formula as its skeleton. Such a skeleton is a propositional formula in which the propositional letters are natural numbers indexing the elements of A. The substitution $\sigma$ can be any function that enumerates A. Given a skeleton $\phi_0$ of $\phi$, we can recover $\phi$ by substituting in $\phi_0$ using $\sigma$, replacing each indexed variable with its corresponding formula in A. For example, for $\phi_1, \phi_2 \in A$, the boolean combination $\phi_1 \lor \neg\phi_2$ can be recovered by applying the substitution map $0 \mapsto \phi_1, 1 \mapsto \phi_2$ from the skeleton $0 \lor \neg 1$.

Now we can characterize the satisfaction of boolean combinations simply. For $\phi = \text{subst } \sigma \phi_0$, we have $M, w \Vdash \phi$ if and only if **peval** ($\lambda p. M, w \Vdash \sigma p$) $\phi_0$. We use this fact to prove the following theorem about the equivalence of modal formulas.

**Theorem 2.6.**

assumes $prop \phi_1 \wedge prop \phi_2 \wedge \phi_1 \equiv_{\iota_a} \phi_2$

shows $subst \sigma \phi_1 \equiv_{\iota_a} subst \sigma \phi_2$

*Proof.* Given a structure $M$ and a world $w \in \text{world } M$, we show that $M, w \Vdash \text{subst } \sigma \phi_1$ is equivalent to $M, w \Vdash \text{subst } \sigma \phi_2$. Define the valuation $\beta = \lambda p. w. M, w \Vdash \sigma p$. Let $M'$ be the structure $(\text{world } M, \text{rel } M, \beta)$. We transfer the equivalence according to the diagram:

$M, w \Vdash \text{subst } \sigma \phi_1 = \text{=} \text{=} \text{=} \text{=} \text{=} M, w \Vdash \text{subst } \sigma \phi_2$

<figure><img src="image_4.png" /></figure>

peval $\beta \phi_1$

<figure><img src="image_5.png" /></figure>

peval $\beta \phi_2$

<figure><img src="image_6.png" /></figure>

peval ($\lambda p. \text{valt } M' p w$) $\phi_1$ peval ($\lambda p. \text{valt } M' p w$) $\phi_2$

<figure><img src="image_7.png" /></figure>

<figure><img src="image_8.png" /></figure>

$M', w \Vdash \phi_1 = \text{=} \text{=} \text{=} \text{=} \text{=} M', w \Vdash \phi_2$

<figure><img src="image_9.png" /></figure>

where solid double lines are known equivalences and the dashed double line is the resulting equivalence. For both rows, from left to right, the first equality follows from the discussion right above, the second equality follows from the definition of $M'$, and the third equality is an instance of (2.1). The right-most (vertical) equivalence holds thanks to the assumption $\phi_1 \equiv_{\iota_a} \phi_2$. $\square$

This theorem implies that non-equivalent boolean combinations can be distinguished by some valuation on their skeletons' variables. We can now prove that for a finite set A of formulas, the quotient set $Q = \{\phi. \text{boolcomb } A \phi\} / \equiv_{\iota_a}$ is finite. Let $r$ be a function that selects representatives from the quotient set $Q$, and let $sk$ be a function that assigns a skeleton to each such representative. The function that maps each equivalence class $\bar{\phi} \in Q$ to the set of valuations that satisfy its skeleton is an injection. Formally, the injection term is

$\lambda \bar{\phi}. \{\beta. \text{peval } \beta (sk (r \bar{\phi})) \wedge (\forall q. \beta q \rightarrow q < \text{card } A)\}$
The second conjunct ensures that we consider only valuations $v$ on the finitely many natural numbers that correspond to elements of $A$ to ensure the finiteness of the codomain.

We can finally prove Theorem 2.4.

*Proof (of Theorem 2.4).* The formal proof largely follows the pen-and-paper proof described above. From a formalization point of view, only the induction step is interesting. We have that $\degwffs(n+1)\tau$ is the boolean combination of the set $U$, defined as

$$ \{\text{Var } p \mid p. p \in \Pi\} \cup \{\Delta_m fl \mid m \text{ fl. } m \in O \wedge \text{length fl} = \rho m \wedge \text{set fl} \subseteq \text{degwffs } n \tau\} $$

However, the inductive hypothesis does not directly establish that there are only finitely many formulas of degree at most $n$, but only the finiteness up to equivalence. By induction on the boolean combination rules, we prove that if every $\phi \in B$ is equivalent to an element $\psi \in A$, then every boolean combination on $B$ is equivalent to a boolean combination on $A$. By combining this fact with the right-to-left direction of Theorem 2.3, the inductive hypothesis implies that $\degwffs(n+1)\tau$ is finite up to equivalence. In turn, this implies that $U$ is finite up to equivalence. Hence, the boolean combinations on $U$ are finite up to equivalence as well. $\square$

Xu and Norrish formalized a similar result [XN20, Lemma 1], but with the additional assumption that $\text{UNIV} :: 'a$ set must be infinite. Their version needs this assumption because it uses both directions of Theorem 2.3, whereas the right-to-left direction suffices here.

These two theorems serve as the first evidence that our formalization of general modal logic semantics is usable. Our approach could also have been implemented in a proof assistant based on dependent type theory. An alternative in such systems would be to make types as descriptive as possible. In particular, well-formedness conditions are typically encoded in type information whenever possible. Therefore, we would mostly work with the type of $\tau$-well-formed formulas for each signature $\tau$. Consequently, the definition of equivalence would always have to carry this parameter even when it is not needed.

### 3. TREE-LIKE FRAMES

Structures in modal logic consist of a multi-frame—i.e., a set of worlds equipped with a family of relations—and a valuation. For a multi-frame $(W, R)$ to be a tree, as for a binary frame, we require a distinguished element $r \in W$, called the *root*, satisfying the conditions:

* Every element of $W$ is reachable from $r$ via $R$.

* Every non-root element $w \in W$ has a unique predecessor with respect to $R$.

* The relation $R$ has no loop.

The notions of “reachable” and “predecessor” are not obvious because multi-frames are equipped with a family of relations. A world is *reachable* from $r$ if it can be reached by repeatedly taking the next step, defined as follows. For a relation family $R$ indexed by a set of modalities $O$, the world $v$ is a *next step* of $w$ if there exists some $m \in O$, such that $R m (w \# vl)$ and $v \in \text{set vl}$. Conversely, $w$ is a *predecessor* of $v$ in this case. When examining the tree condition, we interpret $R m (w \# vl)$ as meaning “$w$ is related to every element in $vl$.” Formally, we define a binary relation $\hat{R}_O$ generated by $R$, where $O$ indexes $R$'s family:

$$ \hat{R}_O = \{(w, v). \exists m \text{ vl. } m \in O \wedge R m (w \# vl) \wedge v \in \text{set vl}\} $$
Equipped with this relation, we define the property of being a tree as follows:

**Definition 3.1.**

$$ \begin{align*} \text{tree } O(W, R) r \leftrightarrow & r \in W \wedge \\ & (\forall w. w \in W \rightarrow (r, w) \in (\widehat{R|_{WO}})^*) \wedge \\ & (\forall w. w \in W \wedge w \neq r \rightarrow \exists! v. (v, w) \in \widehat{R|_{WO}}) \wedge \\ & (\forall w. w \in W \rightarrow (w, w) \notin (\widehat{R|_{WO}})^+) \end{align*} $$

In the above, $R|_W$ is the restriction of $R$ to the set $W$, and $R^*$ and $R^+$ denote the reflexive transitive closure and the transitive closure of a relation $R$, respectively. When the multi-frame $(W, R)$ is part of a structure, we have $R|_W = R$. Regarding the third conjunct, expressing the uniqueness of the predecessor, only the predecessor element is required to be unique. Thus, there might be different relations $R m$ and $R n$ within the family $R$, possibly of different arities, that both relate $w$ to its predecessor $v$. Such multiplicity does not contradict the uniqueness condition, whereas $w$ having two distinct predecessors $v$ and $v'$ is forbidden. Many proofs concerning trees proceed by induction on reachability from $r$. However, it is not possible to define trees inductively, since the definition above allows trees to have infinite width and infinite depth. A coinductive definition [BBB$^{+}$17] is possible, but coinductive principles are not needed in the proofs so it is enough to rely on Definition 3.1.

A tree-like structure is then a structure in which the multi-frame is a tree. The proof of the finite tree-like model property proceeds in two steps: first, we construct a tree-like structure from a given structure; then, we refine this new structure into a finite structure. The intermediate step requires the following tree-like model property:

**Lemma 3.2.**

$$ \begin{align*} \text{assumes } \text{struct\_on}(O, \rho, \Pi) M \wedge \text{wff}(O, \rho, \Pi) \phi \wedge M, w \Vdash \phi \\ \text{shows } \exists M'. \text{struct\_on}(O, \rho, \Pi) M' \wedge \text{tree}(\text{world } M', \text{rel } M') [w] \wedge M, [w] \Vdash \phi \end{align*} $$

The constructed tree-like structure will satisfy the given formula at its root. There is a change in types: we begin with a structure on an '$a$ set but conclude with a structure on an '$a$ list set. This transformation occurs due to a construction known as unraveling. In this process, each world in $M$ that is connected to the root in the original structure becomes a world of type '$a$ list. This new world consists of a list of worlds from $M$, encoding the path from $r$ to that world.

We need a notion of height for elements. Our general definition suits any generated structure (corresponding to definition 2.5 in Blackburn et al. [BRV01]) and behaves as expected on trees. We first collect the lengths of all possible paths from $r$ to $w$ as $\text{height}_\le r OR w$, the set of upper bounds for the height of $w$, defining it inductively using the following two rules:

$$ \begin{align*} 0 &\in \text{height}_\le r OR r \\ n &\in \text{height}_\le r OR w \wedge m \in O \wedge R m (w \# vl) \wedge v \in \text{set } vl \implies n+1 \in \text{height}_\le r OR v \end{align*} $$

Then we define height $r OR w$ to be the natural number $\inf \{n. n \in \text{height}_\le r OR w\}$. When there exists a path from $r$ to $w$, the set from which we take the minimum is non-empty. We prove that the height of each element in a tree is uniquely determined by its unique predecessor. In the following theorem, the set $\mathbf{rset} OR$ is the set of worlds that are related by some relation indexed by an element in the signature $O$.
**Theorem 3.3.**

assumes tree $O(W, R)$ $r \wedge rset O R \subseteq W \wedge w \in W \wedge m \in O \wedge R m$ ($w \# vl$) $\wedge v \in$ set $vl$
shows height $r$ $O R v$ = height $r$ $O R w + 1$

4. CONSTRUCTION OF THE FINITE TREE-LIKE STRUCTURE

We now assemble the above components into a proof of the finite tree-like model property:
any satisfiable modal formula is satisfied at the root of a finite tree-like structure.

**Theorem 4.1.**

assumes wff (O, ρ, Π) φ ∧ struct_on (O, ρ, Π) M ∧ M, (w :: 'a) ⊧ φ
defines τ = (ops φ, ρ, props φ)
shows ∃M<sub>f</sub> (w<sub>f</sub> :: 'a list). struct_on τ M<sub>f</sub> ∧ finite (world M<sub>f</sub>) ∧
tree (ops φ) (world M<sub>f</sub>, rel M<sub>f</sub>) w<sub>f</sub> ∧ M<sub>f</sub>, w<sub>f</sub> ⊧ φ

The pen-and-paper construction works as follows: assume that $M_0, w_0 \Vdash \phi$, where $\deg \phi = k$. From the tree-like model property (Lemma 3.2), we obtain a tree-like structure $M_t$ with root $r$ such that $M_t, r \Vdash \phi$. We select a finite structure by including only those worlds that influence the satisfaction of $\phi$ at $r$. Inductively, we construct finite sets $W_0, \dots, W_k$ of worlds in $M_t$ such that worlds in $W_n$ have height $n$. The finite structure's underlying set is given by $\bigcup_{n \le k} W_n$. We define $W_0 = \{r\}$ and proceed inductively. Assuming $W_n$ has been constructed, we define $W_{n+1}$ as follows: consider the set of well-formed modal formulas up to degree $k$ in the signature consisting of the symbols appearing in $\phi$. For each of the non-equivalent formulas of the form $\Delta_m \mathit{fl}$, we check whether there exists a world $w \in W_n$ such that $M_t, w \Vdash \Delta_m \mathit{fl}$. For each such $w$, we select a list $vl$ such that $\mathit{rel} \ M_t \ m$ ($w \# vl$), where $M_t, (vl \ ! \ i) \Vdash \mathit{fl} \ ! \ i$ for each $i < \mathit{length} \ vl$. Then $W_{n+1}$ consists of all the elements in any of the lists selected in this way.

From the above, once we obtain the tree-like structure $M_t$, we want to select a finite
subset from the world set of $M_t$ so that the resulting structure remains tree-like with root $r$.
We have two tasks left:

* Construct the structure and prove that its world set is finite and that the underlying frame is a tree.

• Prove that the formula remains satisfied at the root of the new structure.

**4.1. Structure construction.** According to the pen-and-paper proof, to construct $W_{n+1}$ from $W_n$, we need to investigate the satisfaction of each triangle formula up to degree $k$ at all $w$ in $W_n$. First, we prove the existence of a function $cwl$ as follows. For a triangle formula $\Delta_m \mathit{fl}$ and a world $w$, if $M_t, w \Vdash \Delta_m \mathit{fl}$, then $cwl$ outputs a list of worlds $vl$ in $M_t$ such that $\mathit{rel} \ M_t \ m$ ($w \# vl$), and for each $i < \mathit{length} \ fl$, the $(i+1)$st formula in $fl$ is satisfied at the $(i+1)$st world in $vl$. Second, we define the finite set $\mathit{reps}_{i,a} \ k \ \tau$ of representatives of well-formed triangle formulas up to degree $k$. When constructing $W_{n+1}$, we apply $cwl$ only on worlds in $W_n$ and elements in $\mathit{reps}_{i,a} \ k \ \tau$. Then, by induction, we can conclude the finiteness of $W_{n+1}$.

The set $\mathit{reps}_{i,a} k \tau$ is constructed from the set $\mathit{degwffs} k \tau$. By Theorem 2.4, the quotient set $\mathit{degwffs} k \tau / \equiv_{i,a}$ is finite. Moreover, since we are concerned only with triangle formulas, it suffices to consider their representatives. However, applying Hilbert's choice (Eps in
$$ \frac{\begin{array}{c} r \in \text{nworld } M r A f 0 \\ v \in \text{nworld } M r A f n \\ w \in \text{nworld } M r A f (n+1) \end{array}}{\begin{array}{c} \Delta_m \text{fl} \in A \\ \Delta_m \text{fl}' \in \text{reps}_{\tau_a} k \tau \\ \exists \text{fl}' \in \text{reps}_{\tau_a} k \tau \wedge \Delta_m \text{fl} \equiv_{\tau_a} \Delta_m \text{fl}' \\ \text{length fl} = \text{length fl}' \\ (\forall j. j < \text{length fl} \rightarrow (\text{fl} ! j) \equiv_{\tau_a} (\text{fl}' ! j)) \end{array}} \text{ (degwffs } k \tau/\equiv_{\tau_a}) - \{\{\}} $$

<caption>Figure 3: Rules for the inductive definition of the world set</caption>

Isabelle) to the set of equivalence classes of triangle formulas may not yield the desired result. For example, the selected formula might take the form $\neg\neg\Delta_m \text{fl}$, which is equivalent to a triangle formula but is not one. Instead, we require that the representatives we choose are syntactically of the form $\Delta_m \text{fl}$, so $M_t, w \models \Delta_m \text{fl}$ directly unfolds into the existence of the worlds we need to include. To satisfy this requirement, we apply Eps to the following set $\mathcal{F}$, defined as:

$$ ((\lambda c. c \cap \{\psi. \exists m \text{fl}. \psi = \Delta_m \text{fl}\}) \cdot (\text{degwffs } k \tau/\equiv_{\tau_a})) - \{\{\}} $$

In the above, $f$ is the image of the set $A$ under the function $f$. We define the image of $\mathcal{F}$ under Eps as the set $\text{reps}_{\tau_a} k \tau$. This set is finite, and for each well-formed triangle formula with a degree no more than $k$, we can find an equivalent triangle formula in it. By combining these observations with Theorem 2.3, we prove the following lemma stating all the properties we need about $\text{reps}_{\tau_a} k \tau$:

**Lemma 4.2.**

assumes $\Delta_m \text{fl} \in \text{degwffs } n \tau \wedge \text{infinite} (\text{UNIV} :: 'a \text{set}) \wedge M, w \models \Delta_m \text{fl}$

shows $\exists \text{fl}' \in \text{reps}_{\tau_a} k \tau \wedge \Delta_m \text{fl}' \equiv_{\tau_a} \Delta_m \text{fl}' \wedge$

$$ \text{length fl} = \text{length fl}' \wedge $$

$$ (\forall j. j < \text{length fl} \rightarrow (\text{fl} ! j) \equiv_{\tau_a} (\text{fl}' ! j)) $$

The function $cwl :: (m, m')$ form $\Rightarrow m \Rightarrow m'$ list is obtained directly by unfolding the definition of satisfaction and skolemizing the existential quantifier. For every world $w$, operator $m$, and formula list $fl$, we have:

**Property 1.**

$$ M_t, w \models \Delta_m \text{fl} \implies $$

$$ \text{length} (cwl (\Delta_m \text{fl}) w) = \text{length fl} \wedge $$

$$ \text{rel} M_t m (w \# (cwl (\Delta_m \text{fl}) w)) \wedge $$

$$ (\forall v \psi. (v, \psi) \in \text{set} (\text{zip} (cwl (\Delta_m \text{fl}) w) \text{fl}) \rightarrow M_t, v \models \psi) $$

Next, we select the world set of the finite structure. Using Isabelle's facility for inductive definitions, we declare the introduction rules in Figure 3.

In these rules, we substitute $M$ by $M_t$, $A$ by $\text{reps}_{\tau_a} k \tau$, and $f$ by the function $cwl$ we obtained from Property 1. The set $\text{nworld } M_t r (\text{reps}_{\tau_a} k \tau) cwl n$ is the $(n+1)$st world set $W_n$ as in the pen-and-paper proof. We now define the structure to witness the variable $M_f$ in Theorem 4.1. The world set is defined as $\bigcup_{n \le k} \text{nworld } M_t r (\text{reps}_{\tau_a} k \tau) cwl n$. The relation and valuation are obtained by restricting those of $M_t$ to this world set. Tree-likeness is straightforward, since the underlying frame of $M_f$ is a connected restriction of a tree.

We simplify the proof compared with Blackburn et al. [BRV01] and Xu and Nørish [XN20]. Their proof (i) restricts the tree-like structure to height $k$ and establishes that $\phi$ is still satisfied by the restricted structure, and (ii) selects a finite structure from the restricted structure. Step (i) aims to eliminate infinite depth in the tree. However, this
step turns out to be unnecessary both in the pen-and-paper proof and in the formalization because we directly define the finite tree-like structure to have height $k$.

**4.2. Satisfaction via n-bisimulation.** It remains to prove that the formula $\phi$ is satisfied at the root $r$ in $M_f$. This is achieved using the concept of *n-bisimulation*. A relation $Z$ is an *n-bisimulation* between two worlds $w$ of $M$ and $w'$ of $M'$ when $\text{nbisim} Z n M M' w w'$ holds, where $\text{nbisim}$ is defined as follows.

**Definition 4.3.**

$$
\begin{align*}
\text{nbisim} Z n M M' w w' &\longleftrightarrow \\
Z n w w' &\wedge \\
(\forall i \, v v'. \, Z i v v' \longrightarrow v \in \text{world } M \wedge v' \in \text{world } M') \wedge \\
(\forall i \, v v'. \, i + 1 \le n \wedge Z (i+1) v v' \longrightarrow Z i v v') \wedge \\
(\forall v \, v' \, p. \, Z 0 v v' \longrightarrow \text{valt } M p v = \text{valt } M' p v') \wedge \\
(\forall i \, v \, v' \, \text{ul } m. \quad &i + 1 \le n \wedge Z (i+1) v v' \wedge \text{rel } M m (v\#ul) \longrightarrow \\
&\phantom{i + 1 \le n \wedge Z (i+1) v v' \wedge } (\exists u l'. \, \text{rel } M' m (v'\#ul') \wedge \\
&\phantom{i + 1 \le n \wedge Z (i+1) v v' \wedge } (\forall u \, u'. \, (u, u') \in \text{set } (\text{zip } ul \, ul') \longrightarrow Z i u u')) \wedge \\
(\forall i \, v \, v' \, \text{ul } m. \quad &i + 1 \le n \wedge Z' (i+1) v v' \wedge \text{rel } M' m (v'\#ul) \longrightarrow \\
&\phantom{i + 1 \le n \wedge Z' (i+1) v v' \wedge } (\exists u l'. \, \text{rel } M m (v\#ul) \wedge \\
&\phantom{i + 1 \le n \wedge Z' (i+1) v v' \wedge } (\forall u \, u'. \, (u, u') \in \text{set } (\text{zip } ul \, ul') \longrightarrow Z i u u'))
\end{align*}
$$

We call the last two conjuncts the *forward* and *backward condition* of nbisim, respectively. Definition 4.3 is designed to work only under the assumption that, for some $\tau$, $M$ and $M'$ are both $\tau$-structures, but it does not depend on $\tau$ as a parameter. Suppose $M$ and $M'$ are structures on the signature $\tau = (O, \rho, \Pi)$. Thus, when establishing an $n$-bisimulation between $M$ and $M'$, it will be sufficient to only check the conditions required by Definition 4.3 for the symbols in $\tau$. For example, when checking the third conjunct, we can assume $p \in \Pi$.

Intuitively, the existence of an $n$-bisimulation between $w$ and $w'$ indicates that whenever a world $v$ can be reached in up to $n$ steps from $w$ in $M$, some world $v'$ can be reached with the same number of steps from $w'$ in $M'$, and vice versa. Thus, as expected, if nbisim $Z n M M' w w'$, then $w$ and $w'$ satisfy the same modal formulas up to degree $n$. We construct an $n$-bisimulation from the root in $M_t$ to the restricted finite structure $M_f$. The relation $Z$ of interest here is given by the term

$$
\begin{align*}
Z ={}& \lambda n \, v \, v'. \, v \in \text{world } M_t \wedge v' \in \text{world } M' \wedge \\
      & \text{height } r \, O \, (\text{rel } M_t) \, v = \text{height } r \, O \, (\text{rel } M_t) \, v' \wedge \\
      & \text{height } r \, O \, (\text{rel } M_t) \, v' \le k - n \wedge \\
      & (\forall \psi. \, \psi \in \text{degwffs } n \, \tau \longrightarrow (M_t, v \Vdash \psi \longleftrightarrow M_t, v' \Vdash \psi))
\end{align*}
$$

This relation is an $n$-bisimulation. We spell out only the proof of the forward condition of nbisim here. Suppose $i + 1 \le k$ and $Z (i + 1) v v'$. Then $v$ and $v'$ belong to $M_t$ and $M_f$ respectively, with the same height $h \le k - (i + 1)$. Moreover, they agree on all the well-formed $\tau$-formulas up to degree $i + 1$. Given that $\text{rel } M_t (v\#ul)$, we want to find a list $ul'$ in $M_f$ such that $\text{rel } M_t (v'\#ul')$, and each corresponding pair of elements in $ul$ and $ul'$ is linked by $Z i$. The height condition imposed by $Z$ requires us to select $ul'$ from the set $\text{nworld } M r (\text{reps}_{i, k} \tau) \, cwl (h + 1)$. We obtain $ul'$ using the rule that defines this set and Property 1 of the function $cwl$.
For each element $u$ of $ul$, consider the well-formed $\tau$-formulas up to degree $i$ satisfied at $u$. By Theorem 2.4, there are only finitely many such formulas up to equivalence, so we can consider their conjunction, that we denote $\Psi$. Then $\Psi \in \text{degwffs } i \tau$, and:

**Property 2.** The formula $\Psi$ is satisfied at a world $w$ in a structure $M$ if and only if for every well-formed formula up to degree $i$, if it is satisfied at $u \in ul$, then it is satisfied at $w$:

$$M, w \Vdash \Psi \longleftrightarrow (\forall \psi. \psi \in \text{degwffs } i \tau \wedge M_t, u \Vdash \psi \longrightarrow M, w \Vdash \psi)$$

We collect all these formulas into a list $\Psi l$. Then $M_t, v \Vdash \deg (\Delta_m \Psi l)$ and $\deg (\Delta_m \Psi l) \le i + 1$. Exploiting the assumption $Z$ $(i+1) v v'$, we obtain $M_t, v' \Vdash \deg (\Delta_m \Psi l)$. From Lemma 4.2, there exists a list $\Psi l'$ for the list $\Psi l$ with specific properties. We set the list $ul'$ to be $cwl (\Delta_m \Psi l') v'$. The most involved goal to prove is the following:

$$(u, u') \in \text{set} (\text{zip } ul \, ul') \wedge \\ \psi \in \text{degwffs } i \tau \longrightarrow (M_t, u \Vdash \psi \longleftrightarrow M_t, u' \Vdash \psi)$$

With Property 2 the goal amounts to proving the existence of $\Psi_0$ and $\Psi'_0$ such that:

$$(u, \Psi_0) \in \text{set} (\text{zip } ul \, \Psi l) \wedge (u', \Psi'_0) \in \text{set} (\text{zip } ul' \, \Psi l') \wedge (\Psi_0, \Psi'_0) \in \text{set} (\text{zip } \Psi l \, \Psi l')$$

For the proof, we have at our disposal the following correspondences involving formulas and worlds among four lists with the same length, namely, $ul, ul', \Psi l, \text{and } \Psi l'$:

$$(u, \Psi) \in \text{set} (\text{zip } ul \, \Psi l) \longrightarrow M_t, u \Vdash \Psi \\ (u', \Psi') \in \text{set} (\text{zip } ul' \, \Psi l') \longrightarrow M_t, u' \Vdash \Psi' \\ (\Psi, \Psi') \in \text{set} (\text{zip } \Psi l \, \Psi l') \longrightarrow \Psi \equiv_{a \text{ list}} \Psi'$$

Conveniently, Sledgehammer [PB10] finds an automatic proof. A detailed proof by a combinatorial argument or by zipping the four lists together and selecting the entry containing the pair $(u, u')$ should be possible. However, either approach would be tedious to spell out.

Checking the backward condition of nbisim is similar but easier, since we do not need to check that the list we obtain is in a restricted subset of world $M_t$.

Finally, we note that although Theorem 2.3 is used, we do not need to assume that the type $'a$, which is the type of the original structure $M_0$'s underlying set, is infinite. This is because passing to a tree-like structure changes the type from $'a$ to $'a \text{ list}$, which is infinite, and this is the type that is used in Theorem 2.3. This type change is not present on paper. Indeed, although the pen-and-paper construction in [BRV01] describes the elements of the constructed tree-like model as lists of worlds, as ZF set theory is untyped, a list in set theory is still a set. The quantification in the original theorem from [BRV01] expands in detail as follows: if in the class of all structures, we can find a model of a formula $\phi$, then we can also find in the class of structures a tree-like model of $\phi$, where $\phi$ is satisfied at the root of the underlying frame. For both the model we start with and the one we construct, the quantifications are on the class of all structures for the signature. However, the two quantifications in Theorem 4.1 are on two different types. This type change is a consequence of using HOL. In this sense, Theorem 4.1 fails to encode the original finite tree-like model property faithfully. Such a change is clumsy and inelegant. The next section addresses this issue.
## 5. USING HOLZF TO AVOID THE TYPE ISSUE

A structure in modal model theory comprises a set of worlds. Such a set is of type 'a set for some HOL type 'a. Due to the definition of equivalence (Definition 2.1), this type parameter appears throughout all relevant definitions and theorems. Even more significantly, the type change in Theorem 4.1 shows that this parameter is not only a placeholder but has a real impact on the formalization.

Type changes are a common challenge in HOL. Such changes can make formal presentations of theorems in a proof assistant less intuitive by requiring assumptions on types that do not appear anywhere in the rest of the statement. One such example is the statement of Van Benthem's characterization theorem in Xu and Norrish [XN20]: To prove that a given formula $\psi$ is equivalent to a standard translation on structures with 'a elements, they need to assume $\psi$ is invariant for bisimulation for structures with ($\mathbb{N} \to 'a$) $\to$ bool elements. This is because the proof uses structures with ($\mathbb{N} \to 'a$) $\to$ bool elements constructed from those with 'a elements, which cannot be inferred from the statement. Ideally, we would like to work as if conducting a pen-and-paper proof, where such type considerations never arise. In this section, we demonstrate that it is possible to hide this parameter using the HOLZF extension of Isabelle/HOL.

**5.1. Preliminaries on HOLZF.** HOLZF, initially introduced by Obua [Obu06] to encode surreal numbers in HOL and later reformulated by Paulson [Pau19], is a formalization of ZF set theory in Isabelle. In contrast to the standalone object logic Isabelle/ZF, HOLZF is an axiomatization within the object logic HOL. This approach allows us to use HOL and its proof automation to reason about ZF set theory.

HOLZF includes a HOL type $V$, declared as a type constant, that is regarded as the type of all ZF sets. A term of type $V$ is semantically a ZF set, and its elements are also ZF sets. The function `elts :: V \Rightarrow V set` is axiomatized to extract the elements of a ZF set and form a HOL set. Axioms involving $V$ and `elts` ensure that the terms of $V$ behave like ZF sets. For example, the extensionality axiom, which states that two sets with the same elements are equal, is stated as:

$$ \text{elts } x = \text{elts } y \implies x = y $$

Whereas every ZF set uniquely determines a HOL set of terms of type $V$, the converse does not always hold. A HOL set of terms of type $V$ does not necessarily arise as a term of $V$, as it may be too large to be a ZF set. For example, the set `UNIV :: V set` cannot be represented as a term of type $V$; it is too large and thus constitutes instead a proper class in the ZF sense. A HOL set of $V$ terms is *small* if it can be represented as a term of type $V$. For example, for each $V$ term $v:V$, we have the HOL set `elts v:V set` is small, since it is represented by the term $v$. The formal definition of smallness is, in fact, more general than this. It applies to a HOL set of any type:

**Definition 5.1.**

$$ \text{small}(X :: 'a \text{ set}) \leftrightarrow (\exists i :: 'a \Rightarrow V. \text{inj_on } i X \wedge i' \text{, } X \in \text{range els}) $$

Observe that *small* is defined for arbitrary terms of type 'a set, not only for ZF classes of type $V$ set.

The property of being a set is fundamentally a matter of size. This can be made explicit by the following theorem, where `=o` denotes equality on cardinals.
**Theorem 5.2.**

$$ \text{small } A \leftrightarrow (\exists B :: V. |A| =_o |\text{elts } B|) $$

According to this characterization, which was formally proved by Dmitriy Traytel at our request, a HOL set A is small if and only if there exists a ZF set B with the same cardinality. In particular, we will use the property, also formally proved by Traytel, that if a HOL set A of type 'a set is small, then the HOL set list A of lists whose elements are drawn from A, of type 'a list set, is also small. The generality of small's type makes it possible to state this property.

**5.2. Applying ZF to refine Theorem 4.1.** Our goal is to hide the type parameter of the underlying set of structures in Theorem 4.1, the finite tree-like model property. We restrict our attention to a certain type of structures, which we call the V-structures, whose underlying set is a ZF set. These structures, like those in Section 1, are also tuples $(W, R, \beta)$, but the first component, $W$, is now of type $V$. The other elements of the tuple are adapted in the following way: $R :: 'm \Rightarrow V$ list $\Rightarrow \text{bool}$ and $\beta :: 'p \Rightarrow V \Rightarrow \text{bool}$. They are both functions on the elements of the ZF set $W$—i.e., the terms of type $V$ in elts $W$.

Instead of inductively defining the semantics of modal formulas in a V-structures, we reuse our general definition of semantics for an ('m, 'p, 'a) structure in general, where we specialize the type 'a to be the type V of ZF sets. There is a slight mismatch between the types of an ('m, 'p, 'a) structure and a V-structure. To address this, we define a function Vstruct2struct that converts a V-structure to an ('m, 'p, V) structure by simply replacing the ZF set of worlds with the corresponding HOL set. We then define a V-structure M to be a $\tau$-structure if Vstruct2struct M is a $\tau$-structure, and we define the semantics on V-structures in terms of our general definition of semantics. In Isabelle:

**Definition 5.3.**

$$ \text{Vstruct2struct} (W, R, V) = (\text{elts } W, R, V) $$

$$ \text{Vstruct\_on } \tau M \leftrightarrow \text{struct\_on } \tau (\text{Vstruct2struct } M) $$

$$ M, w \Vdash_V \phi \leftrightarrow \text{Vstruct2struct } M, w \Vdash \phi $$

This definition of semantics has two advantages. First, we can reuse the results about the general definition of semantics. Second, we obtain coherent definitions of semantics for ('m, 'p, V)-structures and V-structures by construction.

We prove the following V version of Theorem 4.1:

**Theorem 5.4.**

$$ \text{assumes } \text{wff } (O, \rho, \Pi) \phi \wedge \text{Vstruct\_on} (O, \rho, \Pi) M \wedge M, w \Vdash_V \phi $$

$$ \text{defines } \tau = (\text{ops } \phi, \rho, \text{props } \phi) $$

$$ \text{shows } \exists M_f w_f. \text{Vstruct\_on } \tau M_f \wedge \text{finite } (\text{Vworld } M_f) \wedge \text{tree } (\text{ops } \phi) (\text{Vworld } M_f, \text{Vrel } M_f) w_f \wedge M_f, w_f \Vdash_V \phi $$

We do not need to re-prove Theorem 4.1; we use it as a lemma. However, a slight refinement is required. We need the structure $M_f$ from Theorem 4.1 to additionally satisfy the condition world $M_f \subseteq$ list (world $M$), which follows trivially from the construction.

The proof of Theorem 5.2 contains two transitions between V-structures and ('m, 'p, 'a)-structures. This leads to the following three proof steps:

(1) Convert the given V-structure $M$ such that $M, w \Vdash_V \phi$ into a ('m, 'p, V)-structure.
(2) Apply the strengthened version of Theorem 4.1 to obtain a finite tree-like ('m, 'p, V list)-structure $M'$ that satisfies $\phi$ at its root.

(3) Using the fact that the type V list is small, construct a V-structure $M''$ by copying the model $M'$ into the type V that satisfies the requirement from our desired conclusion.

*Proof.* Given the assumptions, we have $V\mathbf{struct2struct} M, w \Vdash \phi$ and $V\mathbf{struct}_\mathbf{on} \tau M$. From the refinement of Theorem 4.1 we obtain a finite structure $M_f$ such that $\mathbf{world} M_f \subseteq \mathbf{list}(\mathbf{world}(V\mathbf{struct2struct} M))$. Since $M$ is a V-structure, its underlying set $\mathbf{world}(V\mathbf{struct2struct} M)$ is small, and so is the set of lists on it. Hence $\mathbf{world} M_f$ is small and corresponds to a term $W_f$ of type V. Then $(W_f, \mathbf{rel} M_f, \mathbf{valt} M_f)$ constitutes the V-structure we want. $\square$

An advantage of this proof is that it is entirely separated from the main proof. It would have been possible to define primitive model-theoretic notions as in Section 1 for V-structures, without referring to the standard HOL notions. Then, every theorem we have proved would have a V-version. However, there is no need to rederive these theorems: in the proof of Theorem above, we use a cardinality argument together with the ZF axiomatization to achieve the translation.

With the help of ZF, we succeed in treating the type issue caused by the choice of HOL as the foundation that we use to formulate mathematics. Compared with Theorem 4.1, we obtain Theorem 5.2 as a more faithful formalization of the original theorem in [BBN11a], where the type of V-structures serves as the class of all structures.

The key point in our method is that reasoning about structures over ZF is simultaneously reasoning about all the structures based on a small type. Therefore, a theorem about ZF structures can effectively serve as a quantification over all small types, though to a restricted extent. We can prove as an explicit instance that:

**Theorem 5.5.**

assumes $\phi_1 \equiv^V \phi_2 \wedge \mathbf{small} (\mathbf{UNIV} :: 'a \mathbf{set})$

shows $\phi_1 \equiv'a \phi_2$

Informally, equivalence in all the V-structures (denoted by $\equiv^V$) implies equivalence in all the structures whenever their underlying sets are small. Semantically, the converse holds as well: if two formulas are equisatisfied in every structure whenever the underlying set of the structure is small, then they are equivalent in all the V-structures. However, such a statement cannot be stated as a HOL statement due to the lack of quantification on types. This does cause practical inconveniences. For example, it prevents us from directly using Theorem 2.3 to obtain its V-counterpart. A formal proof would require copying the structure we presented in Figure 1 to V. It is not always the case that the size argument is enough for switching between the concrete types and ZF. In our proof of Theorem 4.1, we could exploit the fact that we reason about the existence of V-structures, not a property that holds for the whole collection of all the V-structures.

The ZF technique described above can be useful beyond logic and model theory. For example, it can help manage type changes in algebra. In particular, it avoids the change of type when taking quotient—especially in proofs that favor explicit iterated quotients such as $(R/I_1)/I_2$ instead of $R/(I_1+I_2)$, where $R$ is a ring and $I_1, I_2$ are ideals. This approach allows us to work with $R$-algebras with a single type. Such techniques offer promising applications, including the formalization of the functor-of-points approach in algebraic geometry within HOL, where the objects of interest are functors from the category of $R$-algebras.
5.3. **Alternatives.** To address the type issue using HOLZF, an alternative to the above technique would have been to define the semantics only for V-structures from the beginning, using HOLZF all along. However, this would be less general than working with structures of arbitrary types.

Dependently typed systems, such as Lean [MU21] and Rocq [BC04], offer another option. We can have the types play the role of underlying sets of structures. Within a fixed level of type universe, we can quantify over these types. In this setting, the type universe serves as the proper class of all sets, and the type of structures with underlying types in this universe level serve as the proper class of all “set-based structures.” However, there are advantages to working within a simpler type system—in particular, working with Isabelle enables us to use the strong proof automation provided by simp, auto, and Sledgehammer [PB10].

Also note that if we merely want the assumption and conclusion of Theorem 4.1 to use the same type, instead of using ZF, we can assume that *UNIV* :: 'a set is infinite. Under this assumption, 'a list injects back to 'a, allowing us to construct a copy of the finite tree-like structure. However, this method does not generalize well, even in natural cases like the following one. If we consider the proof by Blackburn et al. [BRV01] of the finite model property via filtration (a proof that does not produce a tree-like structure), then we would start from an 'a-structure and end up with an 'a set-structure. But 'a set does not inject back to 'a. Nevertheless, the ZF technique still applies, since the powerset of a ZF set is a ZF set. In general, for each passage to another type, the two types are usually related. By carefully examining the construction, we can determine when a transformation remains within V.

Finally, Xu and Norrish [XN20] provide a different solution that produces an 'a-structure instead of an 'a set-structure. They consider representatives of equivalence classes instead of equivalence classes. However, their construction requires the axiom of choice, which is tricky to reason about [Pau06].

6. RELATED WORK

Our work generalizes aspects of the work by Xu and Norrish [XN20] in HOL4. Whereas Xu and Norrish formalized basic modal logic, our syntax covers multi-modal operators. Later, to effectively enable quantification over types, Xu and Norrish [XN23] reformulated some fragments of their HOL4 formulation in DiaToM/SEAR. In HOL Light, Marco and Brogi [MPB21] formalized the completeness of Gödel-Löb provability logic. In particular, they consider the same class of models, namely Kripke models, as in our work. For all of this work, proofs are written in proof scripts only, while our work benefits from the readability of Isar. The formalization of Kripke semantics has been studied extensively in Rocq, including in Doczkal's PhD thesis [Doc16], Shillito's PhD thesis [Shi23], and Kirst and Hagemeier's work [HK22]. Each of them addresses specific modal proof systems and their semantics.

A related formalization is being developed in Lean as part of the Formalized Formal Logic effort;<fnref n="2" /> it also formalizes aspects of proof theory and establishes soundness and completeness. Further work about proof theory for modal logic in Lean includes Wu and Goré's [WG19] formalization of a decision procedure for the proof systems K, KT, and S4—all of which pertain to the basic modal language. Their approach focuses on tree-like structures by

<footnote n="2">²https://formalizedformallogic.github.io/Book/</footnote>
considering only trees as the underlying frames, rather than proving the tree-like model
property.

We are unaware of any general mechanization efforts for multi-modal logics. Existing work, again on proof theory, focuses on specific instances of non-basic modal languages. Early work by Dawson and Goré [DG98] formalized tense logic $K_t$, which features four modal operators, in Isabelle/HOL. More recently, Dawson et al. [DGW16] also formalized S4C, which has two primary operators. In addition, Li [Li20] and Neeley [Nee21] have worked in Lean on public announcement logic, which involves infinitely many modal operators, for the proof theory S5.

Apart from Xu and Norrish, we are unaware of any attempts at developing modal model
theory in general, as opposed to specifying semantics concretely for a particular syntax and
proof system. Moreover, the formal study of non-unary modal operators remains largely
unexplored. Among the existing formalizations, linear temporal logic appears to be the only
framework incorporating a binary operator, as formalized in Coq by Peigné [Pei23] together
with Rajeev Goré and in Isabelle by Sickert [Sic16] together with Benedikt Seidl.

Logics can also combine modal operators with quantification. The simplest instance of
such a logic was formalized in Coq by Borges [dAB22]. Benzmüller, with various co-authors,
investigated embeddings of modal logic in HOL with interactive and automated proof
assistants [BWP15, SSSB23, PB24]. Moreover, Basin et al. [BRV01] implemented quantified
modal logic using Isabelle’s meta-logic [BMV98]. Benzmüller’s work in Leo-III [Ben10]
demonstrates that quantified modal logic is straightforward to verify once implemented.

Although the logic of multi-arity relational structures has not been extensively formalized,
there exist formalizations on the structures themselves, such as the labeled transition systems
formalization by Schlichtkrull et al. [SSST23] and the automata library by Lammich [Lam14].

Existing formalizations of model theory beyond modal logics include work by Harrison
for first-order logic in HOL Light [Har98], recently translated to Isabelle/HOL [TP25], as
well as work by Michaelis and Nipkow on propositional model theory [MN17].

7. CONCLUSION

We built a foundational framework for formalizing propositional modal model theory in an
arbitrary modal language. Using Isar, we constructed structured, readable proofs. Compared
with Xu and Norrish [XN20], we generalized the theory to any number of modal operators
and any arity and we provided a proof of the finiteness of modal formulas in a finite signature
of degree at most *k*. The extra complexity associated with our more general setting is
evident from the proof of finite tree-like model property.

We confirm that Isabelle is well suited to our objectives. Its automation is valuable,
and the inability to quantify over types does not, in practice, hinder the formulation and
proof of theorems. By using HOLZF, we eliminated type changes in the theorems we proved.
We believe that this approach is broadly applicable to addressing similar challenges in the
formalization of various branches of mathematics.

For future work, it would be sensible to formalize further aspects of modal model theory.
The technique of applying ZF to resolve type issues also deserves further exploration, both
for extending the present work and for formalizing mathematical structures more broadly.
Another promising direction stems from the connection between modal logic and universal
coalgebra [Pat01]. Since modal logic provides a framework for reasoning about systems that
can be modeled by universal coalgebras, it would be interesting to explore relevant tools
from this discipline, such as polynomial functors, for a more elegant and abstract treatment of modal logic and its formalization.

## ACKNOWLEDGEMENT

Xu and Blanchette are co-funded by the European Union (ERC, Nekoka, 101083038). Views and opinions expressed are however those of the authors only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

## REFERENCES

[BBB<sup>+</sup>17] Julian Biendarra, Jasmin Christian Blanchette, Aymeric Bouzy, Martin Desharnais, Mathias Fleury, Johannes Hölzl, Ondrej Kuncar, Andreas Lochbihler, Fabian Meier, Lorenz Panny, Andrei Popescu, Christian Sternagel, René Thiemann, and Dmitriy Traytel. Foundational (co)datatypes and (co)recursion for higher-order logic. In Clare Dixon and Marcelo Finger, editors, *Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Brasília, Brazil, September 27-29, 2017, Proceedings*, volume 10483 of *Lecture Notes in Computer Science*, pages 3–21. Springer, 2017. doi:10.1007/978-3-319-66167-4_1.

[BBN11a] Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. Automatic proof and disproof in Isabelle/HOL. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, *Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings*, volume 6989 of *Lecture Notes in Computer Science*, pages 12–27. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24364-6_2, doi:10.1007/978-3-642-24364-6_2.

[BBN11b] Jasmin Christian Blanchette, Lukas Bulwahn, and Tobias Nipkow. Automatic proof and disproof in isabelle/hol. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, *Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings*, volume 6989 of *Lecture Notes in Computer Science*, pages 12–27. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24364-6_2.

[BC04] Yves Bertot and Pierre Castéran. *Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions*. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: https://doi.org/10.1007/978-3-662-07964-5.

[Ben10] Christoph Benzmüller. *Verifying the Modal Logic Cube Is an Easy Task (For Higher-Order Automated Reasoners)*, pages 117–128. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010. doi:10.1007/978-3-642-17172-7_7.

[BHMN15] Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. Mining the Archive of Formal Proofs. In Manfred Kerber, editor, *CICM 2015*, volume 9150 of LNCS, pages 1–15. Springer, 2015. doi:10.1007/978-3-319-20615-8_1.

[Bla19] Jasmin Christian Blanchette. Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In Assia Mahboubi and Magnus O. Myreen, editors, *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019*, pages 1–13. ACM, 2019. doi:10.1145/3293880.3294087.

[BMV98] David Basin, Seán Matthews, and Luca Viganò. Labelled modal logics: Quantifiers. *Journal of Logic, Language and Information*, 7(3):237–263, 1998. doi:10.1023/a:1008278803780.

[BRV01] Patrick Blackburn, Maarten de Rijke, and Yde Venema. *Modal Logic*. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. doi:10.1017/CBO9781107050884.

[BWP15] Christoph Benzmüller and Bruno Woltzenlogel Paleo. Interacting with modal logics in the Coq proof assistant. In Lev D. Beklemishev and Daniil V. Musatov, editors, *Computer Science – Theory and Applications*, pages 398–411, Cham, 2015. Springer International Publishing.

[dAB22] Ana de Almeida Borges. Towards a Coq formalization of a quantified modal logic, 2022. URL: https://arxiv.org/abs/2206.03358, arXiv:2206.03358.
[DG98] Jeremy E. Dawson and Rajeev Goré. A mechanisation of classical modal tense logics using isabelle. In Grigoris Antoniou and John Slaney, editors, *Advanced Topics in Artificial Intelligence*, pages 107–118, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg.

[DGW16] Jeremy E. Dawson, Rajeev Goré, and Jesse Wu. *Machine-Checked Proof-Theory for Propositional Modal Logics*, pages 173–243. Springer International Publishing, Cham, 2016. doi:10.1007/978-3-319-29198-7_5.

[Doc16] Christian Doczkal. *A machine-checked constructive metatheory of computation tree logic*. PhD thesis, Saarland University, 2016. URL: http://scidok.sulb.uni-saarland.de/volltexte/2016/6451/.

[Fro18] Asta Halkjær From. Epistemic logic: Completeness of modal logics. *Archive of Formal Proofs*, October 2018. https://isa-afp.org/entries/Epistemic_Logic.html, Formal proof development.

[Har98] John Harrison. Formalizing basic first order model theory. In Jim Grundy and Malcolm C. Newey, editors, *Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings*, volume 1479 of Lecture Notes in Computer Science, pages 153–170. Springer, 1998. URL: https://doi.org/10.1007/BFb0055135, doi:10.1007/BFB0055135.

[HK22] Christian Hagemeier and Dominik Kirst. Constructive and mechanised meta-theory of intuitionistic epistemic logic. In *Logical Foundations of Computer Science: International Symposium, LFCS 2022, Deerfield Beach, FL, USA, January 10–13, 2022, Proceedings*, page 90–111, Berlin, Heidelberg, 2022. Springer-Verlag. doi:10.1007/978-3-030-93100-1_7.

[Lam14] Peter Lammich. The cava automata library. *Archive of Formal Proofs*, May 2014. https://isa-afp.org/entries/CAVA_Automata.html, Formal proof development.

[Li20] Jiatu Li. Formalization of PAL-S5 in proof assistant. *CoRR*, abs/2012.09388, 2020. URL: https://arxiv.org/abs/2012.09388, arXiv:2012.09388.

[MN17] Julius Michaelis and Tobias Nipkow. Formalized proof systems for propositional logic. In Andreas Abel, Fredrik Nordvall Forsberg, and Ambrus Kaposi, editors, *23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, Hungary*, volume 104 of LIPIcs, pages 5:1–5:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.TYPES.2017.5, doi:10.4230/LIPICS.TYPES.2017.5.

[MPB21] Marco Maggesi and Cosimo Perini Brogi. A Formal Proof of Modal Completeness for Provability Logic. In Liron Cohen and Cezary Kaliszyk, editors, *12th International Conference on Interactive Theorem Proving (ITP 2021)*, volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1–26:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.26, doi:10.4230/LIPIcs.ITP.2021.26.

[MU21] Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In *Automated Deduction - CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings*, page 625–635, Berlin, Heidelberg, 2021. Springer-Verlag. doi:10.1007/978-3-030-79876-5_37.

[Nee21] Paula Neeley. A formalization of dynamic epistemic logic, 2021. URL: https://paulaneeley.com/wp-content/uploads/2021/05/draft1.pdf.

[NHPD23] Cláudia Nalon, Ullrich Hustadt, Fabio Papacchini, and Clare Dixon. Buy one get 14 free: Evaluating local reductions for modal logic. In Brigitte Pientka and Cesare Tinelli, editors, *Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings*, volume 14132 of Lecture Notes in Computer Science, pages 382–400. Springer, 2023. doi:10.1007/978-3-031-38499-8_22.

[Obu06] Steven Obua. Partizan games in Isabelle/HOLZF. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, *Theoretical Aspects of Computing - ICTAC 2006*, pages 272–286, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg.

[Pat01] Dirk Pattinson. Semantical principles in the modal logic of coalgebras. In Afonso Ferreira and Horst Reichel, editors, *STACS 2001, 18th Annual Symposium on Theoretical Aspects of Computer Science, Dresden, Germany, February 15-17, 2001, Proceedings*, volume 2010 of Lecture Notes in Computer Science, pages 514–526. Springer, 2001. doi:10.1007/3-540-44693-1_45.

[Pau06] Lawrence C. Paulson. Defining functions on equivalence classes. *ACM Trans. Comput. Logic*, 7(4):658–675, October 2006. doi:10.1145/1183278.1183280.
[Pau19] Lawrence C. Paulson. Zermelo fraenkel set theory in higher-order logic. *Archive of Formal Proofs*, October 2019. https://isa-afp.org/entries/ZFC_in_HOL.html, Formal proof development.

[PB10] Lawrence C. Paulson and Jasmin Christian Blanchette. Three years of experience with sledge-hammer, a practical link between automatic and interactive theorem provers. In Geoff Sutcliffe, Stephan Schulz, and Eugenia Ternovska, editors, *The 8th International Workshop on the Implementation of Logics, IWIL 2010, Yogyakarta, Indonesia, October 9, 2011*, volume 2 of *EPiC Series in Computing*, pages 1–11. EasyChair, 2010. URL: https://doi.org/10.29007/36dt, doi:10.29007/36DT.

[PB24] Xavier Parent and Christoph Benzmüller. Conditional normative reasoning as a fragment of HOL. *J. Appl. Non Class. Logics*, 34(4):561–592, 2024. doi:10.1080/11663081.2024.2386917.

[Pei23] Anthony Peigné. Verified tableaux: From modal logics to modal fixpoint logics. Master’s thesis, Australian National University, 2023.

[Shi23] Ian Shillito. *New Foundations for the Proof Theory of Bi-Intuitionistic and Provability Logics Mechanized in Coq*. PhD thesis, Australian National University, Canberra, 2023.

[Sic16] Salomon Sickert. Linear temporal logic. *Archive of Formal Proofs*, March 2016. https://isa-afp.org/entries/LTL.html, Formal proof development.

[Sid10] T. Sider. *Logic for Philosophy*. Oxford University Press, 2010. URL: https://books.google.fr/books?id=-KkPEAAAQBAJ.

[SSSB23] Alexander Steen, Geoff Sutcliffe, Tobias Scholl, and Christoph Benzmüller. Solving modal logic problems by translation to higher-order logic. In Andreas Herzig, Jieting Luo, and Pere Pardo, editors, *Logic and Argumentation - 5th International Conference, CLAR 2023, Hangzhou, China, September 10-12, 2023, Proceedings*, volume 14156 of *Lecture Notes in Computer Science*, pages 25–43. Springer, 2023. doi:10.1007/978-3-031-40875-5\_3.

[SSST23] Anders Schlichtkrull, Morten Konggaard Schou, Jiří Srba, and Dmitriy Traytel. Labeled transition systems. *Archive of Formal Proofs*, October 2023. https://isa-afp.org/entries/Labeled_Transition_Systems.html, Formal proof development.

[TP25] Sophie Tourret and Lawrence C. Paulson. Compactness theorem for first-order logic. *Archive of Formal Proofs*, February 2025. https://isa-afp.org/entries/FOL_Compactness.html, Formal proof development.

[Wen07] Makarius Wenzel. Isabelle/Isar—a generic framework for human-readable proof documents. In Roman Matuszewski and Anna Zalewska, editors, *From Insight to Proof: Festschrift in Honour of Andrzej Trybulec*, volume 10(23) of *Studies in Logic, Grammar, and Rhetoric*. University of Bialystok, 2007.

[WG19] Minchao Wu and Rajeev Goré. Verified decision procedures for modal logics. In *International Conference on Interactive Theorem Proving*, 2019. URL: https://api.semanticscholar.org/CorpusID:201836124.

[XN20] Yiming Xu and Michael Norrish. Mechanised modal model theory. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, *International Joint Conference on Automated Reasoning (IJCAR), Paris, France*, volume 12166 of *Lecture Notes in Computer Science*, pages 518–533. Springer, 2020. doi:10.1007/978-3-030-51074-9\_30.

[XN23] Yiming Xu and Michael Norrish. Dependently sorted theorem proving for mathematical foundations. In Adam Naumowicz and René Thiemann, editors, *14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bialystok, Poland*, volume 268 of *LIPIcs*, pages 33:1–33:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.33, doi:10.4230/LIPICS.ITP.2023.33.