\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*{necessity and possibility}

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

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

[[!include modalities - contents]]

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

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{the_s4_axioms}{The S4 axioms}\dotfill \pageref*{the_s4_axioms} \linebreak
\noindent\hyperlink{the_generality_of_s4}{The generality of S4}\dotfill \pageref*{the_generality_of_s4} \linebreak
\noindent\hyperlink{InFirstOrderLogicAndTypeTheory}{Possible worlds via first-order logic and type theory}\dotfill \pageref*{InFirstOrderLogicAndTypeTheory} \linebreak
\noindent\hyperlink{globally}{Globally}\dotfill \pageref*{globally} \linebreak
\noindent\hyperlink{ViaBaseChangeRelatively}{Relatively}\dotfill \pageref*{ViaBaseChangeRelatively} \linebreak
\noindent\hyperlink{Examples}{Examples}\dotfill \pageref*{Examples} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


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

In the context of [[modal logic]], two key [[modalities]] that one wants to consider are those of \emph{necessity} and \emph{possibility}.

The idea is to consider for any [[proposition]] $p$

\begin{itemize}%
\item a proposition labeled $\Box p$ expressing the idea that ``$p$ is necessarily true'';


\item a proposition labeled $\lozenge p$ expressing the idea that ``$p$ is possibly true''.



\end{itemize}
\hypertarget{the_s4_axioms}{}\subsection*{{The S4 axioms}}\label{the_s4_axioms}

For every comonadic [[modality]] $\Box$, one typically demands that it preserves implication, in the sense that

\begin{displaymath}
\Box(p \to q) \to (\Box p \to \Box q).
\end{displaymath}
This preservation of implication is called the [[K modal logic|K-axiom]]. In traditional non-[[categorical logic]] this is often all that is considered, because in traditional classical modal logic, the operators are considered dual, i.e. $\Box A= \neg (\lozenge (\neg A))$. In an intuitionistic modal logic, one would also demand that $\lozenge$ preserves implication in a suitable sense, such as

\begin{displaymath}
\Box(p\to q) \to (\lozenge p \to \lozenge q).
\end{displaymath}
One may also ask for a further compatibility such as $(\lozenge p \to \Box q) \to \Box(p\to q)$, as \hyperlink{Simpson}{Simpson} does.

Similarly, the axiom $\Box(p \to q) \to (\Box p \to \Box q)$ implies that $\Box$ preserves conjunctions, i.e. $\Box(p\wedge q) \leftrightarrow (\Box p \wedge \Box q)$. The nullary version $\Box(\top)\leftrightarrow \top$ follows from the ``necessitation rule'' which says that if $p$ is provable in the empty context, then so is $\Box p$. (This is an additional rule assumed in modal logics.) From duality, $\Box A= \neg (\lozenge (\neg A))$ it follows that $\lozenge$ preserves disjunctions (both binary and nullary), while intuitionistically one may want to ask for this separately (\hyperlink{Simpson}{Simpson} does, but \hyperlink{BiermanPaiva92}{Biermann and de Paiva} don't).

A minimum further requirement on a formalization of $\Box$ and $\lozenge$ to have the interpretation of ``necessity'' and ``possibility'' is arguably that there are [[implications]]

\begin{itemize}%
\item $\Box p \rightarrow p$;


\item $p \rightarrow \lozenge p$,



\end{itemize}
expressing that if something is necessarily true, then that should mean that it is true in all instances, and that if something is true in one instance, then it is evidently possible for it to be true. With these additions to the above [[K modal logic]], one speaks of [[T modal logic]].

By similar plausibility arguments one often demands that

\begin{itemize}%
\item $\Box p \to \Box \Box p$


\item $\lozenge \lozenge p \to \lozenge p$



\end{itemize}
which may be read as expressing that iterating the previous reasoning does not yield any new insight. This additional enhancement to T modal logic yields \emph{[[S4 modal logic]]}.

\hypertarget{the_generality_of_s4}{}\subsubsection*{{The generality of S4}}\label{the_generality_of_s4}

In terms of [[categorical logic]] interpreting propositional logic into a [[Heyting algebra]], the S4 axioms just say (\hyperlink{BiermanPaiva92}{Bierman \& de Paiva 92}) that

\begin{itemize}%
\item $\Box$ is a (necessarily [[idempotent comonad|idempotent]]) [[comonad]] which is [[monoidal functor|monoidal]], hence product-preserving; and


\item $\lozenge$ is a (necessarily [[idempotent monad|idempotent]]) [[monad]] which is a ``$\Box$-[[strong functor|strong]] functor'', and (perhaps) preserves coproducts.



\end{itemize}
As usual, we can also replace the Heyting algebra by a [[cartesian closed category]], thereby obtaining a ``proof-relevant'' system; in this case monoidality of $\Box$ doesn't imply directly that it preserves products, although one might reasonably ask that it does. See \emph{[[monad in computer science]]}.

The above reasoning makes plausible that any operators expressing ``necessity'' and ``possibility'' should \emph{at least} satisfy these (co)monad axioms. However, not every (co)monad is sensibly interpreted this way.

For example, there is

\begin{itemize}%
\item the (idempotent) comonad $\emptyset$ which sends every proposition to [[false]] (the [[nothing|non-being]]-modality);


\item the (idempotent) monad $\ast$ which sends every proposition to [[true]] (the [[being]]-modality).



\end{itemize}
These $\emptyset \dashv \ast$ satisfy all of the above axioms (as well as more axioms that are being considered, such as those called [[S5 modal logic]]) but they are not a very good interpretation of the informal concepts of ``possibility'' and ``necessity''. Under this interpretation nothing is necessarily true, and everything is possibly true. While this is not nonsensical, it is not very interesting and doesn't correspond well to our intuitive meanings of ``necessary'' and ``possible''.

This issue becomes more pronounced as one generalizes from the small realm of [[propositional logic]] to include both or either of:

\begin{itemize}%
\item [[types]] more general than [[propositions]] (in [[modal type theory]]);


\item [[first-order logic]] with [[quantifiers]], hence [[hyperdoctrines]]/[[dependent types]].



\end{itemize}
There are many [[modal operators]] in such contexts which are all modeled by (idempotent) (co)monads but which do not have the interpretation of expressing the modes of ``necessity'' or ``possibility''. See at \emph{[[modal operator]]} for some examples.

Therefore it makes sense to ask which \emph{additional} axioms on a modal operator make it an accurate formalization of the informal concepts of necessity and possibility. The answer to this may depend on context and intention (after all one is trying to find a precise formulation of an a priori informal idea).

\hypertarget{InFirstOrderLogicAndTypeTheory}{}\subsection*{{Possible worlds via first-order logic and type theory}}\label{InFirstOrderLogicAndTypeTheory}

One common philosophical interpretation of ``necessarily'' and ``possibly'' is in terms of a collection of ``possible worlds'' that are similar to the ``real world'', but not the same. Under this interpretation, a proposition is necessarily true if it is true in all possible worlds, and possibly true if it is true in some possible world.

Now the idea of a proposition being true ``necessarily in all possible cases'' or ``possibly at least in one case'' is formally very well established in \emph{predicate} logic: it is just the interpretation of the [[universal quantifier]] ``for all'' $\forall$ and of the [[existential quantifier]] ``there exists'' $\exists$. In [[categorical logic]], these [[quantifiers]] (see there for details) are part of an [[adjoint triple]] whose middle piece is [[context]] extension, and as such they naturally induce a [[comonad]] and a [[monad]]. Thus, if we interpret ``necessarily'' and ``possibly'' in terms of possible worlds, we can model them by this base change adjoint triple.

\hypertarget{globally}{}\subsubsection*{{Globally}}\label{globally}

In more detail, let $W$ be the [[context]] [[type]] of [[variables]]/[[terms]] on which the propositions depend, i.e. the collection ``of all [[possible worlds semantics|possible worlds]]''. Any specific choice of $W$ may be taken as specifying what is to be understood as a ``possible world''.

Writing $\mathbf{H}_{\ast}$ for the [[category]] of all context-free [[types]] under consideration and writing $\mathbf{H}_{/W}$ for the category of types in [[context]] ``$W$'', then in [[categorical logic]] (for instance $\mathbf{H}_{/(-)}$ might be a [[hyperdoctrine]] over a [[category of contexts]] containing objects $W$ and $\ast$) the [[quantifiers]] $\forall_{x\colon X}$ and $\exists_{x\colon X}$ participate in a [[base change]] [[adjoint triple]]

\begin{displaymath}
(\exists_W \dashv W^\ast \dashv \forall_W)
  \;\colon\;
  \mathbf{H}_{/W}
    \stackrel{\stackrel{\forall_{w \colon W}}{\longrightarrow}}{\stackrel{\stackrel{W^\ast}{\longleftarrow}}{\underset{\exists_{w\colon W}}{\longrightarrow}}}
  \mathbf{H}
  \,.
\end{displaymath}
In a context of pure [[logic]] this would be called

[[existential quantifier]] $\dashv$ [[context extension]] $\dashv$ [[universal quantifier]]

whereas in a context of [[dependent type theory]] this would be called

[[dependent sum]] $\dashv$ [[context extension]] $\dashv$ [[dependent product]].

In either case, under the suitable version of [[propositions as types]] (and using [[bracket types]] etc. if desired), the operations $\forall$ and $\exists$ have the usual interpretation of ``for all'' and ``there exists''.

Note, however, that these operations change the context from $W$ to $\ast$. In other words, if a proposition $P$ depends on $W$, so that it may be true in some worlds and false in others, then $\exists_W P$ and $\forall_W P$ no longer depend on $W$. The idea of a necessity and a possibility modality is to send a proposition in some context to a proposition in the \emph{same} context, so that we can for instance say that $\Box P \to P$ and so on. Thus we need to make $\exists_W P$ and $\forall_W P$ into propositions that again depend on $W$ --- even if they now depend trivially on $W$, being [[context extension|extended]] back from the absolute context $\ast$ to $W$.

This is just what is accomplished by passing from the above [[adjoint triple]] to the induced [[adjoint pair]] on $\mathbf{H}_{/W}$ by forming composites with the [[context extension]] operation $W^\ast$

\begin{displaymath}
(\underset{W}{\lozenge} \dashv \underset{W}{\Box})
  \coloneqq
  \left(
     \left(
     W^\ast \circ \underset{w\colon W}{\exists}
     \right)
     \dashv
     \left(
     W^\ast \circ \underset{w\colon W}{\forall}
     \right)
  \right)
  \;\colon\;
  \mathbf{H}_{/W}
    \longrightarrow
  \mathbf{H}_{/W}
  \,.
\end{displaymath}
With this, if $p\in \mathbf{H}_{/W}$ is a [[proposition]] about terms $w$ of $W$ (a $W$-[[dependent type]]) then

\begin{itemize}%
\item $\underset{W}{\lozenge}(p)$ is [[true]]/[[inhabited type|inhabited]] precisely if $\underset{w \colon W}{\exists} p(w)$ is [[true]]/[[inhabited type|inhabited]], hence (that is the standard interpretation of the [[quantifier]]) if it is possible for $p(w)$ to be true for some $w$;


\item $\underset{W}{\Box}(p)$ is [[true]]/[[inhabited type|inhabited]] precisely if $\underset{w \colon W}{\forall} p(w)$ is [[true]]/[[inhabited type|inhabited]], hence (that is again the standard interpretation of the quantifier) if $p(w)$ necessarily holds for all $w$.



\end{itemize}
(Note that there is also an adjoint pair on $\mathbf{H}_{/\ast}$ in which the left adjoint is given by context extension back to $\mathbf{H}_{/W}$ followed by $\exists_W$, and dually the right adjoint is given by $W^\ast$ followed by $\forall_W$. The former is the [[writer comonad]], whereas the latter is the [[function monad]] (or reader monad).)

Thus, this gives one [[syntax|syntactic]] formalization of the informal meaning of ``necessity'' and ``possibility''. The natural [[semantics]] for these [[base change]] operations is a generalization of the simple traditional \emph{[[possible worlds semantics]]} of propositional necessity and possibility modalities. (There are, however, more complicated possible worlds semantics.)

Moreover, with this formalization, the modal operator $\underset{W}{\lozenge}$ is [[left adjoint]] to $\underset{W}{\Box}$ and hence both form an [[adjoint modality]]. As discussed there, this is a formalization of [[unity of opposites|opposite]] concepts, which reflects well the opposition of necessity and possibility in their informal meaning.

Some technical remarks:

\begin{enumerate}%
\item In general, $\underset{W}{\lozenge}$ and $\underset{W}{\Box}$ as defined above are, while being a [[monad]] and [[comonad]], respectively, not an [[idempotent monad]] and [[idempotent comonad]] if generalized from [[first-order hyperdoctrines]] to more general [[dependent type theories]]. But this just reflects the usual issues with [[propositions as types]], see there for more discussion.


\item While [[base change]]-[[adjunctions]] are essentially unique and not free to choose, there is a genuine choice in the above given by the choice of [[context]] $W$. This is reflected in the subscripts of $\underset{W}{\lozenge}$ and $\underset{W}{\Box}$ above. It is the choice of this $W$ that gives different kinds of possibility and necessity. More generally there is in fact not just a choice of a context, but of a morphism of contexts, reflecting what is often called ``accessibility of possible worlds''. This we come to \hyperlink{ViaBaseChangeRelatively}{below}.



\end{enumerate}
\hypertarget{ViaBaseChangeRelatively}{}\subsubsection*{{Relatively}}\label{ViaBaseChangeRelatively}

With this axiomatization via [[base change]], it is immediate to consider the relative case where instead of [[base change]] to a [[unit type]] $W \to \ast$ one considers [[base change]]

\begin{displaymath}
(\exists_\omega \dashv \omega^\ast \dashv \forall_\omega)
  \;\colon\;
  \mathbf{H}_{/W}
    \stackrel{\stackrel{\forall_{w \colon \omega^{-1}(-)}}{\longrightarrow}}{\stackrel{\stackrel{\omega^\ast}{\longleftarrow}}{\underset{\exists_{w\colon \omega^{-1}(-)}}{\longrightarrow}}}
  \mathbf{H}_{/W_0}
  \,.
\end{displaymath}
along any [[morphism]]

\begin{displaymath}
\omega \colon W \longrightarrow W_0
\end{displaymath}
and set

\begin{displaymath}
(\underset{\omega}{\lozenge} \dashv \underset{\omega}{\Box})
  \coloneqq
  \left(
     \left(
     \omega^\ast \circ \underset{w\colon \omega^{-1}(-)}{\exists}
     \right)
     \dashv
     \left(
     \omega^\ast \circ \underset{w\colon \omega^{-1}(-)}{\forall}
     \right)
  \right)
  \;\colon\;
  \mathbf{H}_{/W}
    \longrightarrow
  \mathbf{H}_{/W}
  \,.
\end{displaymath}
If here $\omega$ is an [[effective epimorphism]] (a [[1-epimorphism]]) then it exibits an [[equivalence relation]] on $W$, where $w_1\sim w_2$ is given by $\omega(w_1) = \omega(w_2)$. In traditional [[possible worlds semantics]] such equivalence relation is called an ``accessibility relation between possible worlds''. Now

\begin{itemize}%
\item $\underset{\omega}{\lozenge} p$ is true/inhabited at $w\in W$ iff it is true/inhabited at at least one $\tilde w$ in the same equivalence class of $w$;


\item $\underset{\omega}{\Box} p$ is true/inhabited at $w\in W$ iff it is true/inhabited at all $\tilde w$ in the same equivalence classes of $w$.



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

Historically, one informal example whose formalization in [[modal logic]] has been controversially discussed (see for instance \hyperlink{IEPCarnapModal}{IEP ``Rudolf Carnap: Modal Logic''}) is the pair of informal assertions

\begin{enumerate}%
\item ``9 is necessarily greater than 7.''


\item ``The number of planets in the solar system is 9.''



\end{enumerate}
(\textbf{Remark.} It maybe adds to the joy of modal logic to notice that the second sentence, which was regarded as true in our world at the time the above example was brought up, actually \href{http://www.universetoday.com/15568/how-many-planets-are-in-the-solar-system/}{no longer is}. Of course this only highlights that indeed this statement is not to be expected to be ``necessarily true'' in any sense.)

The issue with this example is that if one does not fix a decent formalization of these statements, then naively they seem to imply as correct the statement ``The number of planets in the solar system is necessarily greater than 7.'', which however sounds like it ought to be wrong.

We now formalize and then analyze this example with the \hyperlink{InFirstOrderLogicAndTypeTheory}{above} prescription.

So let $W$ be any [[type]], to be thought of as the type of [[possible worlds]]. Write

\begin{displaymath}
w\colon W \vdash \mathbb{N}(w) \colon Type
\end{displaymath}
for the $W$-dependent type that is constant on the ordinary [[type of natural numbers]], i.e.$\mathbb{N}(w) = \mathbb{N}$ for all $w\colon W$.

The terms of $\mathbb{N}$, i.e. the [[natural numbers]], canonically extend to $W$-dependent terms of this dependent type

\begin{displaymath}
w\colon W \vdash 9 \colon \mathbb{N}(w)
\end{displaymath}
namely to the constant terms, which take the same value (here: 9) for all $w \colon W$.

In contrast to this, assume now that $W$ is such there is at least one non-[[constant function]] $W \to \mathbb{N}$. In fact, in the spirit of the informal problem at hand, we require a surjective function. This gives a non-constant term of the constantly $W$-dependent type of natural numbers, which we may just as well call

\begin{displaymath}
w \colon W \vdash NumberOfPlanetsInSolarSystem(w) \colon \mathbb{N}(w)
  \,.
\end{displaymath}
That is the formalization of the above example we consider, and it should be evident enough. Now we may step back and see what the \hyperlink{InFirstOrderLogicAndTypeTheory}{above formalization} produce from this.

So consider the $W$-dependent [[identity type]]

\begin{displaymath}
w \colon W \vdash (9 = NumberOfPlanetsInTheSolarSystem)(w) \colon Type
  \,.
\end{displaymath}
By the assumption that $NumberOfPlanetsInTheSolarSystem(w)$ is not constant in $W$ it follows that the [[dependent product]] over $W$ of that dependent identity type is the [[empty type]], and so the same is true for $\Box_W$ applied to it:

\begin{itemize}%
\item $[\Box_W (9 = NumberOfPlanetsInTheSolarSystem)]$ is [[false]].

\end{itemize}
However, if we assume that there is one $w$ for which indeed $NumberOfPlanetsInTheSolarSystem(w)$ takes the value 9, then the [[dependent sum]] over the dependent identity type contains that coincidence as a term, and so $\lozenge_W$ of our dependent identity type is [[inhabited type|inhabited]]. Hence

\begin{itemize}%
\item $[\lozenge_W (9 = NumberOfPlanetsInTheSolarSystem)]$ is [[true]].

\end{itemize}
In English words, these formal consequences are to be pronounced as:

\begin{enumerate}%
\item ``It is false that it is necessary that the number of planets in the solar system is 9.''


\item ``It is true that it is possible that the number of planets in the solar system is 9.''



\end{enumerate}
Which is just as it should be.

Similarly, the $W$-dependent type

\begin{displaymath}
w \colon W \vdash (NumberOfPlanetsInTheSolarSystem \gt 7)(w) \colon \mathbb{N}(w)
\end{displaymath}
is only going to be [[inhabited type|inhabited]] if indeed the value $NumberOfPlanetsInTheSolarSystem(w)$ is greater than 7 for all $w\colon W$. With our formalization assumption above this is not the case, and so one finds that

\begin{itemize}%
\item $[\Box_W (NumberOfPlanetsInTheSolarSystem \gt 7)]$ is [[false]].

\end{itemize}
hence

\begin{itemize}%
\item ``It is false that it is necessary that the number of planets in the solar system is greater than 7.''

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

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

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

In

\begin{itemize}%
\item [[Kant]], \emph{Critique of pure reason} 1781

\end{itemize}
is discussion of \emph{modality} as one of the [[category (philosophy)|categories of pure thought]], with sub-categories \emph{necessity}, \emph{possibility} and \emph{actuality} (Wirklichkeit).

In

\begin{itemize}%
\item [[Georg Hegel]], \href{http://ncatlab.org/nlab/show/Science+of+Logic#DieWirklichkeit}{book 2, section 3}, especially \href{http://ncatlab.org/nlab/show/Science+of+Logic#DieWirklichkeitKapitel2}{book 2, section 3, chapter 2} in \emph{[[Science of Logic]]} (1812)

\end{itemize}
this is picked up and claimed to be refined to a [[dialectic]] system of [[unity of opposites|unities of opposites]].

\begin{itemize}%
\item [[Saul Kripke]], \emph{[[Naming and Necessity]]} (1980)


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


\item [[Jake Chandler]], \emph{Modality: Necessity and Possibility}, lecture notes (\href{http://www.jakechandler.com/assets/2006MetaphysicsBBK/%5B6%5D%20%5BModality%5D.pdf}{pdf})


\item Gavin Bierman and [[Valeria de Paiva]], \emph{On an Intuitionistic Modal Logic}, Studia Logica (65):383-416, 2000 (preprint from 1992) (\href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.30.5279}{web})


\item Alex K. Simpson, \emph{The Proof Theory and Semantics of Intuitionistic Modal Logic}, Ph.D. Thesis, University of Edinburgh, 1994, \href{http://homepages.inf.ed.ac.uk/als/Research/thesis.pdf}{web}.


\item Internet Encyclopedia of Philosophy, \emph{\href{http://www.iep.utm.edu/cmlogic/}{Rudolf Carnap: Modal Logic}}



\end{itemize}
[[!redirects necessity]] [[!redirects possibility]]

[[!redirects necesecarily]] [[!redirects possibly]]



\end{document}