The Open Logic Text

en · official · sha256:48c9048b2e91855096bd3699b585c65ccad45173090710a0e319efc71924bf21

% Part: normal-modal-logic % Chapter: axioms-systems % Section: derived-rules \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{prf}{der} \olsection{Derived Rules} Finding and writing !!{derivation}s is obviously difficult, cumbersome, and repetitive. For instance, very often we want to pass from $!A \lif !B$ to $\Box !A \lif \Box !B$, i.e., apply rule~\RK. That requires an application of \Nec, then recording the proper instance of~\Ax{K}, then applying~\MP. Passing from $!A \lif !B$ and $!B \lif !C$ to $!A \lif !C$ requires recording the (long) tautological instance \[ (!A \lif !B) \lif ((!B \lif !C) \lif (!A \lif !C)) \] and applying \MP{} twice. Often we want to replace a sub-!!{formula} by a formula we know to be equivalent, e.g., \iftag{prvDiamond}{$\Diamond !A$ by $\lnot\Box\lnot !A$}{$\Box !A$ by $\lnot\Diamond\lnot !A$}, or $\lnot\lnot !A$ by $!A$. So rather than write out the actual !!{derivation}, it is more convenient to simply record why the intermediate steps are !!{derivable}. For this purpose, let us collect some facts about !!{derivability}. \begin{prop} If $\Log{K} \Proves !A_1$, \dots, $\Log{K} \Proves !A_n$, and $!B$ follows from $!A_1$, \dots, $!A_n$ by propositional logic, then $\Log{K} \Proves !B$. \end{prop} \begin{proof} If $!B$ follows from $!A_1$, \dots,~$!A_n$ by propositional logic, then \[ !A_1 \lif (!A_2 \lif \cdots (!A_n \lif !B)\dots) \] is a tautological instance. Applying \MP{} $n$ times gives a !!{derivation} of~$!B$. \end{proof} We will indicate use of this proposition by~\PL. \begin{prop} If $\Log{K} \Proves !A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\dots)$ then $\Log{K} \Proves \Box !A_1 \lif (\Box !A_2 \lif \cdots (\Box !A_{n-1} \lif \Box !A_n)\dots)$. \end{prop} \begin{proof} By induction on $n$, just as in the proof of \olref[nor]{prop:rk}. \end{proof} We will indicate use of this proposition by~\RK. Let's illustrate how these results help establishing !!{derivability} results more easily. \begin{prop} $\Log{K} \Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$ \end{prop} \begin{proof} \begin{derivation} 1. & $\Log{K} \Proves !A \lif (!B \lif (!A \land !B))$ & \Taut \\ 2. & $\Log{K} \Proves \Box!A \lif (\Box !B \lif \Box(!A \land !B)))$ & \RK, 1\\ 3. & $\Log{K} \Proves (\Box!A \land \Box!B) \lif \Box(!A \land !B)$ & \PL, 2 \end{derivation} \end{proof} \begin{prop}\ollabel{prop:rewriting} If $\Log{K} \Proves !A \liff !B$ and $\Log{K} \Proves \Subst{!C}{!A}{q}$ then $\Log{K} \Proves \Subst{!C}{B}{q}$ \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[nml][prf][der]{prop:rewriting} by proving, by induction on the complexity of~$!C$, that if $\Log{K} \Proves !A \liff !B$ then $\Log{K} \Proves \Subst{!C}{!A}{q} \liff \Subst{!C}{!B}{q}$. \end{prob} This proposition comes in handy especially when we want to convert $\Diamond$ into $\Box$ (or vice versa), or remove double negations inside !!a{formula}. In what follows, we will mark applications of \olref{prop:rewriting} by ``$!A$ for $!B$'' whenever we re-write !!a{formula}~$!C(!B)$ for~$!C(!A)$. In other words, ``$!A$ for $!B$'' abbreviates: \begin{derivation} & $\Proves !C(!A)$ \\ & $\Proves !A \liff !B$\\ & $\Proves !C(!B)$ & by \olref{prop:rewriting} \end{derivation} For instance: \begin{prop} $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$ \end{prop} \begin{proof} \iftag{prvDiamond}{% Diamond is primitive \begin{derivation} 1. & $\Log{K} \Proves \Diamond \lnot p \liff \lnot\Box\lnot\lnot p$ & \Dual\\ 2. & $\Log{K} \Proves \lnot \Box \lnot\lnot p \lif \Diamond \lnot p$ & \PL, 1\\ 3. & $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$ & $p$ for $\lnot\lnot p$\\ \end{derivation} }{% Diamond is defined \begin{derivation} 1. & $\Log{K} \Proves \lnot \Box \lnot\lnot p \lif \Diamond \lnot p$ & \Taut\\ 2. & $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$ & $p$ for $\lnot\lnot p$\\ \end{derivation} The formula on line~$1$ is an instance of $\lnot q \lif \lnot q$, substituting $\Box\lnot\lnot p$ for~$q$. $\Diamond\lnot p$ and $\lnot\Box\lnot\lnot p$ are identical, since $\Diamond$ is defined as~$\lnot\Box\lnot$.} \end{proof} In the above !!{derivation}, the final step ``$p$ for $\lnot\lnot p$'' is short for \begin{derivation} & $\Log{K} \Proves \lnot \Box \lnot\lnot p \lif \Diamond \lnot p$\\ & $\Log{K} \Proves \lnot\lnot p \liff p$ & \Taut\\ & $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$ & by \olref{prop:rewriting} \end{derivation} The roles of $!C(q)$, $!A$, and $!B$ in \olref{prop:rewriting} are played here, respectively, by $\lnot \Box q \lif \Diamond \lnot p$, $\lnot\lnot p$, and~$p$. When !!a{formula} contains a sub-!!{formula} $\lnot\Diamond !A$, we can replace it by $\Box\lnot !A$ using \olref{prop:rewriting}, since $\Log{K} \Proves \lnot\Diamond !A \liff \Box\lnot !A$. We'll indicate this and similar replacements simply by ``$\Box\lnot$ for $\lnot\Diamond$.'' The following proposition justifies that we can establish !!{derivability} results schematically. E.g., the previous proposition does not just establish that $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$, but $\Log{K} \Proves \lnot\Box !A \lif \Diamond \lnot !A$ for arbitrary~$!A$. \begin{prop} If $!A$ is a substitution instance of $!B$ and $\Log{K} \Proves !B$, then $\Log{K} \Proves !A$. \end{prop} \begin{proof} It is tedious but routine to verify (by induction on the length of the !!{derivation} of~$!B$) that applying a substitution to an entire !!{derivation} also results in a correct !!{derivation}. Specifically, substitution instances of tautological instances are themselves tautological instances, substitution instances of instances of~\iftag{prvDiamond}{\Dual{} and~}{}\Ax{K} are themselves instances of~\iftag{prvDiamond}{\Dual{} and~}{}\Ax{K}, and applications of \MP{} and~\Nec{} remain correct when substituting !!{formula}s for !!{propositional variable}s in both premise(s) and conclusion. \end{proof} \end{document}

en · official · sha256:bba1814a3a5cb444cfeaa6c70203d71b1aec27f0335a6f4bd67fec935504933d

% Part: normal-modal-logic % Chapter: axioms-systems % Section: normal-logics \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{prf}{nor} \olsection{Normal Modal Logics} Not every set of modal !!{formula}s can easily be characterized as those !!{formula}s derivable from a set of axioms. We want modal logics to be well-behaved. First of all, everything we can !!{derive} in classical propositional logic should still be !!{derivable}, of course taking into account that the !!{formula}s may now contain also \iftag{prvBox}{$\Box$\iftag{prvDiamond}{ and~}{}}{}\iftag{prvDiamond}{$\Diamond$}{}. To this end, we require that a modal logic contain all tautological instances and be closed under modus ponens. \begin{defn} A \emph{modal logic} is a set~$\Sigma$ of modal !!{formula}s which \begin{enumerate} \item contains all tautologies, and \item is closed under substitution, i.e., if $!A \in \Sigma$, and $!D_1$, \dots, $!D_n$ are !!{formula}s, then \[ \SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \in \Sigma, \] \item is closed under \emph{modus ponens}, i.e., if $!A$ and $!A \lif !B \in \Sigma$, then $!B \in \Sigma$. \end{enumerate} \end{defn} In order to use the relational semantics for modal logics, we also have to require that all !!{formula}s valid in all modal models are included. It turns out that this requirement is met as soon as all instances of \Ax{K}\iftag{prvDiamond}{ and~\Dual{}}{} are !!{derivable}, and whenever !!a{formula}~$!A$ is !!{derivable}, so is~$\Box !A$. A modal logic that satisfies these conditions is called \emph{normal}. (Of course, there are also non-normal modal logics, but the usual relational models are not adequate for them.) \begin{defn} A modal logic $\Sigma$ is \emph{normal} if it contains \begin{align*} \tag{\Ax{K}} & \Box(p \lif q) \lif (\Box p \lif \Box q), \iftag{prvDiamond}{\\ \tag{\Dual} & \Diamond p \liff \lnot\Box\lnot p}{} \end{align*} and is closed under \emph{necessitation}, i.e., if $!A \in \Sigma$, then $\Box !A \in \Sigma$. \end{defn} Observe that while tautological implication is ``fine-grained'' enough to preserve \emph{truth at a world}, the rule \Nec{} only preserves \emph{truth in a model} (and hence also validity in a frame or in a class of frames). \begin{prop}\ollabel{prop:rk} Every normal modal logic is closed under rule \RK, \begin{prooftree} \AxiomC{$!A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\cdots)$} \RightLabel{\RK} \UnaryInfC{$\Box!A_1 \lif (\Box!A_2 \lif \cdots (\Box!A_{n-1} \lif \Box!A_n)\cdots).$} \end{prooftree} \end{prop} \begin{proof} By induction on~$n$: If $n = 1$, then the rule is just \Nec, and every normal modal logic is closed under \Nec. Now suppose the result holds for $n-1$; we show it holds for~$n$. Assume \begin{align*} & !A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\cdots) \in \Sigma \intertext{By the induction hypothesis, we have} & \Box!A_1 \lif (\Box!A_2 \lif \cdots \Box(!A_{n-1} \lif !A_n)\cdots) \in \Sigma \intertext{Since $\Sigma$ is a normal modal logic, it contains all instances of~$\Ax{K}$, in particular} & \Box(!A_{n-1} \lif !A_n) \lif (\Box!A_{n-1} \lif \Box!A_n) \in \Sigma \intertext{Using modus ponens and suitable tautological instances we get} & \Box!A_1 \lif (\Box!A_2 \lif \cdots (\Box!A_{n-1} \lif \Box!A_n)\cdots) \in \Sigma. \end{align*} \end{proof} \begin{prop}\ollabel{prop:notDiamondBot} Every normal modal logic $\Sigma$ contains~$\lnot\Diamond\lfalse$. \end{prop} \begin{prob} Prove \olref[nml][prf][nor]{prop:notDiamondBot}. \end{prob} \begin{prop} Let $!A_1$, \dots, $!A_n$ be !!{formula}s. Then there is a smallest modal logic $\Sigma$ containing all instances of $!A_1$, \dots, $!A_n$. \end{prop} \begin{proof} Given $!A_1$, \dots, $!A_n$, define $\Sigma$ as the intersection of all normal modal logics containing all instances of $!A_1$, \dots, $!A_n$. The intersection is non-empty as $\Frm[L]$, the set of all !!{formula}s, is such a modal logic. \end{proof} \begin{defn} The smallest normal modal logic containing $!A_1$, \dots, $!A_n$ is called a \emph{modal system} and denoted by $\Log{K} !A_1 \dots !A_n$. The smallest normal modal logic is denoted by~\Log{K}. \end{defn} \end{document}

Referencing norms: COND_NEC_THEOREM_ONLY, MODAL_CALCULUS, NECESSITATION, NORMAL_LOGIC, SYS_K, system_contains_schema

en · official · sha256:a08ed5d4407d11b68181f226b7cf4cda55fb86d5f44219ec43efaf7bc166a8ed

% Part: normal-modal-logic % Chapter: axioms-systems % Section: proofs-modal-systems \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{prf}{prs} \olsection{Proofs in Modal Systems} We now come to proofs in systems of modal logic other than~\Log{K}. \begin{prop}\ollabel{prop:S5facts} The following provability results obtain: \begin{enumerate} \item $\Log{KT5} \Proves \Ax{B}$; \item $\Log{KT5} \Proves \Ax{4}$; \item $\Log{KDB4} \Proves \Ax{T}$; \item $\Log{KB4} \Proves \Ax{5}$; \item $\Log{KB5} \Proves \Ax{4}$; \item \ollabel{prop:S5facts-KT-D}$\Log{KT} \Proves \Ax{D}$. \end{enumerate} \end{prop} \begin{proof} We exhibit proofs for each. \begin{enumerate} \item $\Log{KT5} \Proves \Ax{B}$: \begin{derivation} 1. & $\Log{KT5} \Proves \Diamond!A \lif \Box\Diamond!A$ & \Ax{5}\\ 2. & $\Log{KT5} \Proves !A \lif \Diamond!A$ & $\Ax{T_\Diamond}$\\ 3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL, 2, 1. \end{derivation} \item $\Log{KT5} \Proves \Ax{4}$: \begin{derivation} 1. &$\Log{KT5} \Proves \Diamond\Box!A \lif \Box\Diamond\Box!A$ & \Ax{5} with $\Box!A$ for $p$\\ 2. & $\Log{KT5} \Proves \Box!A \lif \Diamond\Box!A$ & $\Ax{T_\Diamond}$ with $\Box!A$ for $p$\\ 3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 2, 1\\ 4. & $\Log{KT5} \Proves \Diamond\Box!A \lif \Box!A$ & $\Ax{5_\Diamond}$\\ 5. & $\Log{KT5} \Proves \Box\Diamond\Box!A \lif \Box\Box!A$ & \RK{}, 4 \\ 6. & $\Log{KT5} \Proves \Box!A \lif \Box\Box!A$ & \PL, 3, 5. \\ \end{derivation} \item $\Log{KDB4} \Proves \Ax{T}$: \begin{derivation} 1. & $\Log{KDB4} \Proves \Diamond\Box!A \lif !A $ & $\Ax{B_\Diamond}$ \\ 2. & $\Log{KDB4} \Proves \Box\Box!A \lif \Diamond\Box!A$ & $\Ax{D}$ with $\Box!A$ for $p$\\ 3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL, 1, 2\\ 4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\ 5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 4, 3. \\ \end{derivation} \item $\Log{KB4} \Proves \Ax{5}$: \begin{derivation} 1. & $\Log{KB4} \Proves \Diamond!A \lif \Box \Diamond\Diamond!A$ & \Ax{B} with $\Diamond!A$ for $p$\\ 2. & $\Log{KB4} \Proves \Diamond\Diamond !A \lif \Diamond !A$ & $\Ax{4_\Diamond}$ \\ 3. & $\Log{KB4} \Proves \Box\Diamond\Diamond !A \lif \Box \Diamond!A$ & \RK{}, 2 \\ 4. & $\Log{KB4} \Proves \Diamond!A \lif \Box\Diamond!A$ & \PL, 1, 3. \end{derivation} \item $\Log{KB5} \Proves \Ax{4}$: \begin{derivation} 1. & $\Log{KB5} \Proves \Box!A \lif \Box\Diamond\Box !A$ & \Ax{B} with $\Box!A$ for $p$ \\ 2. & $\Log{KB5} \Proves \Diamond\Box!A \lif \Box !A$ & $\Ax{5_\Diamond}$\\ 3. & $\Log{KB5} \Proves \Box\Diamond\Box!A \lif \Box\Box !A$ & \RK{}, 2 \\ 4. & $\Log{KB5} \Proves \Box!A \lif \Box\Box!A$ & \PL, 1, 3. \end{derivation} \item $\Log{KT} \Proves \Ax{D}$: \begin{derivation} 1. & $\Log{KT} \Proves \Box !A \lif !A$ & \Ax{T} \\ 2. & $\Log{KT} \Proves !A \lif \Diamond!A$ & $\Ax{T_\Diamond}$ \\ 3. & $\Log{KT} \Proves \Box !A \lif \Diamond !A$ & \PL, 1, 2 \end{derivation} \end{enumerate} \end{proof} \begin{defn} Following tradition, we define \Log{S4} to be the system \Log{KT4}, and \Log{S5} the system \Log{KTB4}. \end{defn} The following proposition shows that the classical system \Log{S5} has several equivalent axiomatizations. This should not surprise, as the various combinations of axioms all characterize equivalence relations (see \olref[frd][es5]{prop:equivalences}). \begin{prop}\ollabel{prop:S5} $\Log{KTB4} = \Log{KT5} = \Log{KDB4} = \Log{KDB5}$. \end{prop} \begin{proof} Exercise. \end{proof} \begin{prob} Prove \olref[nml][prf][prs]{prop:S5}. \end{prob} \end{document}

Referencing norms: SYS_S4, SYS_S5

en · official · sha256:18bc62b6890453c84f6fe873b297644ddde91fd94c7981f132e97c2f2dce8603

% Part: normal-modal-logic % Chapter: axioms-systems % Section: systems-distinct \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{prf}{dis} \olsection{Showing Systems are Distinct} In \olref[prs]{sec} we saw how to prove that two systems of modal logic are in fact the same system. \olref[snd]{thm:soundness} allows us to show that two modal systems $\Sigma$ and $\Sigma'$ are distinct, by finding !!a{formula}~$!A$ such that $\Sigma' \Proves !A$ that fails in a model of~$\Sigma$. \begin{prop} $\Log{KD} \subsetneq \Log{KT}$ \end{prop} \begin{proof} This is the syntactic counterpart to the semantic fact that all reflexive relations are serial. To show $\Log{KD} \subseteq \Log{KT}$ we need to see that $\Log{KD} \Proves !B$ implies $\Log{KT} \Proves !B$, which follows from $\Log{KT} \Proves \Log{D}$, as shown in \olref[prs]{prop:S5facts}\olref[prs]{prop:S5facts-KT-D}. To show that the inclusion is proper, by Soundness (\olref[snd]{thm:soundness}), it suffices to exhibit a model of \Log{KD} where \Ax{T}, i.e., $\Box p \lif p$, fails (an easy task left as an exercise), for then by Soundness $\Log{KD} \Proves/ \Box p \lif p$. \end{proof} \begin{prop} $\Log{KB} \neq \Log{K4}$. \end{prop} \begin{proof} We construct a symmetric model where some instance of \Ax{4} fails; since obviously the instance is !!{derivable} for \Log{K4} but not in \Log{KB}, it will follow $\Log{K4} \nsubseteq \Log{KB}$. Consider the symmetric model $\mModel{M}$ of \olref{fig:Bnot4}. Since the model is symmetric, \Ax{K} and~\Ax{B} are true in~$\mModel{M}$ (by \olref[syn][sch]{prop:Kvalid} and \olref[frd][acc]{thm:soundschemas}, respectively). However, $\mSat/{M}{\Box p \lif \Box\Box p}[w_1]$. \end{proof} \begin{figure}[htpb] \centering \begin{tikzpicture}[modal] \node[world] (w1) [label=above:\mFalse{p}, label={below:$\mSat{{}}{\Box p}$\\ $\mSat/{{}}{\Box\Box p}$}] {$w_1$}; \node[world] (w2) [label=above:\mTrue{p}, label=below:$\mSat/{{}}{\Box p}$, right=of w1]{$w_2$}; \draw[->, bend left] (w1) to (w2); \draw[->, bend left] (w2) to (w1); \end{tikzpicture} \caption{A symmetric model falsifying an instance of \Ax{4}.} \ollabel{fig:Bnot4} \end{figure} \begin{thm}\ollabel{thm:KTBnot45} $\Log{KTB} \Proves/ \Log{4}$ and $\Log{KTB} \Proves/ \Log{5}$. \end{thm} \begin{proof} By \olref[frd][acc]{thm:soundschemas} we know that all instances of \Ax{T} and \Ax{B} are true in every reflexive symmetric model (respectively). So by soundness, it suffices to find a reflexive symmetric model containing a world at which some instance of~\Ax{4} fails, and similarly for~\Ax{5}. We use the same model for both claims. Consider the symmetric, reflexive model in \olref{fig:KTBnot45}. Then $\mSat/{M}{\Box p \to \Box \Box p}[w_1]$, so \Ax{4} fails at $w_1$. Similarly, $\mSat/{M}{\Diamond \lnot p \lif \Box \Diamond \lnot p}[w_2]$, so the instance of~\Ax{5} with $!A = \lnot p$ fails at~$w_2$. \end{proof} \begin{figure}[htpb] \centering \begin{tikzpicture}[modal] \node[world] (w1) [label={right:\mTrue{p}}, label={below: $\mSat{{}}{\Box p}$\\ $\mSat/{{}}{\Box\Box p}$\\ $\mSat/{{}}{\Diamond\lnot p}$}] {$w_1$}; \draw[reflexive above] (w1) to (w1); \node[world] (w2) [label={right:\mTrue{p}}, label={below: $\mSat{{}}{\Diamond\lnot p}$\\ $\mSat/{{}}{\Box\Diamond\lnot p}$}, right=of w1] {$w_2$} ; \draw[reflexive above] (w2) to (w2); \node[world] (w3) [label={right:\mFalse{p}},right=of w2] {$w_3$}; \draw[reflexive above] (w3) to (w3); \draw[->, bend left] (w1) to (w2); \draw[->, bend left] (w2) to (w3); \draw[->, bend left] (w3) to (w2); \draw[->, bend left] (w2) to (w1); \end{tikzpicture} \caption{The model for \olref{thm:KTBnot45}.} \ollabel{fig:KTBnot45} \end{figure} \begin{thm}\ollabel{thm:KD5not4} $\Log{KD5} \neq \Log{KT4} = \Log{S4}$. \end{thm} \begin{proof} By \olref[frd][acc]{thm:soundschemas} we know that all instances of \Ax{D} and~\Ax{5} are true in all serial euclidean models. So it suffices to find a serial euclidean model containing a world at which some instance of~\Ax{4} fails. Consider the model of \olref{fig:KD5not4}, and notice that $\mSat/{M}{\Box p \lif \Box\Box p}[w_1]$. \end{proof} \begin{figure}[t] \centering \begin{tikzpicture}[modal] \node[world] (w2) [label=north west:\mTrue{p}]{$w_2$} ; \draw[reflexive left] (w2) to (w2); \node[world] (w1) [label=right:\mFalse{p}, label=below:{$\mSat{{}}{\Box p}, \mSat/{{}}{\Box\Box p}$}, below right=of w2]{$w_1$}; \node[world] (w3) [label=north east:\mTrue{p}, above right=of w1]{$w_3$} ; \draw[reflexive right] (w3) to (w3); \node[world] (w4) [label=right:\mFalse{p},above right=of w2]{$w_4$}; \draw[reflexive above] (w4) to (w4); \draw[->] (w1) to (w2); \draw[->] (w1) to (w3); \draw[->, bend left=15] (w2) to (w3); \draw[->, bend left=15] (w3) to (w2); \draw[->, bend left=15] (w2) to (w4); \draw[->, bend left=15] (w4) to (w2); \draw[->, bend left=15] (w3) to (w4); \draw[->, bend left=15] (w4) to (w3); \end{tikzpicture} \caption{The model for \olref{thm:KD5not4}.} \ollabel{fig:KD5not4} \end{figure} \begin{prob} Give an alternative proof of \olref[nml][prf][dis]{thm:KD5not4} using a model with $3$ worlds. \end{prob} \begin{prob} Provide a single reflexive transitive model showing that both $\Log{KT4} \Proves/ \Ax{B}$ and $\Log{KT4} \Proves/ \Ax{5}$. \end{prob} \end{document}

Referencing norms: PublishedAlias, SYS_T, published_alias, system_alias

en · official · sha256:055c6ccb889402f6c21941adf8e0d35831092b0ad7df1e8ffcbda5c0861fc267

% Part: normal-modal-logic % Chapter: completeness % Section: frame-completeness \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{com}{fra} \olsection{Frame Completeness} The completeness theorem for \Log{K} can be extended to other modal systems, once we show that the canonical model for a given logic has the corresponding frame property. \begin{thm}\ollabel{thm:completeframeprops} If a normal modal logic $\Sigma$ contains one of the !!{formula}s on the left-hand side of \olref{tab:correspondencetable}, then the canonical model for~$\Sigma$ has the corresponding property on the right-hand side. \end{thm} \begin{table}[htp] \centering \begin{tabular}{| l || l |} \hline \emph{If $\Sigma$ contains \dots} & \emph{\dots the canonical model for $\Sigma$ is:} \\ \hline \hline \Ax{D}:\;\; $\Box!A \lif \Diamond !A$ & \quad serial; \\ \hline \Ax{T}:\;\; $\Box!A \lif !A$ &\quad reflexive;\\ \hline \Ax{B}: \;\;$!A \lif \Box\Diamond!A$ &\quad symmetric; \\ \hline \Ax{4}: \;\; $\Box!A \lif \Box\Box!A$ & \quad transitive; \\ \hline \Ax{5}: \;\; $\Diamond !A \lif \Box\Diamond!A$& \quad euclidean.\\ \hline \end{tabular} \caption{Basic correspondence facts.} \ollabel{tab:correspondencetable} \end{table} \begin{proof} We take each of these up in turn. Suppose $\Sigma$ contains \Ax{D}, and let $\Delta \in W^\Sigma$; we need to show that there is a $\Delta'$ such that $R^\Sigma \Delta\Delta'$. It suffices to show that $\Box^{-1}\Delta$ is $\Sigma$-consistent, for then by Lindenbaum's Lemma, there is a complete $\Sigma$-consistent set $\Delta' \supseteq \Box^{-1}\Delta$, and by definition of $R^\Sigma$ \iftag{prvBox}{}{and \olref[mod]{lem:box-iff-diamond} }we have $R^\Sigma \Delta\Delta'$. So, suppose for contradiction that $\Box^{-1}\Delta$ is \emph{not} $\Sigma$-consistent, i.e., $\Box^{-1}\Delta \Proves[\Sigma] \lfalse$. By \olref[mod]{lem:box2}, $\Delta \Proves[\Sigma] \Box\lfalse$, and since $\Sigma$ contains \Ax{D}, also $\Delta \Proves[\Sigma] \Diamond\lfalse$. But $\Sigma$ is normal, so $\Sigma \Proves \lnot\Diamond \lfalse$ (\olref[prf][nor]{prop:notDiamondBot}), whence also $\Delta \Proves[\Sigma] \lnot\Diamond \lfalse$, against the consistency of~$\Delta$. Now suppose $\Sigma$ contains \Ax{T}, and let $\Delta \in W^\Sigma$. We want to show $R^\Sigma \Delta\Delta$, i.e.,\iftag{prvBox}{}{ by \olref[mod]{lem:box-iff-diamond},} $\Box^{-1}\Delta \subseteq \Delta$. But if $\Box!A \in \Delta$ then by \Ax{T} also $!A \in \Delta$, as desired. Now suppose $\Sigma$ contains \Ax{B}, and suppose $R^\Sigma \Delta\Delta'$ for $\Delta$, $\Delta' \in W^\Sigma$. We need to show that $R^\Sigma \Delta'\Delta$, i.e.,\iftag{prvBox}{ $\Box^{-1}\Delta' \subseteq \Delta$. By \olref[mod]{lem:box-iff-diamond}, this is equivalent to}{} $\Diamond\Delta \subseteq \Delta'$. So suppose $!A \in \Delta$. By \Ax{B}, also $\Box\Diamond!A \in \Delta$. By the hypothesis that $R^\Sigma \Delta\Delta'$\iftag{prvBox}{}{ and \olref[mod]{lem:box-iff-diamond}}, we have that $\Box^{-1}\Delta \subseteq \Delta'$, and hence $\Diamond!A \in \Delta'$, as required. Now suppose $\Sigma$ contains \Ax{4}, and suppose $R^\Sigma \Delta_1\Delta_2$ and $R^\Sigma \Delta_2\Delta_3$. We need to show $R^\Sigma \Delta_1\Delta_3$. From the hypothesis\iftag{prvBox}{}{ and \olref[mod]{lem:box-iff-diamond}} we have both $\Box^{-1}\Delta_1 \subseteq \Delta_2$ and $\Box^{-1}\Delta_2 \subseteq \Delta_3$. In order to show $R^\Sigma \Delta_1\Delta_3$ it suffices to show $\Box^{-1}\Delta_1 \subseteq \Delta_3$. So let $!B \in \Box^{-1}\Delta_1$, i.e., $\Box!B \in \Delta_1$. By \Ax{4}, also $\Box\Box!B \in \Delta_1$ and by hypothesis we get, first, that $\Box!B \in \Delta_2$ and, second, that $!B \in \Delta_3$, as desired. Now suppose $\Sigma$ contains \Ax{5}, suppose $R^\Sigma \Delta_1\Delta_2$ and $R^\Sigma \Delta_1\Delta_3$. We need to show $R^\Sigma \Delta_2\Delta_3$. The first hypothesis gives $\Box^{-1}\Delta_1 \subseteq \Delta_2$\iftag{prvBox}{}{ by \olref[mod]{lem:box-iff-diamond}}, and the second hypothesis is equivalent to $\Diamond\Delta_3 \subseteq \Delta_1$\iftag{prvBox}{, by \olref[mod]{lem:box-iff-diamond}}{}. To show $R^\Sigma \Delta_2\Delta_3$\iftag{prvBox}{, by \olref[mod]{lem:box-iff-diamond}, it suffices to}{ we have to} show $\Diamond\Delta_3 \subseteq \Delta_2$. So let $\Diamond!A \in \Diamond\Delta_3$, i.e., $!A \in \Delta_3$. By the second hypothesis $\Diamond!A \in \Delta_1$ and by \Ax{5}, $\Box\Diamond!A \in \Delta_1$ as well. But now the first hypothesis gives $\Diamond!A \in \Delta_2$, as desired. \end{proof} As a corollary we obtain completeness results for a number of systems. For instance, we know that $\Log{S5} = \Log{KT5} = \Log{KTB4}$ is complete with respect to the class of all reflexive euclidean models, which is the same as the class of all reflexive, symmetric and transitive models. \begin{thm}\ollabel{thm:generaldet} Let $\mClass{C}_\Ax{D}$, $\mClass{C}_\Ax{T}$, $\mClass{C}_\Ax{B}$, $\mClass{C}_\Ax{4}$, and $\mClass{C}_\Ax{5}$ be the class of all serial, reflexive, symmetric, transitive, and euclidean models (respectively). Then for any schemas $!A_1$, \dots, $!A_n$ among \Ax{D}, \Ax{T}, \Ax{B}, \Ax{4}, and \Ax{5}, the system $\Log{K}!A_1 \dots !A_n$ is determined by the class of models $\mClass{C} = \mClass{C}_{!A_1} \cap \dots \cap \mClass{C}_{!A_n}$. \end{thm} \begin{prop} Let $\Sigma$ be a normal modal logic; then: \begin{enumerate} \item\ollabel{prop:anotherfive-a}% If $\Sigma$ contains the schema $\Diamond!A \lif \Box !A$ then the canonical model for $\Sigma$ is partially functional. \item If $\Sigma$ contains the schema $\Diamond!A \liff \Box !A$ then the canonical model for $\Sigma$ is functional. \item If $\Sigma$ contains the schema $\Box\Box!A \lif \Box !A$ then the canonical model for $\Sigma$ is weakly dense. \end{enumerate} (see \olref[frd][acc]{tab:anotherfive} for definitions of these frame properties). \end{prop} \begin{proof} \begin{enumerate} \item Suppose that $\Sigma$ contains the schema $\Diamond !A \lif \Box !A$, to show that $R^\Sigma$ is partially functional we need to prove that for any $\Delta_1$, $\Delta_2$, $\Delta_3 \in W^\Sigma$, if $R^\Sigma \Delta_1\Delta_2$ and $R^\Sigma \Delta_1\Delta_3$ then $\Delta_2=\Delta_3$. Since $R^\Sigma \Delta_1\Delta_2$ we have $\Box^{-1}\Delta_1 \subseteq \Delta_2$ and since $R^\Sigma \Delta_1\Delta_3$ also $\Box^{-1}\Delta_1 \subseteq \Delta_3$\iftag{prvBox}{}{, both by \olref[mod]{lem:box-iff-diamond}}. The identity $\Delta_2=\Delta_3$ will follow if we can establish the two inclusions $\Delta_2 \subseteq \Delta_3$ and $\Delta_3 \subseteq \Delta_2$. For the first inclusion, let $!A \in \Delta_2$; then $\Diamond!A \in \Delta_1$, and by the schema and deductive closure of $\Delta_1$ also $\Box!A \in \Delta_1$, whence by the hypothesis that $R^\Sigma \Delta_1\Delta_3$, $!A \in \Delta_3$. The second inclusion is similar. \item This follows immediately from part~\olref{prop:anotherfive-a} and the seriality proof in \olref{thm:completeframeprops}. \item Suppose $\Sigma$ contains the schema $\Box\Box!A \lif \Box!A$ and to show that $R^\Sigma$ is weakly dense, let $R^\Sigma \Delta_1\Delta_2$. We need to show that there is a complete $\Sigma$-consistent set $\Delta_3$ such that $R^\Sigma \Delta_1\Delta_3$ and $R^\Sigma \Delta_3\Delta_2$. Let: \[ \Gamma = \Box^{-1}\Delta_1 \cup \Diamond\Delta_2. \] It suffices to show that $\Gamma$ is $\Sigma$-consistent, for then by Lindenbaum's Lemma it can be extended to a complete $\Sigma$-consistent set~$\Delta_3$ such that $\Box^{-1}\Delta_1 \subseteq \Delta_3$ and $\Diamond\Delta_2 \subseteq \Delta_3$, i.e., $R^\Sigma \Delta_1\Delta_3$\iftag{prvBox}{}{ (by \olref[mod]{lem:box-iff-diamond})} and $R^\Sigma \Delta_3\Delta_2$\iftag{prvBox}{ (by \olref[mod]{lem:box-iff-diamond})}{}. Suppose for contradiction that $\Gamma$ is not consistent. Then there are !!{formula}s $\Box!A_1$, \dots, $\Box!A_n \in \Delta_1$ and $!B_1$, \dots,~$!B_m \in \Delta_2$ such that \[!A_1, \dots, !A_n, \Diamond!B_1, \dots, \Diamond!B_m \Proves[\Sigma] \lfalse.\] Since $\Diamond (!B_1 \land \dots \land !B_m) \to (\Diamond!B_1 \land \dots \land \Diamond!B_m)$ is !!{derivable} in every normal modal logic, we argue as follows, contradicting the consistency of~$\Delta_2$: \begin{align*} !A_1, \dots, !A_n, & \Diamond!B_1, \dots, \Diamond!B_m \Proves[\Sigma] \lfalse \\ !A_1, \dots,!A_n & \Proves[\Sigma] (\Diamond!B_1 \land \dots \land \Diamond!B_m) \lif \lfalse\\ & \qquad\text{by the deduction theorem}\\ & \qquad\text{\olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-deduction}, and \Taut} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \Diamond(!B_1 \land \dots \land !B_m) \lif \lfalse\\ & \qquad \text{since $\Sigma$ is normal} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \lnot\Diamond (!B_1 \land \dots \land !B_m)\\ & \qquad\text{by \PL} \\ !A_1, \dots,!A_n & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ & \qquad\text{$\Box\lnot$ for $\lnot\Diamond$} \\ \Box!A_1, \dots,\Box!A_n & \Proves[\Sigma] \Box\Box \lnot (!B_1 \land \dots \land !B_m)\\ & \qquad\text{by \olref[mod]{lem:box1}} \\ \Box!A_1, \dots,\Box!A_n & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ &\qquad\text{by schema $\Box\Box!A \lif \Box!A$} \\ \Delta_1 & \Proves[\Sigma] \Box\lnot (!B_1 \land \dots \land !B_m)\\ &\qquad\text{by monotonicity, \olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-monotonicity}} \\ & \Box\lnot (!B_1 \land \dots \land !B_m) \in \Delta_1\\ &\qquad\text{by deductive closure}; \\ & \lnot (!B_1 \land \dots \land !B_m) \in \Delta_2\\ &\qquad \text{since } R^\Sigma \Delta_1\Delta_2. \end{align*} \end{enumerate} \end{proof} On the strength of these examples, one might think that every system~$\Sigma$ of modal logic is \emph{complete}, in the sense that it proves every formula which is valid in every frame in which every theorem of $\Sigma$ is valid. Unfortunately, there are many systems that are not complete in this sense. \end{document}

en · official · sha256:570f058139f28b61158a6ff51e4e3afd80822632726cdc17fee753a261fa0413

% 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 the properties considered in \olref[acc]{thm:soundschemas}, it \emph{is} true that if !!a{formula} is valid in a \emph{frame} then the accessibility relation of that frame has the corresponding property. So, the !!{formula}s considered \emph{define} the classes of frames 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 only frames~$\mModel{F} \in \mClass{F}$. \end{defn} We now proceed to establish the full definability results for frames. \begin{thm}\ollabel{thm:fullCorrespondence} If the !!{formula} on the right side of \olref[acc]{tab:five} is valid in a frame~$\mModel{F}$, then $\mModel{F}$ has the property on the left side. \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 \in W$. We have to show that there is a $v$ such that~$Rwv$. Suppose not: 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 \Box p \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 other than $p$, $V(q)$ is arbitrary, say $V(q) = \emptyset)$. Let $\mModel{M} = \tuple{W, R, V}$. By construction, for all $u$ such that $Rwu$: $\mSat{M}{p}[u]$, and hence $\mSat{M}{\Box p}[w]$. But by hypothesis $\Box p \lif p$ is true at~$w$, so that $\mSat{M}{p}[w]$, but by definition of $V$ this is possible only if~$Rww$. \item We prove the contrapositive: Suppose $\mModel{F}$ is not symmetric, we show that \Ax{B}, i.e., $p \lif \Box\Diamond p$ is not valid in $\mModel{F}= \tuple{W, R}$. If $\mModel{F}$ is not symmetric, 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]$ since not~$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 valid in~$\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$ be arbitrary 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}$. By definition 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 \Box p}[u]$. Since $Ruv$ and $Rvw$, we have $\mSat{M}{p}[w]$, but by definition 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 it falsifies~\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 for all worlds $z$, $z \in V(p)$ if and only if it is \emph{not} the case that~$Ruz$. Let $\mModel{M} =\tuple{W, R, V}$. Then by hypothesis $\mSat{M}{p}[v]$ and since $Rwv$ also $\mSat{M}{\Diamond p}[w]$. However, there is no world $y$ such that $Ruy$ and $\mSat{M}{p}[y]$ so $\mSat/{M}{\Diamond p}[u]$. Since $Rwu$, it follows that $\mSat/{M}{\Box\Diamond p}[w]$, so that \Ax{5}, $\Diamond p \lif \Box\Diamond p$, fails at~$w$. \end{enumerate} \end{proof} You'll notice a difference between the proof for \Ax{D} and the other cases: no mention was made of the valuation~$V$. In effect, we proved that 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} defines the 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 the property on the left, the !!{formula} on the right is true in it. 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 a frame that does \emph{not} satisfy the property on the left, and define a suitable~$V$ such that the !!{formula} on the right is false at some world. \end{prob} \olref{thm:fullCorrespondence} also shows that the properties can be combined: for instance if both \Ax{B} and \Ax{4} are valid in~$\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 in all 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., in all those where both \Ax{T} and~\Ax{4} are valid. \Log{S5} is the set of all formulas valid in all reflexive, symmetric, and euclidean frames, i.e., all those where all of \Ax{T}, \Ax{B}, and \Ax{5} are valid. Logical relationships between properties of $R$ in general correspond to relationships between the corresponding defining !!{formula}s. For instance, 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 such relationships. \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 it is 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}

en · official · sha256:04ea39c27bf689d5b9609cfcc19997c3b36ac873b469a9ebb593fda8123e08e5

% 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}s valid on all universal frames, i.e., every world is accessible from every world, including itself. In such a scenario, $\Box$ corresponds to necessity and $\Diamond$ to possibility: $\Box !A$ is true if $!A$ is true at \emph{every} world, and $\Diamond !A$ is true if $!A$ is true at \emph{some} world. It turns out that \Log{S5} can also be characterized 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} if and 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 \in W$. \end{defn} Since \Ax{T}, \Ax{B}, and \Ax{4} characterize the reflexive, symmetric, and transitive frames, the frames where the accessibility relation is an equivalence relation are exactly those in which all three !!{formula}s are valid. It turns out that the equivalence relations can also be characterized by other combinations of !!{formula}s, since the conditions with which we've defined equivalence relations are equivalent to combinations of other familiar conditions 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 are equivalent. \end{prob} \olref{prop:equivalences} is the semantic counterpart to \olref[prf][prs]{prop:S5}, in that it gives an equivalent characterization of the modal logic of frames over which $R$ is an equivalence relation (the logic traditionally referred to as \Log{S5}). What is the relationship between universal and equivalence relations? Although every universal relation is an equivalence relation, clearly not every equivalence relation is universal. However, the !!{formula}s valid on all universal relations are exactly the same as those valid on all equivalence relations. \begin{prop} Let $R$ be an equivalence relation, and for each $w \in W$ define the \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 mutually exclusive 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 in all 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 an equivalence. Hence, if $!A$ is valid in all frames where $R$ is an equivalence it is valid in all universal frames. For the other direction, 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 the shaded area in \olref{fig:partition}.) It is easy to see that $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 and only if $\mSat{M}{!A}[w']$ for each $!A$ (this makes sense since $W' \subseteq W$). In particular, $\mSat/{M'}{!B}[w]$, and $!B$ fails in a 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}

en · official · sha256:c5ec6f91afe146697bb08ca6312ff22228c5b3fe87843c247df27b20c2a08446

% 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 a non-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}$ for every 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 between schemas and properties of the accessibility relation~$R$ is at the level of frames, \emph{not of models}. For instance, although \Ax{T} is true in all reflexive models, not every model in which \Ax{T} is true is reflexive. However, it \emph{is} true that not only is \Ax{T} \emph{valid} on all reflexive \emph{frames}, also every frame in which \Ax{T} is valid is reflexive. \begin{rem} Validity in a class of frames is a special case of the notion of validity in a class of models: $\mClass{F} \Entails !A$ iff $\mClass{C} \Entails !A$ where $\mClass{C}$ is the class of all models based on a frame in~$\mClass{F}$. Obviously, if !!a{formula} or a schema is valid, i.e., valid with respect to the class of \emph{all} models, it is also valid with respect to any class~$\mClass{F}$ of frames. \end{rem} \end{document}

Referencing norms: FRAME

en · official · sha256:7e379d018c0cfac076de8e15ad1122f37f3b10a1eb46940ba129b6cc7bc2a5bb

% 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, and even familiar, properties of the accessibility relation. In one direction, that means that any model that has a given property makes a corresponding !!{formula} (and all its substitution instances) true. We begin with five classical examples of kinds of accessibility relations and the formulas the truth of which they guarantee. \begin{thm}\ollabel{thm:soundschemas} Let $\mModel{M} = \tuple{W, R, V}$ be a model. If $R$ has the property 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 a model we need to show that all of its instances are true at all worlds in the model. So let $!A \lif \Box\Diamond !A$ be a given instance of \Ax{B}, and let $w \in W$ be an arbitrary world. Suppose the antecedent $!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 at all $w'$ accessible from $w$. Now, for any $w'$ such that $Rww'$ we have, 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 such that $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} do not hold: it's not true that if a model verifies a schema, then the accessibility relation of that model has the corresponding property. In the case of \Ax{T} and reflexive models, it is easy to give an example of a model in which \Ax{T} itself fails: let $W = \{w\}$ and $V(p) = \emptyset$. Then $R$ is not reflexive, but $\mSat{M}{\Box p}[w]$ and $\mSat/{M}{p}[w]$. But here we have just a single instance 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 examples where \emph{every substitution instance} of~\Ax{T} is true in~$\mModel{M}$ and $\mModel{M}$ is not reflexive. But there are such models, 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 for some---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 accessibility relations. The accessibility relation~$R$ is partially functional, if from every world at most one world is accessible. If it is the case that from every world exactly one world is accessible, we call it functional. (Thus the functional relations are precisely those that are both serial and partially functional). They are called ``functional'' because the accessibility relation operates like a (partial) function. A relation is weakly dense if whenever $Ruv$, there is a~$w$ ``between'' $u$ and~$v$. So weakly dense relations are in a sense the opposite of transitive relations: in a transitive relation, whenever you can reach $v$ from~$u$ by a detour via~$w$, you can reach $v$ from $u$ directly; in a weakly dense relation, whenever you can reach $v$ from~$u$ directly, you can also reach it by a detour via some~$w$. A relation is weakly directed if whenever you can reach worlds $u$ and~$v$ from some world~$w$, you can reach a single world~$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 the corresponding right-hand formula is true in~$\mModel{M}$. \end{prob} \end{document}

Referencing norms: AX_4, AX_5, AX_B, AX_D, AX_T, OneWayCorrespondence, S_4, S_4_ANTE, S_4_ANTE_A, S_4_CONS, S_4_CONS_A, S_4_CONS_IN, S_T, S_T_A, S_T_BOX, S_T_BOX_A, SystemFrameCondition, V_4_A, V_T_A, correspondence_direction, frame_condition, one_way_correspondence, system_frame_condition

en · official · sha256:1a73e087507d26665457df05efea6e2def1eb8ebfef8b94a333899ebfef0b401

% Part: normal-modal-logic % Chapter: syntax-and-semantics % Section: language-modal-logic \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{syn}{lan} \olsection{The Language of Basic Modal Logic} \begin{defn} The basic language of modal logic contains \begin{enumerate} \tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{} \tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{} \item A !!{denumerable}s set of !!{propositional variable}s: $\Obj p_0$, $\Obj p_1$, $\Obj p_2$, \dots \item The propositional connectives: \startycommalist \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}% \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}% \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}% \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}% \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}. \tagitem{prvBox}{The modal operator $\Box$.}{} \tagitem{prvDiamond}{The modal operator $\Diamond$.}{} \end{enumerate} \end{defn} \begin{defn} \emph{!!^{formula}s} of the basic modal language are inductively defined as follows: \begin{enumerate} \tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{} \tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{} \item Every !!{propositional variable} $\Obj p_i$ is an (atomic) !!{formula}. \tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is !!a{formula}.}{} \tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land !B)$ is !!a{formula}.}{} \tagitem{prvOr}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$ is !!a{formula}.}{} \tagitem{prvIf}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$ is !!a{formula}.}{} \tagitem{prvIff}{If $!A$ and $!B$ are !!{formula}s, then $(!A \liff !B)$ is !!a{formula}.}{} \tagitem{prvBox}{If $!A$ is !!a{formula}, then $\Box !A$ is !!a{formula}.}{} \tagitem{prvDiamond}{If $!A$ is !!a{formula}, then $\Diamond !A$ is !!a{formula}.}{} \tagitem{limitClause}{Nothing else is !!a{formula}.}{} \end{enumerate} \end{defn} \begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defBox,defDiamond} \begin{defn} Formulas constructed using the defined operators are to be understood as follows: \begin{tagenumerate}{defTrue,defFalse,defNot,defOr,defAnd,defIf,defIff,defBox,defDiamond} \tagitem{defTrue}{$\ltrue$ abbreviates \iftag{prvFalse}{$\lnot\lfalse$}{$(!A \lor \lnot !A)$ for some fixed atomic !!{formula}~$!A$}.}{} \tagitem{defFalse}{$\lfalse$ abbreviates \iftag{prvTrue}{$\lnot\ltrue$}{$(!A \land \lnot !A)$ for some fixed atomic !!{formula}~$!A$}.}{} \tagitem{defNot}{$\lnot !A$ abbreviates $!A \lif \lfalse$.}{} \tagitem{defOr}{$!A \lor !B$ abbreviates \iftag{prvAnd}{$\lnot(\lnot !A \land \lnot !B)$}{$\lnot !A \lif !B$}.}{} \tagitem{defAnd}{$!A \land !B$ abbreviates \iftag{prvOr}{$\lnot(\lnot !A \lor \lnot !B)$}{$\lnot (!A \lif \lnot !B)$}.}{} \tagitem{defIf}{$!A \lif !B$ abbreviates \iftag{prvOr}{$\lnot !A \lor !B)$}{$\lnot (!A \land \lnot !B)$}.}{} \tagitem{defIff}{$!A \liff !B$ abbreviates $(!A \lif !B) \land (!B \lif !A)$.}{} \tagitem{defBox}{$\Box !A$ abbreviates $\lnot\Diamond\lnot !A$. }{} \tagitem{defDiamond}{$\Diamond !A$ abbreviates $\lnot\Box\lnot !A$.}{} \end{tagenumerate} \end{defn} \end{tagblock} If !!a{formula}~$!A$ does not contain $\Box$ or $\Diamond$, we say it is \emph{modal-free}. \end{document}

Referencing norms: BOX, DIAMOND, L_MODAL

en · official · sha256:e4d976bf686c1d285389dc8df112ff034f6293e33d80e32b98eac135aa41c84e

% Part: normal-modal-logic % Chapter: syntax-and-semantics % Section: modal-validity \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{syn}{val} \olsection{Validity} \begin{explain} !!^{formula}s that are true in all models, i.e., true at every world in every model, are particularly interesting. They represent those modal propositions which are true regardless of how $\Box$ and $\Diamond$ are interpreted, as long as the interpretation is ``normal'' in the sense that it is generated by some accessibility relation on possible worlds. We call such !!{formula}s \emph{valid}. For instance, $\Box(p \land q) \lif \Box p$ is valid. Some !!{formula}s one might expect to be valid on the basis of the alethic interpretation of $\Box$, such as $\Box p \lif p$, are not valid, however. Part of the interest of relational models is that different interpretations of $\Box$ and $\Diamond$ can be captured by different kinds of accessibility relations. This suggests that we should define validity not just relative to \emph{all} models, but relative to all models \emph{of a certain kind}. It will turn out, e.g., that $\Box p \lif p$ is true in all models where every world is accessible from itself, i.e., $R$ is reflexive. Defining validity relative to classes of models enables us to formulate this succinctly: $\Box p \lif p$ is valid in the class of reflexive models. \end{explain} \begin{defn} !!^a{formula}~$!A$ is \emph{valid} in a class $\mClass{C}$ of models if it is true in every model in~$\mClass{C}$ (i.e., true at every world in every model in~$\mClass{C}$). If $!A$ is valid in~$\mClass{C}$, we write $\mClass{C} \Entails !A$, and we write $\Entails !A$ if $!A$ is valid in the class of \emph{all} models. \end{defn} \begin{prop}\ollabel{prop:subset-class} If $!A$ is valid in $\mClass{C}$ it is also valid in each class $\mClass{C}' \subseteq \mClass{C}$. \end{prop} \begin{prop}\ollabel{prop:Nec-rule} If $!A$ is valid, then so is $\Box!A$. \end{prop} \begin{proof} Assume $\Entails !A$. To show $\Entails \Box!A$ let $\mModel{M} = \tuple{W, R, V}$ be a model and $w \in W$. If $Rww'$ then $\mSat{M}{!A}[w']$, since $!A$ is valid, and so also $\mSat{M}{\Box!A}[w]$. Since $\mModel{M}$ and $w$ were arbitrary, $\Entails \Box!A$. \end{proof} \begin{prob} Show that the following are valid: \begin{enumerate} \item $\Box p \lif \Box (q \lif p)$; \item $\Box \lnot \lfalse$; \item $\Box p \lif (\Box q \lif \Box p)$. \end{enumerate} \end{prob} \begin{prob} Show that $!A \lif \Box!A$ is valid in the class $\mClass{C}$ of models $\mModel{M} = \tuple{W, R, V}$ where $W = \{w\}$. Similarly, show that $!B \lif \Box !A$ and $\Diamond !A \lif !B$ are valid in the class of models $\mModel{M} = \tuple{W, R, V}$ where $R = \emptyset$. \end{prob} \end{document}

Referencing norms: TRUTH_IN_MODEL

en · official · sha256:81154ca7f8e3c253200d2b611cb3884e37af60293a8fdfdf95fab168101c2e20

% Part: normal-modal-logic % Chapter: syntax-and-semantics % Section: normal-modal-logics \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{syn}{nor} \olsection{Normal Modal Logics} A modal logic can be seen as any suitably well-behaved set of !!{formula}s. There are some modal logics which are of particular interest, both because they have interesting interpretations and applications, but mainly because they are theoretically well understood. Those are the so-called normal modal logics. \begin{defn}\ollabel{defn:modal-logic} A \emph{modal logic}~$\Log L$ is a set of !!{formula}s of the basic modal language which \begin{enumerate} \item contains all propositional tautologies, \item is closed under uniform substitution, and \item is closed under modus ponens, i.e., whenever $!A$ and $(!A \lif !B) \in \Log L$ then also $!B \in \Log L$. \end{enumerate} \end{defn} \begin{ex} Some admittedly not very interesting sets of !!{formula}s which satisfy this definition and therefore count as modal logics are: \begin{enumerate} \item the set of all tautologies \item the set of all !!{formula}s (the inconsistent modal logic) \end{enumerate} \end{ex} \begin{defn}\label{defn:normal-modal-logic} A modal logic~$\Log L$ is \emph{normal} iff \begin{enumerate} \item it contains both \begin{align} \tag{K} \Box(p \lif q) & \lif (\Box p \lif \Box q) \\ \tag{Dual} \Diamond p & \liff \lnot \Box \lnot p \end{align} \item and it is closed under necessitation, i.e., whenever $!A \in \Log L$, then also $\Box !A \in \Log L$. \end{enumerate} \end{defn} We will encounter two main ways of defining modal logics. One is proof-theoretically, as the set of !!{formula}s that can be derived in certain !!{derivation} systems. The other is model-theoretically, as sets of !!{formula}s which are valid in certain classes of models. This mirrors the situation in ordinary propositional logic (or first-order logic, for that matter). Here we can also single out a set of !!{formula}s in two different ways, e.g., as the set of tautologies which are true in all truth-value assignments and as the set of all !!{derivable} !!{formula}s in some !!{derivation} system. For normal modal logics, this two-fold way of specifying modal logics is possible using relational models and axiomatic (Hilbert-type) proof systems. \end{document}

Referencing norms: FRAME_VALIDITY

en · official · sha256:73044250626697e2bdf57247abebbe8f8d1cb20608d19d47584fbee686609571

% Part: normal-modal-logic % Chapter: syntax-and-semantics % Section: relational-models \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{syn}{rel} \olsection{Relational Models} The basic concept of semantics for normal modal logics is that of a \emph{relational model}. It consists of a set of worlds, which are related by a binary ``accessibility relation,'' together with an assignment which determines which !!{propositional variable}s count as ``true'' at which worlds. \begin{defn} A \emph{model} for the basic modal language is a triple $\mModel{M} = \tuple{W, R, V}$, where \begin{enumerate} \item $W$ is a nonempty set of ``worlds,'' \item $R$ is a binary accessibility relation on~$W$, and \item $V$ is a function assigning to each !!{propositional variable}~$p$ a set $V(p)$ of possible worlds. \end{enumerate} When $Rww'$ holds, we say that $w'$ is \emph{accessible from}~$w$. When $w \in V(p)$ we say $p$ is \emph{true at}~$w$. \end{defn} The great advantage of relational semantics is that models can be represented by means of simple diagrams, such as the one in \olref{fig:simple}. Worlds are represented by nodes, and world~$w'$ is accessible from~$w$ precisely when there is an arrow from~$w$ to~$w'$. Moreover, we label a node (world) by~$\mTrue{p}$ when $w \in V(p)$, and otherwise by~\mFalse{p}. \olref{fig:simple} represents the model with $W = \{w_1, w_2, w_3\}$, $R = \{\tuple{w_1, w_2},\tuple{w_1, w_3}\}$, $V(p) = \{w_1, w_2\}$, and $V(q) = \{w_2\}$. \begin{figure} \begin{center} \begin{tikzpicture}[modal] \node[world] (w1) [label={[align=right]right:\mTrue{p}\\ \mFalse{q}}]{$w_1$}; \node[world] (w2) [label={[align=right]right:\mTrue{p}\\ \mTrue{q}}, above right=of w1]{$w_2$}; \node[world] (w3) [label={[align=right]right:\mFalse{p}\\ \mFalse{q}}, below right=of w1] {$w_3$}; \draw[->] (w1) to (w2); \draw[->] (w1) to (w3); \end{tikzpicture} \end{center} \caption{A simple model.} \ollabel{fig:simple} \end{figure} \end{document}

Referencing norms: ACCESSIBILITY, RELATIONAL_MODEL

en · official · sha256:a0e86181df28718a091c98efe35c931e1c759a5aeb08b837d5a372ceab5332e9

% Part: normal-modal-logic % Chapter: syntax-and-semantics % Section: truth-at-w \documentclass[../../../include/open-logic-section]{subfiles} \begin{document} \olfileid{nml}{syn}{trw} \olsection{Truth at a World} Every modal model determines which modal !!{formula}s count as true at which worlds in it. The relation ``model $\mModel{M}$ makes !!{formula}~$!A$ true at world~$w$'' is the basic notion of relational semantics. The relation is defined inductively and coincides with the usual characterization using truth tables for the non-modal operators. \begin{defn}\ollabel{defn:mmodels} \emph{Truth of !!a{formula}~$!A$ at~$w$} in a~$\mModel M$, in symbols: $\mSat{M}{!A}[w]$, is defined inductively as follows: \begin{enumerate} \tagitem{prvFalse}{\indcase{!A}{\lfalse}{Never $\mSat{M}{\lfalse}[w]$}.}{} \tagitem{prvTrue}{\indcase{!A}{\ltrue}{Always $\mSat{M}{\ltrue}[w]$}.}{} \item $\mSat{M}{p}[w]$ iff $w \in V(p)$. \tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\mSat{M}{\indfrm}[w]$ iff $\mSat/{M}{!B}[w]$}.}{} \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{$\mSat{M}{\indfrm}[w]$ iff $\mSat{M}{!B}[w]$ and $\mSat{M}{!C}[w]$}.}{} \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{$\mSat{M}{\indfrm}[w]$ iff $\mSat{M}{!B}[w]$ or $\mSat{M}{!C}[w]$} (or both).}{} \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{$\mSat{M}{\indfrm}[w]$ iff $\mSat/{M}{!B}[w]$ or $\mSat{M}{!C}[w]$}.}{} \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{$\mSat{M}{\indfrm}[w]$ iff either both $\mSat{M}{!B}[w]$ and $\mSat{M}{!C}[w]$ or neither $\mSat{M}{!B}[w]$ nor $\mSat{M}{!C}[w]$}.}{} \item\ollabel{defn:sub:mmodels-box} \indcase{!A}{\Box !B}{$\mSat{M}{\indfrm}[w]$ iff $\mSat{M}{!B}[w']$ for all $w' \in W$ with $Rww'$.} \item\ollabel{defn:sub:mmodels-diamond} \indcase{!A}{\Diamond !B}{$\mSat{M}{\indfrm}[w]$ iff $\mSat{M}{!B}[w']$ for at least one $w' \in W$ with $Rww'$.} \end{enumerate} \end{defn} Note that by clause~\olref{defn:sub:mmodels-box}, !!a{formula}~$\Box !B$ is true at~$w$ whenever there are no~$w'$ with $Rww'$. In such a case $\Box !B$ is \emph{vacuously} true at~$w$. Also, $\Box !B$ may be satisfied at~$w$ even if $!B$ is not. The truth of~$!B$ at~$w$ does not guarantee the truth of~$\Diamond !B$ at~$w$. This holds, however, if $Rww$, e.g., if $R$ is reflexive. If there is no $w'$ such that $Rww'$, then $\mSat/{M}{\Diamond !A}[w]$, for any~$!A$. \begin{prob} Consider the model of \olref[nml][syn][rel]{fig:simple}. Which of the following hold? \begin{enumerate} \item $\mSat{M}{q}[w_1]$; \item $\mSat{M}{\lnot q}[w_3]$; \item $\mSat{M}{p \lor q}[w_1]$; \item $\mSat{M}{\Box (p \lor q)}[w_1]$; \item $\mSat{M}{\Box q}[w_3]$; \item $\mSat{M}{\Box \bot}[w_3]$; \item $\mSat{M}{\Diamond q}[w_1]$; \item $\mSat{M}{\Box q}[w_1]$; \item $\mSat{M}{\lnot \Box\Box \lnot q}[w_1]$. \end{enumerate} \end{prob} % Prove duality of \Box and \Diamond \begin{tagblock}{prvDiamond} \begin{prop}\ollabel{prop:dual} \begin{enumerate} \item $\mSat{M}{\Box !A}[w]$ iff $\mSat{M}{\lnot\Diamond\lnot !A}[w]$. \item $\mSat{M}{\Diamond !A}[w]$ iff $\mSat{M}{\lnot\Box\lnot !A}[w]$. \end{enumerate} \end{prop} \begin{proof} \begin{enumerate} \item $\mSat{M}{\lnot\Diamond\lnot !A}[w]$ iff $\mSat/{M}{\Diamond\lnot !A}[w]$ by definition of $\mSat{M}{}[w]$. $\mSat{M}{\Diamond\lnot !A}[w]$ iff for some $w'$ with $Rww'$, $\mSat{M}{\lnot !A}[w']$. Hence, $\mSat/{M}{\Diamond\lnot !A}[w]$ iff for all $w'$ with $Rww'$, $\mSat/{M}{\lnot !A}[w']$. We also have $\mSat/{M}{\lnot !A}[w']$ iff $\mSat{M}{!A}[w']$. Together we have $\mSat{M}{\lnot\Diamond\lnot !A}[w]$ iff for all $w'$ with $Rww'$, $\mSat{M}{!A}[w']$. Again by definition of $\mSat{M}{}[w]$, that is the case iff $\mSat{M}{\Box !A}[w]$. \item \iftag{probDiamond}{Exercise.}{$\mSat{M}{\lnot\Box\lnot !A}[w]$ iff $\mSat/{M}{\Box\lnot !A}$. $\mSat{M}{\Box\lnot !A}[w]$ iff for all $w'$ with $Rww'$, $\mSat{M}{\lnot !A}[w']$. Hence, $\mSat/{M}{\Box\lnot !A}[w]$ iff for some $w'$ with $Rww'$, $\mSat/{M}{\lnot !A}[w']$. We also have $\mSat/{M}{\lnot !A}[w']$ iff $\mSat{M}{!A}[w']$. Together we have $\mSat{M}{\lnot\Box\lnot !A}[w]$ iff for some~$w'$ with $Rww'$, $\mSat{M}{!A}[w']$. Again by definition of $\mSat{M}{}[w]$, that is the case iff $\mSat{M}{\Diamond !A}[w]$.} \end{enumerate} \end{proof} \begin{probtag}{probDiamond} Complete the proof of \olref[nml][syn][trw]{prop:dual}. \end{probtag} \end{tagblock} \begin{prob} Let $\mModel{M} = \tuple{W, R, V}$ be a model, and suppose $w_1, w_2 \in W$ are such that: \begin{enumerate} \item $w_1 \in V(p)$ if and only if $w_2 \in V(p)$ (for every !!{propositional variable} $p$); and \item for all $w \in W$: $Rw_1w$ if and only if $Rw_2w$. \end{enumerate} Using induction on !!{formula}s, show that for all !!{formula}s $!A$: $\mSat{M}{!A}[w_1]$ if and only if $\mSat{M}{!A}[w_2]$. \end{prob} \begin{probtag}{prvDiamond} Let $\mModel{M} = \tuple{W, R, V}$. Show that $\mSat{M}{\lnot\Diamond !A}[w]$ if and only if $\mSat{M}{\Box\lnot!A}[w]$. \end{probtag} \end{document}

Referencing norms: ReadingAvailableFor, TRUTH_AT_WORLD, reading_available_for, reading_step