\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*{modal logic}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{category_theory}{}\paragraph*{{$(0,1)$-Category theory}}\label{category_theory}

[[!include (0,1)-category theory - contents]]

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\hypertarget{modalities_closure_and_reflection}{}\paragraph*{{Modalities, Closure and Reflection}}\label{modalities_closure_and_reflection}

[[!include modalities - contents]]

\hypertarget{modal_logics}{}\section*{{Modal Logics}}\label{modal_logics}

\noindent\hyperlink{Idea}{Idea}\dotfill \pageref*{Idea} \linebreak
\noindent\hyperlink{Definition}{Definition}\dotfill \pageref*{Definition} \linebreak
\noindent\hyperlink{modal+language}{Modal Languages}\dotfill \pageref*{modal+language} \linebreak
\noindent\hyperlink{modal_logics_2}{Modal logics}\dotfill \pageref*{modal_logics_2} \linebreak
\noindent\hyperlink{common_modal_axioms}{Common modal axioms}\dotfill \pageref*{common_modal_axioms} \linebreak
\noindent\hyperlink{Examples}{Examples}\dotfill \pageref*{Examples} \linebreak
\noindent\hyperlink{semantics}{Semantics}\dotfill \pageref*{semantics} \linebreak
\noindent\hyperlink{in_kripke_frames__relational_structures}{In Kripke frames / relational structures}\dotfill \pageref*{in_kripke_frames__relational_structures} \linebreak
\noindent\hyperlink{AlgebraicSemantics}{Algebraic semantics}\dotfill \pageref*{AlgebraicSemantics} \linebreak
\noindent\hyperlink{coalgebraic_semantics}{Coalgebraic semantics}\dotfill \pageref*{coalgebraic_semantics} \linebreak
\noindent\hyperlink{CategoricalSemantics}{Categorical semantics}\dotfill \pageref*{CategoricalSemantics} \linebreak
\noindent\hyperlink{theorems}{Theorems}\dotfill \pageref*{theorems} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{links}{Links}\dotfill \pageref*{links} \linebreak
\noindent\hyperlink{References}{References}\dotfill \pageref*{References} \linebreak


\hypertarget{Idea}{}\subsection*{{Idea}}\label{Idea}

The term \emph{modal logic} refers to an enrichment of standard formal [[logic]] where the standard operations ([[and]], [[or]], [[not]], implication and perhaps [[universal quantifier|forall]], etc.) are accompanied by certain extra operations -- called \emph{modal operators} and often denoted by ``$\lozenge$'' and ``$\Box$'' or similar -- such that for $p$ any [[proposition]] the expression $\Box p$ is a new proposition whose interpretation is roughly as ``$p$ holds (only) in some \emph{mode}'' or ``$p$ holds (only) \emph{in a certain way}'', such as: ``$p$ is \emph{possibly} true'', ``$p$ will \emph{eventually become} true'', ``$p$ is \emph{believed} to be true'', etc.

There is no established axiom set that an operator on propositions has to satisfy to count as a \emph{modal operator}. As a result, for instance in the preface of (\hyperlink{BlackburnDeRijkeVenema}{Blackburn-deRijke-Venema}) et al.) it says

\begin{quote}%
\emph{`Ask three modal logicians what modal logic is, and you are likely to get at least three different answers'}.


\end{quote}
Hence there is a good bit of flexibility in the notion \emph{modal logic}. The archetypical example of a modal logic, often taken to be the default example, is a system, called \emph{[[S4 modal logic]]} or some slight variants (S1, S2, \ldots{}) of it, that aims to model the idea of propositions being ``possibly true'' or ``necessarily true''. We list and discuss further examples of modal logic in more detail below in \emph{\hyperlink{Examples}{Examples}}.

One way to view the axioms of [[S4 modal logic]] is as being those of [[propositional logic]] together with a [[monad (in computer science)|co-monad]] $\Box$ on the [[type of propositions|universe of propositions]]. Accordingly, many other flavours of modal operators that are being considered (but not all) are also (co)monads, see below at \emph{\href{modal%20type%20theory#RelationToMonads}{modal type theory -- Relation to monads}}. This has an evident generalization to \emph{[[modal type theory]]}, which is concerned with [[type theory|type theories]] equipped with [[monad (in computer science)|(co)monads]] on their [[type of types|type universe]]. Hence when restricted to modalities that are required to be (co)monads, then modal logic is the counterpart in \emph{[[computational trinitarianism]]} to [[category theory]] making use of [[closure operator]] [[monads]] and to [[computer science]] with [[monads in computer science]].

For a good survey of and introduction to modal logic see \emph{\hyperlink{SEPModernOrigins}{SEP - Modern Origins of Modal Logic}} for (historical) motivation and introduction and then \emph{\hyperlink{SEPModalLogic}{SEP - Modal logic}} for more technical details.

Modal logics have [[semantics]] in terms of sets with [[relations]], called \emph{[[Kripke frames]]} in the context of modal logic. They also have algebraic semantics in terms of algebras with (co)-closure operators. For instance, [[temporal logic|temporal logics]] can have [[posets]] as [[models]].

\hypertarget{Definition}{}\subsection*{{Definition}}\label{Definition}

\hypertarget{modal+language}{}\subsubsection*{{Modal Languages}}\label{modal+language}

Modal logics are built on \textbf{modal languages}, that is the usual propositional language plus those extra modalities. (Note that modalities may also be added to predicate logic, see [[first-order modal logic]].) The way the modalities work has to be laid down in an axiom system for the logic in question, for instance, for the temporal logic we might require an axiom saying `If $F F\phi$ is true, then $F\phi$ is true', which will read a `if it is going be true in the future that $\phi$ is going to be true in the future, then \ldots{}', see [[temporal logic]]. (Is this going to be something what we might want in `[[provability logic]]'; is it the case that we should expect that if it is provable that something is provable then that something must be itself provable. This concentrates the modelling process on exactly how we wish to have our `context' to behave.) In this way the relational nature of a context that we are looking at can get encoded into the logic.

Modal languages add one or more modal operator, often denoted $\square$ or $\lozenge$ into the usual [[propositional logics]]. (For the moment, we will keep things fairly simple so assume these to be unary operators and we will not be considering operators that have more than one input, for the moment at least. The general case will be considered later on, but in any case is discussed in detail in some of the books on modal logic listed below.)

We will give a modal language with $n$ modal operators, $\lozenge_i$, $i = 1,\ldots, n$, which can be applied to propositions of the language to form new propositions. If $n=1$, we will refer to the language, defined below, as the \emph{basic modal language}.

\begin{defn}
\label{}\hypertarget{}{}
We suppose given a set of variables, the \emph{$n$-operator basic modal language}, $\mathcal{L}_\omega(n)$, given by

\begin{displaymath}
\phi ::= p_\lambda \mid \bot \mid \neg \phi \mid \phi_1 \vee \phi_2 \mid \lozenge_i\phi,
\end{displaymath}
where the $p_\lambda$ are the propositional variables ordered by finite ordinals, $\lambda$, and, as usual, $\lozenge_i$ is a modality for each $i=1, \ldots , n$.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
This form of definition needs a bit of interpreting if you have not met it before. It gives a way of deciding if a formula is `well-formed'. The well formed formulae of $\mathcal{L}_\omega(n)$ are defined as follows: A formula is either

\begin{itemize}%
\item a proposition variable,


\item the propositional constant $\bot$, that is \emph{falsum},


\item a negated formula,


\item a disjunction of two formulae, or


\item a formula prefixed by one of the diamonds / modal operators.



\end{itemize}
\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
The basic modal language will be $\mathcal{L}_\omega(1)$. We will sometimes write $Prop$ for the set of propositional variables / atomic formulae or whatever other reasonable term is used in a context.

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
The interpretation of $\lozenge \phi$ depends on the context (to some extent), but in the initial form here it is usually said to mean `possibly $\phi$'.

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
Some authors use an equivalent generation rule using $\square \phi$, which is $\neg \lozenge \neg \phi$. Of course, this interprets as `necessarily $\phi$' in this initial form. In [[epistemic logic]] the basic modal language interprets $\square \phi$ as saying `the agent knows that $\phi$'.

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
Other formulations replace $\vee$ and $\neg$ by implication $\phi_1\to \phi_2$, or by $\wedge$ and $\neg$.

\end{remark}
\hypertarget{modal_logics_2}{}\subsubsection*{{Modal logics}}\label{modal_logics_2}

\begin{defn}
\label{}\hypertarget{}{}
A \textbf{modal logic} in $\mathcal{L}_\omega(n)$ is any set $\Lambda$ of $\mathcal{L}_\omega(n)$-formulae such that

\begin{itemize}%
\item $\Lambda$ includes all $\mathcal{L}_\omega(n)$-formulae that are instances of tautologies,

\end{itemize}
and

\begin{itemize}%
\item $\Lambda$ is closed under the inference rule \emph{if $\phi$, $\phi\to \psi \in \Lambda$ then $\psi \in \Lambda$} , i.e. detachment or \textbf{modus ponens}.

\end{itemize}
\end{defn}
One of the basic axiom systems leads to \emph{[[normal modal logics]]}.

\begin{defn}
\label{}\hypertarget{}{}
\textbf{(deducibility)}

Suppose given a [[normal modal logic]], $\Lambda$ in $\mathcal{L}_\omega(n)$. A formula $\phi$ is \textbf{$\Lambda$-deducible} from a set, $\Gamma$ of formulae, if there are finitely many formulae $\psi_0,\ldots,\psi_m\in \Gamma$ such that

\begin{displaymath}
\vdash_\Lambda (\psi_0\to (\psi_1\to (\ldots \to (\psi_m\to \phi)\ldots)
\end{displaymath}
that is the formula $(\psi_0\to (\psi_1\to (\ldots \to (\psi_m\to \phi)\ldots)$ is in $\Lambda$.

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
As the set of all formulae in $\mathcal{L}_\omega(n)$ satisfies the conditions for a logic and any intersection of logics is itself also a logic, we have that given a set of formulae decreed to be `axioms' for a logic, there is a smallest modal logic containing them.

\end{remark}
\hypertarget{common_modal_axioms}{}\subsubsection*{{Common modal axioms}}\label{common_modal_axioms}

\begin{itemize}%
\item ([[axiom K (modal logic)|K]]) $\Box(A \to B) \to \Box A \to \Box B$
\item (M) $\Box A \to A$
\item (4) $\Box A \to \Box \Box A$
\item (5) $\lozenge A \to \Box \lozenge A$
\item (B) $A \to \Box \lozenge A$

\end{itemize}
\hypertarget{Examples}{}\subsection*{{Examples}}\label{Examples}

Here is a brief list of flavors of modal logic. More details are discussed below.

\begin{itemize}%
\item [[epistemic logics]]: it is known to $X$ that, it is common knowledge that (see \hyperlink{EpistemicLogic}{below} for more);


\item [[dynamic logic]]: after the program/computation/action finishes, the program enables, throughout the computation;


\item tense logic: henceforth, eventually, hitherto, previously, now, tomorrow, yesterday, since, until, inevitably, finally, ultimately, endlessly, it will have been, it is being \ldots{}


\item deontic logic: it is obligatory/forbidden/permitted/unlawful that


\item doxastic logic: it is believed that


\item [[Lawvere-Tierney topology|geometric logic]]: it is locally the case that


\item metalogic: it is valid/satisfiable/provable/consistent that (\hyperlink{Goldblatt}{Goldblatt}).

The metalogical version was important in the \href{http://plato.stanford.edu/entries/logic-modal-origins/}{history of modern modal logic}. G\"o{}del played an important role there.


\item [[temporal logic|temporal logics]];


\item [[arrow structures|arrow logics]];


\item [[provability logics]]

\begin{itemize}%
\item [[Löb's axiom]] ([[incompleteness theorem]])

\end{itemize}


\end{itemize}
\hypertarget{semantics}{}\subsection*{{Semantics}}\label{semantics}

We discuss the [[semantics]] of modal logics, its [[models]].

\hypertarget{in_kripke_frames__relational_structures}{}\subsubsection*{{In Kripke frames / relational structures}}\label{in_kripke_frames__relational_structures}

The usual [[semantics]] of modal languages is in terms of [[frame (modal logic)|frames]], and this is where the link with relational structures comes in. (These are quite often called `Kripke frames' as Kripke was one of the first to use relational semantics in this context.

A discussion of the history can be found in (\hyperlink{BlackburnDeRijkeVenema}{BlackburnDeRijkeVenema, page 42}).

(As there is another sense to [[frame]] as the dual of a [[locale]], we need to consider the terminology here and where necessary will use [[frame (modal logic)]] as the entry name.) A more detailed discussion of [[frame (modal logic)|frames]], models and the whole question of the semantics of modal logics is to be found at that entry.

Modal logics are thus also the logics of [[relational structures]], in fact, Blackburn et al (see references) have as their first slogan: \textbf{Modal languages are simple but expressive languages for talking about relational structures.} The temporal logic that satisfies the axiom $(4)$ has models that are [[posets]], for instance, whilst many of the [[epistemic logics]] have models which are sets with equivalence relations on them. In each case, the idea is that the relational structure gives all the possible states of some system and the modal logic describes that system. This explains the great interest in computer science and artificial intelligence of applications of modal logics.

\hypertarget{AlgebraicSemantics}{}\subsubsection*{{Algebraic semantics}}\label{AlgebraicSemantics}

The usual algebraic semantics of modal logic is in terms of Boolean algebras with operators and is described in the entry [[algebraic models for modal logic]].

\hypertarget{coalgebraic_semantics}{}\subsubsection*{{Coalgebraic semantics}}\label{coalgebraic_semantics}

The geometric / relational /Kripke semantics of modal logics are instances of [[coalgebraic model for modal logic|coalgebraic semantics]]. This type of semantics also provides an excellent motivation and intuition for various types of modal logic that arise naturally in computer science.

\hypertarget{CategoricalSemantics}{}\subsubsection*{{Categorical semantics}}\label{CategoricalSemantics}

Every [[category]] comes with its [[internal logic]]. Modal operators in this internal logic can at least sometimes be identified with (co)reflectors into specified [[reflective subcategory|(co)reflective subcategories]]. See at \emph{[[modal type theory]]} for more on this.

Examples for this are [[local toposes]] and [[cohesive toposes]]. See there for more details.

\hypertarget{theorems}{}\subsection*{{Theorems}}\label{theorems}

\begin{itemize}%
\item [[Goldblatt-Thomason theorem]]

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

\begin{itemize}%
\item [[modal hyperdoctrine]]


\item [[modal operator]]


\item [[adjoint modality]]


\item [[adjoint logic]]


\item [[modal type theory]]


\item [[algebraic model for modal logic]]


\item [[geometric model for modal logic]]


\item [[coalgebraic model for modal logic]]


\item [[coalgebra for an endofunctor]]


\item The discussion of ``[[possible worlds semantics]]'' in modal logic is reminiscent of some discussion in the context of the ``[[multiverse]]''.



\end{itemize}
\hypertarget{links}{}\subsection*{{Links}}\label{links}

\begin{itemize}%
\item Stanford Encyclopedia of Philosophy: \emph{\href{http://plato.stanford.edu/entries/logic-modal-origins/}{Modern Origins of Modal Logic}}.


\item Stanford Encyclopedia of Philosophy: \emph{\href{http://plato.stanford.edu/entries/logic-modal/}{Modal Logic}}.



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

A nice historical overview of modern modal logic that might serve as a general introduction as well can be found in

\begin{itemize}%
\item [[R. Goldblatt]], \emph{Mathematical Modal Logic: a View of its Evolution} , in Gabbay, Woods (eds.), \emph{Handbook of the History of Logic vol. 6} , Elsevier Amsterdam 2005. (\href{http://homepages.mcs.vuw.ac.nz/~rob/papers/modalhist.pdf}{draft})

\end{itemize}
One of the earliest texts that exhibits the [[intuitionism|intuitionist]] context is

\begin{itemize}%
\item Oskar Becker, \emph{Zur Logik der Modalit\"a{}ten} , Jahrbuch f\"u{}r Philosophie und ph\"a{}nomenologische Forschung \textbf{11} (1930) pp.497-548. (\href{http://www.digizeitschriften.de/dms/img/?PID=PPN827944462_0011%7CLOG_0010}{digizeit})

\end{itemize}
A standard textbook and reference is

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

\end{itemize}
Two standard references are

\begin{itemize}%
\item P. Blackburn, J. van Benthem, F. Wolter (eds.), \emph{The Handbook of Modal Logic} , Elsevier Amsterdam 2007.


\item [[Marcus Kracht]], \emph{Tools and Techniques in Modal Logic} , Studies in Logic and the Foundation of Mathematics \textbf{142} Elsevier Amsterdam 1999. (\href{http://wwwhomes.uni-bielefeld.de/mkracht/html/tools/book.pdf}{draft})



\end{itemize}
Other texts on modal logic include

\begin{itemize}%
\item [[Dana Scott]], \emph{Advice on Modal Logic}, in [[Karel Lambert]] (ed.) \emph{Philosophical problems in Logic -- Some recent developments}, Reidel 1970

\begin{quote}%
Here is what I consider one of the biggest mistakes in all of modal logic: concentration on a system with just \emph{one} modal operator. (p. 161)


\end{quote}

\item [[Michael Makkai]], [[Gonzalo Reyes]], \emph{Completeness results for intuitionistic and modal logic in a categorical setting}, Annals of Pure and Applied Logic 72 (1995) 25-101

(on [[de dicto and de re]] phenomena in [[hyperdoctrine|hyperdoctrinal]] modal logic)



\end{itemize}
A formulation of modal logic in terms of [[type|typing]] [[judgements]] and [[type formation rules]] is in

\begin{itemize}%
\item [[Frank Pfenning]], Rowan Davies, \emph{A judgemental reconstruction of modal logic}, Mathematical Structures in Comp. Sci., 11(4):511\{540, August 2001. (2000) (\href{http://www.cs.cmu.edu/~fp/papers/mscs00.pdf}{pdf})

\end{itemize}
A discussion of coalgebraic modal logic and of general modal logic in terms of [[coalgebra]] and the [[terminal coalgebra of an endofunctor]] is in

\begin{itemize}%
\item [[Corina Cirstea]], [[Alexander Kurz]], Dirk Pattinson, Lutz Schr\"o{}der and [[Yde Venema]], \emph{Modal logics are coalgebraic} (\href{http://eprints.soton.ac.uk/267144/1/ModalCoalgRev.pdf}{pdf})

\end{itemize}
Formalization of modalities ([[higher modalities]]) in [[homotopy type theory]] appears around definition 1.11 of

\begin{itemize}%
\item [[Egbert Rijke]], [[Bas Spitters]], \emph{Sets in homotopy type theory} (\href{http://arxiv.org/abs/1305.3835}{arXiv:1305.3835})

\end{itemize}
An overview of applications of modal logic in [[linguistics]] can be found in

\begin{itemize}%
\item Lawrence S. Moss, Hans-J\"o{}rg Tiede, \emph{Applications of Modal Logic in Linguistics} , pp.299-341 in Blackburn, van Benthem, Wolter (eds.), \emph{The Handbook of Modal Logic} , Elsevier Amsterdam 2007. (\href{http://www.indiana.edu/~iulg/moss/linguistics.pdf}{draft})

\end{itemize}
[[!redirects modal logic]] [[!redirects modal logics]]



\end{document}