Frame Definability

Source file content/normal-modal-logic/frame-definability/frame-definability.tex

Source file content/normal-modal-logic/frame-definability/introduction.tex

Introduction

One question that interests modal logicians is the relationship between the accessibility relation and the truth of certain formulas in models with that accessibility relation. For instance, suppose the accessibility relation is reflexive, i.e., for every $w \in W$source, $Rww$source. In other words, every world is accessible from itself. That means that when $\Box !A$source is true at a world $w$source, $w$source itself is among the accessible worlds at which $!A$source must therefore be true. So, if the accessibility relation $R$source of $\mModel{M}$source is reflexive, then whatever world $w$source and formula $!A$source we take, $\Box !A \lif !A$source will be true there (in other words, the schema $\Box p \lif p$source and all its substitution instances are true in $\mModel{M}$source).

The converse, however, is false. It's not the case, e.g., that if $\Box p \lif p$source is true in $\mModel{M}$source, then $R$source is reflexive. For we can easily find a non-reflexive model $\mModel{M}$source where $\Box p \lif p$source is true at all worlds: take the model with a single world $w$source, not accessible from itself, but with $w \in V(p)$source. By picking the truth value of $p$source suitably, we can make $\Box !A \lif !A$source true in a model that is not reflexive.

The solution is to remove the variable assignment $V$source from the equation. If we require that $\Box p \lif p$source is true at all worlds in $\mModel{M}$source, regardless of which worlds are in $V(p)$source, then it is necessary that $R$source is reflexive. For in any non-reflexive model, there will be at least one world $w$source such that not $Rww$source. If we set $V(p) = W \setminus \{w\}$source, then $p$source will be true at all worlds other than $w$source, and so at all worlds accessible from $w$source (since $w$source is guaranteed not to be accessible from $w$source, and $w$source is the only world where $p$source is false). On the other hand, $p$source is false at $w$source, so $\Box p \lif p$source is false at $w$source.

This suggests that we should introduce a notation for model structures without a valuation: we call these frames. A frame $\mModel{F}$source is simply a pair $\tuple{W, R}$source consisting of a set of worlds with an accessibility relation. Every model $\tuple{W, R, V}$source is then, as we say, based on the frame $\tuple{W, R}$source. Conversely, a frame determines the class of models based on it; and a class of frames determines the class of models which are based on any frame in the class. And we can define $\mModel{F} \Entails !A$source, the notion of a formula being valid in a frame as: $\mSat{M}{!A}$source for all $\mModel{M}$source based on $\mModel{F}$source.

With this notation, we can establish correspondence relations between formulas and classes of frames: e.g., $\mModel{F} \Entails \Box p \lif p$source if, and only if, $\mModel{F}$source is reflexive.

Source file content/normal-modal-logic/frame-definability/properties-accessibility.tex

Properties of Accessibility Relations

Many modal formulas turn out to be characteristic of simple, and even familiar, properties of the accessibility relation. In one direction, that means that any model that has a given property makes a corresponding formula (and all its substitution instances) true. We begin with five classical examples of kinds of accessibility relations and the formulas the truth of which they guarantee.

Notice that the converse implications of the theorem that five accessibility properties guarantee their corresponding modal schemas do not hold: it's not true that if a model verifies a schema, then the accessibility relation of that model has the corresponding property. In the case of AxT and reflexive models, it is easy to give an example of a model in which AxT itself fails: let $W = \{w\}$source and $V(p) = \emptyset$source. Then $R$source is not reflexive, but $\mSat{M}{\Box p}[w]$source and $\mSat/{M}{p}[w]$source. But here we have just a single instance of AxT that fails in $\mModel{M}$source; other instances, e.g., $\Box \lnot p \lif \lnot p$source are true. It is harder to give examples where every substitution instance of AxT is true in $\mModel{M}$source and $\mModel{M}$source is not reflexive. But there are such models, too:

Although we will focus on the five classical formulas AxD, AxT, AxB, Ax4, and Ax5, we record in the table of five additional correspondence facts a few more properties of accessibility relations. The accessibility relation $R$source is partially functional, if from every world at most one world is accessible. If it is the case that from every world exactly one world is accessible, we call it functional. (Thus the functional relations are precisely those that are both serial and partially functional). They are called “functional” because the accessibility relation operates like a (partial) function. A relation is weakly dense if whenever $Ruv$source, there is a $w$source “between” $u$source and $v$source. So weakly dense relations are in a sense the opposite of transitive relations: in a transitive relation, whenever you can reach $v$source from $u$source by a detour via $w$source, you can reach $v$source from $u$source directly; in a weakly dense relation, whenever you can reach $v$source from $u$source directly, you can also reach it by a detour via some $w$source. A relation is weakly directed if whenever you can reach worlds $u$source and $v$source from some world $w$source, you can reach a single world $t$source from both $u$source and $v$source---this is sometimes called the “diamond property” or “confluence.”

Source file content/normal-modal-logic/frame-definability/frames.tex

Frames

The reason frames are interesting is that correspondence between schemas and properties of the accessibility relation $R$source is at the level of frames, not of models. For instance, although AxT is true in all reflexive models, not every model in which AxT is true is reflexive. However, it is true that not only is AxT valid on all reflexive frames, also every frame in which AxT is valid is reflexive.

Remark. Validity in a class of frames is a special case of the notion of validity in a class of models: $\mClass{F} \Entails !A$source iff $\mClass{C} \Entails !A$source where $\mClass{C}$source is the class of all models based on a frame in $\mClass{F}$source.

Obviously, if a formula or a schema is valid, i.e., valid with respect to the class of all models, it is also valid with respect to any class $\mClass{F}$source of frames. End remark.

Source file content/normal-modal-logic/frame-definability/definability.tex

Frame Definability

Even though the converse implications of the theorem that five accessibility properties guarantee their corresponding modal schemas fail, they hold if we replace “model” by “frame”: for the properties considered in the theorem that five accessibility properties guarantee their corresponding modal schemas, it is true that if a formula is valid in a frame then the accessibility relation of that frame has the corresponding property. So, the formulas considered define the classes of frames that have the corresponding property.

We now proceed to establish the full definability results for frames.

You'll notice a difference between the proof for AxD and the other cases: no mention was made of the valuation $V$source. In effect, we proved that if $\mSat{M}{\Ax{D}}$source then $\mModel{M}$source is serial. So AxD defines the class of serial models, not just frames.

the full correspondence theorem for D, T, B, four, and five also shows that the properties can be combined: for instance if both AxB and Ax4 are valid in $\mModel{F}$source then the frame is both symmetric and transitive, etc. Many important modal logics are characterized as the set of formulas valid in all frames that combine some frame properties, and so we can characterize them as the set of formulas valid in all frames in which the corresponding defining formulas are valid. For instance, the classical system LogS4 is the set of all formulas valid in all reflexive and transitive frames, i.e., in all those where both AxT and Ax4 are valid. LogS5 is the set of all formulas valid in all reflexive, symmetric, and euclidean frames, i.e., all those where all of AxT, AxB, and Ax5 are valid.

Logical relationships between properties of $R$source in general correspond to relationships between the corresponding defining formulas. For instance, every reflexive relation is serial; hence, whenever AxT is valid in a frame, so is AxD. (Note that this relationship is not that of entailment. It is not the case that whenever $\mSat{M}{\Ax{T}}[w]$source then $\mSat{M}{\Ax{D}}[w]$source.) We record some such relationships.

Source file content/normal-modal-logic/frame-definability/first-order-definability.tex

First-order Definability

We've seen that a number of properties of accessibility relations of frames can be defined by modal formulas. For instance, symmetry of frames can be defined by the formula AxB, $p \lif \Box\Diamond p$source. The conditions we've encountered so far can all be expressed by first-order formulas in a language involving a single two-place predicate symbol. For instance, symmetry is defined by $\lforall[x][\lforall[y][(\Atom{Q}{x,y} \lif \Atom{Q}{y, x})]]$source in the sense that a first-order structure $\Struct{M}$source with $\Domain{M} = W$source and $\Assign{Q}{M} = R$source satisfies the preceding formula iff $R$source is symmetric. This suggests the following definition:

It turns out that the properties and modal formulas that define them considered so far are exceptional. Not every formula defines a first-order definable class of frames, and not every first-order definable class of frames is definable by a modal formula.

A counterexample to the first is given by the Löb formula:

AxW defines the class of transitive and converse well-founded frames. A relation is well-founded if there is no infinite sequence $w_1$source, $w_2$source, dots such that $Rw_2w_1$source, $Rw_3w_2$source, dots. For instance, the relation $<$source on $\Nat$source is well-founded, whereas the relation $<$source on $\Int$source is not. A relation is converse well-founded iff its converse is well-founded. So converse well-founded relations are those where there is no infinite sequence $w_1$source, $w_2$source, dots such that $Rw_1w_2$source, $Rw_2w_3$source, dots.

There is, however, no first-order formula defining transitive converse well-founded relations. For suppose $\Sat{M}{!F}$source iff $R = \Assign{Q}{M}$source is transitive converse well-founded. Let $!A_n$source be the formula

Now consider the set of formulas

Every finite subset of $\Gamma$source is satisfiable: Let $k$source be largest such that $!A_k$source is in the subset, $\Domain{M_k} = \{1, \dots, k\}$source, $\Assign{a_i}{M_k} = i$source, and $\Assign{Q}{M_k} = <$source. Since $<$source on $\{1, \dots, k\}$source is transitive and converse well-founded, $\Sat{M_k}{!F}$source. $\Sat{M_k}{!A_i}$source by construction, for all $i \le k$source. By the Compactness Theorem for first-order logic, $\Gamma$source is satisfiable in some structure $\Struct{M}$source. By hypothesis, since $\Sat{M}{!F}$source, the relation $\Assign{Q}{M}$source is converse well-founded. But clearly, $\Assign{a_1}{M}$source, $\Assign{a_2}{M}$source, dots would form an infinite sequence of the kind ruled out by converse well-foundedness.

A counterexample to the second claim is given by the property of universality: for every $u$source and $v$source, $Ruv$source. Universal frames are first-order definable by the formula $\lforall[x][\lforall[y][\Atom{Q}{x,y}]]$source. However, no modal formula is valid in all and only the universal frames. This is a consequence of a result that is independently interesting: the formulas valid in universal frames are exactly the same as those valid in reflexive, symmetric, and transitive frames. There are reflexive, symmetric, and transitive frames that are not universal, hence every formula valid in all universal frames is also valid in some non-universal frames.

Source file content/normal-modal-logic/frame-definability/equivalence-S5.tex

Equivalence Relations and LogS5

The modal logic LogS5 is characterized as the set of formulas valid on all universal frames, i.e., every world is accessible from every world, including itself. In such a scenario, $\Box$source corresponds to necessity and $\Diamond$source to possibility: $\Box !A$source is true if $!A$source is true at every world, and $\Diamond !A$source is true if $!A$source is true at some world. It turns out that LogS5 can also be characterized as the formulas valid on all reflexive, symmetric, and transitive frames, i.e., on all equivalence relations.

Since AxT, AxB, and Ax4 characterize the reflexive, symmetric, and transitive frames, the frames where the accessibility relation is an equivalence relation are exactly those in which all three formulas are valid. It turns out that the equivalence relations can also be characterized by other combinations of formulas, since the conditions with which we've defined equivalence relations are equivalent to combinations of other familiar conditions on $R$source.

the proposition giving four equivalent characterizations of equivalence relations is the semantic counterpart to the later proposition listing four equivalent axiomatizations of S five, in that it gives an equivalent characterization of the modal logic of frames over which $R$source is an equivalence relation (the logic traditionally referred to as LogS5).

What is the relationship between universal and equivalence relations? Although every universal relation is an equivalence relation, clearly not every equivalence relation is universal. However, the formulas valid on all universal relations are exactly the same as those valid on all equivalence relations.

Source file content/normal-modal-logic/frame-definability/second-order-definability.tex

Second-order Definability

Not every frame property definable by modal formulas is first-order definable. However, if we allow quantification over one-place predicates (i.e., monadic second-order quantification), we define all modally definable frame properties. The trick is to exploit a systematic way in which the conditions under which a modal formula is true at a world are related to first-order formulas. This is the so-called standard translation of modal formulas into first-order formulas in a language containing not just a two-place predicate symbol $Q$source for the accessibility relation, but also a one-place predicate symbol $P_i$source for the propositional variables $\Obj p_i$source occurring in $!A$source.

For instance, $\ST_x(\Box p \lif p)$source is $\lforall[y][(\Atom{Q}{x,y} \lif \Atom{P}{y})] \lif \Atom{P}{x}$source. Any structure for the language of $\ST_x(!A)$source requires a domain, a two-place relation assigned to $Q$source, and subsets of the domain assigned to the one-place predicate symbols $P_i$source. In other words, the components of such a structure are exactly those of a model for $!A$source: the domain is the set of worlds, the two-place relation assigned to $Q$source is the accessibility relation, and the subsets assigned to $P_i$source are just the assignments $V(\Obj p_i)$source. It won't surprise that satisfaction of $!A$source in a modal model and of $\ST_x(!A)$source in the corresponding structure agree:

As an example, consider again the formula $\Box p \lif p$source. It defines reflexivity. Reflexivity is of course first-order definable by the sentence $\lforall[x][\Atom{Q}{x,x}]$source. But it is also definable by the monadic second-order sentence

This means, of course, that the two sentences are equivalent. Here's how you might convince yourself of this directly: First suppose the second-order sentence is true in a structure $\Struct{M}$source. Since $x$source and $X$source are universally quantified, the remainder must hold for any $x \in W$source and set $X \subseteq W$source, e.g., the set $\Setabs{z}{Rxz}$source where $R = \Assign{Q}{M}$source. So, for any $s$source with $s(x) \in W$source and $s(X) = \Setabs{z}{Rxz}$source we have $\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})] \lif \Atom{X}{x}}$source. But by the way we've picked $s(X)$source that means $\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif \Atom{Q}{x,y})] \lif \Atom{Q}{x,x}}[s]$source, which is equivalent to $\Atom{Q}{x,x}$source since the antecedent is valid. Since $s(x)$source is arbitrary, we have $\Sat{M}{\lforall[x][\Atom{Q}{x,x}]}$source.

Now suppose that $\Sat{M}{\lforall[x][\Atom{Q}{x,x}]}$source and show that $\Sat{M}{\lforall[X][\lforall[x][(\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})] \lif \Atom{X}{x})]]}$source. Pick any assignment $s$source, and assume $\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})]}[s]$source. Let $s'$source be the $y$source-variant of $s$source with $s'(y) = s(x)$source; we have $\Sat{M}{\Atom{Q}{x,y} \lif \Atom{X}{y}}[s']$source, i.e., $\Sat{M}{\Atom{Q}{x,x} \lif \Atom{X}{x}}[s]$source. Since $\Sat{M}{\lforall[x][\Atom{Q}{x,x}]}$source, the antecedent is true, and we have $\Sat{M}{\Atom{X}{x}}[s]$source, which is what we needed to show.

Since some definable classes of frames are not first-order definable, not every monadic second-order sentence of the form $!A'$source is equivalent to a first-order sentence. There is no effective method to decide which ones are.