content/normal-modal-logic/frame-definability/frame-definability.tex
% Part: normal-modal-logic% Chapter: frame-definability\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{nml}{frd}{Frame Definability}\olimport{introduction}\olimport{properties-accessibility}\olimport{frames}\olimport{definability}\olimport{first-order-definability}\olimport{equivalence-S5}\olimport{second-order-definability}\OLEndChapterHook\end{document}
content/normal-modal-logic/frame-definability/introduction.tex
% Part: normal-modal-logic% Chapter: frame-correspondence% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{frd}{int}\olsection{Introduction}One question that interests modal logicians is the relationshipbetween the accessibility relation and the truth of certain!!{formula}s in models with that accessibility relation. For instance,suppose the accessibility relation is reflexive, i.e., for every $w\in W$, $Rww$. In other words, every world is accessible fromitself. That means that when $\Box !A$ is true at a world~$w$, $w$itself is among the accessible worlds at which~$!A$ must therefore betrue. So, if the accessibility relation~$R$ of~$\mModel{M}$ isreflexive, then whatever world $w$ and formula $!A$ we take, $\Box !A\lif !A$ will be true there (in other words, the schema $\Box p \lifp$ and all its substitution instances are true in~$\mModel{M}$).The converse, however, is false. It's not the case, e.g., that if$\Box p \lif p$ is true in~$\mModel{M}$, then $R$ is reflexive. For wecan easily find a non-reflexive model~$\mModel{M}$ where $\Box p \lifp$ is true at all worlds: take the model with a single world~$w$, notaccessible from itself, but with $w \in V(p)$. By picking the truthvalue of $p$ suitably, we can make $\Box !A \lif !A$ true in a modelthat is not reflexive.The solution is to remove the variable assignment~$V$ from theequation. If we require that $\Box p \lif p$ is true at all worldsin~$\mModel{M}$, regardless of which worlds are in~$V(p)$, then it isnecessary that $R$ is reflexive. For in any non-reflexive model, therewill be at least one world~$w$ such that not $Rww$. If we set $V(p) =W \setminus \{w\}$, then $p$ will be true at all worlds otherthan~$w$, and so at all worlds accessible from~$w$ (since $w$ isguaranteed not to be accessible from~$w$, and $w$ is the only worldwhere~$p$ is false). On the other hand, $p$ is false at $w$, so $\Boxp \lif p$ is false at~$w$.This suggests that we should introduce a notation for model structureswithout a valuation: we call these \emph{frames}. A frame $\mModel{F}$is simply a pair $\tuple{W, R}$ consisting of a set of worlds with anaccessibility relation. Every model $\tuple{W, R, V}$ is then, as wesay, \emph{based on} the frame $\tuple{W, R}$. Conversely, a framedetermines the class of models based on it; and a class of framesdetermines the class of models which are based on any frame in theclass. And we can define $\mModel{F} \Entails !A$, the notion of !!a{formula}being \emph{valid} in a frame as: $\mSat{M}{!A}$ for all $\mModel{M}$based on~$\mModel{F}$.With this notation, we can establish correspondence relations between!!{formula}s and classes of frames: e.g., $\mModel{F} \Entails \Box p \lif p$if, and only if, $\mModel{F}$ is reflexive.\end{document}
content/normal-modal-logic/frame-definability/properties-accessibility.tex
% Part: normal-modal-logic% Chapter: frame-correspondence% Section: properties-accessibility\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{frd}{acc}\olsection{Properties of Accessibility Relations}Many modal !!{formula}s turn out to be characteristic of simple, andeven familiar, properties of the accessibility relation. In onedirection, that means that any model that has a given property makes acorresponding !!{formula} (and all its substitution instances)true. We begin with five classical examples of kinds of accessibilityrelations and the formulas the truth of which they guarantee.\begin{thm}\ollabel{thm:soundschemas}Let $\mModel{M} = \tuple{W, R, V}$ be a model. If $R$ has theproperty on the left side of \olref{tab:five}, every instance of the!!{formula} on the right side is true in~$\mModel{M}$.\end{thm}\begin{table}[t]\begin{tabular}{| l || l |}\hline{\emph{If $R$ is \dots}} & {\emph{then \dots is true in~$\mModel{M}$:}} \\\hline \hline\emph{serial}: $\forall u \exists v Ruv$ & \hbox to.43\textwidth{$\Box p \lif \Diamond p$ \hfill (\Ax{D})} \\\hline\emph{reflexive}: $\forall w Rww$& \hbox to.43\textwidth{$\Box p \lif p$ \hfill (\Ax{T})} \\\hline\emph{symmetric}: & \hbox to .43\textwidth{$p \lif \Box\Diamond p$ \hfill (\Ax{B})} \\$\forall u\forall v(Ruv \lif Rvu)$ & \\\hline\emph{transitive}: & \hbox to.43\textwidth{$\Box p \lif \Box \Box p$ \hfill (\Ax{4})} \\$\forall u \forall v \forall w ((Ruv \land Rvw) \lif Ruw)$ & \\\hline\emph{euclidean}: & \hbox to .43\textwidth{$\Diamond p \lif \Box\Diamond p$ \hfill (\Ax{5})} \\$\forall w \forall u \forall v ((Rwu \land Rwv) \lif Ruv)$ &\\\hline\end{tabular}\caption{Five correspondence facts.}\ollabel{tab:five}\end{table}\begin{proof}Here is the case for \Ax{B}: to show that the schema is true in amodel we need to show that all of its instances are true at all worldsin the model. So let $!A \lif \Box\Diamond !A$ be a given instanceof \Ax{B}, and let $w \in W$ be an arbitrary world. Suppose theantecedent $!A$ is true at $w$, in order to show that $\Box \Diamond!A$ is true at $w$. So we need to show that $\Diamond !A$ is true atall $w'$ accessible from $w$. Now, for any $w'$ such that $Rww'$ wehave, using the hypothesis of symmetry, that also $Rw'w$ (see\olref{fig:Bsymm}). Since $\mSat{M}{!A}[w]$, we have$\mSat{M}{\Diamond !A}[w']$. Since $w'$ was an arbitrary world suchthat $Rww'$, we have $\mSat{M}{\Box\Diamond!A}[w]$.We leave the other cases as exercises.\end{proof}\begin{prob}Complete the proof of \olref[nml][frd][acc]{thm:soundschemas}.\end{prob}\begin{figure}\begin{center}\begin{tikzpicture}[modal]\node[world] (w1) [label={below:$\mSat{{}}{\formula{A}}$\\$\mSat{{}}{\Box\Diamond \formula{A}}$}] {$w$};\node[world] (w2) [label=below:{$\mSat{{}}{\Diamond \formula{A}}$},right=of w1] {$w'$};\draw[->, bend left] (w1) to (w2);\draw[->, bend left] (w2) to (w1);\end{tikzpicture}\end{center}\caption{The argument from symmetry.}\ollabel{fig:Bsymm}\end{figure}Notice that the converse implications of \olref{thm:soundschemas} donot hold: it's not true that if a model verifies a schema, then theaccessibility relation of that model has the corresponding property.In the case of \Ax{T} and reflexive models, it is easy to give anexample of a model in which \Ax{T} itself fails: let $W = \{w\}$ and$V(p) = \emptyset$. Then $R$ is not reflexive, but $\mSat{M}{\Boxp}[w]$ and $\mSat/{M}{p}[w]$. But here we have just a singleinstance of \Ax{T} that fails in~$\mModel{M}$; other instances, e.g.,$\Box \lnot p \lif \lnot p$ are true. It is harder to give exampleswhere \emph{every substitution instance} of~\Ax{T} is truein~$\mModel{M}$ and $\mModel{M}$ is not reflexive. But there are suchmodels, too:\begin{prop}\ollabel{prop:reflexive}Let $\mModel{M} = \tuple{W, R, V}$ be a model such that $W = \{u, v\}$, where worlds $u$ and $v$ are related by $R$: i.e., both $Ruv$and $Rvu$. Suppose that for all $p$: $u \in V(p) \Leftrightarrow v\in V(p)$. Then:\begin{enumerate}\item For all $!A$: $\mSat{M}{!A}[u]$ if and only if$\mSat{M}{!A}[v]$ (use induction on $!A$).\item Every instance of~\Ax{T} is true in $\mModel{M}$.\end{enumerate}Since $\mModel{M}$ is not reflexive (it is, in fact,\emph{irreflexive}), the converse of \olref{thm:soundschemas}fails in the case of \Ax{T} (similar arguments can be given forsome---though not all---the other schemas mentioned in\olref{thm:soundschemas}).\end{prop}\begin{prob}Prove the claims in \olref[nml][frd][acc]{prop:reflexive}.\end{prob}Although we will focus on the five classical !!{formula}s \Ax{D},\Ax{T}, \Ax{B}, \Ax{4}, and \Ax{5}, we record in\olref{tab:anotherfive} a few more properties of accessibilityrelations. The accessibility relation~$R$ is partially functional, iffrom every world at most one world is accessible. If it is the casethat from every world exactly one world is accessible, we call itfunctional. (Thus the functional relations are precisely those thatare 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$,there is a~$w$ ``between'' $u$ and~$v$. So weakly dense relations arein a sense the opposite of transitive relations: in a transitiverelation, whenever you can reach $v$ from~$u$ by a detour via~$w$, youcan reach $v$ from $u$ directly; in a weakly dense relation, wheneveryou can reach $v$ from~$u$ directly, you can also reach it by a detourvia some~$w$. A relation is weakly directed if whenever you can reachworlds $u$ and~$v$ from some world~$w$, you can reach a singleworld~$t$ from both $u$ and~$v$---this is sometimes called the``diamond property'' or ``confluence.''\begin{table}[t]\begin{tabular}{| p{.50\textwidth} || p{.43\textwidth} |}\hline{\emph{If $R$ is \dots}} & {\emph{then \dots is true in~$\mModel{M}$:}} \\\hline \hline\emph{partially functional}: &\multirow{2}{*}{$\Diamond p \lif \Box p$} \\$ \forall w \forall u \forall v ((Rwu \land Rwv) \lif u =v )$ & \\\hline\multirow{2}{*}{\emph{functional}: $\forall w \exists v \forall u(Rwu \liff \eq[u][v]) $}& \multirow{2}{*}{$\Diamond p \liff \Box p$} \\& \\\hline\emph{weakly dense}: & \multirow{2}{*}{$\Box \Box p \lif\Box p$} \\$\forall u\forall v(Ruv \lif \exists w(Ruw \land Rwv))$ & \\\hline\emph{weakly connected}: &\multirow{3}{*}{\hbox to.43\textwidth{$\begin{array}{@{}l@{}}\Box ((p \land \Box p) \lif q) \lor {} \\\qquad \Box ((q \land \Box q) \lif p)\end{array}$ \hfill (\Ax{L})}} \\$\forall w \forall u \forall v ((Rwu \land Rwv) \lif {}$ &\\\qquad $(Ruv \lor u=v \lor Rvu))$ & \\\hline\emph{weakly directed}: & \multirow{3}{*}{\hbox to .43\textwidth{$\Diamond\Box p \lif \Box\Diamond p$\hfill (\Ax{G})}} \\$\forall w \forall u \forall v ((Rwu \land Rwv) \lif {}$ & \\\qquad $\exists t (Rut \land Rvt))$ & \\\hline\end{tabular}\caption{Five more correspondence facts.}\ollabel{tab:anotherfive}\end{table}\begin{prob}Let $\mModel{M} = \tuple{W, R, V}$ be a model. Show that if $R$satisfies the left-hand properties of\olref[nml][frd][acc]{tab:anotherfive}, every instance of thecorresponding right-hand formula is true in~$\mModel{M}$.\end{prob}\end{document}
content/normal-modal-logic/frame-definability/frames.tex
% Part: normal-modal-logic% Chapter: frame-correspondence% Section: frames\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{frd}{fra}\olsection{Frames}\begin{defn}A \emph{frame} is a pair $\mModel{F} = \tuple{W,R}$ where $W$ is anon-empty set of worlds and $R$ a binary relation on~$W$. A model$\mModel{M}$ is \emph{based on} a frame $\mModel{F} = \tuple{W,R}$if and only if $\mModel{M} = \tuple{W, R, V}$ for some valuation $V$.\end{defn}\begin{defn}If $\mModel{F}$ is a frame, we say that $!A$ is \emph{valid in$\mModel{F}$,} $\mModel{F} \Entails !A$, if $\mSat{M}{!A}$ forevery model~$\mModel{M}$ based on~$\mModel{F}$.If $\mClass{F}$ is a class of frames, we say $!A$ is \emph{valid in$\mClass{F}$,} $\mClass{F} \Entails !A$, iff $\mModel{F} \Entails!A$ for every frame~$\mModel{F} \in \mClass{F}$.\end{defn}The reason frames are interesting is that correspondence betweenschemas and properties of the accessibility relation~$R$ is at thelevel of frames, \emph{not of models}. For instance, although \Ax{T}is true in all reflexive models, not every model in which \Ax{T} istrue is reflexive. However, it \emph{is} true that not only is \Ax{T}\emph{valid} on all reflexive \emph{frames}, also every frame inwhich \Ax{T} is valid is reflexive.\begin{rem}Validity in a class of frames is a special case of the notion ofvalidity in a class of models: $\mClass{F} \Entails !A$ iff$\mClass{C} \Entails !A$ where $\mClass{C}$ is the class of all modelsbased on a frame in~$\mClass{F}$.Obviously, if !!a{formula} or a schema is valid, i.e., valid withrespect to the class of \emph{all} models, it is also valid withrespect to any class~$\mClass{F}$ of frames.\end{rem}\end{document}
content/normal-modal-logic/frame-definability/definability.tex
% Part: normal-modal-logic% Chapter: frame-definability% Section: definability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{frd}{def}\olsection{Frame Definability}Even though the converse implications of \olref[acc]{thm:soundschemas}fail, they hold if we replace ``model'' by ``frame'': for theproperties considered in \olref[acc]{thm:soundschemas}, it \emph{is}true that if !!a{formula} is valid in a \emph{frame} then theaccessibility relation of that frame has the correspondingproperty. So, the !!{formula}s considered \emph{define} the classes offrames that have the corresponding property.\begin{defn}If $\mClass{F}$ is a class of frames, we say $!A$\emph{defines}~$\mClass{F}$ iff $\mModel{F} \Entails !A$ for all and onlyframes~$\mModel{F} \in \mClass{F}$.\end{defn}We now proceed to establish the full definability results forframes.\begin{thm}\ollabel{thm:fullCorrespondence}If the !!{formula} on the right side of \olref[acc]{tab:five} is valid in aframe~$\mModel{F}$, then $\mModel{F}$ has the property on the leftside.\end{thm}\begin{proof}\begin{enumerate}\item Suppose \Ax{D} is valid in $\mModel{F} = \tuple{W, R}$, i.e.,$\mModel{F} \Entails \Box p \lif \Diamond p$. Let $\mModel{M} =\tuple{W, R, V}$ be a model based on~$\mModel{F}$, and $w \inW$. We have to show that there is a $v$ such that~$Rwv$. Supposenot: then both $\mSat{M}{\Box !A}$ and $\mSat/{M}{\Diamond !A}[w]$for any~$!A$, including~$p$. But then $\mSat/{M}{\Box p \lif\Diamond p}[w]$, contradicting the assumption that $\mModel{F}\Entails \Box p \lif \Diamond p$.\item Suppose \Ax{T} is valid in $\mModel{F}$, i.e., $\mModel{F} \Entails \Boxp \lif p$. Let $w \in W$ be an arbitrary world; we need to show$Rww$. Let $u \in V(p)$ if and only if $Rwu$ (when $q$ is otherthan $p$, $V(q)$ is arbitrary, say $V(q) = \emptyset)$. Let$\mModel{M} = \tuple{W, R, V}$. By construction, for all $u$ suchthat $Rwu$: $\mSat{M}{p}[u]$, and hence $\mSat{M}{\Box p}[w]$. Butby hypothesis $\Box p \lif p$ is true at~$w$, so that$\mSat{M}{p}[w]$, but by definition of $V$ this is possible onlyif~$Rww$.\item We prove the contrapositive: Suppose $\mModel{F}$ is notsymmetric, we show that \Ax{B}, i.e., $p \lif \Box\Diamond p$ isnot valid in $\mModel{F}= \tuple{W, R}$. If $\mModel{F}$ is notsymmetric, there are $u$, $v \in W$ such that $Ruv$ but not$Rvu$. Define $V$ such that $w \in V(p)$ if and only if not $Rvw$(and $V$ is arbitrary otherwise). Let $\mModel{M} =\tuple{W, R,V}$. Now, by definition of $V$, $\mSat{M}{p}[w]$ for all $w$such that not $Rvw$, in particular, $\mSat{M}{p}[u]$ sincenot~$Rvu$. Also, since $Rvw$ iff $w \notin V(p)$, there is no~$w$such that $Rvw$ and $\mSat{M}{p}[w]$, and hence$\mSat/{M}{\Diamond p}[v]$. Since~$Ruv$, also$\mSat/{M}{\Box\Diamond p}[u]$. It follows that $\mSat/{M}{p \lif\Box\Diamond p}[u]$, and so $\Ax{B}$ is not validin~$\mModel{F}$.\item Suppose \Ax{4} is valid in $\mModel{F} = \tuple{W,R}$, i.e.,$\mModel{F} \Entails \Box p \lif \Box\Box p$, and let $u$, $v$, $w \in W$ bearbitrary worlds such that $Ruv$ and $Rvw$; we need to show that$Ruw$. Define $V$ such that $z \in V(p)$ if and only if $Ruz$ (and$V$ is arbitrary otherwise). Let $\mModel{M} =\tuple{W, R, V}$. Bydefinition of $V$, $\mSat{M}{p}[z]$ for all $z$ such that $Ruz$,and hence $\mSat{M}{\Box p}[u]$. But by hypothesis \Ax{4}, $\Box p\lif \Box \Box p$, is true at $u$, so that $\mSat{M}{\Box \Boxp}[u]$. Since $Ruv$ and $Rvw$, we have $\mSat{M}{p}[w]$, but bydefinition of~$V$ this is possible only if $Ruw$, as desired.\item We proceed contrapositively, assuming that the frame$\mModel{F} = \tuple{W, R}$ is not euclidean, and show that itfalsifies~\Ax{5}, i.e., $\mModel{F} \Entails/ \Diamond p \lif\Box\Diamond p$. Suppose there are worlds $u$, $v$, $w \in W$such that $Rwu$ and $Rwv$ but not~$Ruv$. Define $V$ such that forall worlds $z$, $z \in V(p)$ if and only if it is \emph{not} thecase that~$Ruz$. Let $\mModel{M} =\tuple{W, R, V}$. Then byhypothesis $\mSat{M}{p}[v]$ and since $Rwv$ also$\mSat{M}{\Diamond p}[w]$. However, there is no world $y$ suchthat $Ruy$ and $\mSat{M}{p}[y]$ so $\mSat/{M}{\Diamondp}[u]$. Since $Rwu$, it follows that $\mSat/{M}{\Box\Diamondp}[w]$, so that \Ax{5}, $\Diamond p \lif \Box\Diamond p$, failsat~$w$.\end{enumerate}\end{proof}You'll notice a difference between the proof for \Ax{D} and the othercases: no mention was made of the valuation~$V$. In effect, we provedthat if $\mSat{M}{\Ax{D}}$ then $\mModel{M}$ is serial. So \Ax{D}defines the class of serial \emph{models}, not just frames.\begin{cor}\ollabel{prop:D-serial}Any model where \Ax{D} is true is serial.\end{cor}\begin{cor}Each !!{formula} on the right side of \olref[acc]{tab:five} definesthe class of frames which have the property on the left side.\end{cor}\begin{proof}In \olref[acc]{thm:soundschemas}, we proved that if a model has theproperty on the left, the !!{formula} on the right is true init. Thus, if a frame~$\mModel{F}$ has the property on the left, the!!{formula} on the right is valid in~$\mModel{F}$. In\olref{thm:fullCorrespondence}, we proved the converse implications:if !!a{formula} on the right is valid in~$\mModel{F}$, $\mModel{F}$has the property on the left.\end{proof}\begin{prob}Show that if the !!{formula} on the right side of\olref[nml][frd][acc]{tab:anotherfive} is valid in a frame~$\mModel{F}$, then$\mModel{F}$ has the property on the left side. To do this, consider aframe that does \emph{not} satisfy the property on the left, anddefine a suitable~$V$ such that the !!{formula} on the right is falseat some world.\end{prob}\olref{thm:fullCorrespondence} also shows that the properties can becombined: for instance if both \Ax{B} and \Ax{4} are validin~$\mModel{F}$ then the frame is both symmetric and transitive,etc. Many important modal logics are characterized as the set of!!{formula}s valid in all frames that combine some frame properties,and so we can characterize them as the set of !!{formula}s valid inall frames in which the corresponding defining !!{formula}s are valid.For instance, the classical system \Log{S4} is the set of all!!{formula}s valid in all reflexive and transitive frames, i.e., inall those where both \Ax{T} and~\Ax{4} are valid. \Log{S5} is the setof all formulas valid in all reflexive, symmetric, and euclideanframes, i.e., all those where all of \Ax{T}, \Ax{B}, and \Ax{5} arevalid.Logical relationships between properties of $R$ in general correspondto relationships between the corresponding defining !!{formula}s. Forinstance, every reflexive relation is serial; hence, whenever \Ax{T}is valid in a frame, so is~\Ax{D}. (Note that this relationship is\emph{not} that of entailment. It is not the case that whenever$\mSat{M}{\Ax{T}}[w]$ then $\mSat{M}{\Ax{D}}[w]$.) We record some suchrelationships.\begin{prop}\ollabel{prop:relation-facts}Let $R$ be a binary relation on a set $W$; then:\begin{enumerate}\item If $R$ is reflexive, then it is serial.\item If $R$ is symmetric, then it is transitive if and only if itis euclidean.\item If $R$ is symmetric or euclidean then it is weakly directed(it has the ``diamond property'').\item If $R$ is euclidean then it is weakly connected.\item If $R$ is functional then it is serial.\end{enumerate}\end{prop}\begin{prob}Prove \olref[nml][frd][def]{prop:relation-facts}.\end{prob}\end{document}
content/normal-modal-logic/frame-definability/first-order-definability.tex
% Part: normal-modal-logic% Chapter: frame-correspondence% Section: first-order-definability\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{frd}{fol}\olsection{First-order Definability}We've seen that a number of properties of accessibility relations offrames can be defined by modal !!{formula}s. For instance, symmetry offrames can be defined by the !!{formula}~\Ax{B}, $p \lif \Box\Diamondp$. The conditions we've encountered so far can all be expressed byfirst-order !!{formula}s in !!a{language} involving a single two-place!!{predicate}. For instance, symmetry is defined by$\lforall[x][\lforall[y][(\Atom{Q}{x,y} \lif \Atom{Q}{y, x})]]$ in thesense that a first-order !!{structure}~$\Struct{M}$ with $\Domain{M} =W$ and $\Assign{Q}{M} = R$ satisfies the preceding formula iff $R$ issymmetric. This suggests the following definition:\begin{defn}A class~$\mClass{F}$ of frames is \emph{first-order definable} if there is!!a{sentence}~$!A$ in the first-order language with a singletwo-place !!{predicate}~$Q$ such that $\mModel{F} =\tuple{W, R} \in \mClass{F}$ iff $\Sat{M}{!A}$ in the first-order!!{structure}~$\Struct{M}$ with $\Domain{M} = W$ and $\Assign{Q}{M}= R$.\end{defn}It turns out that the properties and modal !!{formula}s that definethem considered so far are exceptional. Not every !!{formula} definesa first-order definable class of frames, and not every first-orderdefinable class of frames is definable by a modal formula.A counterexample to the first is given by the L\"ob formula:\begin{equation}\Box(\Box p \lif p) \lif \Box p. \tag{\Ax{W}}\end{equation}\Ax{W} defines the class of transitive and converse well-foundedframes. A relation is well-founded if there is no infinite sequence$w_1$, $w_2$, \dots{} such that $Rw_2w_1$, $Rw_3w_2$, \dots. Forinstance, the relation $<$ on~$\Nat$ is well-founded, whereas therelation $<$ on~$\Int$ is not. A relation is converse well-foundediff its converse is well-founded. So converse well-founded relationsare those where there is no infinite sequence $w_1$, $w_2$, \dots{}such that $Rw_1w_2$, $Rw_2w_3$, \dots.There is, however, no first-order !!{formula} defining transitiveconverse well-founded relations. For suppose~$\Sat{M}{!F}$ iff $R =\Assign{Q}{M}$ is transitive converse well-founded. Let $!A_n$ be the!!{formula}\[(\Atom{Q}{a_1,a_2} \land \dots \land\Atom{Q}{a_{n-1},a_{n}})\]Now consider the set of !!{formula}s\[\Gamma = \{!F, !A_1, !A_2, \dots\}.\]Every finite subset of $\Gamma$ is satisfiable: Let $k$ be largestsuch that $!A_k$ is in the subset, $\Domain{M_k} = \{1, \dots, k\}$,$\Assign{a_i}{M_k} = i$, and $\Assign{Q}{M_k} = <$. Since $<$ on $\{1,\dots, k\}$ is transitive and converse well-founded,$\Sat{M_k}{!F}$. $\Sat{M_k}{!A_i}$ by construction, for all $i \le k$.By the Compactness Theorem for first-order logic, $\Gamma$ issatisfiable in some !!{structure}~$\Struct{M}$. By hypothesis, since$\Sat{M}{!F}$, the relation $\Assign{Q}{M}$ is conversewell-founded. But clearly, $\Assign{a_1}{M}$, $\Assign{a_2}{M}$,\dots{} would form an infinite sequence of the kind ruled out byconverse well-foundedness.A counterexample to the second claim is given by the property ofuniversality: for every $u$ and $v$, $Ruv$. Universal frames arefirst-order definable by the formula$\lforall[x][\lforall[y][\Atom{Q}{x,y}]]$. However, no modal formulais valid in all and only the universal frames. This is a consequenceof a result that is independently interesting: the formulas valid inuniversal frames are exactly the same as those valid in reflexive,symmetric, and transitive frames. There are reflexive, symmetric, andtransitive frames that are not universal, hence every !!{formula}valid in all universal frames is also valid in some non-universalframes.\end{document}
content/normal-modal-logic/frame-definability/equivalence-S5.tex
% Part: normal-modal-logic% Chapter: frame-correspondence% Section: equivalence-S5\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{frd}{es5}\olsection{Equivalence Relations and \Log{S5}}The modal logic \Log{S5} is characterized as the set of !!{formula}svalid on all universal frames, i.e., every world is accessible fromevery world, including itself. In such a scenario, $\Box$ correspondsto necessity and $\Diamond$ to possibility: $\Box !A$ is true if $!A$is true at \emph{every} world, and $\Diamond !A$ is true if $!A$ istrue at \emph{some} world. It turns out that \Log{S5} can also becharacterized as the !!{formula}s valid on all reflexive, symmetric,and transitive frames, i.e., on all \emph{equivalence relations}.\begin{defn}A binary relation $R$ on $W$ is an \emph{equivalence relation} ifand only if it is reflexive, symmetric and transitive. A relation$R$ on $W$ is \emph{universal} if and only if $Ruv$ for all $u,v \inW$.\end{defn}Since \Ax{T}, \Ax{B}, and \Ax{4} characterize the reflexive,symmetric, and transitive frames, the frames where the accessibilityrelation is an equivalence relation are exactly those in which allthree !!{formula}s are valid. It turns out that the equivalencerelations can also be characterized by other combinations of!!{formula}s, since the conditions with which we've definedequivalence relations are equivalent to combinations of other familiarconditions on~$R$.\begin{prop}\ollabel{prop:equivalences}The following are equivalent:\begin{enumerate}\item $R$ is an equivalence relation;\item $R$ is reflexive and euclidean;\item $R$ is serial, symmetric, and euclidean;\item $R$ is serial, symmetric, and transitive.\end{enumerate}\end{prop}\begin{proof}Exercise.\end{proof}\begin{prob}Prove \olref[nml][frd][es5]{prop:equivalences} by showing:\begin{enumerate}\item If $R$ is symmetric and transitive, it is euclidean.\item If $R$ is reflexive, it is serial.\item If $R$ is reflexive and euclidean, it is symmetric.\item If $R$ is symmetric and euclidean, it is transitive.\item If $R$ is serial, symmetric, and transitive, it is reflexive.\end{enumerate}Explain why this suffices for the proof that the conditions areequivalent.\end{prob}\olref{prop:equivalences} is the semantic counterpart to\olref[prf][prs]{prop:S5}, in that it gives an equivalent characterization ofthe modal logic of frames over which $R$ is an equivalence relation (the logictraditionally referred to as \Log{S5}).What is the relationship between universal and equivalence relations?Although every universal relation is an equivalence relation, clearlynot every equivalence relation is universal. However, the !!{formula}svalid on all universal relations are exactly the same as those validon all equivalence relations.\begin{prop}Let $R$ be an equivalence relation, and for each $w \in W$ definethe \emph{equivalence class} of $w$ as the set $[w] = \{w'\in W :Rww'\}$. Then:\begin{enumerate}\item $w \in [w]$;\item $R$ is universal on each equivalence class $[w]$;\item The collection of equivalence classes partitions $W$ into mutuallyexclusive and jointly exhaustive subsets.\end{enumerate}\end{prop}\begin{prop}\ollabel{prop:S5=univ}!!^a{formula}~$!A$ is valid in all frames $\mModel{F} =\tuple{W,R}$where $R$ is an equivalence relation, if and only if it is valid inall frames $\mModel{F} =\tuple{W,R}$ where $R$ is universal. Hence,the logic of universal frames is just \Log{S5}.\end{prop}\begin{proof}It's immediate to verify that a universal relation~$R$ on~$W$ is anequivalence. Hence, if $!A$ is valid in all frames where $R$ is anequivalence it is valid in all universal frames. For the otherdirection, we argue contrapositively: suppose $!B$ is !!a{formula}that fails at a world $w$ in a model $\mModel{M} = \tuple{W, R, V}$based on a frame $\tuple{W,R}$, where $R$ is an equivalence on$W$. So $\mSat/{M}{!B}[w]$. Define a model $\mModel{M}' = \tuple{W',R', V'}$ as follows:\begin{enumerate}\item $W' = [w]$;\item $R'$ is universal on $W'$;\item $V'(p) = V(p) \cap W'$.\end{enumerate}(So the set $W'$ of worlds in $\mModel{M}'$ is represented by theshaded area in \olref{fig:partition}.) It is easy to seethat $R$ and $R'$ agree on $W'$. Then one can show by induction on!!{formula}s that for all $w' \in W'$: $\mSat{M'}{!A}[w']$ if andonly if $\mSat{M}{!A}[w']$ for each $!A$ (this makes sense since $W'\subseteq W$). In particular, $\mSat/{M'}{!B}[w]$, and $!B$ fails ina model based on a universal frame.\end{proof}\begin{figure}[t]\centering\begin{tikzpicture}[node distance=2cm, auto, thick]\clip [rounded corners] (0,0) -- (6,0) -- (6,4) -- (0,4) -- cycle;\begin{scope}\clip (0,0) -- (2,0) .. controls (1.5,1.5) and (4.5,1.5).. (4,4) -- (0,4) -- (0,0) -- cycle;\filldraw[fill=gray!40] (0,4) -- (0,2) .. controls (1.5,1.5)and (4.5,1.5) .. (4.5,0) -- (6,0) -- (6,4) -- (0,4) -- cycle;\end{scope}\draw [name path=line1] (2,0) .. controls (1.5,1.5) and (4.5,1.5) .. (4,4);\draw [name path=line2] (0,2) .. controls (1.5,1.5) and (4.5,1.5) .. (4.5,0);\path [name intersections={of=line1 and line2}];\draw [rounded corners, use as bounding box, very thick] (0,0)-- (6,0) -- (6,4) -- (0,4) -- cycle;\node at (2,3) {$[w]$} ;\node at (1,1) {$[u]$} ;\node at (3,0.75) {$[v]$} ;\node at (4.75,2) {$[z]$} ;\end{tikzpicture}\caption{A partition of $W$ in equivalence classes.}\ollabel{fig:partition}\end{figure}\end{document}
content/normal-modal-logic/frame-definability/second-order-definability.tex
% Part: normal-modal-logic% Chapter: frame-correspondence% Section: standard-translation\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{frd}{st}\olsection{Second-order Definability}Not every frame property definable by modal formulas is first-orderdefinable. However, if we allow quantification over one-placepredicates (i.e., monadic second-order quantification), we define allmodally definable frame properties. The trick is to exploit asystematic way in which the conditions under which a modal !!{formula}is true at a world are related to first-order !!{formula}s. This isthe so-called standard translation of modal formulas into first-orderformulas in a language containing not just a two-place!!{predicate}~$Q$ for the accessibility relation, but also a one-place!!{predicate}~$P_i$ for the !!{propositional variable}s~$\Obj p_i$occurring in~$!A$.\begin{defn}The \emph{standard translation}~$\ST_x(!A)$ is inductively definedas follows:\begin{enumerate}\tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\ST_x(\indfrm) = \lfalse$.}}{}\tagitem{prvTrue}{\indcase{!A}{\lfalse}{$\ST_x(\indfrm) = \ltrue$.}}{}\item \indcase{!A}{\Obj p_i}{$\ST_x(\indfrm) = \Atom{P_i}{x}$.}\tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\ST_x(\indfrm) = \lnot \ST_x(!B)$.}}{}\tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{$\ST_x(\indfrm) = (\ST_x(!B)\land \ST_x(!C))$.}}{}\tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{$\ST_x(\indfrm) = (\ST_x(!B)\lor \ST_x(!C))$.}}{}\tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{$\ST_x(\indfrm) = (\ST_x(!B)\lif \ST_x(!C))$.}}{}\tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{$\ST_x(\indfrm) = (\ST_x(!B)\liff \ST_x(!C))}$.}{}\tagitem{prvBox}{\indcase{!A}{\Box !B}{$\ST_x(\indfrm) =\lforall[y][(\Atom{Q}{x,y} \lif \ST_y(!B))]$.}}{}\tagitem{prvDiamond}{\indcase{!A}{\Diamond !B}{$\ST_x(\indfrm) =\lexists[y][(\Atom{Q}{x,y} \land \ST_y(!B))]$.}}{}\end{enumerate}\end{defn}For instance, $\ST_x(\Box p \lif p)$ is $\lforall[y][(\Atom{Q}{x,y}\lif \Atom{P}{y})] \lif \Atom{P}{x}$. Any !!{structure} for thelanguage of~$\ST_x(!A)$ requires a domain, a two-place relationassigned to~$Q$, and subsets of the domain assigned to the one-place!!{predicate}s~$P_i$. In other words, the components of such!!a{structure} are exactly those of a model for~$!A$: the domain isthe set of worlds, the two-place relation assigned to~$Q$ is theaccessibility relation, and the subsets assigned to~$P_i$ are just theassignments~$V(\Obj p_i)$. It won't surprise that satisfaction of $!A$in a modal model and of $\ST_x(!A)$ in the corresponding !!{structure}agree:\begin{prop}\ollabel{prop:st}Let $\mModel{M} = \tuple{W, R, V}$, $\Struct{M'}$ be the first-order!!{structure} with $\Domain{M'} = W$, $\Assign{Q}{M'} = R$, and$\Assign{P_i}{M'} = V(\Obj p_i)$, and $s(x) = w$. Then\[\mSat{M}{!A}[w] \text{ iff } \Sat{M'}{\ST_x(!A)}[s]\]\end{prop}\begin{proof}By induction on~$!A$.\end{proof}\begin{prop}Suppose $!A$ is a modal !!{formula} and $\mModel{F} = \tuple{W, R}$is a frame. Let $\Struct{F'}$ be the first-order !!{structure} with$\Domain{F'} = W$ and $\Assign{Q}{F'} = R$, and let $!A'$ be thesecond-order formula\[\lforall[X_1][\dots\lforall[X_n][\lforall[x][\SSubst{\ST_x(!A)}{\subst{X_1}{P_1}, \dots,\subst{X_n}{P_n}}]]],\]where $P_1$, \dots, $P_n$ are all one-place !!{predicate}sin~$\ST_x(!A)$. Then\[\mModel{F} \Entails !A \text{ iff } \Sat{F'}{!A'}\]\end{prop}\begin{proof}$\Sat{F'}{!A'}$ iff for every !!{structure}~$\mModel{M'}$ where$\Assign{P_i}{M'} \subseteq W$ for $i = 1$, \dots,~$n$, and forevery $s$ with $s(x) \in W$, $\Sat{M'}{\ST_x(!A)}[s]$. By\olref{prop:st}, that is the case iff for all models~$\mModel{M}$based on~$\mModel{F}$ and every world~$w \in W$, $\mSat{M}{!A}[w]$,i.e., $\mModel{F} \Entails !A$.\end{proof}\begin{defn}A class~$\mClass{F}$ of frames is \emph{second-order definable} ifthere is !!a{sentence}~$!A$ in the second-order language with asingle two-place !!{predicate}~$P$ and quantifiers only over monadicset variables such that $\mModel{F} = \tuple{W, R} \in \mClass{F}$iff $\Sat{M}{!A}$ in the !!{structure}~$\Struct{M}$ with$\Domain{M} = W$ and $\Assign{P}{M} = R$.\end{defn}\begin{cor}If a class of frames is definable by !!a{formula}~$!A$, thecorresponding class of accessibility relations is definable by amonadic second-order sentence.\end{cor}\begin{proof}The monadic second-order sentence~$!A'$ of the preceding proof hasthe required property.\end{proof}As an example, consider again the !!{formula}~$\Box p \lif p$. Itdefines reflexivity. Reflexivity is of course first-order definable bythe !!{sentence}~$\lforall[x][\Atom{Q}{x,x}]$. But it is also definable by themonadic second-order !!{sentence}\[\lforall[X][\lforall[x][(\lforall[y][(\Atom{Q}{x,y} \lif \Atom{X}{y})]\lif \Atom{X}{x})]].\]This means, of course, that the two sentences are equivalent. Here'show you might convince yourself of this directly: First suppose thesecond-order sentence is true in !!a{structure}~$\Struct{M}$. Since $x$ and $X$are universally quantified, the remainder must hold for any $x \in W$and set~$X \subseteq W$, e.g., the set $\Setabs{z}{Rxz}$ where $R =\Assign{Q}{M}$. So, for any~$s$ with $s(x) \in W$ and $s(X) =\Setabs{z}{Rxz}$ we have $\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif\Atom{X}{y})] \lif \Atom{X}{x}}$. But by the way we've picked$s(X)$ that means $\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif\Atom{Q}{x,y})] \lif \Atom{Q}{x,x}}[s]$, which is equivalent to$\Atom{Q}{x,x}$ since the antecedent is valid. Since $s(x)$ isarbitrary, we have $\Sat{M}{\lforall[x][\Atom{Q}{x,x}]}$.Now suppose that $\Sat{M}{\lforall[x][\Atom{Q}{x,x}]}$ and show that$\Sat{M}{\lforall[X][\lforall[x][(\lforall[y][(\Atom{Q}{x,y} \lif\Atom{X}{y})] \lif \Atom{X}{x})]]}$. Pick any assignment~$s$,and assume $\Sat{M}{\lforall[y][(\Atom{Q}{x,y} \lif\Atom{X}{y})]}[s]$. Let $s'$ be the $y$-variant of~$s$ with $s'(y)= s(x)$; we have $\Sat{M}{\Atom{Q}{x,y} \lif \Atom{X}{y}}[s']$, i.e.,$\Sat{M}{\Atom{Q}{x,x} \lif \Atom{X}{x}}[s]$. Since$\Sat{M}{\lforall[x][\Atom{Q}{x,x}]}$, the antecedent is true, and wehave $\Sat{M}{\Atom{X}{x}}[s]$, 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'$ isequivalent to a first-order !!{sentence}. There is no effective methodto decide which ones are.\end{document}
Source-census fragment evidence
The complete original formula is shown in Read and Explore. These immutable census fragments are retained for traceability.
Census fragment projected-formula-0025131 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-ab06abe3932feaeb"><semantics><mrow><mo>∀</mo><mi>w</mi><mo>∀</mo><mi>u</mi><mo>∀</mo><mi>v</mi><mo>(</mo><mo>(</mo><mi>R</mi><mi>w</mi><mi>u</mi><mo>∧</mo><mi>R</mi><mi>w</mi><mi>v</mi><mo>)</mo><mo>→</mo><mspace width="0em"></mspace></mrow><annotation encoding="application/x-tex">\forall w \forall u \forall v ((Rwu \land Rwv) \lif {}</annotation></semantics></math>Census fragment projected-formula-0025132 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-02e18552519285db"><semantics><mrow><mo>(</mo><mi>R</mi><mi>u</mi><mi>v</mi><mo>∨</mo><mi>u</mi><mo>=</mo><mi>v</mi><mo>∨</mo><mi>R</mi><mi>v</mi><mi>u</mi><mo>)</mo><mo>)</mo></mrow><annotation encoding="application/x-tex">(Ruv \lor u=v \lor Rvu))</annotation></semantics></math>Census fragment projected-formula-0025134 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-ab06abe3932feaeb"><semantics><mrow><mo>∀</mo><mi>w</mi><mo>∀</mo><mi>u</mi><mo>∀</mo><mi>v</mi><mo>(</mo><mo>(</mo><mi>R</mi><mi>w</mi><mi>u</mi><mo>∧</mo><mi>R</mi><mi>w</mi><mi>v</mi><mo>)</mo><mo>→</mo><mspace width="0em"></mspace></mrow><annotation encoding="application/x-tex">\forall w \forall u \forall v ((Rwu \land Rwv) \lif {}</annotation></semantics></math>Census fragment projected-formula-0025135 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-84dd6ba0577ab84b"><semantics><mrow><mo>∃</mo><mi>t</mi><mo>(</mo><mi>R</mi><mi>u</mi><mi>t</mi><mo>∧</mo><mi>R</mi><mi>v</mi><mi>t</mi><mo>)</mo><mo>)</mo></mrow><annotation encoding="application/x-tex">\exists t (Rut \land Rvt))</annotation></semantics></math>