A class of Kripke frames is called modally definable if there is a set of modal formulas such that the class consists exactly of frames on which every formula from that set is valid, i. e. globally true under any valuation. Here, existential definability of Kripke frame classes is defined analogously, by demanding that each formula from a defining set is satisfiable under any valuation. This is equivalent to the definability by the existential fragment of modal language enriched with the universal modality. A model theoretic characterization of this type of definability is given.
Model theoretic closure conditions that are necessary and sufficient for an
elementary class of frames (i. e. first-order definable property of relational structures) to be
modally definable are given by the famous Goldblatt-Thomason Theorem.
Theorem (Goldblatt-Thomason [
All of the frame constructions used in the theorem – bounded morphisms, disjoint
unions, generated subframes and ultrafilter extensions – are presented in detail in [
Now, an alternative notion of definability is proposed here as follows. Definition. A class K of Kripke frames is called modally ∃-definable if there is a set Σ of modal formulas such that for any Kripke frame F we have: F ∈ K if and only if each ϕ ∈ Σ is satisfiable in M, for any model M based on F. If this is the case, we denote K = Fr∃(Σ).
The definition does not require that all formulas of Σ are satisfied at the same point – it suffices that each formula of Σ is satisfied at some point.
In the sequel, a notation Mod(F ) is used for a class of structures defined by a first-order formula F . Similarly, if Σ = {ϕ} is a singleton set of modal formulas, we write Fr∃(ϕ) instead of Fr∃({ϕ}).
Example 1. It is well-known that the formula p → ✸p defines reflexivity, i. e. Fr(p → ✸p) = Mod(∀xRxx). Now, it is easy to see that Fr∃(p → ✸p) is the class of all frames such that R 6= ∅, that is Fr∃(p → ✸p) = Mod(∃x∃yRxy). This class is not modally definable in the usual sense, since it is clearly not closed under generated subframes. Note that the condition R 6= ∅ is ∃-definable also by a simpler formula ✸⊤.
Theorem 1. Let K be an elementary class of Kripke frames. Then K is modally ∃definable if and only if it is closed under surjective bounded morphisms and reflects generated subframes and ultrafilter extensions.
This is an analogue of a similar characterization of existentially definable Kripke
model classes, given in [
The starting point of correspondence between first-order and modal logic is the standard translation, a mapping that translates each modal formula ϕ to the first-order formula STx(ϕ), as follows:
STx(p) = P x, for each p ∈ Φ, STx(⊥) = ⊥, STx(¬ϕ) = ¬STx(ϕ), STx(ϕ ∨ ψ) = STx(ϕ) ∨ STx(ψ),
STx(✸ϕ) = ∃y(Rxy ∧ STy(ϕ)).
Clearly, we have M, w ϕ if and only if M |= STx(ϕ)[w], and M ϕ if and only
if M |= ∀xSTx(ϕ). But, validity of a formula on a frame generally is not first-order
expressible, since we need to quantify over valuations. We have a second-order standard
translation, that is, F ϕ if and only if F |= ∀P1 . . . ∀Pn∀xSTx(ϕ), where P1, . . . , Pn
are monadic second-order variables, one for each propositional variable occurring in ϕ.
So, the notion of modal definability is equivalent to the definability by a set of
secondorder formulas of the form ∀P1 . . . ∀Pn∀xSTx(ϕ). However, in many cases a formula
of this type is equivalent to a first-order formula. Namely, this holds for any Sahlqvist
formula (the definition is omitted here – see [
Now, ∃-definability is clearly also equivalent to the definability by a type of secondorder formulas – those of the form ∀P1 . . . ∀Pn∃xSTx(ϕ). Consider another example of a modally ∃-definable class.
Example 2. The condition F = ∃x∀y(Rxy → ∃zRyz) is not modally definable, since it is not closed under generated subframes, but it is modally ∃-definable by the formula ϕ = p → ✷✸p.
To prove this, we need to show Fr∃(ϕ) = Mod(F ). But F = (W, R) ∈ Fr∃(ϕ) if and only if F |= ∀P ∃x(P x → ∀y(Rxy → ∃z(Ryz ∧ P z))). So in particular, under the assignment which assigns the entire W to the second-order variable P , we get F |= ∃x∀y(Rxy → ∃zRyz), thus F ∈ Mod(F ). The reverse inclusion is proved similarly.
Other changes of quantifiers or the order of first and second-order quantifiers would
result in other types of definability, perhaps also worthy of exploring. In fact, this has
already been done by Venema [
Proposition 1. Let ϕ be a modal formula which has a first-order local correspondent, i. e. there is a first-order formula F (x) such that for any frame F = (W, R) and any w ∈ W we have F, w ϕ if and only if F |= F (x)[w]. (In particular, this holds for any Sahlqvist formula.)
Then we have Fr−(ϕ) = Mod(∀x¬F (x)).
Proof. We have F ∈ Fr−(ϕ) if and only if F |= ∀x∃P1 . . . ∃PnSTx(¬ϕ) if and only if F 6|= ∃x∀P1 . . . ∀PnSTx(ϕ). But this means that there is no w ∈ W such that F |= ∀P1 . . . ∀PnSTx(ϕ)[w]. The latter holds if and only if F, w ϕ, which is by assumption equivalent to F |= F (x)[w]. The fact that such w does not exist, is equivalent to F ∈ Mod(∀x¬F (x)). ⊓⊔
So for example, since p → ✸p locally corresponds to Rxx, we have that p → ✸p negatively defines irreflexivity, which is not modally definable property, since it is not preserved under surjective bounded morphisms.
This section can be used, if needed, for a quick reference of the basic facts about constructions used in the main theorem. Otherwise it can be omitted.
A bisimulation between Kripke models M = (W, R, V ) and M′ = (W ′, R′, V ′) is a relation Z ⊆ W × W ′ such that: (at) if wZw′ then we have: w ∈ V (p) if and only if w′ ∈ V ′(p), for all p ∈ Φ, (forth) if wZw′ and Rwv, then there is v′ such that vZv′ and R′w′v′, (back) if wZw′ and R′w′v′, then there is v such that vZv′ and Rwv.
The basic property of bisimulations is that (at) extends to all formulas: if wZw′ then M, w ϕ if and only if M′, w′ ϕ, i. e. (M, w) and (M′, w′) are modally equivalent. We get the definition of bisimulation between frames by omitting the condition (at).
A bounded morphism from a frame F = (W, R) to F′ = (W ′, R′) is a function f : W → W ′ such that: (forth) Rwv implies R′f (w)f (v), (back) if R′f (w)v′, then there is v such that v′ = f (v) and Rwv.
Clearly, a bounded morphism is a bisimulation that is also a function.
A generated subframe of F = (W, R) is a frame F′ = (W ′, R′) where W ′ ⊆ W such that w ∈ W ′ and Rwv implies v ∈ W ′, and R′ = R ∩ (W ′ × W ′). A generated submodel of M = (W, R, V ) is a model based on a generated subframe, with the valuation V ′(p) = V (p) ∩ W ′, for all p ∈ Φ. It is easy to see that the global truth of a modal formula is preserved on a generated submodel.
To define the ultraproducts and ultrafilter extensions, we need the notion of ultrafilters. An ultrafilter over a set I 6= ∅ is a family U ⊆ P(I) such that: (1) I ∈ U , (2) if A, B ∈ U , then A ∩ B ∈ U , (3) if A ∈ U and A ⊆ B ⊆ I, then B ∈ U , (4) for all A ⊆ I we have: A ∈ U if and only if I \ A ∈/ U .
The existence of ultrafilters is provided by a fact that any family of subsets which
has the finite intersection property (that is, each finite intersection is non-empty) can
be extended to an ultrafilter (see e. g. [
Let {Mi = (Wi, Ri, Vi) : i ∈ I} be a family of Kripke models and let U be an ultrafilter over I. The ultraproduct of this family over U is the model QU Mi = (W, R, V ) such that:
(1) W is the set of equivalence classes f U of the following relation defined on the Cartesian product of the family: f ∼ g if and only if {i ∈ I : f (i) = g(i)} ∈ U , (2) f U RgU if and only if {i ∈ I : f (i)Rig(i)} ∈ U , (3) f U ∈ V (p) if and only if {i ∈ I : f (i) ∈ Vi(p)} ∈ U , for all p.
The basic property of ultraproducts is that (3) extends to all formulas. Proposition 2. Let {Mi : i ∈ I} be a family of Kripke models and let U be an ultrafilter over I.
Then we have QU Mi, f U ϕ if and only if {i ∈ I : Mi, f (i) ϕ} ∈ U , for any f U . Furthermore, we have QU Mi ϕ if and only if {i ∈ I : Mi ϕ} ∈ U .
This is an analogue of the Lo´s Fundamental Theorem on ultraproducts from the
first-order model theory (see [
An ultraproduct such that Mi = M for all i ∈ I is called an ultrapower of M and denoted QU M. From the Lo´s Theorem it follows that any ultrapower of a model is elementarily equivalent to the model, that is, the same first-order sentences are true on M and QU M. Definition of an ultraproduct of a family of frames is obtained by omitting the clause regarding valuation.
Another notion needed in the proof of the main theorem is modal saturation, the
modal analogue of ω-saturation from the classical model theory. The definition of
saturation is omitted here, since we only need some facts which it implies. Most importantly,
saturation implies a converse of the basic property of bisimulations, which generally
does not hold. In fact, modal equivalence between points of modally saturated
models is a bisimulation. Also, we use the fact that any ω-saturated Kripke model is also
modally saturated (see [
Finally, the ultrafilter extension of a model M = (W, R, V ) is the model ueM =
(Uf(W ), Rue, V ue), where Uf(W ) is the set of all ultrafilters over W , Rueuv holds if
and only if A ∈ v implies m✸(A) ∈ u, where m✸(A) denotes the set of all w ∈ W
such that Rwa for some a ∈ A, and u ∈ V ue(p) if and only if V (p) ∈ u. The basic
property is that this extends to any modal formula, i. e. we have u ∈ V ue(ϕ) if and
only if V (ϕ) ∈ u (see [
The ultrafilter extension of a frame F = (W, R) is ueF = (Uf(W ), Rue). 4
In this section Theorem 1 is proved in detail. Arguments and techniques used in the
proof are similar to the ones used in the proof of Goldblatt-Thomason theorem as
presented in [
Proof (of Theorem 1). Let K = Fr∃(Σ). Let F = (W, R) ∈ K and let f be a surjective bounded morphism from F to some F′ = (W ′, R′). Take any ϕ ∈ Σ and any model M′ = (W ′, R′, V ′) based on F′. Put V (p) = {w ∈ W : f (w) ∈ V ′(p)}. Then V is a well defined valuation on F. Put M = (W, R, V ). Since F ∈ K, there exists w ∈ W such that M, w ϕ. But then M′, f (w) ϕ. This proves that K is closed under surjective bounded morphisms.
To prove that K reflects generated subframes and ultrafilter extensions, let F = (W, R) ∈/ K. This means that there is ϕ ∈ Σ and a model M = (W, R, V ) based on F such that M ¬ϕ. Let F′ = (W ′, R′) be a generated subframe of F. Define V ′(p) = V (p) ∩ W ′, for all p. Then we have M′ ¬ϕ, which proves F′ ∈/ K, as desired. Also, ueM is a model based on the ultrafilter extension ueF and we have ueM ¬ϕ, which proves ueF ∈/ K.
For the converse, let K be an elementary class of frames that is closed under surjective bounded morphisms and reflects generated subframes and ultrafilter extensions. Denote by Σ the set of all formulas that are satisfiable in all models based on all frames in K. Then K ⊆ Fr∃(Σ) and it remains to prove the reverse inclusion.
Let F = (W, R) ∈ Fr∃(Σ). Let Φ be a set of propositional variables that contains a propositional variable pA for each A ⊆ W . Let M = (W, R, V ), where V (pA) = A for all A ⊆ W . Denote by Δ the set of all modal formulas over Φ which are globally true on M. Now, for any finite δ ⊆ Δ there is Fδ ∈ K and a model Mδ based on Fδ such that Mδ δ. Otherwise, since Δ is closed under conjunctions, there is ϕ ∈ Δ such that ¬ϕ ∈ Σ, thus ¬ϕ is satisfiable in M, which contradicts M Δ.
Now, let I be the family of all finite subsets of Δ. For each ϕ ∈ Δ, put ϕˆ = {δ ∈ I : ϕ ∈ δ}. The family {ϕˆ : ϕ ∈ Δ} clearly has the finite intersection property, so it can be extended to an ultrafilter U over I. But for all ϕ ∈ Δ we have {δ ∈ I : Mδ ϕ} ⊇ ϕˆ and ϕˆ ∈ U , thus {δ ∈ I : Mδ ϕ} ∈ U , so the Proposition 2 implies QU Mδ ϕ. The model QU Mδ is based on the frame QU Fδ. Since K is elementary, it is also closed under ultraproducts, so QU Fδ ∈ K. It remains to prove that there is a surjective bounded morphism from some ultrapower of QU Fδ to a generated subframe of ueF. Then the assumed properties of K imply that F ∈ K, as desired.
The classical model theory provides that there is an ω-saturated ultrapower of
QU Mδ (cf. [
First we need to prove that f is well-defined, i. e. that f (w) is indeed an ultrafilter over W .
(1) We easily obtain W ∈ f (w), since pW ∈ Δ by the definition of V . (2) If A, B ∈ f (w), then MΔ, w pA ∧ pB. Clearly, M pA ∧ pB ↔ pA∩B. Thus MΔ pA ∧ pB ↔ pA∩B, so MΔ, w pA∩B, i. e. A ∩ B ∈ f (w).
(3) If A ∈ f (w) and A ⊆ B ⊆ W , then from the definition of V it follows M pA → pB. But then also MΔ pA → pB, hence MΔ, w pB, so B ∈ f (w).
(4) For all A ⊆ W we have M pA ↔ ¬pW \A, which similarly as in the previous points implies A ∈ f (w) if and only if W \ A ∈/ f (w), as desired.
Assume for the moment that we have: u = f (w) if and only if (ueM, u) and (MΔ, w) are modally equivalent. Since ueM and MΔ are modally saturated, the modal equivalence between their points is a bisimulation. So f is a bisimulation, but it is also a function, which means that it is a bounded morphism from FΔ to ueF. But then the corestriction of f to its image is a surjective bounded morphism from an ultrapower of QU Fδ to a generated subframe of ueF, which we needed.
So to conclude the proof, it remains to show that u = f (w) holds if and only if (ueM, u) and (MΔ, w) are modally equivalent. Let u = f (w). Then we have ueM, u ϕ if and only if V (ϕ) ∈ u, which is by the definition of f equivalent to MΔ, w pV (ϕ). But the definition of V clearly implies M ϕ ↔ pV (ϕ), so also MΔ ϕ ↔ pV (ϕ), which provides the needed modal equivalence.
For the converse, the assumption implies that we have ueM, u pA if and only if MΔ, w pA, for all A ⊆ W . This means that V (pA) = A ∈ u if and only if A ∈ f (w), i. e. u = f (w). ⊓⊔ 5
Although the approach of this paper is to define ∃-definability as a metalingual notion,
it should be noted that it can be included in the language itself. That is, the satisfiability
of a modal formula under any valuation on a frame can be expressed by a formula of
the modal language enriched with the universal modality (BMLU). The syntax is an
extension of the basic modal language by new modal operator Aϕ, and we can also
define its dual Eϕ := ¬A¬ϕ. We call A the universal modality, and E the existential
modality. The semantics of the new operators is standard modal semantics, with respect
to the universal binary relation W × W on a frame F = (W, R). This means that the
standard translation of universal and existential operators is as follows (cf. [
Now, let K be a class of Kripke frames. Clearly, K is modally ∃-definable if and only if it is definable by a set of formulas of the existential fragment of BMLU, i. e. by a set of formulas of the form Eϕ, where ϕ is a formula of BML. This immediately follows from the clear fact that for any frame F and any ϕ we have F Eϕ if and only if F |= ∀P1 . . . ∀Pn∃ySTy(ϕ), where P1, . . . , Pn correspond to propositional variables that occur in ϕ, and the letter holds if and only if ϕ is satisfiable under any valuation on F.
Goranko and Passy [
As for some further questions that might be worth exploring, for example, similarly
to the notion of ±-definability from [
On the other hand, a question to be addressed is which modally ∃-definable classes are elementary, and is there an effective procedure analogous to the one for Sahlqvist formulas, to obtain a first-order formula equivalent to a second-order translation ∀P1 . . . ∀Pn∃xSTx(ϕ) for some sufficiently large and interesting class of modal formulas.