Filtrations and Decidability

Definition of subformula and modal closure

A set $\Gamma$source of formulas is closed under subformulas if it contains every subformula of a formula in $\Gamma$source. Further, $\Gamma$source is modally closed if it is closed under subformulas and moreover $!A \in \Gamma$source implies $\Box!A, \Diamond!A \in \Gamma$source.

Filtration equivalence relation

Let $\mModel{M} =\tuple{W, R, V}$source and suppose $\Gamma$source is closed under sub-formulas. Define a relation $\equiv$source on $W$source to hold of any two worlds that make the same formulas from $\Gamma$source true, i.e.:

The equivalence class $[w]_\equiv$source of a world $w$source, or $[w]$source for short, is the set of all worlds $\equiv$source-equivalent to $w$source:

The filtration relation is an equivalence relation

Given $\mModel{M}$source and $\Gamma$source, $\equiv$source as defined above is an equivalence relation, i.e., it is reflexive, symmetric, and transitive.

Proof

The relation $\equiv$source is reflexive, since $w$source makes exactly the same formulas from $\Gamma$source true as itself. It is symmetric since if $u$source makes the same formulas from $\Gamma$source true as $v$source, the same holds for $v$source and $u$source. It is also transitive, since if $u$source makes the same formulas from $\Gamma$source true as $v$source, and $v$source as $w$source, then $u$source makes the same formulas from $\Gamma$source true as $w$source.

Definition of a filtration

Let $\Gamma$source be closed under subformulas and $\mModel{M} = \tuple{W, R, V}$source. A filtration of $\mModel{M}$source through $\Gamma$source is any model $\mModel{M^*} = \tuple{W^*,R^*,V^*}$source, where:

1. $W^* = \Setabs{[w]}{w \in W}$source;

2. For any $u,v \in W$source:

   1. If $Ruv$source then $R^*[u][v]$source;

   2. If $R^*[u][v]$source then for any $\Box !A \in \Gamma$source, if $\mSat{M}{\Box!A}[u]$source then $\mSat{M}{!A}[v]$source;

   3. If $R^*[u][v]$source then for any $\Diamond !A \in \Gamma$source, if $\mSat{M}{!A}[v]$source then $\mSat{M}{\Diamond!A}[u]$source.

3. $V^*(p) = \Setabs{[u]}{u \in V(p)}$source.

Filtration Theorem

If $\mModel{M^*}$source is a filtration of $\mModel{M}$source through $\Gamma$source, then for every $!A \in \Gamma$source and $w \in W$source, we have $\mSat{M}{!A}[w]$source if and only if $\mSat{M^*}{!A}[{[w]}]$source.

Proof

By induction on $!A$source, using the fact that $\Gamma$source is closed under subformulas. Since $!A \in \Gamma$source and $\Gamma$source is closed under sub-formulas, all sub-formulas of $!A$source are also $\in \Gamma$source. Hence in each inductive step, the induction hypothesis applies to the sub-formulas of $!A$source.

1. Case: $!A \ident \lfalse$source

   Neither $\mSat{M}{\indfrm}[w]$source nor $\mSat{M^*}{\indfrm}[{[w]}]$source.

2. Case: $!A \ident p$source

   The left-to-right direction is immediate, as $\mSat{M}{\indfrm}[w]$source only if $w \in V(p)$source, which implies $[w] \in V^*(p)$source, i.e., $\mSat{M^*}{\indfrm}[{[w]}]$source. Conversely, suppose $\mSat{M^*}{\indfrm}[{[w]}]$source, i.e., $[w] \in V^*(p)$source. Then for some $v \in V(p)$source, $w \equiv v$source. Of course then also $\mSat{M}{p}[v]$source. Since $w \equiv v$source, $w$source and $v$source make the same formulas from $\Gamma$source true. Since by assumption $p \in \Gamma$source and $\mSat{M}{p}[v]$source, $\mSat{M}{\indfrm}[w]$source.

3. Case: $!A \ident \lnot !B$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat/{M}{!B}[w]$source. By induction hypothesis, $\mSat/{M}{!B}[w]$source iff $\mSat/{M^*}{!B}[{[w]}]$source. Finally, $\mSat/{M^*}{!B}[{[w]}]$source iff $\mSat{M^*}{\indfrm}[{[w]}]$source.

4. Exercise.

5. Case: $!A \ident (!B \lor !C)$source

   $\mSat{M}{\indfrm}[w]$source iff $\mSat{M}{!B}[w]$source or $\mSat{M}{!C}[w]$source. By induction hypothesis, $\mSat{M}{!B}[w]$source iff $\mSat{M^*}{!B}[{[w]}]$source, and $\mSat{M}{!C}[w]$source iff $\mSat{M^*}{!C}[{[w]}]$source. And $\mSat{M^*}{\indfrm}[{[w]}]$source iff $\mSat{M^*}{!B}[{[w]}]$source or $\mSat{M^*}{!C}[{[w]}]$source.

6. Exercise.

7. Case: $!A \ident \Box !B$source

   Suppose $\mSat{M}{\indfrm}[w]$source; to show that $\mSat{M^*}{\indfrm}[{[w]}]$source, let $v$source be such that $R^*[w][v]$source. From the definition of a filtrationthe necessity-preservation condition for a filtration, we have that $\mSat{M}{!B}[v]$source, and by inductive hypothesis $\mSat{M^*}{!B}[{[v]}]$source. Since $v$source was arbitrary, $\mSat{M^*}{\indfrm}[{[w]}]$source follows.

   Conversely, suppose $\mSat{M^*}{\indfrm}[{[w]}]$source and let $v$source be arbitrary such that $Rwv$source. From the definition of a filtrationthe inherited-edge condition for a filtration, we have $R^*[w][v]$source, so that $\mSat{M^*}{!B}[{[v]}]$source; by inductive hypothesis $\mSat{M}{!B}[v]$source, and since $v$source was arbitrary, $\mSat{M}{\indfrm}[w]$source.

8. Exercise.

Exercise completing the Filtration Theorem

Complete the proof of the Filtration Theorem preserving truth of formulas in Gamma

Model truth and class validity under filtration

Let $\Gamma$source be closed under subformulas. Then:

1. If $\mModel{M^*}$source is a filtration of $\mModel{M}$source through $\Gamma$source then for any $!A \in \Gamma$source: $\mSat{M}{!A}$source if and only if $\mSat{M^*}{!A}$source.

2. If $\mClass{C}$source is a class of models and $\Gamma(\mClass{C})$source is the class of $\Gamma$source-filtrations of models in $\mClass{C}$source, then any formula $!A \in \Gamma$source is valid in $\mClass{C}$source if and only if it is valid in $\Gamma(\mClass{C})$source.

Definition of the finest filtration

Where $\Gamma$source is closed under subformulas, the finest filtration $\mModel{M^*}$source of a model $\mModel{M}$source is defined by putting:

The finest construction is a filtration

The finest filtration $\mModel{M^*}$source is indeed a filtration.

Proof

We need to check that $R^*$source, so defined, satisfies the definition of a filtrationthe accessibility conditions in the definition of a filtration. We check the three conditions in turn.

If $Ruv$source then since $u \in [u]$source and $v \in [v]$source, also $R^*[u][v]$source, so the inherited-edge condition for a filtration is satisfied.

For the necessity-preservation condition for a filtration, suppose $\Box!A \in \Gamma$source, $R^*[u][v]$source, and $\mSat{M}{\Box!A}[u]$source. By definition of $R^*$source, there are $u' \equiv u$source and $v' \equiv v$source such that $Ru'v'$source. Since $u$source and $u'$source agree on $\Gamma$source, also $\mSat{M}{\Box!A}[u']$source, so that $\mSat{M}{!A}[v']$source. By closure of $\Gamma$source under sub-formulas, $v$source and $v'$source agree on $!A$source, so $\mSat{M}{!A}[v]$source, as desired.

We leave the verification of the possibility-preservation condition for a filtration as an exercise.

Exercise completing the finest-filtration proof

probBox,probDiamond Complete the proof of the proposition that the finest construction is a filtration.

Definition of the coarsest filtration

Where $\Gamma$source is closed under subformulas, the coarsest filtration $\mModel{M^*}$source of a model $\mModel{M}$source is defined by putting $R^*[u][v]$source if and only if

both of the following conditions are met:

The coarsest construction is a filtration

The coarsest filtration $\mModel{M^*}$source is indeed a filtration.

Proof

Given the definition of $R^*$source, the only condition that is left to verify is the implication from $Ruv$source to $R^*[u][v]$source. So assume $Ruv$source. Suppose $\Box!A \in \Gamma$source and $\mSat{M}{\Box!A}[u]$source; then obviously $\mSat{M}{!A}[v]$source , and the box clause in the definition of the coarsest filtration is satisfied. Suppose $\Diamond!A \in \Gamma$source and $\mSat{M}{!A}[v]$source. Then $\mSat{M}{\Diamond!A}[u]$source since $Ruv$source , and the diamond clause in the definition of the coarsest filtration is satisfied .

Infinite alternating model and its filtrations

Let $W = \PosInt$source, $Rnm$source iff $m = n + 1$source, and $V(p) = \Setabs{2n}{n \in \Nat}$source. The model $\mModel{M} = \tuple{W, R, V}$source is depicted in the figure showing the infinite alternating model and its two filtrations. The worlds are $1$source, $2$source, etc.; each world can access exactly one other world---its successor---and $p$source is true at all and only the even numbers.

Now let $\Gamma$source be the set of sub-formulas of $\Box p \lif p$source, i.e., $\{p, \Box p, \Box p \lif p\}$source. $p$source is true at all and only the even numbers, $\Box p$source is true at all and only the odd numbers, so $\Box p \lif p$source is true at all and only the even numbers. In other words, every odd number makes $\Box p$source true but $p$source and $\Box p \lif p$source false; every even number makes $p$source and $\Box p \lif p$source true, but $\Box p$source false. So $W^* = \{ [1], [2] \}$source, where $[1] = \{1, 3, 5, \dots\}$source and $[2] = \{2, 4, 6, \dots\}$source. Since $2 \in V(p)$source, $[2] \in V^*(p)$source; since $1 \notin V(p)$source, $[1] \notin V^*(p)$source. So $V^*(p) = \{[2]\}$source.

Any filtration based on $W^*$source must have an accessibility relation that includes $\tuple{[1], [2]}, \tuple{[2],[1]}$source: since $R12$source, we must have $R^*[1][2]$source by the definition of a filtrationthe inherited-edge condition for a filtration, and since $R23$source we must have $R^*[2][3]$source, and $[3]=[1]$source. It cannot include $\tuple{[1],[1]}$source: if it did, we'd have $R^*[1][1]$source, $\mSat{M}{\Box p}[1]$source but $\mSat/{M}{p}[1]$source, contradicting the necessity-preservation condition for a filtration. Nothing requires or rules out that $R^*[2][2]$source. So, there are two possible filtrations of $\mModel{M}$source, corresponding to the two accessibility relations

In either case, $p$source and $\Box p \lif p$source are false and $\Box p$source is true at $[1]$source; $p$source and $\Box p \lif p$source are true and $\Box p$source is false at $[2]$source.

Exercise filtering an infinite binary tree

Consider the following model $\mModel{M} = \tuple{W, R, V}$source where $W = \Setabs{0\sigma}{\sigma \in \Bin^*}$source, the set of sequences of $0$sources and $1$sources starting with $0$source, with $R\sigma\sigma'$source iff $\sigma' = \sigma 0$source or $\sigma' = \sigma 1$source, and $V(p) = \Setabs{\sigma 0}{\sigma \in \Bin^*}$source and $V(q) = \Setabs{\sigma 1}{\sigma \in \Bin^* \setminus \{1\}}$source. Here's a picture:

We have $\mSat/{M}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[w]$source for every $w$source.

Let $\Gamma$source be the set of sub-formulas of $\Box(p \lor q) \lif (\Box p \lor \Box q)$source. What are $W^*$source and $V^*$source? What is the accessibility relation of the finest filtration of $\mModel{M}$source? Of the coarsest?

Finite size of a filtration

If $\Gamma$source is finite then any filtration $\mModel{M^*}$source of a model $\mModel{M}$source through $\Gamma$source is also finite.

Proof

The size of $W^*$source is the number of different classes $[w]$source under the equivalence relation $\equiv$source. Any two worlds $u$source, $v$source in such class---that is, any $u$source and $v$source such that $u \equiv v$source---agree on all formulas $!A$source in $\Gamma$source, $!A \in \Gamma$source either $!A$source is true at both $u$source and $v$source, or at neither. So each class $[w]$source corresponds to subset of $\Gamma$source, namely the set of all $!A \in \Gamma$source such that $!A$source is true at the worlds in $[w]$source. No two different classes $[u]$source and $[v]$source correspond to the same subset of $\Gamma$source. For if the set of formulas true at $u$source and that of formulas true at $v$source are the same, then $u$source and $v$source agree on all formulas in $\Gamma$source, i.e., $u \equiv v$source. But then $[u] = [v]$source. So, there is an injective function from $W^*$source to $\Pow{\Gamma}$source, and hence $\card{W^*} \le \card{\Pow{\Gamma}}$source. Hence if $\Gamma$source contains $n$source sentences, the cardinality of $W^*$source is no greater than $2^n$source.

Definition of the finite model property

A system $\Sigma$source of modal logic is said to have the finite model property if whenever a formula $!A$source is true at a world in a model of $\Sigma$source then $!A$source is true at a world in a finite model of $\Sigma$source.

Finite model property for K

LogK has the finite model property.

Proof

LogK is the set of valid formulas, i.e., any model is a model of LogK. By the Filtration Theorem preserving truth of formulas in Gamma, if $\mSat{M}{!A}[w]$source, then $\mSat{M^*}{!A}[w]$source for any filtration of $\mModel{M}$source through the set $\Gamma$source of sub-formulas of $!A$source. Any formula only has finitely many sub-formulas, so $\Gamma$source is finite. By the proposition bounding the size of a filtration, $\card{W^*} \le 2^n$source, where $n$source is the number of formulas in $\Gamma$source. And since LogK imposes no restriction on models, $\mModel{M^*}$source is a LogK-model.

Universal validity reduced to finite universal models

Let $\mClass{U}$source be the class of universal models (see the equivalence between S five models and universal models used here) and $\mClass{U}_\mathrm{Fin}$source the class of all finite universal models. Then any formula $!A$source is valid in $\mClass{U}$source if and only if it is valid in $\mClass{U}_\mathrm{Fin}$source.

Proof

Finite universal models are universal models, so the left-to-right direction is trivial. For the right-to left direction, suppose that $!A$source is false at some world $w$source in a universal model $\mModel{M}$source. Let $\Gamma$source contain $!A$source as well as all of its subformulas; clearly $\Gamma$source is finite. Take a filtration $\mModel{M^*}$source of $\mModel{M}$source; then $\mModel{M^*}$source is finite by the proposition bounding the size of a filtration, and by the Filtration Theorem preserving truth of formulas in Gamma, $!A$source is false at $[w]$source in $\mModel{M^*}$source. It remains to observe that $\mModel{M^*}$source is also universal: given $u$source and $v$source, by hypothesis $Ruv$source and by the definition of a filtrationthe accessibility conditions in the definition of a filtration, also $R^*[u][v]$source.

Finite model property for S five

LogS5 has the finite model property.

Proof

By the equivalence between S five models and universal models used here, if $!A$source is true at a world in some reflexive and euclidean model then it is true at a world in a universal model. By the proposition reducing universal-model validity to finite universal models, it is true at a world in a finite universal model (namely the filtration of the model through the set of sub-formulas of $!A$source). Every universal model is also reflexive and euclidean; so $!A$source is true at a world in a finite reflexive euclidean model.

Exercise on serial and reflexive filtrations

Show that any filtration of a serial or reflexive model is also serial or reflexive (respectively).

Exercise finding property-losing filtrations

Find a non-symmetric (non-transitive, non-euclidean) filtration of a symmetric (transitive, euclidean) model.

Decidability of S five

LogS5 is decidable.

Proof

Let $!A$source be given, and suppose the propositional variables occurring in $!A$source are among $p_1$source, dots, $p_k$source. Since for each $n$source there are only finitely many models with $n$source worlds assigning a value to $p_1$source, dots, $p_k$source, we can enumerate, in parallel, all the theorems of LogS5 by generating proofs in some systematic way; and all the models containing $1$source, $2$source, dots worlds and checking whether $!A$source fails at a world in some such model. Eventually one of the two parallel processes will give an answer, as by the general canonical-model determination theorem and the finite model property corollary for S five, either $!A$source is derivable or it fails in a finite universal model.

Conditions for accessibility-preserving filtrations

[ht] centering

captionConditions on possible worlds for defining filtrations.

Filtrations with selected accessibility properties

Let $\mModel{M} =\tuple{W,R,V}$source be a model, $\Gamma$source closed under sub-formulas. Let $W^*$source and $V^*$source be defined as in the definition of a filtration. Then:

1. Suppose $R^*[u][v]$source if and only if $C_1(u, v) \land C_2(u,v)$source. Then $R^*$source is symmetric, and $\mModel{M^*} = \tuple{W^*,R^*,V^*}$source is a filtration if $\mModel{M}$source is symmetric.

2. Suppose $R^*[u][v]$source if and only if $C_1(u, v) \land C_3(u,v)$source. Then $R^*$source is transitive, and $\mModel{M^*}=\tuple{W^*,R^*,V^*}$source is a filtration if $\mModel{M}$source is transitive.

3. Suppose $R^*[u][v]$source if and only if $C_1(u, v) \land C_2(u,v) \land C_3(u,v) \land C_4(u,v)$source. Then $R^*$source is symmetric and transitive, and $\mModel{M^*}=\tuple{W^*,R^*,V^*}$source is a filtration if $\mModel{M}$source is symmetric and transitive.

4. Suppose $R^*$source is defined as $R^*[u][v]$source if and only if $C_1(u, v) \land C_3(u,v) \land C_4(u,v)$source. Then $R^*$source is transitive and euclidean, and $\mModel{M^*}=\tuple{W^*,R^*,V^*}$source is a filtration if $\mModel{M}$source is transitive and euclidean.

Proof

1. It's immediate that $R^*$source is symmetric, since $C_1(u,v) \Leftrightarrow C_2(v,u)$source and $C_2(u,v) \Leftrightarrow C_1(v,u)$source. So it's left to show that if $\mModel{M}$source is symmetric then $\mModel{M^*}$source is a filtration through $\Gamma$source. Condition $C_1(u,v)$source guarantees that

   the necessity-preservation condition for a filtration and the possibility-preservation condition for a filtration of the definition of a filtration are

   satisfied. So we just have to verify the definition of a filtrationthe inherited-edge condition for a filtration, i.e., that $Ruv$source implies $R^*[u][v]$source.

   So suppose $Ruv$source. To show $R^*[u][v]$source we need to establish that $C_1(u,v)$source and $C_2(u,v)$source. For $C_1$source: if $\Box!A \in\Gamma$source and $\mSat{M}{\Box!A}[u]$source then also $\mSat{M}{!A}[v]$source (since $Ruv$source). Similarly, if $\Diamond!A \in \Gamma$source and $\mSat{M}{!A}[v]$source then $\mSat{M}{\Diamond!A}[u]$source since $Ruv$source. For $C_2$source: if $\Box!A \in \Gamma$source and $\mSat{M}{\Box!A}[v]$source then $Ruv$source implies $Rvu$source by symmetry, so that $\mSat{M}{!A}[u]$source. Similarly, if $\Diamond!A \in\Gamma$source and $\mSat{M}{!A}[u]$source then $\mSat{M}{\Diamond!A}[v]$source (since $Rvu$source by symmetry).

2. Exercise.

3. Exercise.

4. Exercise.