content/normal-modal-logic/filtrations/filtrations.tex
1% Part: modal-logic2% Chapter: filtrations3\documentclass[../../../include/open-logic-chapter]{subfiles}5\begin{document}7\olchapter{nml}{fil}{Filtrations and Decidability}9\olimport{introduction}11\olimport{preliminaries}12\olimport{filtrations-def}13\olimport{examples-of-filtrations}14\olimport{finite}15\olimport{S5-fmp}16\olimport{S5-decidable}17\olimport{more-filtrations}18\olimport{euclidean-filtrations}19\OLEndChapterHook21\end{document}23
content/normal-modal-logic/filtrations/introduction.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: introduction4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{int}10\olsection{Introduction}12One important question about a logic is always whether it is14decidable, i.e., if there is an effective procedure which will answer15the question ``is this !!{formula} valid.'' Propositional logic is16decidable: we can effectively test if !!a{formula} is a tautology by17constructing a truth table, and for a given !!{formula}, the truth18table is finite. But we can't obviously test if a modal formula is19true in all models, for there are infinitely many of them. We can20list all the finite models relevant to a given formula, since only the21assignment of subsets of worlds to !!{propositional variable}s which22actually occur in the !!{formula} are relevant. If the accessibility23relation is fixed, the possible different assignments $V(p)$ are just24all the subsets of~$W$, and if $\card{W} = n$ there are $2^n$ of25those. If our !!{formula}~$!A$ contains $m$ !!{propositional26 variable}s there are then $2^{nm}$ different models with~$n$27worlds. For each one, we can test if~$!A$ is true at all worlds,28simply by computing the truth value of~$!A$ in each. Of course, we29also have to check all possible accessibility relations, but there are30only finitely many relations on~$n$ worlds as well (specifically, the31number of subsets of $W \times W$, i.e., $2^{n^2}$.32If we are not interested in the logic~\Log{K}, but a logic defined by34some class of models (e.g., the reflexive transitive models), we also35have to be able to test if the accessibility relation is of the right36kind. We can do that whenever the frames we are interested in are37definable by modal !!{formula}s (e.g., by testing if \Ax{T} and \Ax{4}38valid in the frame). So, the idea would be to run through all the39finite frames, test each one if it is a frame in the class we're40interested in, then list all the possible models on that frame and41test if $!A$ is true in each. If not, stop: $!A$ is not valid in the42class of models of interest.43There is a problem with this idea: we don't know when, if ever, we can45stop looking. If the !!{formula} has a finite countermodel, our procedure will46find it. But if it has no finite countermodel, we won't get an47answer. The !!{formula} may be valid (no countermodels at all), or it48may have only an infinite countermodel, which we'll never look at. This49problem can be overcome if we can show that every !!{formula} that has50a countermodel has a finite countermodel. If this is the case we say51the logic has the \emph{finite model property}.52But how would we show that a logic has the finite model property? One54way of doing this would be to find a way to turn an infinite55(counter)model of~$!A$ into a finite one. If that can be done, then56whenever there is a model in which $!A$ is not true, then the57resulting finite model also makes $!A$ not true. That finite model58will show up on our list of all finite models, and we will eventually59determine, for every formula that is not valid, that it isn't. Our60procedure won't terminate if the formula is valid. If we can show in61addition that there is some maximum size that the finite model our62procedure provides can have, and that this maximum size depends only63on the !!{formula}~$!A$, we will have a size up to which we have to64test finite models in our search for countermodels. If we haven't65found a countermodel by then, there are none. Then our procedure will,66in fact, decide the question ``is $!A$ valid?'' for any67!!{formula}~$!A$.68A strategy that often works for turning infinite structures into70finite structures is that of ``identifying'' !!{element}s of the71structure which behave the same way in relevant respects. If there are72infinitely many worlds in~$\mModel{M}$ that behave the same in73relevant respects, then we may be able to collect \emph{all} worlds in74finitely many (possibly infinite) ``classes'' of such worlds. In other75words, we should partition the set of worlds in the right way, i.e.,76in such a way that each partition contains infinitely many worlds, but77there are only finitely many partitions. Then we define a new78model~$\mModel{M^*}$ where the worlds are the partitions. Finitely79many partitions in the old model give us finitely many worlds in the80new model, i.e., a finite model. Let's call the partition a world~$w$81is in $[w]$. We'll want it to be the case that $\mSat{M}{!A}[w]$ iff82$\mSat{M^*}{!A}[{[w]}]$, since we want the new model to be a83countermodel to~$!A$ if the old one was. This requires that we define84the partition, as well as the accessibility relation of~$\mModel{M^*}$85in the right way.86To see how this would go, first imagine we have no accessibility88relation. $\mSat{M}{\Box !B}[w]$ iff for some $v \in W$,89$\mSat{M}{\Box !B}[v]$, and the same for $\mModel{M^*}$, except with90$[w]$ and $[v]$. As a first idea, let's say that two worlds $u$ and91$v$ are equivalent (belong to the same partition) if they agree on all92!!{propositional variable}s in~$\mModel{M}$, i.e., $\mSat{M}{p}[u]$93iff $\mSat{M}{p}[v]$. Let $V^*(p) = \Setabs{[w]}{\mSat{M}{p}[w]}$.94Our aim is to show that $\mSat{M}{!A}[w]$ iff95$\mSat{M^*}{!A}[{[w]}]$. Obviously, we'd prove this by induction: The96base case would be $!A \equiv p$. First suppose $\mSat{M}{p}[w]$. Then97$[w] \in V^*$ by definition, so $\mSat{M^*}{p}[{[w]}]$. Now suppose98that $\mSat{M^*}{p}[{[w]}]$. That means that $[w] \in V^*(p)$, i.e.,99for some $v$ equivalent to~$w$, $\mSat{M}{p}[v]$. But ``$w$ equivalent100to $v$'' means ``$w$ and $v$ make all the same !!{propositional variable}s101true,'' so $\mSat{M}{p}[w]$. Now for the inductive step, e.g., $!A102\ident \lnot !B$. Then $\mSat{M}{\lnot !B}[w]$ iff $\mSat/{M}{!B}[w]$103iff $\mSat/{M^*}{!B}[{[w]}]$ (by inductive hypothesis) iff104$\mSat{M^*}{\lnot !B}[{[w]}]$. Similarly for the other non-modal105operators. It also works for $\Box$: suppose $\mSat{M^*}{\Box106 !B}[{[w]}]$. That means that for every $[u]$,107$\mSat{M^*}{!B}[{[u]}]$. By inductive hypothesis, for every $u$,108$\mSat{M}{!B}[u]$. Consequently, $\mSat{M}{\Box !B}[w]$.109In the general case, where we have to also define the accessibility111relation for $\mModel{M^*}$, things are more complicated. We'll call a112model~$\mModel{M^*}$ a \emph{filtration} if its accessibility113relation~$R^*$ satisfies the conditions required to make the inductive114proof above go through. Then any filtration~$\mModel{M^*}$ will make115$!A$ true at $[w]$ iff $\mModel{M}$ makes $!A$ true at~$w$. However,116now we also have to show that there \emph{are} filtrations, i.e., we117can define~$R^*$ so that it satisfies the required conditions. In118order for this to work, however, we have to require that worlds $u$,119$v$ count as equivalent not just when they agree on all120!!{propositional variable}s, but on all sub-!!{formula}s121of~$!A$. Since $!A$ has only finitely many sub-!!{formula}s, this will122still guarantee that the filtration is finite. There is not just one123way to define a filtration, and in order to make sure that the124accessibility relation of the filtration satisfies the required125properties (e.g., reflexive, transitive, etc.) we have to be inventive126with the definition of~$R^*$.127\end{document}130
content/normal-modal-logic/filtrations/preliminaries.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: preliminaries4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{pre}10\olsection{Preliminaries}12Filtrations allow us to establish the decidability of our systems of14modal logic by showing that they have the \emph{finite model15 property}, i.e., that any !!{formula} that is true (false) in a16model is also true (false) in a \emph{finite} model. Filtrations are17defined relative to sets of !!{formula}s which are closed under18subformulas.19\begin{defn}\ollabel{defn:modallyclosed}21 A set $\Gamma$ of !!{formula}s is \emph{closed under subformulas} if it22 contains every subformula of !!a{formula} in $\Gamma$. Further,23 $\Gamma$ is \emph{modally closed} if it is closed under subformulas24 and moreover $!A \in \Gamma$ implies $\Box!A,25 \Diamond!A \in \Gamma$. 26\end{defn}27For instance, given !!a{formula}~$!A$, the set of all its29sub-!!{formula}s is closed under sub-!!{formula}s. When we're defining30a filtration of a model through the set of sub-!!{formula}s of~$!A$,31it will have the property we're after: it makes $!A$ true (false) iff32the original model does.33The set of worlds of a filtration of~$\mModel{M}$ through~$\Gamma$ is35defined as the set of all equivalence classes of the following36equivalence relation.37\begin{defn}39Let $\mModel{M} =\tuple{W, R, V}$ and suppose $\Gamma$ is closed under40sub-!!{formula}s. Define a relation $\equiv$ on $W$ to hold of any two41worlds that make the same !!{formula}s from $\Gamma$ true, i.e.:42\[43u \equiv v \quad \text{if and only if } \quad 44\forall !A \in \Gamma : \mSat{M}{!A}[u] \Leftrightarrow \mSat{M}{!A}[v].45\]46The equivalence class~$[w]_\equiv$ of a world~$w$, or $[w]$ for short,47is the set of all worlds $\equiv$-equivalent to~$w$:48\[49[w] = \Setabs{v}{v \equiv w}.50\]51\end{defn}52\begin{prop}54 Given $\mModel{M}$ and $\Gamma$, $\equiv$ as defined above is an55 equivalence relation, i.e., it is reflexive, symmetric, and56 transitive.57\end{prop}58\begin{proof}60 The relation $\equiv$ is reflexive, since $w$ makes exactly the same61 !!{formula}s from~$\Gamma$ true as itself. It is symmetric since if62 $u$ makes the same !!{formula}s from~$\Gamma$ true as $v$, the same63 holds for $v$ and~$u$. It is also transitive, since if $u$ makes the64 same !!{formula}s from~$\Gamma$ true as~$v$, and $v$ as $w$, then65 $u$ makes the same !!{formula}s from~$\Gamma$ true as~$w$.66\end{proof}67The relation $\equiv$, like any equivalence relation, divides~$W$ into69\emph{partitions}, i.e., subsets of~$W$ which are pairwise disjoint,70and together cover all of~$W$. Every $w \in W$ is !!a{element} of one71of the partitions, namely of~$[w]$, since $w \equiv w$. So the72partitions $[w]$ cover all of~$W$. They are pairwise disjoint, for if73$u \in [w]$ and $u \in [v]$, then $u \equiv w$ and $u \equiv v$, and74by symmetry and transitivity, $w \equiv v$, and so $[w] = [v]$.75\end{document}
content/normal-modal-logic/filtrations/filtrations-def.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: filtrations-def4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{fil}10\olsection{Filtrations}12Rather than define ``the'' filtration of $\mModel{M}$ through14$\Gamma$, we define when a model~$\mModel{M^*}$ counts as a filtration15of~$\mModel{M}$. All filtrations have the same set of worlds~$W^*$ and16the same valuation~$V^*$. But different filtrations may have different17accessibility relations~$R^*$. To count as a filtration, $R^*$ has to18satisfy a number of conditions, however. These conditions are exactly19what we'll require to prove the main result, namely that20$\mSat{M}{!A}[w]$ iff $\mSat{M^*}{!A}[{[w]}]$, provided $!A \in21\Gamma$.22\begin{defn}\ollabel{defn:filtration}24 Let $\Gamma$ be closed under subformulas and $\mModel{M} = \tuple{W,25 R, V}$. A \emph{filtration of $\mModel{M}$ through $\Gamma$} is26 any model $\mModel{M^*} = \tuple{W^*,R^*,V^*}$, where:27 \begin{enumerate}28 \item $W^* = \Setabs{[w]}{w \in W}$;29 \item \ollabel{defn:filtration-R}%30 For any $u,v \in W$:31 \begin{enumerate}32 \item \ollabel{defn:filtration-R1}%33 If $Ruv$ then $R^*[u][v]$;34 \tagitem{prvBox}{\ollabel{defn:filtration-R2}%35 If $R^*[u][v]$ then for any $\Box !A \in \Gamma$, if36 $\mSat{M}{\Box!A}[u]$ then $\mSat{M}{!A}[v]$}{};37 \tagitem{prvDiamond}{\ollabel{defn:filtration-R3}%38 If $R^*[u][v]$ then for any $\Diamond !A \in \Gamma$, if39 $\mSat{M}{!A}[v]$ then $\mSat{M}{\Diamond!A}[u]$.}{}40 \end{enumerate}41 \item $V^*(p) = \Setabs{[u]}{u \in V(p)}$.42 \end{enumerate}43\end{defn}44It's worthwhile thinking about what $V^*(p)$ is: the set consisting of46the equivalence classes~$[w]$ of all worlds~$w$ where $p$ is true47in~$\mModel{M}$. On the one hand, if $w \in V(p)$, then $[w] \in48V^*(p)$ by that definition. However, it is not necessarily the case49that if $[w] \in V^*(p)$, then $w \in V(p)$. If $[w] \in V^*(p)$ we50are only guaranteed that $[w] = [u]$ for \emph{some}~$u \in V(p)$. Of51course, $[w] = [u]$ means that $w \equiv u$. So, when $[w] \in52V^*(p)$ we can (only) conclude that $w \equiv u$ for some $u \in53V(p)$.54\begin{thm}\ollabel{thm:filtrations}56 If $\mModel{M^*}$ is a filtration of $\mModel{M}$ through $\Gamma$,57 then for every $!A \in \Gamma$ and $w \in W$, we have58 $\mSat{M}{!A}[w]$ if and only if $\mSat{M^*}{!A}[{[w]}]$.59\end{thm}60\begin{proof}62 By induction on $!A$, using the fact that $\Gamma$ is closed under63 subformulas. Since $!A \in \Gamma$ and $\Gamma$ is closed under64 sub-!!{formula}s, all sub-!!{formula}s of~$!A$ are also $\in65 \Gamma$. Hence in each inductive step, the induction hypothesis66 applies to the sub-!!{formula}s of~$!A$.67 \begin{enumerate}68 \tagitem{prvFalse}{\indcase{!A}{\lfalse}{Neither69 $\mSat{M}{\indfrm}[w]$ nor $\mSat{M^*}{\indfrm}[{[w]}]$.}}{}70 \tagitem{prvTrue}{\indcase{!A}{\ltrue}{Both71 $\mSat{M}{\indfrm}[w]$ and $\mSat{M^*}{\indfrm}[{[w]}]$.}}{}72 \item \indcase{!A}{p}{The left-to-right direction is immediate, as73 $\mSat{M}{\indfrm}[w]$ only if $w \in V(p)$, which implies $[w]74 \in V^*(p)$, i.e., $\mSat{M^*}{\indfrm}[{[w]}]$. Conversely,75 suppose $\mSat{M^*}{\indfrm}[{[w]}]$, i.e., $[w] \in76 V^*(p)$. Then for some $v \in V(p)$, $w \equiv v$. Of course77 then also $\mSat{M}{p}[v]$. Since $w \equiv v$, $w$ and $v$ make78 the same !!{formula}s from~$\Gamma$ true. Since by assumption $p79 \in \Gamma$ and $\mSat{M}{p}[v]$, $\mSat{M}{\indfrm}[w]$.}80 \tagitem{prvNot}{\iftag{probNot}{Exercise.}{\indcase{!A}{\lnot82 !B}{$\mSat{M}{\indfrm}[w]$ iff $\mSat/{M}{!B}[w]$. By83 induction hypothesis, $\mSat/{M}{!B}[w]$ iff84 $\mSat/{M^*}{!B}[{[w]}]$. Finally, $\mSat/{M^*}{!B}[{[w]}]$85 iff $\mSat{M^*}{\indfrm}[{[w]}]$.}}}{}86 87 \tagitem{prvAnd}{\iftag{probAnd}{Exercise.}{\indcase{!A}{(!B \land88 !C)}{$\mSat{M}{\indfrm}[w]$ iff $\mSat{M}{!B}[w]$ and89 $\mSat{M}{!C}[w]$. By induction hypothesis, $\mSat{M}{!B}[w]$90 iff $\mSat{M^*}{!B}[{[w]}]$, and $\mSat{M}{!C}[w]$ iff91 $\mSat{M^*}{!C}[{[w]}]$. And $\mSat{M^*}{\indfrm}[{[w]}]$92 iff $\mSat{M^*}{!B}[{[w]}]$ and93 $\mSat{M^*}{!C}[{[w]}]$.}}}{}94 \tagitem{prvOr}{\iftag{probOr}{Exercise.}{\indcase{!A}{(!B \lor96 !C)}{$\mSat{M}{\indfrm}[w]$ iff $\mSat{M}{!B}[w]$ or97 $\mSat{M}{!C}[w]$. By induction hypothesis, $\mSat{M}{!B}[w]$98 iff $\mSat{M^*}{!B}[{[w]}]$, and $\mSat{M}{!C}[w]$ iff99 $\mSat{M^*}{!C}[{[w]}]$. And $\mSat{M^*}{\indfrm}[{[w]}]$100 iff $\mSat{M^*}{!B}[{[w]}]$ or101 $\mSat{M^*}{!C}[{[w]}]$.}}}{}102 \tagitem{prvIf}{\iftag{probIf}{Exercise.}{\indcase{!A}{(!B \lif104 !C)}{$\mSat{M}{\indfrm}[w]$ iff $\mSat/{M}{!B}[w]$ or105 $\mSat{M}{!C}[w]$. By induction hypothesis, $\mSat{M}{!B}[w]$106 iff $\mSat{M^*}{!B}[{[w]}]$, and $\mSat{M}{!C}[w]$ iff107 $\mSat{M^*}{!C}[{[w]}]$. And $\mSat{M^*}{\indfrm}[{[w]}]$108 iff $\mSat/{M^*}{!B}[{[w]}]$ or109 $\mSat{M^*}{!C}[{[w]}]$.}}}{}110 \tagitem{prvIff}{\iftag{probIff}{Exercise.}{\indcase{!A}{(!B \liff112 !C)}{$\mSat{M}{\indfrm}[w]$ iff $\mSat{M}{!B}[w]$ and113 $\mSat{M}{!C}[w]$, or $\mSat/{M}{!B}[w]$ and114 $\mSat/{M}{!C}[w]$. By induction hypothesis, $\mSat{M}{!B}[w]$115 iff $\mSat{M^*}{!B}[{[w]}]$, and $\mSat{M}{!C}[w]$ iff116 $\mSat{M^*}{!C}[{[w]}]$. And $\mSat{M^*}{\indfrm}[{[w]}]$117 iff $\mSat{M^*}{!B}[{[w]}]$ and118 $\mSat{M^*}{!C}[{[w]}]$, or $\mSat/{M^*}{!B}[{[w]}]$ and119 $\mSat/{M^*}{!C}[{[w]}]$.}}}{}120 \tagitem{prvBox}{\iftag{probBox}{Exercise.}{\indcase{!A}{\Box122 !B}{Suppose $\mSat{M}{\indfrm}[w]$; to show that123 $\mSat{M^*}{\indfrm}[{[w]}]$, let $v$ be such that124 $R^*[w][v]$. From125 \olref{defn:filtration}\olref{defn:filtration-R2}, we have126 that $\mSat{M}{!B}[v]$, and by inductive hypothesis127 $\mSat{M^*}{!B}[{[v]}]$. Since $v$ was arbitrary,128 $\mSat{M^*}{\indfrm}[{[w]}]$ follows.129 Conversely, suppose $\mSat{M^*}{\indfrm}[{[w]}]$ and let $v$131 be arbitrary such that $Rwv$. From132 \olref{defn:filtration}\olref{defn:filtration-R1}, we have133 $R^*[w][v]$, so that $\mSat{M^*}{!B}[{[v]}]$; by inductive134 hypothesis $\mSat{M}{!B}[v]$, and since $v$ was arbitrary,135 $\mSat{M}{\indfrm}[w]$.}}}{}136 137 \tagitem{prvDiamond}{\iftag{probDiamond}{Exercise.}{\indcase{!A}{\Diamond138 !B}{Suppose $\mSat{M}{\indfrm}[w]$. Then for some $v \in W$,139 $Rwv$ and $\mSat{M}{!B}[v]$. By inductive hypothesis140 $\mSat{M^*}{!B}[{[v]}]$, and by141 \olref{defn:filtration}\olref{defn:filtration-R1}, we have142 $R^*[w][v]$. Thus, $\mSat{M^*}{\indfrm}[{[w]}]$.143 Now suppose $\mSat{M^*}{\indfrm}[{[w]}]$. Then for some $[v]145 \in W^*$ with $R^*[w][v]$, $\mSat{M^*}{!B}[{[v]}]$. By146 inductive hypothesis $\mSat{M}{!B}[v]$. By147 \olref{defn:filtration}\olref{defn:filtration-R3}, we have148 that $\mSat{M}{\indfrm}[w]$.}}}{}149 \end{enumerate}150\end{proof}151\begin{prob}153 Complete the proof of \olref[nml][fil][fil]{thm:filtrations}154\end{prob}155What holds for truth at worlds in a model also holds for truth in a157model and validity in a class of models.158\begin{cor}160 Let $\Gamma$ be closed under subformulas. Then:161 \begin{enumerate}162 \item If $\mModel{M^*}$ is a filtration of $\mModel{M}$ through163 $\Gamma$ then for any $!A \in \Gamma$: $\mSat{M}{!A}$ if and only164 if $\mSat{M^*}{!A}$.165 \item If $\mClass{C}$ is a class of models and $\Gamma(\mClass{C})$166 is the class of $\Gamma$-filtrations of models in $\mClass{C}$,167 then any !!{formula}~$!A \in \Gamma$ is valid in $\mClass{C}$ if168 and only if it is valid in $\Gamma(\mClass{C})$.169 \end{enumerate}170\end{cor}171\end{document}
content/normal-modal-logic/filtrations/examples-of-filtrations.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: examples-of-filtrations4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{exf}10\olsection{Examples of Filtrations}12We have not yet shown that there are any filtrations. But indeed, for14any model $\mModel{M}$, there are many filtrations of $\mModel{M}$15through $\Gamma$. We identify two, in particular: the finest and16coarsest filtrations. Filtrations of the same models will differ in17their accessibility relation (as \olref[fil]{defn:filtration} stipulates18directly what $W^*$ and~$V^*$ should be). The finest filtration19will have as few related worlds as possible, whereas the coarsest will20have as many as possible.21\begin{defn}23 Where $\Gamma$ is closed under subformulas, the \emph{finest}24 filtration $\mModel{M^*}$ of a model $\mModel{M}$ is defined by putting:25 \[26 R^*[u][v] \quad \text{if and only if} \quad \exists u'\in [u] \;27 \exists v' \in [v] : Ru'v'.28 \]29\end{defn}30\begin{prop}\ollabel{prop:finest}32 The finest filtration $\mModel{M^*}$ is indeed a filtration. 33\end{prop}34\begin{proof}36 We need to check that $R^*$, so defined, satisfies37 \olref[fil]{defn:filtration}\olref[fil]{defn:filtration-R}. We check38 the three conditions in turn.39 If $Ruv$ then since $u \in [u]$ and $v \in [v]$, also $R^*[u][v]$,41 so \olref[fil]{defn:filtration-R1} is satisfied.42 43 \iftag{prvBox}{\iftag{probBox}{We leave the verification of44 \olref[fil]{defn:filtration-R2} as an exercise.}{For45 \olref[fil]{defn:filtration-R2}, suppose $\Box!A \in \Gamma$,46 $R^*[u][v]$, and $\mSat{M}{\Box!A}[u]$. By definition of47 $R^*$, there are $u' \equiv u$ and $v' \equiv v$ such that48 $Ru'v'$. Since $u$ and $u'$ agree on $\Gamma$, also49 $\mSat{M}{\Box!A}[u']$, so that $\mSat{M}{!A}[v']$. By closure50 of $\Gamma$ under sub-!!{formula}s, $v$ and $v'$ agree on51 $!A$, so $\mSat{M}{!A}[v]$, as desired.}}{}52 53 \iftag{prvDiamond}{\iftag{probDiamond}{We leave the verification of54 \olref[fil]{defn:filtration-R3} as an exercise.}{To verify55 \olref[fil]{defn:filtration-R3}, suppose $\Diamond!A \in56 \Gamma$, $R^*[u][v]$, and $\mSat{M}{!A}[v]$. By definition of57 $R^*$, there are $u' \equiv u$ and $v' \equiv v$ such that58 $Ru'v'$. Since $v$ and $v'$ agree on~$\Gamma$, and $\Gamma$ is59 closed under sub-!!{formula}s, also $\mSat{M}{!A}[v']$, so60 that $\mSat{M}{\Diamond !A}[u']$. Since $u$ and $u'$ also61 agree on $\Gamma$, $\mSat{M}{\Diamond !A}[u]$.}}{}62\end{proof}63\begin{probtag}{probBox,probDiamond}65 Complete the proof of \olref[nml][fil][exf]{prop:finest}.66\end{probtag}67\begin{defn}69 Where $\Gamma$ is closed under subformulas, the \emph{coarsest}70 filtration~$\mModel{M^*}$ of a model~$\mModel{M}$ is defined by71 putting $R^*[u][v]$ if and only if72 \iftag{notprvBox,notprvDiamond}{the following condition is73 met:}{\emph{both} of the following conditions are met:}74 \begin{tagenumerate}{prvBox,prvDiamond}75 \tagitem{prvBox}{\ollabel{defn:coarsest-Box}If $\Box!A \in \Gamma$76 and $\mSat{M}{\Box!A}[u]$ then77 $\mSat{M}{!A}[v]$\iftag{prvDiamond}{;}{.}}{}78 \tagitem{prvDiamond}{\ollabel{defn:coarsest-Diamond}If $\Diamond!A79 \in \Gamma$ and $\mSat{M}{!A}[v]$ then80 $\mSat{M}{\Diamond!A}[u]$.}{}81 \end{tagenumerate}82\end{defn}83\begin{prop}85 The coarsest filtration $\mModel{M^*}$ is indeed a filtration. 86\end{prop}87\begin{proof}89 Given the definition of $R^*$, the only condition that is left to90 verify is the implication from $Ruv$ to $R^*[u][v]$. So assume91 $Ruv$. \iftag{prvBox}{Suppose $\Box!A \in \Gamma$ and92 $\mSat{M}{\Box!A}[u]$; then obviously93 $\mSat{M}{!A}[v]$\iftag{prvDiamond}{, and94 \olref{defn:coarsest-Box} is95 satisfied. }{.}}{}\iftag{prvDiamond}{Suppose $\Diamond!A \in96 \Gamma$ and $\mSat{M}{!A}[v]$. Then $\mSat{M}{\Diamond!A}[u]$97 since~$Ruv$\iftag{prvBox}{, and \olref{defn:coarsest-Diamond} is98 satisfied}{}.}{}99\end{proof}100\begin{ex}102 Let $W = \PosInt$, $Rnm$ iff $m = n + 1$, and $V(p) = \Setabs{2n}{n \in103 \Nat}$. The model $\mModel{M} = \tuple{W, R, V}$ is depicted in104 \olref{fig:ex-filtration}. The worlds are $1$, $2$, etc.; each105 world can access exactly one other world---its successor---and $p$ is106 true at all and only the even numbers.107 \begin{figure}109 \centering110 \begin{tikzpicture}[modal]111 \node[world] (1) [label=below:\mFalse{p}] {$1$};112 \node[world] (2) [label=below:\mTrue{p}, right=of 1] {$2$};113 \node[world] (3) [label=below:\mFalse{p}, right=of 2] {$3$};114 \node[world] (4) [label=below:\mTrue{p}, right=of 3] {$4$};115 \node[phantom] (5) [right=of 4] {};116 \draw[->] (1) to (2);117 \draw[->] (2) to (3);118 \draw[->] (3) to (4);119 \draw[dotted] (4) to (5);120 \end{tikzpicture}121 \begin{tikzpicture}[modal]123 \node[world] (1) [label=below:\mFalse{p}] {$[1]$};124 \node[world] (2) [label=below:\mTrue{p}, right=of 1] {$[2]$};125 \draw[->,bend left] (1) to (2);126 \draw[->,bend left] (2) to (1);127 128 \node[world] (3) [label=below:\mFalse{p},right=of 2] {$[1]$};129 \node[world] (4) [label=below:\mTrue{p}, right=of 3] {$[2]$};130 \draw[->,bend left] (3) to (4);131 \draw[->,bend left] (4) to (3);132 \draw[->,reflexive above] (4) to (4);133 \end{tikzpicture}134 \caption{An infinite model and its filtrations.}135 \ollabel{fig:ex-filtration}136 \end{figure}137 138 Now let $\Gamma$ be the set of sub-!!{formula}s of~$\Box p \lif p$,139 i.e., $\{p, \Box p, \Box p \lif p\}$. $p$ is true at all and only140 the even numbers, $\Box p$ is true at all and only the odd numbers,141 so $\Box p \lif p$ is true at all and only the even numbers. In142 other words, every odd number makes $\Box p$ true but $p$ and $\Box143 p \lif p$ false; every even number makes $p$ and $\Box p \lif p$144 true, but $\Box p$ false. So $W^* = \{ [1], [2] \}$, where $[1] =145 \{1, 3, 5, \dots\}$ and $[2] = \{2, 4, 6, \dots\}$. Since $2 \in146 V(p)$, $[2] \in V^*(p)$; since $1 \notin V(p)$, $[1] \notin147 V^*(p)$. So $V^*(p) = \{[2]\}$.148 Any filtration based on $W^*$ must have an accessibility relation150 that includes $\tuple{[1], [2]}, \tuple{[2],[1]}$: since $R12$, we151 must have $R^*[1][2]$ by152 \olref[fil]{defn:filtration}\olref[fil]{defn:filtration-R1}, and153 since $R23$ we must have $R^*[2][3]$, and $[3]=[1]$. It cannot154 include $\tuple{[1],[1]}$: if it did, we'd have $R^*[1][1]$,155 $\mSat{M}{\Box p}[1]$ but $\mSat/{M}{p}[1]$, contradicting156 \olref[fil]{defn:filtration-R2}. Nothing requires or rules out that157 $R^*[2][2]$. So, there are two possible filtrations of~$\mModel{M}$,158 corresponding to the two accessibility relations159 \[160 \{\tuple{[1],[2]}, \tuple{[2],[1]}\} \text{ and }161 \{\tuple{[1],[2]}, \tuple{[2],[1]}, \tuple{[2],[2]}\}.162 \]163 In either case, $p$ and $\Box p \lif p$ are false and $\Box p$ is164 true at~$[1]$; $p$ and $\Box p \lif p$ are true and $\Box p$ is165 false at~$[2]$.166\end{ex}167\begin{prob}170 Consider the following model $\mModel{M} = \tuple{W, R, V}$ where $W171 = \Setabs{0\sigma}{\sigma \in \Bin^*}$, the set of sequences of $0$s172 and~$1$s starting with~$0$, with $R\sigma\sigma'$ iff $\sigma' =173 \sigma 0$ or $\sigma' = \sigma 1$, and $V(p) = \Setabs{\sigma174 0}{\sigma \in \Bin^*}$ and $V(q) = \Setabs{\sigma 1}{\sigma \in175 \Bin^* \setminus \{1\}}$. Here's a picture:176 \begin{center}177 \begin{tikzpicture}[modal,178 node distance=2cm179 ]180 \node[world] (0) [label={below:\mTrue{p}\\\mFalse{q}},font=\tiny] {$0$};182 \node[world] (00) [label={below:\mTrue{p}\\\mFalse{q}},183 above right=of 0,font=\tiny] {$00$};184 \node[world] (000) [label={below:\mTrue{p}\\\mFalse{q}},185 right=of 00, yshift=.8cm, font=\tiny] {$000$};186 \node[phantom] (0000) [right=of 000, yshift=.5cm] {};187 \node[phantom] (0001) [right=of 000, yshift=-.5cm] {};188 \node[world] (001) [label={below:\mFalse{p}\\\mTrue{q}},189 right=of 00, yshift=-.8cm, font=\tiny] {$001$};190 \node[phantom](0010) [right=of 001, yshift=.5cm] {};191 \node[phantom](0011) [right=of 001, yshift=-.5cm] {};192 \node[world] (01) [label={below:\mFalse{p}\\\mTrue{q}},193 below right=of 0,font=\tiny] {$01$};194 \node[world] (010) [label={below:\mTrue{p}\\\mFalse{q}},195 right=of 01, yshift=.8cm,font=\tiny] {$010$};196 \node[phantom] (0100) [right=of 010, yshift=.5cm] {};197 \node[phantom] (0101) [right=of 010, yshift=-.5cm] {};198 \node[world] (011) [label={below:\mFalse{p}\\\mTrue{q}},199 right=of 01, yshift=-.8cm,font=\tiny] {$011$};200 \node[phantom] (0110) [right=of 011, yshift=.5cm] {};201 \node[phantom] (0111) [right=of 011, yshift=-.5cm] {};202 \draw[->] (0) to (00);204 \draw[->] (0) to (01);205 \draw[->] (00) to (000);206 \draw[dotted] (000) to (0000);207 \draw[dotted] (000) to (0001);208 \draw[->] (00) to (001);209 \draw[dotted] (001) to (0010);210 \draw[dotted] (001) to (0011);211 \draw[->] (01) to (010);212 \draw[dotted] (010) to (0100);213 \draw[dotted] (010) to (0101);214 \draw[->] (01) to (011);215 \draw[dotted] (011) to (0110);216 \draw[dotted] (011) to (0111);217 \end{tikzpicture}218 \end{center}219 We have $\mSat/{M}{\Box(p \lor q) \lif (\Box p \lor \Box q)}[w]$ for220 every~$w$.221 Let $\Gamma$ be the set of sub-!!{formula}s of~$\Box(p \lor q) \lif223 (\Box p \lor \Box q)$. What are $W^*$ and~$V^*$? What is the224 accessibility relation of the finest filtration of~$\mModel{M}$? Of the225 coarsest?226\end{prob}227\end{document}
content/normal-modal-logic/filtrations/finite.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: finite4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{fin}10\olsection{Filtrations are Finite}12We've defined filtrations for any set~$\Gamma$ that is closed under14sub-!!{formula}s. Nothing in the definition itself guarantees that15filtrations are finite. In fact, when $\Gamma$ is infinite (e.g., is16the set of all !!{formula}s), it may well be infinite. However, if17$\Gamma$ is finite (e.g., when it is the set of sub-!!{formula}s of a18given !!{formula}~$!A$), so is any filtration through~$\Gamma$.19\begin{prop}\ollabel{prop:filt-are-finite}21 If $\Gamma$ is finite then any filtration $\mModel{M^*}$ of a model22 $\mModel{M}$ through $\Gamma$ is also finite.23\end{prop}24\begin{proof}26 The size of $W^*$ is the number of different classes~$[w]$ under the27 equivalence relation~$\equiv$. Any two worlds $u$, $v$ in such28 class---that is, any $u$ and $v$ such that~$u \equiv v$---agree on29 all !!{formula}s~$!A$ in~$\Gamma$, $!A \in \Gamma$ either $!A$ is30 true at both $u$ and $v$, or at neither. So each class~$[w]$31 corresponds to subset of~$\Gamma$, namely the set of all $!A \in32 \Gamma$ such that $!A$ is true at the worlds in~$[w]$. No two33 different classes $[u]$ and $[v]$ correspond to the same subset34 of~$\Gamma$. For if the set of !!{formula}s true at $u$ and that of35 !!{formula}s true at $v$ are the same, then $u$ and $v$ agree on all36 formulas in~$\Gamma$, i.e., $u \equiv v$. But then $[u] = [v]$. So,37 there is !!a{injective} function from $W^*$ to $\Pow{\Gamma}$, and38 hence $\card{W^*} \le \card{\Pow{\Gamma}}$. Hence if $\Gamma$39 contains $n$ sentences, the cardinality of $W^*$ is no greater40 than~$2^n$.41\end{proof}42\end{document}44
content/normal-modal-logic/filtrations/S5-fmp.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: S5-fmp4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{fmp}10\olsection{\Log{K} and \Log{S5} have the Finite Model Property}12\begin{defn}14 A system $\Sigma$ of modal logic is said to have the \emph{finite15 model property} if whenever !!a{formula}~$!A$ is true at a world16 in a model of $\Sigma$ then $!A$ is true at a world in a17 \emph{finite} model of~$\Sigma$.18\end{defn}19\begin{prop}\ollabel{prop:K-fmp}21 \Log{K} has the finite model property.22\end{prop}23\begin{proof}25 \Log{K} is the set of valid !!{formula}s, i.e., any model is a model26 of~\Log{K}. By \olref[fil]{thm:filtrations}, if27 $\mSat{M}{!A}[w]$, then $\mSat{M^*}{!A}[w]$ for any filtration28 of~$\mModel{M}$ through the set $\Gamma$ of sub-!!{formula}s29 of~$!A$. Any !!{formula} only has finitely many sub-!!{formula}s, so30 $\Gamma$ is finite. By \olref[fin]{prop:filt-are-finite},31 $\card{W^*} \le 2^n$, where $n$ is the number of !!{formula}s32 in~$\Gamma$. And since \Log{K} imposes no restriction on models,33 $\mModel{M^*}$ is a \Log{K}-model.34\end{proof}35To show that a logic~\Log{L} has the finite model property via37filtrations it is essential that the filtration of an \Log{L}-model is38itself a \Log{L}-model. Often this requires a fair bit of work, and39not any filtration yields a \Log{L}-model. However, for universal40models, this still holds.41\begin{prop}\ollabel{prop:univ-fin}43 Let $\mClass{U}$ be the class of universal models (see44 \olref[frd][es5]{prop:S5=univ}) and $\mClass{U}_\mathrm{Fin}$ the45 class of all finite universal models. Then any !!{formula}~$!A$ is46 valid in $\mClass{U}$ if and only if it is valid in47 $\mClass{U}_\mathrm{Fin}$.48\end{prop}49\begin{proof}51 Finite universal models are universal models, so the left-to-right52 direction is trivial. For the right-to left direction, suppose53 that~$!A$ is false at some world $w$ in a universal model54 $\mModel{M}$. Let $\Gamma$ contain $!A$ as well as all of its55 subformulas; clearly $\Gamma$ is finite. Take a filtration56 $\mModel{M^*}$ of $\mModel{M}$; then $\mModel{M^*}$ is finite by57 \olref[fin]{prop:filt-are-finite}, and by58 \olref[fil]{thm:filtrations}, $!A$ is false at $[w]$ in59 $\mModel{M^*}$. It remains to observe that $\mModel{M^*}$ is also60 universal: given $u$ and $v$, by hypothesis $Ruv$ and by61 \olref[fil]{defn:filtration}\olref[fil]{defn:filtration-R},62 also $R^*[u][v]$.63\end{proof}64\begin{cor}\ollabel{cor:S5fmp}66 \Log{S5} has the finite model property.67\end{cor}68\begin{proof}70 By \olref[frd][es5]{prop:S5=univ}, if $!A$ is true at a world in71 some reflexive and euclidean model then it is true at a world in a72 universal model. By \olref{prop:univ-fin}, it is true at a world in73 a finite universal model (namely the filtration of the model through74 the set of sub-!!{formula}s of~$!A$). Every universal model is also75 reflexive and euclidean; so $!A$ is true at a world in a finite76 reflexive euclidean model.77\end{proof}78\begin{prob}80 Show that any filtration of a serial or reflexive model is also81 serial or reflexive (respectively).82\end{prob}83\begin{prob}85 Find a non-symmetric (non-transitive, non-euclidean) filtration of a86 symmetric (transitive, euclidean) model.87\end{prob}88\end{document}
content/normal-modal-logic/filtrations/S5-decidable.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: S5-decidable4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{dec}10\olsection{\Log{S5} is Decidable}12The finite model property gives us an easy way to show that systems of13modal logic given by schemas are \emph{decidable} (i.e., that there is14a computable procedure to determine whether !!a{formula} is !!{derivable} in15the system or not).16\begin{thm}18 \Log{S5} is decidable.19\end{thm}20\begin{proof}22 Let $!A$ be given, and suppose the !!{propositional variable}s23 occurring in $!A$ are among $p_1$, \dots, $p_k$. Since for each24 $n$ there are only finitely many models with $n$ worlds assigning a25 value to $p_1$, \dots, $p_k$, we can enumerate, \emph{in parallel}, all26 the theorems of \Log{S5} by generating proofs in some systematic27 way; and all the models containing $1$, $2$, \dots worlds and checking28 whether $!A$ fails at a world in some such model. Eventually29 one of the two parallel processes will give an answer, as by30 \olref[com][fra]{thm:generaldet} and \olref[fmp]{cor:S5fmp}, either31 $!A$ is !!{derivable} or it fails in a finite universal model.32\end{proof}33The above proof works for \Log{S5} because filtrations of universal35models are automatically universal. The same holds for reflexivity and36seriality, but more work is needed for other properties.37\end{document}
content/normal-modal-logic/filtrations/more-filtrations.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: more-filtrations4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{acc}10\olsection{Filtrations and Properties of Accessibility}12As noted, filtrations of universal, serial, and reflexive models are14always also universal, serial, or reflexive. But not every filtration15of a symmetric or transitive model is symmetric or transitive,16respectively. In some cases, however, it is possible to define17filtrations so that this does hold. In order to do so, we proceed as18in the definition of the coarsest filtration, but add additional19conditions to the definition of~$R^*$. Let $\Gamma$ be closed under20sub-!!{formula}s. Consider the relations~$C_i(u,v)$ in21\olref{tab:Cn-filtrations} between worlds $u$, $v$ in a model22$\mModel{M} =\tuple{W, R, V}$. We can define $R^*[u][v]$ on the basis23of combinations of these conditions. For instance, if we stipulate24that $R^*[u][v]$ iff the condition $C_1(u,v)$ holds, we get exactly25the coarsest filtration. If we stipulate $R^*[u][v]$ iff both26$C_1(u,v)$ and $C_2(u, v)$ hold, we get a different filtration. It is27``finer'' than the coarsest since fewer pairs of worlds satisfy28$C_1(u,v)$ and $C_2(u,v)$ than $C_1(u,v)$ alone.29\begin{table}[ht]31 \centering32 \begin{tabular}{|ll|}33 \hline34 \multirow{2}{*}{$C_1(u,v)$:}35 \iftag{prvBox}{&36 if $\Box!A \in \Gamma$ and $\mSat{M}{\Box!A}[u]$37 then $\mSat{M}{!A}[v]$;\iftag{prvDiamond}{ and}{}\\}{}38 \iftag{prvDiamond}{&39 if $\Diamond!A \in \Gamma$ and $\mSat{M}{!A}[v]$40 then $\mSat{M}{\Diamond!A}[u]$; \\}{}41 \hline42 \multirow{2}{*}{$C_2(u,v)$:} 43 \iftag{prvBox}{&44 if $\Box!A \in \Gamma$ and $\mSat{M}{\Box!A}[v]$45 then $\mSat{M}{!A}[u]$;\iftag{prvDiamond}{ and}{}\\}{}46 \iftag{prvDiamond}{&47 if $\Diamond!A \in \Gamma$ and $\mSat{M}{!A}[u]$48 then $\mSat{M}{\Diamond!A}[v]$; \\}{}49 \hline50 \multirow{2}{*}{$C_3(u,v)$:}51 \iftag{prvBox}{&52 if $\Box!A \in \Gamma$ and $\mSat{M}{\Box!A}[u]$53 then $\mSat{M}{\Box!A}[v]$;\iftag{prvDiamond}{ and}{}\\}{}54 \iftag{prvDiamond}{&55 if $\Diamond!A \in \Gamma$ and $\mSat{M}{\Diamond!A}[v]$56 then $\mSat{M}{\Diamond!A}[u]$; \\}{}57 \hline58 \multirow{2}{*}{$C_4(u,v)$:}59 \iftag{prvBox}{&60 if $\Box!A \in \Gamma$ and $\mSat{M}{\Box!A}[v]$61 then $\mSat{M}{\Box!A}[u]$;\iftag{prvDiamond}{ and}{}\\}{}62 \iftag{prvDiamond}{&63 if $\Diamond!A \in \Gamma$ and $\mSat{M}{\Diamond!A}[u]$64 then $\mSat{M}{\Diamond!A}[v]$; \\}{}65 \hline66 \end{tabular}67 \caption{Conditions on possible worlds for defining68 filtrations.}69 \ollabel{tab:Cn-filtrations}70\end{table}71\begin{thm}\ollabel{thm:more-filtrations}73 Let $\mModel{M} =\tuple{W,R,V}$ be a model, $\Gamma$ closed under74 sub-!!{formula}s. Let $W^*$ and $V^*$ be defined as in75 \olref[fil]{defn:filtration}. Then:76 \begin{enumerate}77 \item Suppose $R^*[u][v]$ if and only if $C_1(u, v) \land78 C_2(u,v)$. Then $R^*$ is symmetric, and $\mModel{M^*} =79 \tuple{W^*,R^*,V^*}$ is a filtration if $\mModel{M}$ is symmetric.80 \item Suppose $R^*[u][v]$ if and only if $C_1(u, v)81 \land C_3(u,v)$. Then $R^*$ is transitive, and82 $\mModel{M^*}=\tuple{W^*,R^*,V^*}$ is a filtration if $\mModel{M}$83 is transitive.84 \item Suppose $R^*[u][v]$ if and only if $C_1(u, v) \land C_2(u,v)85 \land C_3(u,v) \land C_4(u,v)$. Then $R^*$ is symmetric and86 transitive, and $\mModel{M^*}=\tuple{W^*,R^*,V^*}$ is a filtration87 if $\mModel{M}$ is symmetric and transitive.88 \item Suppose $R^*$ is defined as $R^*[u][v]$ if and only if $C_1(u,89 v) \land C_3(u,v) \land C_4(u,v)$. Then $R^*$ is transitive and90 euclidean, and $\mModel{M^*}=\tuple{W^*,R^*,V^*}$ is a filtration91 if $\mModel{M}$ is transitive and euclidean.92 \end{enumerate}93\end{thm}94\begin{proof}96 \begin{enumerate}97 \item It's immediate that $R^*$ is symmetric, since $C_1(u,v)98 \Leftrightarrow C_2(v,u)$ and $C_2(u,v) \Leftrightarrow99 C_1(v,u)$. So it's left to show that if $\mModel{M}$ is100 symmetric then $\mModel{M^*}$ is a filtration101 through~$\Gamma$. Condition $C_1(u,v)$ guarantees that102 \iftag{prvBox}{%103 \iftag{prvDiamond}{%104 \olref[fil]{defn:filtration-R2} and105 \olref[fil]{defn:filtration-R3} of106 \olref[fil]{defn:filtration} are}{%107 \olref[fil]{defn:filtration}\olref[fil]{defn:filtration-R2} is}}{%108 \olref[fil]{defn:filtration}\olref[fil]{defn:filtration-R3} is}109 satisfied. So we just have to verify110 \olref[fil]{defn:filtration}\olref[fil]{defn:filtration-R1},111 i.e., that $Ruv$ implies $R^*[u][v]$.112 So suppose $Ruv$. To show $R^*[u][v]$ we need to establish that114 $C_1(u,v)$ and $C_2(u,v)$. For $C_1$: \iftag{prvBox}{if $\Box!A115 \in\Gamma$ and $\mSat{M}{\Box!A}[u]$ then also116 $\mSat{M}{!A}[v]$ (since $Ruv$).\iftag{prvDiamond}{ Similarly,117 }{}}{}\iftag{prvDiamond}{if $\Diamond!A \in \Gamma$ and118 $\mSat{M}{!A}[v]$ then $\mSat{M}{\Diamond!A}[u]$ since119 $Ruv$.}{} For $C_2$: \iftag{prvBox}{if $\Box!A \in \Gamma$ and120 $\mSat{M}{\Box!A}[v]$ then $Ruv$ implies $Rvu$ by symmetry, so121 that $\mSat{M}{!A}[u]$.\iftag{prvDiamond}{ Similarly,122 }{}}{}\iftag{prvDiamond}{if $\Diamond!A \in\Gamma$ and123 $\mSat{M}{!A}[u]$ then $\mSat{M}{\Diamond!A}[v]$ (since $Rvu$124 by symmetry).}{}125 \item Exercise.126 \item Exercise.127 \item Exercise.128 \end{enumerate}129\end{proof}130\begin{prob}132 Complete the proof of \olref[nml][fil][acc]{thm:more-filtrations}.133\end{prob}134\end{document}
content/normal-modal-logic/filtrations/euclidean-filtrations.tex
1% Part: normal-modal-logic2% Chapter: filtrations3% Section: euclidean-filtrations4\documentclass[../../../include/open-logic-section]{subfiles}6\begin{document}8\olfileid{nml}{fil}{euc}10\olsection{Filtrations of Euclidean Models}12The approach of \olref[acc]{sec} does not work in the case of models14that are euclidean or serial and euclidean. Consider the model at the15top of \olref{fig:ser-eucl}, which is both euclidean and serial. Let16$\Gamma = \{p, \Box p \}$. When taking a filtration through $\Gamma$,17then $[w_1] = [w_3]$ since $w_1$ and $w_3$ are the only worlds that18agree on~$\Gamma$. Any filtration will also have the arrow inherited19from $\mModel{M}$, as depicted in \olref{fig:ser-eucl2}. That model20isn't euclidean. Moreover, we cannot add arrows to that model in order21to make it euclidean. We would have to add double arrows between22$[w_2]$ and $[w_4]$, and then also between $w_2$ and~$w_5$. But $\Box23p$ is supposed to be true at~$w_2$, while $p$ is false at~$w_5$.24\begin{figure}[htpb]26 \centering27 \begin{tikzpicture}[modal]28 \node[world] (w1)29 [label={left: \mFalse{p}},30 label={below: $\mSat{{}}{\Box p}$}] {$w_1$}; 31 \node[world] (w2)32 [label={right: \mTrue{p}},33 label = {below: $\mSat{{}}{\Box p}$},34 right=of w1] {$w_2$}; 35 \draw[->] (w1) to (w2);36 \node[world] (w3)37 [label={left: \mFalse{p}},38 label={below: $\mSat{{}}{\Box p}$},39 below=of w1] {$w_3$}; 40 \node[world] (w4)41 [label={right:\mTrue{p}},42 label={below: $\mSat/{{}}{\Box p}$},43 right=of w3] {$w_4$};44 \draw[->] (w3) to (w4);45 \draw[reflexive above] (w4) to (w4); 46 \node[world] (w5)47 [label={right: \mFalse{p}},48 label=below:$\mSat/{{}}{\Box p}$,49 right=of w4] {$w_5$}; 50 \draw[->, bend left] (w4) to (w5);51 \draw[->, bend left] (w5) to (w4);52 \draw[reflexive above] (w5) to (w5); 53 \end{tikzpicture}54 \caption{A serial and euclidean model.}55 \ollabel{fig:ser-eucl}56\end{figure}57\begin{figure}[ht]59 \centering60 \begin{tikzpicture}[modal,every text node part/.style={align=center}]61 \node[world] (w1)62 [label={left: \mFalse{p}},63 label={right:$[w_1]=[w_3]$},64 label={below: $\mSat{{}}{\Box p}$}] {$[w_1]$}; 65 \node[world] (w2)66 [label={right: \mTrue{p}},67 label = {below: $\mSat{{}}{\Box p}$},68 right=of w1, yshift=1.5cm] {$[w_2]$}; 69 \draw[->] (w1) to (w2);70 \node[world] (w4)71 [label={right:\mTrue{p}},72 label={below: $\mSat/{{}}{\Box p}$},73 right=of w1,yshift=-1.5cm] {$[w_4]$};74 \draw[->] (w1) to (w4);75 \draw[reflexive above] (w4) to (w4); 76 \node[world] (w5)77 [label={right: \mFalse{p}},78 label=below:$\mSat/{{}}{\Box p}$,79 right=of w4] {$[w_5]$}; 80 \draw[->, bend left] (w4) to (w5);81 \draw[->, bend left] (w5) to (w4);82 \draw[reflexive above] (w5) to (w5); 83 \end{tikzpicture}84 \caption{The filtration of the model in \olref{fig:ser-eucl}.}85 \ollabel{fig:ser-eucl2}86\end{figure}87In particular, to obtain a euclidean filtration it is not enough to89consider filtrations through arbitrary $\Gamma$'s closed under90sub-!!{formula}s. Instead we need to consider sets $\Gamma$ that are91\emph{modally closed} (see \olref[pre]{defn:modallyclosed}). Such sets92of sentences are infinite, and therefore do not immediately yield a93finite model property or the decidability of the corresponding system.94\begin{thm}\ollabel{thm:modal-closed-filt}96 Let $\Gamma$ be modally closed, $\mModel{M}=\tuple{W,R,V}$, and97 $\mModel{M^*} = \tuple{W^*,R^*,V^*}$ be a coarsest filtration of98 $\mModel{M}$.99 \begin{enumerate}100 \item If $\mModel{M}$ is symmetric, so is $\mModel{M^*}$.101 \item If $\mModel{M}$ is transitive, so is $\mModel{M^*}$.102 \item If $\mModel{M}$ is euclidean, so is $\mModel{M^*}$.103 \end{enumerate}104\end{thm}105\begin{proof}107\begin{enumerate}108 \item If $\mModel{M^*}$ is a coarsest filtration, then by definition109 $R^*[u][v]$ holds if and only if $C_1(u,v)$. For transitivity,110 suppose $C_1(u,v)$ and $C_1(v,w)$; we have to show111 $C_1(u,w)$. \iftag{prvBox}{Suppose $\mSat{M}{\Box !A}[u]$; then112 $\mSat{M}{\Box\Box!A}[u]$ since \Ax{4} is valid in all113 transitive models; since $\Box\Box!A \in \Gamma$ by closure,114 also by $C_1(u,v)$, $\mSat{M}{\Box!A}[v]$ and by $C_1(v,w)$,115 also $\mSat{M}{!A}[w]$. }{}\iftag{prvDiamond}{Suppose116 $\mSat{M}{!A}[w]$; then $\mSat{M}{\Diamond !A}[v]$ by117 $C_1(v,w)$, since $\Diamond !A \in \Gamma$ by modal closure. By118 $C_1(u,v)$, we get $\mSat{M}{\Diamond\Diamond !A}[u]$ since119 $\Diamond\Diamond!A \in \Gamma$ by modal closure. Since120 $\Ax{4}_\Diamond$ is valid in all transitive models,121 $\mSat{M}{\Diamond!A}[u]$.}{}122 \item Exercise. Use the fact that both \Ax{5} and $\Ax{5_\Diamond}$123 are valid in all euclidean models.124 \item Exercise. Use the fact that \Ax{B} and $\Ax{B_\Diamond}$ are125 valid in all symmetric models.126\end{enumerate}127\end{proof}128\begin{prob}130 Complete the proof of \olref[nml][fil][euc]{thm:modal-closed-filt}.131\end{prob}132\end{document}