\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{geometric model for modal logics}

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{models_in_modal_logics}{Models in Modal Logics}\dotfill \pageref*{models_in_modal_logics} \linebreak
\noindent\hyperlink{models_in_monomodal_logics}{Models in Monomodal Logics}\dotfill \pageref*{models_in_monomodal_logics} \linebreak
\noindent\hyperlink{gloss}{Gloss}\dotfill \pageref*{gloss} \linebreak
\noindent\hyperlink{satisfaction}{Satisfaction}\dotfill \pageref*{satisfaction} \linebreak
\noindent\hyperlink{notes}{Notes}\dotfill \pageref*{notes} \linebreak
\noindent\hyperlink{what_is_a_valuation}{What is a valuation?}\dotfill \pageref*{what_is_a_valuation} \linebreak
\noindent\hyperlink{models_in_multimodal_logics}{Models in Multimodal Logics}\dotfill \pageref*{models_in_multimodal_logics} \linebreak
\noindent\hyperlink{satisfaction_in_the_multimodal_case}{Satisfaction in the multimodal case}\dotfill \pageref*{satisfaction_in_the_multimodal_case} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{models_in_modal_logics}{}\subsection*{{Models in Modal Logics}}\label{models_in_modal_logics}

To give the standard (geometric) semantics of [[modal logics]], one needs models and these will be discussed here and in the companion [[algebraic models for modal logics]].

(This outlines the basics of the semantics often called \textbf{Kripke semantics} of these logics. We concentrate on modal languages with unary modalities and therefore on relational structures with binary relations in them only. This is largely for the sake of keeping the exposition fairly straightforward and simple. This means the frames used will be `Kripke frames'. There may be a need later (or elsewhere in the Lab) to discuss more general frames.)

\hypertarget{models_in_monomodal_logics}{}\subsubsection*{{Models in Monomodal Logics}}\label{models_in_monomodal_logics}

Again we look at the basic model language.

\begin{udefn}
A \emph{model} for $\mathcal{L}_\omega(1)$ is a pair $\mathfrak{M} = (\mathfrak{F},V)$, where $\mathfrak{F}$ is a [[frame (modal logic) |frame]] (for $\mathcal{L}_\omega(1)$) and $V: Prop \to \mathcal{P}(W)$, is a function, called a \emph{valuation}, assigning to each atomic proposition $p$ a subset of the set, $W$, of worlds.

\end{udefn}
\hypertarget{gloss}{}\subsubsection*{{Gloss}}\label{gloss}

\begin{enumerate}%
\item Informally we think of $V(p)$ as the set of `worlds' in our model where $p$ is true.


\item Frames are `mathematical pictures' of ontologies that are found interesting (for the context), whilst a model `puts some flesh on' the frame by adding contingent information.


\item Frames give a \textbf{combinatorial}, \textbf{relational} or \textbf{geometric} basis for the semantics of these logics. There is also an \textbf{algebraic} semantics that will be examined in another entry. (To be done)



\end{enumerate}
\hypertarget{satisfaction}{}\subsection*{{Satisfaction}}\label{satisfaction}

\begin{udefn}
Suppose that $w$ is a state in a model $\mathfrak{M} = (W,R,V)$. We inductively define the notion of a formula $\phi$ being satisfied in the model at state $w$, as follows:

\begin{itemize}%
\item for $p\in Prop$, $\mathfrak{M},w \models p$ if and only if $w\in V(p)$;


\item $\mathfrak{M},w \models \bot$ never;


\item $\mathfrak{M},w \models \neg \phi$ if and only if it is not true that $\mathfrak{M},w \models \phi$;


\item $\mathfrak{M},w \models \phi \vee \psi$ if and only if $\mathfrak{M},w \models\phi$ or $\mathfrak{M},w \models\psi$;


\item $\mathfrak{M},w \models \Diamond \phi$ if and only if, for some $v \in W$ such that $R w v$, $\mathfrak{M},v \models \phi$.



\end{itemize}
\end{udefn}
\hypertarget{notes}{}\subsubsection*{{Notes}}\label{notes}

\begin{enumerate}%
\item The terminology used in talking about `satisfaction' tends to interpret $\mathfrak{M},v \models \phi$ as saying the formula $\phi$ is \textbf{true} in $\mathfrak{M}$ at state $v$. We will adopt this usage, but we will avoid entering into the niceties of discussing `what is truth?',\ldots{} at least in this entry!


\item $\mathfrak{M},w \models \square \phi$ if and only if $\forall v\in W$ $R w n$ implies $\mathfrak{M},v \models  \phi$. (The proof is fairly routine manipulation of negations.)


\item We say a set $\Sigma$ of formulae is true at state $w\in W$ of a model $\mathfrak{M}$, written $\mathfrak{M},w \models \Sigma$, if all members of $\Sigma$ are satisfied as $w$.


\item It is convenient to extend the valuation $V$ to arbitrary formulae by setting $V(\phi) := \{w \mid \mathfrak{M},w \models \phi\}$. We then get useful interpretations such as: if for all worlds $v$, $\mathfrak{M},v \models  (\phi\to \psi)$ and \emph{modus ponens} holds, (i.e. we have a logic as such in which we are working, then $V(\phi)\subseteq V(\psi)$. (This comment is deliberately slightly vague, but indicates a common type of argument that will be behind many results, where more precision is available, so think of it as a template for a result rather than a result as such.)



\end{enumerate}
\hypertarget{what_is_a_valuation}{}\subsubsection*{{What is a valuation?}}\label{what_is_a_valuation}

In the definition of a Kripke model the valuation is all important. It is what puts meaning onto the frame. It is very useful to push this idea around through a couple of adjunctions and reinterpretations. The process is fairly intuitive, but it pays to do things reasonably formally:

\begin{enumerate}%
\item Note that the power set $\mathcal{P}(W)$ can also be written as $\mathbf{2}^W$ the set of functions from $W$ to $\mathbf{2}$, where we write $\mathbf{2}$ for the `set' of classical [[truth values]], $\{\bot \to \top\}$, or $\{true,false\}$, or $\{0,1\}$ or \ldots{} . We wrote `set' in inverted commas for several reasons:

\begin{itemize}%
\item Firstly an important role here is played by the multiple structures that $\mathbf{2}$ has. It is a [[Heyting algebra]]; it has a natural [[poset]] structure; it is the [[subobject classifier]] in the [[topos]] of sets, and so on. In fact it is the source of most of the logic semantic structure within this context. Its structure induces similar structures on the powerset, $\mathcal{P}(W)$, given by union etc, that made the semantics work above. (See also the discussion on [[dualizing object|ambimorphic objects]] in the entry on the [[Chu construction]].)


\item Next note that although we said `set' we could do a lot of this in other settings. For instance we could work within a more general topos with an object of possible worlds and an object of propositions. We would need the extra [[Heyting algebra]] structure on what would there probably be written as $\Omega$, and our negation interpretation would be more subtle.


\item Finally we could categorify things. For the moment we will leave this aside, but note the discussion at [[truth value]].



\end{itemize}

\item For convenience we will write $P$ for $Prop$, then a valuation is $V: P\to \mathbf{2}^W$, and using co[[currying]] this corresponds to $V: P\times W\to \mathbf{2}$. That, of course, corresponds to a subset of $P\times W$. That subset consists of all pairs, $(p,w)$, for which $w\in V(p)$ so interprets as the set of pairs in which the proposition $p$ is `true' in world $w$.


\item We could re[[currying|curry]] after transposing $P$ and $W$, to get $V$ to correspond to $\tilde{V}: W \to \mathcal{P}(P)$, so that $\tilde{V}(w)$ is the set of propositions true about the world $w$.


\item Another useful direction is to see this as giving a binary [[Chu construction|Chu space]]. (To be investigated later.)



\end{enumerate}
\hypertarget{models_in_multimodal_logics}{}\subsection*{{Models in Multimodal Logics}}\label{models_in_multimodal_logics}

Again we look at the basic model language this time with $n$ unary modal operators.

\begin{udefn}
A \emph{model} for $\mathcal{L}_\omega(n)$ is a pair $\mathfrak{M} = (\mathfrak{F},V)$, where $\mathfrak{F}$ is a frame (for $\mathcal{L}_\omega(n)$) and $V: Prop \to \mathcal{P}(W)$, is a function, called a \emph{valuation}, assigning to each atomic proposition $p$ a subset of the set, $W$, of worlds.

\end{udefn}
\hypertarget{satisfaction_in_the_multimodal_case}{}\subsection*{{Satisfaction in the multimodal case}}\label{satisfaction_in_the_multimodal_case}

This is virtually the same as in the monomodal case, except for the last case which involves the $n$ modal operators. (We give it in full repeating the earlier cases for convenience.)

\begin{udefn}
Suppose that $w$ is a state in a model $\mathfrak{M} = (W,R,V)$. We inductively define the notion of a formula $\phi$ being satisfied in the model at state $w$, as follows:

\begin{itemize}%
\item for $p\in Prop$, $\mathfrak{M},w \models p$ if and only if $w\in V(p)$;


\item $\mathfrak{M},w \models \bot$ never;


\item $\mathfrak{M},w \models \neg \phi$ if and only if it is not true that $\mathfrak{M},w \models \phi$;


\item $\mathfrak{M},w \models \phi \vee \psi$ if and only if $\mathfrak{M},w \models\phi$ or $\mathfrak{M},w \models\psi$;


\item for each $i = 1, \ldots, n$, $\mathfrak{M},w \models \Diamond_i \phi$ if and only if, for some $v \in W$ such that $R_i w v$, $\mathfrak{M},v \models \phi$.



\end{itemize}
\end{udefn}
Satisfaction on a class of models is related to [[validity]] of modal formulae. In this way a class of frames can determine a logic and then the logic determines a class of frames. The axiomatisation of that class/logic is then an interesting challenge.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[modal type theory]]


\item [[algebraic model for modal logic]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

Generally this entry is based on

\begin{itemize}%
\item P. [[Blackburn]], M. de Rijke and Y. [[Venema]], \emph{Modal Logic}, Cambridge Tracts in Theoretical Computer Science, vol. 53, 2001,

\end{itemize}
(any mistakes or errors of interpretation are due to \ldots{}.!)

[[!redirects geometric model for modal logic]] [[!redirects geometric model for modal logics]] [[!redirects geometric models for modal logic]] [[!redirects geometric models for modal logics]]

[[!redirects Kripke semantics]]



\end{document}