Introduction to Modal Logic (Lecture)

I followed this course by, Prof. Nick Bezhanishvili during my 5th Semester at the ILLC Amsterdam for my M.Sc. Logic (UvA). I covered most of the material already in Modal Logic (Lecture). I paired for exercises with Josje van der Laan. The notes are from the book: Modal Logic by P. Blackburn, M. de Rijke, Y. Venema, (2010), Cambridge University Press.

Assignments

1. Overleaf: IML, 1
2. Overleaf: IML, 2
3. Overleaf: IML, 3
4. Overleaf: IML, 4
5. Overleaf: IML, 5

Lecture Notes

• Bisimilarity & Invariance Lemma, as in: 3. Expressive Power and Invariance.
  • converse of invariance lemma holds with $n$-bisimilarity for $n\in \mathbb{N}$. (see 2.24)
  • $\mathcal{M}=(M,R,V)$ is image finite if ${\forall }_{x\in M}|R[x]|<{\aleph }_0$
    • $R[x]:=\{y\in M:xRy\}$
  • for $\mathcal{M}$, ${\mathcal{M}}^{\prime }$ image finite, ${\forall }_{x\in M}{\forall }_{x^{\prime }\in M^{\prime }}\mathcal{M},x\equiv {\mathcal{M}}^{\prime },x^{\prime }\Rightarrow \mathcal{M},x\underline{\leftrightarrow }{\mathcal{M}}^{\prime },x^{\prime }$ (Hennessy - Milner)
    • $\equiv$ often written as $\leftrightsquigarrow$
    • $\mathcal{M},x\equiv {\mathcal{M}}^{\prime },x^{\prime }\Rightarrow \mathcal{M},x\underline{\leftrightarrow }{\mathcal{M}}^{\prime },x^{\prime }$ often written as $x\equiv x^{\prime }\Rightarrow x\underline{\leftrightarrow }{x}^{\prime }$.
  • [for $k\in ON$ the maximal complexity of a formula in ${\mathcal{L}}_{ML}^k$, a $k$-inductively defined modal logic, then ${\forall }_{x\in M}{\forall }_{x^{\prime }\in M^{\prime }}\mathcal{M},x\equiv {\mathcal{M}}^{\prime },x^{\prime }\Rightarrow \mathcal{M},x{\underline{\leftrightarrow }}^k{\mathcal{M}}^{\prime },x^{\prime }$ for ${\underline{\leftrightarrow }}^k$ the $k$-bisimulation, as defined in: Overleaf: IML, 1]

Types (from the Book)

• $\tau =(O,\rho )$ is a modal similarity type for $O\ne \varnothing$, $\rho :O\to \mathbb{N}$, 1.11
  • elements of $O$ are modal operators
    • use ${△}_0,{△}_1,...$ to denote its elements.
      • for $i\in \mathbb{N}$, ${▽}_i({\phi }_1,...,{\phi }_n):=\neg {△}_i(\neg {\phi }_1,...,\neg {\phi }_n)$
  • $\rho$ assigns to each operator $△$ a finite arity.
• $ML(\tau ,\Phi )$ is a modal language for $\tau =(O,\rho )$ and a set of prop.lett $\Phi$, 1.12
  • $Form(\tau ,\Phi )$ is given by $⟨p|\perp |\neg \phi |{\phi }_1\wedge {\phi }_2|△({\phi }_1,...,{\phi }_{\rho (△)})⟩$
• $\tau$-type at $w$ is $\{\phi :\mathcal{M},w\models \phi \}$, 2.1
  • two $\tau$-types at $w$ and $w^{\prime }$, for $w\in M,w^{\prime }\in M^{\prime }$, s.t. $\mathcal{M},{\mathcal{M}}^{\prime }$ have same mod.sim.type $\tau$, write $w\leftrightsquigarrow w^{\prime }$ if $\tau$-type.$w$ is $\tau$-type.$w^{\prime }$.
  • $\mathcal{M}\leftrightsquigarrow {\mathcal{M}}^{\prime }$ iff ${\bigcap }_{w\in M}\{\phi :\mathcal{M},w\models \phi \}={\bigcap }_{w^{\prime }\in M^{\prime }}\{\phi :{\mathcal{M}}^{\prime },w^{\prime }\models \phi \}$
  • $\mathcal{M}⨆\mathcal{N}$ preserves all information.
• for $\tau$ mod.sim.type, ${\mathcal{M}}_i$ $\tau$-models, then ${\forall }_{\phi \in {\mathcal{L}}_{\tau -ML}}{\forall }_{i\in I}{\forall }_{w\in M_i}{\mathcal{M}}_i,w\models \phi \iff {\bigcup }_{i\in I}{\mathcal{M}}_i,w\models \phi$, 2.3

17.09, Filtrations

• A (generated) submodel ${\mathcal{M}}^{\prime }$ of $\mathcal{M}$ is a model s.t.
  1. $W^{\prime }\subseteq W$
  2. $R^{\prime }=R\cap (W^{\prime }\times W^{\prime })$
  3. $V^{\prime }(p)=V(p)\cap W^{\prime }$ (4.) ${\forall }_{w\in M^{\prime }}wRv\to v\in W^{\prime }$
  • ${\mathcal{M}}^{\prime }$ is gen.sub, of $\mathcal{M}$, $x\in W^{\prime }$, then $\mathcal{M},x\underline{\leftrightarrow }{\mathcal{M}}^{\prime },x$
• $\mathcal{M}$ is rooted if exists $w\in M$, a root, that generates the whole model, 2.5
• Morphisms
  • Homo- for $\mathcal{M},{\mathcal{M}}^{\prime }$ $\tau$-models, $f:\mathcal{M}\to {\mathcal{M}}^{\prime }$ hom., if: , 2.7
    1. ${\forall }_{p\in \text{Prop}}{\forall }_{w\in W}w\in V(p)\to f(w)\in V^{\prime }(p)$
    2. ${\forall }_{n\in {\mathbb{N}}_0}{\forall }_{△\in \tau }\rho (△=n\to {\forall }_{W\subseteq M}|W|=n+1\to W=(w_0,...,w_n)\in R_{△}\to (f(w_0),...,f(w_n))\in R_{△}^{\prime }$
    • Modal formulas are not invariant under homomorphism, structure of the domain (source) is reflected in the image (target), not the riverse.
    • ${\forall }_{w\in M}{\forall }_{w^{\prime }\in M^{\prime }}{\exists }_{f:\mathcal{M}\to {\mathcal{M}}^{\prime }}f(w)=w^{\prime }\Rightarrow ({\forall }_{\phi \in {\mathcal{L}}_{ML}}\mathcal{M},w\models \phi \iff {\mathcal{M}}^{\prime },w^{\prime }\models \phi )$, 2.9
    • $\mathcal{M}\cong {\mathcal{M}}^{\prime }\Rightarrow \mathcal{M}\leftrightsquigarrow {\mathcal{M}}^{\prime }$, 2.9
  • Bounded: if
    1. ${\forall }_{w\in M}{\forall }_{p\in \text{Prop}}\mathcal{M},w\models p\iff {\mathcal{M}}^{\prime },f(w)\models p$
    2. $f$ is homom. to $R$
    3. ${\forall }_{w\in M}{\forall }_{v^{\prime }\in M^{\prime }}f(w)R{v}^{\prime }\to {\exists }_{v\in M}wRv\wedge f(v)=v^{\prime }$
    • let $f:\mathcal{M}\to {\mathcal{M}}^{\prime }$ bound.morph., then ${\forall }_{\phi \in {\mathcal{L}}_{ML}}{\forall }_{w\in M}\mathcal{M},w\models \phi \iff {\mathcal{M}}^{\prime },f(w)\models \phi$
      • for $\mathcal{M},{\mathcal{M}}^{\prime }$ models, $f:W\to W^{\prime }$ a bound.morph., then $\mathcal{M},x\underline{\leftrightarrow }{\mathcal{M}}^{\prime },f(x)$
  • for $\{{\mathcal{M}}_i{\}}_{i\in I}$ for ${\mathcal{M}}_i$ model, the disj.union (On Disjoint Union) is a model $\mathcal{M}$ s.t.
    1. $W:={⨆}_{i\in I}{W}_i$, $R={\bigcup }_{i\in I}{R}_i$, $V(p)={\bigcup }_{i\in I}{V}_i(p)$
• 5. Finite Model Property:
  • Modal Depth:\is $deg$ defined as follows:
    1. (i) $deg(p)=0$, (ii) $deg(\perp )=0$, (iii) $deg(\neg \varphi )=deg(\varphi )$, (iv) $deg(\varphi \wedge \psi )=\max \{deg(\varphi ),deg(\psi )\}$
    2. (v) $deg(△({\varphi }_1,...,{\varphi }_n))=1+max\{deg({\varphi }_1),...,deg(\varphi {)}_n\}$
  • $w{\underline{\leftrightarrow }}_n{w}^{\prime }$ i.e. bisimulate up to depth $n$.
    • if, for $\text{Prop}⊊{\mathcal{L}}_{ML}$, $|\text{Prop}|<{\aleph }_0$, then $({\forall }_{n\in \mathbb{N}}\mathcal{M},w{\underline{\leftrightarrow }}_n{\mathcal{M}}^{\prime },w^{\prime })\iff ({\forall }_{\phi \in {\mathcal{L}}_{ML}}\mathcal{M},w\models \phi \iff {\mathcal{M}}^{\prime },w^{\prime }\models \phi )$, 2.30-1
  • for $\mathcal{M}$ rooted model in $w$, define:, 2.32
    1. ${\forall }_{w^{\prime }\in M}ht(w^{\prime })=0\to w^{\prime }=w$
    2. $\forall w^{\prime }\in Mht(w^{\prime })=n+1\to {\exists }_{w^{\prime \prime }\in M}ht(w^{\prime \prime })=n\wedge w^{\prime \prime }R{w}^{\prime }$
    • $ht(\mathcal{M})=\max \{ht(w^{\prime }):w^{\prime }\in M\}$
    • $\mathcal{M}{|}_k=(M{|}_k,R{|}_k,V{|}_k)$
      1. $M{|}_k=\{w^{\prime }\in M:ht(w^{\prime })\le k\}$, $R{|}_k=R{|}_{M{|}_k}$ and $V{|}_k=V{|}_{M{|}_k}$.
  • if $\tau$ has only diamonds, $\varphi$ is sat. iff sat. on a finite mode, 2.34
  • Filtrations from 2.25
    • for $\Sigma \subseteq {\mathcal{L}}_{ML}$ cl.under subformulae, 2.36
    • $W_{\Sigma }:=\{[x]:x\in W\}$
      • $[x{]}_{(\Sigma )}:=\{y\in W:x{\leftrightsquigarrow }_{\Sigma }y\}$
        • $x{\leftrightsquigarrow }_{\Sigma }y:={\forall }_{\phi \in \Sigma }(\mathcal{M},x\models \phi \iff \mathcal{M},y\models \phi )$
    • the filtration model ${\mathcal{M}}^f$, 2.36
      1. $W^f=W_{\Sigma }$
      2. ${\forall }_{x,y\in M}xRy\Rightarrow [x]R^f[y]$
      3. ${\forall }_{x,y\in M}([x]R^f[y]\Rightarrow {\forall }_{◊\phi \in \Sigma }(\mathcal{M},y\models \phi \Rightarrow \mathcal{M},x\models ◊\phi ))$
      4. $V^f(p)=\{[x]:\mathcal{M},x\models p\}$
    • ${\forall }_{\Sigma \subseteq {\mathcal{L}}_{ML}}|\Sigma |<{\aleph }_0\to {\forall }_{\phi \in \Sigma }{\forall }_{x\in W}\mathcal{M},x\models \phi \iff {\mathcal{M}}^f,[x]\models \phi$, 2.39
      • ${\forall }_{\Sigma \subseteq {\mathcal{L}}_{ML}}|\Sigma |<{\aleph }_0\to |M^f|\le 2^{|\Sigma |}$, 2.38
      • every formula that is satisfiable, is satisfiable in a finite model, 2.41
        • for ${\Sigma }_{\varphi }$ the subformula-closure of $\{\varphi \}$.
    • One can always define filtration through:, 2.39
      1. $[w]R^s[v]\iff {\exists }_{w^{\prime }\in [w]}{\exists }_{v^{\prime }\in [v]}{w}^{\prime }R{v}^{\prime }$ (smallest)
      2. $[w]R^l[v]\iff ({\forall }_{◊\varphi \in \Sigma }\mathcal{M},v\models \varphi \Rightarrow \mathcal{M},w\models ◊\varphi )$ (largest)
      • $R^s\subseteq R^f\subseteq R^l$
      • $[w]R^t[v]\iff {\forall }_{◊\varphi \in \Sigma }((\mathcal{M},v\models \varphi \wedge ◊\varphi )\to \mathcal{M},w\models ◊\varphi )$
        • $R$ trans. $\Rightarrow R^t$ trans.
        • for $R$ trans., define $C\subseteq M$, $(C,R{|}_C,V{|}_C)$ (cluster), 2.43
          • a cluser is simple, if $C=\{c\}$ s.t. $cRc$ and proper if $|C|\ge 2$.

24.09, IV. Trees

• a tree $(T,S)$ is a frame s.t.
  1. $T$ is rooted (i.e. ${\forall }_{t\in T}\exists {!}_{r\in T}r{S}^{\ast }t$)
     1. for $S^{\ast }$ the refl.trans.cl. of $S$
  2. ${\forall }_{t\in T}t\ne r\to \exists {!}_{t^{\prime }\in T}{t}^{\prime }St$
  3. ${\forall }_{t\in T}\neg t{S}^{+}t$
     1. for $S^{+}$ the trans.cl. of $S$
• for $\mathcal{M}=(W,R,V)$, ex. $\mathcal{T}=(T,S,V)$ s.t. $f:T\to V$ surj. bounded morphism.
• a path in $\mathcal{M}$ is a seq. $(r,u_1,...,u_n)$ s.t. $u_{i}R{u}_{i+1}$

Standard Translation

01.10, V. Frame Definability

• a class of frames $C$ is definable if there is a modal formula $\phi$ s.t. $\mathcal{F}\models \phi \iff \mathcal{F}\in \mathcal{C}$.
• recall bounded functions from 17.09, Filtrations.
  • for $f$ bounded morphism, s.t. $dom(f)=F$, $f(F)=G$, then ${\forall }_{\phi \in {\mathcal{L}}_{ML}}\mathcal{F}\models \phi \Rightarrow \mathcal{G}\models \phi$.
    • “modally definable classes are closed under bounded morphisms.”
• recall disjoint union from 17.09, Filtrations. We define it now for frames.
  • for $C$ a definable class of frames: ${\forall }_{\mathcal{F},\mathcal{G}\in C}\mathcal{F}⨆\mathcal{G}\in C$
• for $C$ FO.def.class of frames, then $C$ is mod.def. iff. $C$ is cl. under bounded morphic images, hgenerated subframes, disjoint unions and reflects untrafitler extensions (Goldlatt - Thomson Theorem)
  • see Model Theory (Lecture) for ultrafilters, but also First Bachelor Thesis Concept.
• Löb formula: $\square (\square p\to p)\to \square p$
  • for $p=\perp$, $\square (\square \perp \to \perp )\to \perp \iff \square \neg \square \perp \to \square \perp$, if you prove smth consistent, it is false (Gödel)
• Gödel Logic (GL)
  • $\mathcal{F}$ is conversely well-founded if there is no ascending infinite chain
    • (it is not FO-def.)
  • $\mathcal{F}$ not trans., $\mathcal{F}$ not conv.well.foud. then $\mathcal{F}/\models \square (\square p\to p)\to \square p$.
  • $\mathcal{F}\models \phi \iff {\forall }_p{\forall }_{x}S{T}_x(\phi )$ ?

08.10, VI. Correspondence

• $(\mathcal{F},V)\models \phi \iff (\mathcal{F},V)\models {\forall }_{x}S{T}_x(\phi )$, this is the general form of correspondence
  • $\mathcal{F}\models \phi (p_1,...,p_n)\iff \mathcal{F}{\forall }_{p_1,...,p_n}{\forall }_{x}S{T}_x(\phi )$, with a second order quantification
  • for some, second order is not needed: $\mathcal{F}\models p\to ◊p\iff \mathcal{F}\models {\forall }_{x}xRx$
    • which is: ${\forall }_p{\forall }_{x}S{T}_x(p\to ◊p)$
• ${\forall }_{\phi \in {\mathcal{L}}_{ML}}{\exists }_{\alpha (x)\in {\mathcal{L}}_{FOL}}{\forall }_{\mathcal{F}=(M,R)}\mathcal{F}\models \phi \iff \mathcal{F}\models {\forall }_x\alpha (x)$, call "${\forall }_x\alpha (x)$" is a FO-correspondent of $\phi$.
  • example: $\mathcal{F}\models ◊\top \iff {\forall }_{p_1,...,p_n}{\forall }_x{\exists }_y(xRy\wedge y=y)\iff \mathcal{F}\models {\forall }_x{\exists }_{y}xRy$
    • $\phi \in {\mathcal{L}}_{ML}$ is closed if ${\forall }_{p\in \text{Prop}}\dot{p}\notin \phi$
    • if $\phi$ is closed, it has a FO-corr., which is effectively computable form $\phi$.
• more clearly than in the book: Sahlqvist.pdf
• for $\phi \in {\mathcal{L}}_{ML}$, write occurrences as $\dot{p}\in \phi$, call it positive if $p$ is under an even number of negations in $\phi$
  • I write $\dot{p}{\in }_{+}\phi$. occurrences are either positive or negative ("${\in }_{-}$")
• $\phi \in {\mathcal{L}}_{ML}$ is positive if ${\forall }_{p\in \text{Prop}}\dot{p}{\in }_{+}\phi$
  • formulae are positive, negative or either of the two.
  • clearly, ${\forall }_{\phi \in {\mathcal{L}}_{ML}}pos.(\phi )\iff neg.(\neg \phi )$
• for $\phi \in {\mathcal{L}}_{ML}$, $p\in \text{Prop}$ s.t. $\dot{p}{\in }_{+}\phi$, let $V$ a val. on $\mathcal{F}$, and $V^{\prime }$ a val. s.t. ${\forall }_{q\ne p}{V}^{\prime }(q)=V(q)$ and $V(p)\subseteq V^{\prime }(p)$, then $(\mathcal{F},V),w\models \phi \models \phi \Rightarrow (\mathcal{F},V^{\prime }),w\models \phi$.
  • $\Leftarrow$ for $\neg p$.
• there always is a minimal valuation that makes the formula false

12.11, General Frames & Incomplete Logics

• $(W,R,A)$ is a general frame if $(W,R)$ is a kripke frame and $A\subseteq \mathcal{P}(X)$ s.t.
  1. $W,\varnothing \in A$
  2. ${\forall }_{U,V\in A}U\cup V\in A$
  3. ${\forall }_{U,V\in A}U\setminus V\in A$
  4. ${\forall }_{U\in A}\{x\in W:{\exists }_{y\in U}xRy\}\in A$
     • ${◊}_{R}U:=\{x\in W:{\exists }_{y\in U}xRy\}$
• for $(W,R,A)$ a gen.fr. then:
  1. ${\forall }_{U,V\in A}U\cap V\in A$
  2. ${\forall }_{U\in A}\{x\in W:R[x]\subseteq U\}\in A$
     1. $R[x]:=\{y:xRy\}$
     • ${\square }_{R}U:=\{x\in W:R[x]\subseteq U\}$
• $(W,R,A,V)$ is a gen.mod. for $(W,R,A)$ a gen.fr and $V:\text{Prop}\to A$.
  • $[[\phi ]]:=\{x\in W:\mathcal{M},x\models \phi \wedge \phi \in A\}$
• $F=(W,R,A)$ gen.fr and $Log(F):=\{\phi :F\models \phi \}$ is a consistent normal modal logic.
• Define $K_{t}Tho$ (M)
  1. ${◊}_{F}p\wedge {◊}_{F}q\to {◊}_F(p\wedge {◊}_{F}q)\vee {◊}_F(p\wedge q)\vee {◊}_F({◊}_{F}p\vee q)$
  2. ${◊}_F\top$
  3. ${\square }_P({\square }_{P}q\to q)\to {\square }_{P}q$
  • (M) ${\square }_F{◊}_{F}p\to {◊}_F{\square }_{F}p$
• $K_{t}ThoM$ is an consistent and complete logic

26.10 Completeness of PDL

Definition (Atom) let $\Sigma$ be a set of formulae, $A$ is an Atom if $A\text{subs}\neg FL(\Sigma )isconsistentA/{⊢}_{\text{PDL}}\perp$ and $AsubsetneqB\subset \neg \text{FL}(\Sigma ),then$B \vdahs_{\PDL} \bot$

Also define $At(\Sigma ).=\{A|A$ is an atom in $\lnot FL(\Sigma)}

Lemma let $A$ \in At(\Sigma), then:

1. \varphi \in \lnot FL(\Sigma): exatly one \varphi \in A or \lnot \varphi \in A
2. … (sry missed those, but simple equivalence following the definitions of the ways combining programs given in \FL).

Lemma At(\Sigma) = {\Gamma \cap \lnot FL(\Sigma) : for some MCS \Gamma} Proof \Gamma \cap \lnot FL(\Sigma) is consistent \not \vdash \bot as $\Gamma /⊢\perp suppose\Gamma \cap \neg \text{FL}(\Sigma )⊊B\subseteq \neg \text{FL}(\Sigma ),thenthereisa\phi \in B$ but \varpgu \not \in \Gamma \cap \lnot FL(\Sigma), so \varphi \not \in \Gamma. We then. conclide \lnot \varphi \in \Gamma, so…

For the other direction, simple application of the Lindenbaum lemma. $A \subseteq \Gamma \ca \lnto FL(\Sigma) \Rightarrow A = \Gamma \cap \lnot FL(\Sigma) as both are atoms.

Consider that all proof swe are doing are constructive by finiteness of \Sigma and hence of $\text{FL}(\Sigma )$

Lemma if \varphi \in \lnot \FL(\Sigma) and $\{\phi \}isconsistent,\phi /⊢\perp thenthereisaa$A \in At(\Sigma)$ s.t. \varphi \in A. Proof by Lindenbaum

Definition (finite canonical model over $\Sigma$) “temporary definition”. Let $\Sigma$ be a finite set of formulas, the finite canonical model over $\Sigma$ is made by $(At(\Sigma ),\{S_{\pi }{\}}_{\pi \in \Pi },V^{\Sigma })$ where $V^{\Sigma }(p)=\{A\in At(\Sigma ):p\in A\}$. We then define $A{S}_{\pi }^{\text{Sijgma}}B\iff \hat{A}\wedge ⟨\pi ⟩\hat{B}$., where $\hat{A}:=\bigwedge \{\phi :\phi \in A\}$.

Note now: $S_{{\pi }_1\cup {\pi }_2}\ne S_{p{i}_1}\cup S_{{\pi }_2}$ and $S_{{\pi }^{\ast }}\ne (S_{\pi }{)}^{\ast }$ and we dont like it! We massage the canonical model in order to prove this but still prove the Truths Lemma.

Lemma let $A$ \in At(\Sigma) and $\langle \pi \rangle