\documentclass[draft]{article}
\usepackage{setspace}
\usepackage{latexsym}
\input linear
\input theorem
\input prooftree
\title{A Judgmental Deconstruction of Modal Logic}
\author{Jason Reed}
\bibliographystyle{alpha}
\def\pprov{\dashv\vdash}
\def\provpd{\prov_{\hbox{\tiny PD}}}
\def\provll{\prov_{\hbox{\tiny LL}}}
\def\amp{\&}
\def\easyrule#1#2{\begin{prooftree}#1\justifies #2\end{prooftree}}
\def\gap{\quad\hfil\quad}
\def\lax{\bigcirc}
\def\dia{\Diamond}
\def\rprop{\mathop{\mathsf {prop}}\nolimits}
\def\rtrue{\mathop{\mathsf {true}}\nolimits}
\def\rlax{\mathop{\mathsf {lax}}\nolimits}
\def\rposs{\mathop{\mathsf {poss}}\nolimits}
\def\rvalid{\mathop{\mathsf {valid}}\nolimits}
\def\adjust{{\downharpoonright}}
\begin{document}
\maketitle
\begin{abstract}
The modalities $\square$ and $\lax$ of necessary and lax truth
described by Pfenning and Davies can be seen to arise from the same pair
of adjoint logical operators $F$ and $U$, which pass in both
directions between two judgments of differing strength. This may be
generalized to a logic with many such adjunctions, across judgments
subject to different substructral disciplines, allowing explanation of
possibility $\dia$, linear logic's modality $!$, and
intuitionistic labelled deduction as well.
\end{abstract}
\section{Introduction}
Insidious rumors may have reached your ears to the effect of
\begin{itemize}
\item In judgmental modal S4 \cite{pfenning-davies01} according to
  Pfenning and Davies, the validity judgment itself is
  right-asynchronous and left-synchronous
\item In linear logic \cite{linear87}, the modality ! is made of two mysterious
  `half-connectives'
\item The point of judgments \cite{siena.lectures} is to allow the same proposition to be judged in different ways
\end{itemize}

The goal of this note is to clear up the confusion: Judgments are not
left- or right-asynchronous or -synchronous or anything else of the
sort.  $!, \square, \lax$ are each constituted from two perfectly
ordinary and well-behaved logical connectives --- given a certain
generosity of interpretation, the {\em same} two.

Moreover, there is no particular need when simply defining a modal
logic to have many different judgments upon exactly the same underlying
logical data. Nothing {\em prevents} us from doing so --- nothing ever
prevents us from defining whatever predicates we like after the fact
--- but the typical judgments that encode {\em modes of truth} may
fruitfully be arranged so that {\em different} modes of truth are to
be predicated on entirely {\em different} classes of propositions. In
short, it is helpful to live in a world where the sort of thing that
is eligible to be true is different from the sort of thing that is
eligible to be, for instance, {\em necessarily} true. In a slogan:
\begin{center}Different judgments judge different things.\end{center}

But don't worry: there is still a circumstance that allows us to not
lose the expressive power we thought we had a moment ago, when one and
the same proposition could be proven or supposed true, necessary,
possible, lax, constructible from the current set of resources, true
at time $t$, true according to agent $K$, and so forth: it is the
ubiquity of unary logical connectives that act as {\em coercions}
between different judgments, i.e.  different notions of truth. Indeed
in everyday life we depend on some kind of transport between the
propositions we utter and those uttered by our neighbors to bring them
into correspondence, but, as the category theorists admonish us, we
should not confuse {\em identity} with {\em isomorphism}.

And of course we should not necessarily expect every round-trip around
these propositional transportations to be the identity. It becomes
evident in fact that the most common and familiar modal operations are
precisely the `failure of holonomy' of certain paths among modes of truth.

\section{Language}
The logical language described below, call it `adjoint logic', is parametrized by a set $M$ of
modes of truth, together with a preorder (reflexive, transitive
relation) $\le$ on $M$.  For typical elements of $M$ we use the
letters $p,q,r$.
%, and $\alpha,\beta$ for variables standing for the
% same.

For each $p\in M$, there is a notion of proposition-at-$p$. Its syntax is as follows
$$\begin{tabular}{r@{ }c@{ }l}
$A_p$&$::=$&$F_{q\ge p}A_q \celse U_{q\le p}A_q \celse A_p \land_p A_p \celse A_p \lor_p A_p \celse A_p \imp_p A_p \celse \top_p \celse \bot_p \celse a_p$\\
\end{tabular}$$
The subscript $p$ on the familiar logical connectives indicates that
formally we are keeping track of {\em where} (i.e at which mode of
truth) the conjunction, disjunction, implication is taking
place. Likewise there is a separate class of atomic propositions $a_p$
for each $p$. The notation $F_{q\ge p}$ and $U_{q\le p}$ is meant to
convey that {\em if} $q \ge p$ in the preorder structure supposed on
$M$, then $F_{q\ge p}$ is in fact allowed to be used as a logical
connective, and similarly for $U$ with the inequality running the
opposite direction.

We are careful {\em not} to indulge in the Martin-L\"ofian absurdity of saying 
$$
\begin{prooftree}
\prov A_q \rprop_q \qquad \prov q \ge p
\justifies
\prov F_{q \ge p}A_q \rprop_p
\end{prooftree}
$$
as if this defined the syntax of propostions via inference rules on
the same putative footing as those that tell us how to {\em prove}
$F_{q \ge p}A_q$, despite the absence of anything telling us where the
{\em subject} $F_{q \ge p}A_q$ of the allegedly one-place judgment
$\rprop_p$ (`is a proposition-at-$p$') {\em comes} from in the first place.

Instead, if
forced to used inference rules, we would much better
say
$$
\begin{prooftree}
\prov \rprop_q \qquad \prov q \ge p
\using F
\justifies
\prov \rprop_p
\end{prooftree}
$$
reserving $F$ for simply the {\em name} of the inference rule itself,
and taking $\rprop_p$ instead as a zero-place predicate `{\em there
  is} a proposition-at-$p$'.  The constructive reading of `if there is
a proposition at $q$, and $q\ge p$, then there is a proposition at
$p$' gives us precsisely what we want --- the set of propositions is
precisely the set of proofs that the set of propositions is inhabited.

\section{Proofs}
We now give a sequent calculus for adjoint logic and observe that it is
internally sound and complete.

A context $\Gamma$ is something of the grammar
$$\begin{tabular}{rcl}
$\Gamma$&$::=$&$\cdot \celse \Gamma, A_p \rtrue_p$
\end{tabular}$$
For the time being we will
ignore substructural logics and suppose that all hypotheses are
subject to weakening and contraction as in ordinary intuitionistic
logic. Linear and other substructural logics are taken up in Section~\ref{section.linearlogic}.

A sequent, the sort of thing amenable to {\em being provable}, 
is something of the form
$$\Gamma \prov A_p \rtrue_p$$ subject to the restriction that for
every $A_q \rtrue_q \in\Gamma$, we have $q \ge p$. Lest this
requirement pass too quickly by the reader's eyes, it should be noted
that it is the central mechanism by which modalities have any force in
the logic. If $\le$ is viewed as ordering modes of truth by strength,
we are positing that it {\em does not make sense} to think about a
entailing a proposition under a certain mode of truth if it is subject
to any hypotheses of a {\em weaker} mode of truth.

The rules of the sequent calculus are as follows, omitting the
judgmental scaffolding $\rtrue_p$ and the subscript $p$ on connectives
when the choice of $p$ is obvious from context. They include the
familiar hypothesis rule and left and right rules for all the standard
connectives:

\begin{center}
\vskip-2em
\setstretch{4}
\footnotesize
$
\begin{prooftree}
\using hyp
\justifies
\Gamma, a_p \prov a_p
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma\prov A_p \qquad \Gamma \prov B_p
\using{\land R}
\justifies
\Gamma\prov A_p \land B_p
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma, A_p, B_p\prov C_r
\using{\land L}
\justifies
\Gamma, A_p \land B_p \prov C_r
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma\prov A_p
\using{\lor R_1}
\justifies
\Gamma\prov A_p \lor B_p
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma\prov B_p
\using{\lor R_2}
\justifies
\Gamma\prov A_p \lor B_p
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma, A_p\prov C_r \qquad \Gamma, B_p \prov C_r
\using{\lor L}
\justifies
\Gamma, A_p \lor B_p \prov C_r
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma,A_p \prov B_p
\using{\imp R}
\justifies
\Gamma\prov A_p \imp B_p
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma \prov A_p \qquad \Gamma, B_p \prov C_r
\using{\imp L}
\justifies
\Gamma, A_p \imp B_p \prov Cr
\end{prooftree}
$
\gap
$
\begin{prooftree}
\using \bot L \justifies
\Gamma, \bot_p\prov C_r
\end{prooftree}
$
\gap
$
\begin{prooftree}
\using \top R \justifies
\Gamma\prov \top_p
\end{prooftree}
$
\end{center}
as well as rules for $F$ and $U$:
\begin{center}
\vskip-2em
\setstretch{4}
\footnotesize
$
\begin{prooftree}
\Gamma\prov A_q
\using{U R}
\justifies
\Gamma\prov U_{q\le p}A_q
\end{prooftree}
$
\gap
$
\begin{prooftree}
q \ge r \qquad \Gamma, A_q \prov C_r
\using{U L}
\justifies
\Gamma, U_{q\le p}A_q \prov C_r
\end{prooftree}
$
\gap
$
\begin{prooftree}
\Gamma\adjust_{\ge q}\prov A_q
\using{F R}
\justifies
\Gamma\prov F_{q\ge p}A_q
\end{prooftree}
$
\gap
$
\begin{prooftree}
 \Gamma, A_q \prov C_r
\using{F L}
\justifies
\Gamma, F_{q\ge p}A_q \prov C_r
\end{prooftree}
$
\end{center}
where $\Gamma \adjust_{\ge q}$ means the context made of only those
$A_p \rtrue_p$ found in $\Gamma$ such that $p\ge q$.

We then have
\begin{lemma}[Cut Admissibility]
For any $\Gamma, p, r$ such that $p \le r$ and every $\rtrue_q$ in $\Gamma$ has $q \le p$, if $\Gamma \prov A_p$ and $\Gamma, A_p \prov C_r$,
then $\Gamma\prov C_r$.
\end{lemma}
\begin{proof}
By induction on $A_p$ and the relevant derivations,
using standard structural cut elimination techniques \cite{Pfenning95lics,Pfenning00ic} \cqed
\end{proof}
and
\begin{lemma}[Identity]
For any $A_p$, we have $A_p \prov A_p$
\end{lemma}
\begin{proof}
By induction on $A_p$.
\cqed
\end{proof}

Some comments are due about the behavior of this system with respect
to Andreoli-style focusing \cite{andreoli.focusing92}: $U$ is a {\em negative}
connective, left-synchronous and right-asynchronous, and $F$ is
conversely {\em positive}, i.e. left-asynchronous and
right-synchronous. Without proving that focusing discipline is
correct for the entire system, a task for another paper, we can at
least observe that $U$ is invertible on the right precisely because it
moves `with the grain' with respect to the central invariant on
sequents that their right sides are $\le$-smaller than their left, for
$U$ as it is stripped away only transports the right side of the
sequent to a mode of truth that is {\em even smaller} by $\le$ than it
already was, which by the assumed transitivity of $\le$ guarantees the
invariant is still satisfied. We find $F$ is invertible on the left
for exactly the same reason.

\section{Representations}
In this section we discuss how various logics and logical features can be construed as
special cases of adjoint logic.
\subsection{Pfenning-Davies $\square$}
Pfenning and Davies \cite{pfenning-davies01} describe an
intuitionistic alethic modal logic which, if rendered classical by the
addition of suitable axioms, is equivalent to the familiar classical
modal logic S4.

The entailment relation has the form
$$\Delta; \Gamma \provpd A $$
where $\Delta$ is something of the form $A_1\rvalid, \ldots, A_n\rvalid$,
and $\Gamma$ of the form $A_1\rtrue, \ldots A_n \rtrue$.

The important rules natural deduction for our purposes are introduction
and elimination for $\square$, and the use of valid hypotheses:

$$
\easyrule{\Delta;\Gamma\provpd \square A\qquad \Delta, A \rvalid;\Gamma\provpd C}
{\Delta;\Gamma\provpd C}\qquad
\easyrule{\Delta;\cdot\provpd A}{\Delta;\Gamma \provpd \square A}\qquad
\easyrule{}{\Delta, A \rvalid;\Gamma\provpd A}
$$
This logic corresponds to a simple subset of adjoint logic for $M$ being the
preorder with two points, call them $t$ and $v$, in which $t \le v$
and not $v \le t$. The subset we need contains the traditional
connectives (as well as $F$) only at $t$, and the only connective at
all at the mode $v$ is $U$. Formally, we are only considering

$$\begin{tabular}{rcl}
$A_v$&$::=$&$U_{t\le v}A_t$\\
$A_t$&$::=$&$F_{v\ge t}A_v  \celse A_t \land_t A_t \celse A_t \lor_t A_t \celse A_t \imp_t A_t \celse \top_t \celse \bot_t \celse a_t$\\
\end{tabular}$$

Note that there is only one pertinent $F$ and one $U$ in this system
so we can refer to them as simply $F$ and $U$.  Let the translation
$A^*$ of a PD proposition $A$ be $A$ with every $\square$
replaced by $FU$ and every other connective replaced by the
appropriate $t$-subscripted analogue.

We then have (lifting operations such as $\dash^*$ and $U$ to contexts in the evident way)
\begin{theorem}\ 
\begin{itemize}
\item $\Delta; \cdot \provpd A$ iff $U\Delta^* \prov  UA^* \rtrue_v$ 
\item $\Delta; \Gamma \provpd A$ iff $U\Delta^*, \Gamma^* \prov A^* \rtrue_t$ 
\end{itemize}
\end{theorem}
\begin{proof}
By induction on the relevant derivations, taking advantage of the fact
that $U$ is invertible on the right, the substitution principle for
the natural deduction system, and identity and cut admissibility for
the sequent calculus. \cqed
\end{proof}

The correspondence between $A \rvalid$ in the PD system
and $UA^*$ in adjoint logic reveals that the vague
notion that $\rvalid$ was somehow `intrinsically negative as a
judgment' (and therefore compatible with left focus, and appearing
only transiently on the right by dint of being asynchronous there) is
really an epiphenomenon of it systematically concealing a perfectly
ordinary negative connective $U$.

We might as well have begun by defining a `native' sequent calculus for PD modal
logic, perhaps by the rules
$$
\easyrule{\Delta;\Gamma, A\rtrue \provpd C}
{\Delta, A\rvalid;\Gamma\provpd C}\qquad
\easyrule{\Delta;\cdot\provpd A}{\Delta;\Gamma\provpd \square A}\qquad
\easyrule{\Delta, A \rvalid;\Gamma\provpd C}{\Delta;\Gamma,\square A \provpd C}
$$
in which case we can see that the process of decomposing a $\square$ on either side of the turnstile is isomorphic to that of decomposing $FU$.
On the left, consider
$$
\easyrule
{\Delta, A \rvalid;\Gamma \prov C}
{\Delta;\Gamma,\square A \rtrue \prov C}
\qquad\Longleftrightarrow\qquad
\begin{prooftree}
\Gamma, UA^* \rtrue_v \prov C^* 
\justifies
\Gamma, FUA^* \rtrue_t \prov C^*
\end{prooftree}
$$
and furthermore the erstwhile structural `copy' rule becomes simply
the left rule for $U$.
$$
\easyrule
{\Delta;\Gamma, A \rtrue \prov C}
{\Delta, A \rvalid;\Gamma \prov C}
\qquad\Longleftrightarrow\qquad
\begin{prooftree}
\Gamma, A^* \rtrue_t \prov C^* 
\justifies
\Gamma, UA^* \rtrue_v \prov C^*
\end{prooftree}
$$
Meanwhile on the right we see the correspondence
$$
\easyrule
{\Delta; \cdot \prov A\rtrue}
{\Delta;\Gamma\prov \square A \rtrue}
\qquad\Longleftrightarrow\qquad
\begin{prooftree}
\[
\Gamma\adjust_{\ge v} \prov C^*\rtrue_t
\justifies
\Gamma\adjust_{\ge v} \prov UC^*\rtrue_v
\]
\justifies
\Gamma \prov FUC^*\rtrue_t
\end{prooftree}
$$ 
where the forced sequencing on the right is justified by essentially
focusing reasoning since $U$ is right-asynchronous --- once we
decompose the $F$ there is no reason not to continue decomposing the
$U$.

\subsection{Pfenning-Davies $\lax$}

The Pfenning-Davies account of lax logic (also found in
\cite{pfenning-davies01}) is concerned with a different modality $\lax$,
defined by allowing the entailment to be one of the two forms
$$\Gamma \provpd A \rtrue \qquad \Gamma \provpd A \rlax$$
for $\Gamma$ consisting only of hypotheses of the form $A \rtrue$,
and giving the rules
$$
\easyrule{\Gamma \prov \lax A \qquad \Gamma, A \provpd C \rlax}
{\Gamma \provpd C \rlax}
\qquad
\easyrule{\Gamma\provpd A \rlax}{\Gamma\provpd \lax A \rtrue}
\qquad
\easyrule{\Gamma\provpd A \rtrue}{\Gamma\provpd A \rlax}
$$

Somewhat remarkably, the subset required for encoding
$\lax$ is the same as that for $\square$ but upside-down.
We again take the two-point preorder, this time calling the two points $\ell \le t$ (though it should be noted that the names do not actually matter!) and inhabiting only the mode $t$ with most of the connectives:
$$\begin{tabular}{rcl}
$A_t$&$::=$&$U_{\ell \le t}A_\ell  \celse A_t \land_t A_t \celse A_t \lor_t A_t \celse A_t \imp_t A_t \celse \top_t \celse \bot_t \celse a_t$\\
$A_\ell$&$::=$&$F_{t\ge \ell}A_t$\\
\end{tabular}$$

The translation in this case requires that $A^*$ replaces every
occurrence of $\lax$ with $UF$, and every other connective with its
$t$-subscripted twin.  The theorem that realizes the encoding's
adequacy is
\begin{theorem}\ 
\begin{itemize}
\item $\Gamma \provpd A \rtrue$ iff $\Gamma^* \prov  A^*$
\item $\Gamma \provpd A \rlax$ iff $\Gamma^* \prov FA^*$
\item $\Gamma, A \provpd C \rlax$ iff $\Gamma^*, FA^* \prov FC^*$
\end{itemize}
\end{theorem}
\begin{proof}
By induction on the relevant derivations, taking advantage of the fact
that $F$ is invertible on the left, the substitution principle for
the natural deduction system, and identity and cut admissibility for
the sequent calculus. \cqed
\end{proof}

Here we find that the `structural' rule that allows us to infer $A \rtrue$ from m $A \rlax$ is none other than the right rule for the connective $F$.

It is perspicuous again to consider the `native' sequent calculus
rules for the PD lax modality, namely
$$
\easyrule{  \Gamma, A \provpd C \rlax}
{\Gamma, \lax A  \provpd C \rlax}
\qquad
\easyrule{\Gamma\provpd A \rlax}{\Gamma\provpd \lax A \rtrue}
\qquad
\easyrule{\Gamma\provpd A \rtrue}{\Gamma\provpd A \rlax}
$$
and identify the relationships 
$$
\easyrule{  \Gamma, A \provpd C \rlax}
{\Gamma, \lax A  \provpd C \rlax}
\qquad\Longleftrightarrow\qquad
\easyrule{
\[
  \Gamma^*, A^* \prov FC^*
\justifies
  \Gamma^*, FA^* \prov FC^*
\]}
{\Gamma^*, UFA^*  \prov FC^* }
$$ 
$$
\easyrule{\Gamma\provpd A \rlax}{\Gamma\provpd \lax A \rtrue}
\qquad\Longleftrightarrow\qquad
\easyrule{\Gamma^*\prov FA^*}{\Gamma^* \prov UFA^*}
$$ $$
\easyrule{\Gamma\provpd A \rtrue}{\Gamma\provpd A \rlax}
\qquad\Longleftrightarrow\qquad
\easyrule{\Gamma^*\prov A^*}{\Gamma^*\prov FA^*}
$$
between partial derivations in PD and its encoding.
\subsection{Multimodal Logics}
A multimodal logic with many $\square$s of differing strengths
corresponds simply to having a large preorder for $M$, and assigning
basic `ordinary truth' to its least element (at which all ordinary connectives are defined), and each $\square$ a
round-trip of the form $FU$ up to some high strength mode of truth,
and back down to `ordinary truth'.

However adjoint logic does not {\em require} this stereotypical
setup where there is a single distinguished mode of truth that is
`basic' but rather allows all connectives to be defined at every mode,
and implicitly allows a different $\square$ and different $\lax$ for
every `round trip through a higher mode' and `round trip through a
lower mode' respectively.
 
\subsection{Linear Logic with $!$}
\label{section.linearlogic}

We may extend adjoint logic with substructural features by allowing a
specification for each mode of truth of which structural rules it is
required to satisfy, so long as if $p \le q$, we have that any
structural rule satisfied by $p$ is also satisfied by $q$. This is so
that, for instance, $F_{q\ge p}$ remains correctly left-invertible.
Otherwise, it might be that one would like to apply structural rules
at mode $p$ before (in a bottom-up reading) moving via $F$ to mode $q$
where those structural rules are no longer available, meaning that
proof search incorporating eager decomposition of $F$ would not be
complete.

To accomodate substructrual properties we must slightly generalize the right rule for $F$ to be the following
$$
\begin{prooftree}
\Gamma \rightsquigarrow \Gamma_{\ge q} \qquad \Gamma_{\ge q}\prov A_q
\using{F R}
\justifies
\Gamma\prov F_{q\ge p}A_q
\end{prooftree}
$$ 
where $\Gamma \rightsquigarrow \Gamma_{\ge q}$ means that $\Gamma$
can be converted to $\Gamma_{\ge q}$ via allowed structural rules, and
in fact $ \Gamma_{\ge q}$ is a context containing only judgments
$\rtrue_p$ where $p \ge q$. In this way we allow, for instance,
weakening of hypotheses at modes that were marked as allowing
weakening, but we cannot apply the $F$ right rule at all until all
unweakenable hypotheses have been eliminated.

Having done this we can now encode linear logic with $!$, which winds
up unsurprisingly being very similar to PD $\square$. The subset of
adjoint logic required is again a two-point $M$ with $r \le u$, (for
{\bf r}esources and {\bf u}nrestricted hypotheses) where at now we say
that at $u$ we allow weakening and contraction, and at $r$ we do
not. The connectives used are

$$\begin{tabular}{rcl}
$A_u$&$::=$&$U_{r\le u}A_r$\\
$A_r$&$::=$&$F_{u\ge r}A_u  \celse A_r \amp_r A_r \celse A_r \oplus_r A_r \celse A_r \tensor_r A_r \celse A_r \lol_r A_r \celse$\\
&&$ \top_r \celse 0_r \celse 1_r \celse a_r$\\
\end{tabular}$$
where the linear connectives in adjoint logic have the evident rules
identical to those from linear logic except generalized to adjoint
logic contexts and conclusions.

To embed linear logic with entailments $\Delta;\Gamma\provll A$ where
$\Delta$ is full of unrestricted assumptions and $\Gamma$ linear resources,
we say that $A^*$ replaces every $!$ in $A$ with $FU$ and again subscripts every other connective appropriately, and check
\begin{theorem}\ 
\begin{itemize}
\item $\Delta; \cdot \provll A$ iff $U\Delta^* \prov  UA^* \rtrue_u$ 
\item $\Delta; \Gamma \provll A$ iff $U\Delta^*, \Gamma^* \prov A^* \rtrue_r$ 
\end{itemize}
\end{theorem}
One distinct advantage of treating linear logic in this way is that we
are able to smoothly incorporate the connectives of nonlinear
intuitionistic logic in the same system. They may simply be added as
connectives native to the mode of truth $u$, leaving us with the
following adjoint logic
$$\begin{tabular}{rcl}
$A_u$&$::=$&$U_{r\le u}A_r \celse A_u \land_u A_u \celse A_u \lor_u A_u \celse A_u \imp_u A_u \celse
 \top_u \celse \bot_u\celse a_u$\\
$A_r$&$::=$&$F_{u\ge r}A_u  \celse A_r \amp_r A_r \celse A_r \oplus_r A_r \celse A_r \tensor_r A_r \celse A_r \lol_r A_r \celse$\\
&&$ \top_r \celse 0_r \celse 1_r \celse a_r$\\
\end{tabular}$$
In it we can conveniently see directly by construction of small
prooftrees that, for instance, $F$ commutes with positive connectives
and $U$ with negative connectives:
$$\begin{tabular}{cc}
$FA \tensor FB \pprov F(A \land B)$&$ UA \land UB \pprov U(A \amp B)$\\
$FA \oplus FB \pprov F(A \lor B)$&$A \imp UB \pprov U(FA \lol B)$\\
$1 \pprov F\top$&$\top_u \pprov U\top_r$\\
$0 \pprov F\bot$\\
\end{tabular}$$
We can then derive more familiar identities involving $!$ such as $!A
\tensor !B \pprov !(A \amp B)$ because $FUA \tensor FUA \pprov
F(UA\land UB) \pprov FU(A \amp B)$. Seeing how $!$ separated into
positive $F$ and negative $U$, we can see this arises directly from
the ambipolarity of $\land$ in nonlinear intuitionistic logic.  In the
same way, we are also able to see more clearly why $\lax (A \land B)
\pprov \lax A \land \lax B$ in lax logic, but not, for instance, $\lax
(A \lor B) \pprov \lax A \lor \lax B$ or $\lax A \imp \lax B \prov
\lax (\lax A \imp B) $, even though $F(A \lor_t B) \pprov FA \lor_\ell
FB$ and $U(FA \imp_\ell B) \pprov (A \imp_t UB)$ if we bother to
include `natively lax' connectives $\imp_\ell$ and $\lor_\ell$.

\subsection{Pfenning-Davies $\dia$}
Deepak Garg noted (personal communication) that lax logic can also be
encoded in linear logic via the definition $\lax A = (A \lol a) \lol
a$ for $a$ a fresh atom. We can represent $\dia$ similarly as a
`parameteric De Morgan dual of $\square$' (see also
\cite{judgmental.linear03} for other examples of parametric
translations in linear logic) interposing a PD $\square$ between the
two `negations' $\dash\lol a$ and making the definition $\dia A =
(\square (A \lol a)) \lol a$. Subsequently we may reuse our
interpretation above of $\square$ as $FU$.

To achieve this, however, we need a notion of hypotheses that are at
once linear, to maintain the intuitionistic character of the
logic\footnote{Otherwise `possibility continuations' in the context
  would overstay their welcome.}, and somehow `more valid' than
ordinary linear hypotheses, to achieve the context-clearing effect of
the PD elimination rule for $\dia$. We cannot use the notion of
validity already in the logic, since it is not linear, but fortunately
the generality of the adjoint logic easily permits introducing a mode
of truth `more valid than' another, and requiring that it behaves
linearly.

First let us recall the PD natural deduction calculus for $\dia$. 
There are valid contexts $\Delta$ and true contexts $\Gamma$, and
two entailments,
$$\Delta;\Gamma \provpd A \rtrue \qquad \Delta;\Gamma \provpd A \rposs$$
and rules governing $\rposs$ and $\dia$
$$
\easyrule{\Delta;\Gamma \prov \dia A \qquad \Delta; A \provpd C \rposs}
{\Delta;\Gamma \provpd C \rposs}
\qquad
\easyrule{\Delta;\Gamma\provpd A \rposs}{\Delta;\Gamma\provpd \dia A \rtrue}
\qquad
\easyrule{\Delta;\Gamma\provpd A \rtrue}{\Delta;\Gamma\provpd A \rposs}
$$
Note that $\Gamma$ is erased in the second premise of the elimination rule. 
In sequent form this erasure appears in the left rule as
$$
\easyrule{\Delta; A \provpd C \rposs}
{\Delta;\Gamma, \dia A \provpd C \rposs}
$$ 

To encode this logic we take adjoint logic with $M$ a four-point\footnote{And in fact diamond-shaped!}
 preorder $\{r, s, u, v\}$, with $r\le \{u, s\} \le v$, and allow
  contraction and weakening only at $v$ and $u$. The connectives we need are

$$\begin{tabular}{rcl}
$A_v$&$::=$&$U_{u\le v}A_u$\\
$A_u$&$::=$&$F_{v\ge u}A_v\celse U_{r\le u}A_r  \celse A_u \land_u A_u \celse \cdots$\\
$A_s$&$::=$&$ U_{r\le s} A_r$\\
$A_r$&$::=$&$F_{u\ge r}A_u\celse F_{s\ge r}A_s \celse A_r\lol A_r \celse a_r  $\\
\end{tabular}$$
and subsequently the definition of the modalities are given by
giving clauses for translation
$$\begin{tabular}{rl}
$(\dia A)^* =$&$ U_{r\le u}((F_{s\ge r}U_{r\le s}(F_{u\ge r}A^* \lol a_r)) \lol a_r)$\\
$(\square A)^* =$&$ F_{v\ge u}U_{u \le v} A^*$
\end{tabular}$$
We can see that $\dia$ still consists of only two focusing monopoles, one
that begins negative on the outside, switches to positive without
interruption through the outer $\lol$, which is interrupted between
$F_{s\ge r}$ and $U_{r\le s}$, and then begins another negative
stretch which continues through the other $\lol$ and switches smoothly
to positive. In other words, we could have said
$$\begin{tabular}{rl}
$(\dia_1 A)^* =$&$ U_{r\le u}(F_{s\ge r}A^* \lol a_r)$\\
$(\dia_2 A)^* =$&$ U_{r\le s}(F_{u\ge r}A^* \lol a_r)$\\
\end{tabular}$$
and then $(\dia A)^* = (\dia_1\dia_2 A)^*$.

The correspondence between sequent derivations before and
after translation obeys
$$
\begin{tabular}{rcl}
$\Delta; \Gamma \prov A \rtrue$&$\Longleftrightarrow$&
$U_{u\le v}\Delta^*, \Gamma^* \prov A^*\rtrue_u $\\
$\Delta; \Gamma \prov A \rposs$&$\Longleftrightarrow$&
$U_{u\le v}\Delta^*, \Gamma^*, (\dia_2 A)^*  \rtrue_s \prov a_r \rtrue_r$
\end{tabular}
$$

and we can see the correspondence of partial derivations

$$
\easyrule{\Delta; A \provpd C \rposs}
{\Delta;\Gamma, \dia A \provpd C \rposs}
\ \Longleftrightarrow\ 
\easyrule
{
\[
\[
\[
\[
\[
U_{u\le v}\Delta^*,   A^*\rtrue_u, (\dia_2 C)^* \prov a_r 
\justifies
U_{u\le v}\Delta^*, (\dia_2 C)^*,  F_{u \ge r} A^*\rtrue_r \prov a_r 
\]
\justifies
U_{u\le v}\Delta^*, (\dia_2 C)^* \prov  F_{u \ge r} A^*\lol a_r \rtrue_r
\]
\justifies
U_{u\le v}\Delta^*, (\dia_2 C)^* \prov ( \dia_2 A)^* \rtrue_s
\]
\justifies
\cdots \prov F_{s\ge r} ( \dia_2 A)^*\rtrue_r
\]
 \[\justifies a_r \prov a_r\]
\justifies
\cdots, F_{s\ge r} ( \dia_2 A)^*\lol a_r\rtrue_r   \prov a_r 
\]
}
{U_{u\le v}\Delta^*, \Gamma^*, (\dia A)^*, (\dia_2 C)^*   \prov a_r }
$$

$$
\easyrule{\Delta;\Gamma\provpd A \rposs}{\Delta;\Gamma\provpd \dia A \rtrue}
\qquad\Longleftrightarrow\qquad
\easyrule
{
\[
\[
U_{u\le v}\Delta^*,\Gamma^*, (\dia_2 A)^*\rtrue_s\prov a_r \rtrue_r
\justifies
U_{u\le v}\Delta^*,\Gamma^*, F_{s\ge r}(\dia_2 A)^*\rtrue_r\prov a_r \rtrue_r
\]
\justifies
U_{u\le v}\Delta^*,\Gamma^*\prov F_{s\ge r}(\dia_2 A)^*\lol a_r \rtrue_r
\]}
{U_{u\le v}\Delta^*,\Gamma^*\prov (\dia_1\dia_2 A)^* \rtrue_u}
$$

$$
\easyrule{\Delta;\Gamma\provpd A \rtrue}{\Delta;\Gamma\provpd A \rposs}
\qquad\Longleftrightarrow\qquad
\easyrule
{
\[
\[
\[
\justifies
U_{u\le v}\Delta^*,\Gamma^* \prov A^* \rtrue_u
\]
\justifies
U_{u\le v}\Delta^*,\Gamma^* \prov F_{u\ge r}A^* \rtrue_r
\]
\[\justifies a_r \prov a_r\]
\justifies
U_{u\le v}\Delta^*,\Gamma^*, F_{u\ge r}A^* \lol a_r \rtrue_r\prov a_r 
\]
}
{U_{u\le v}\Delta^*,\Gamma^*, (\dia_2 A)^*\rtrue_s\prov a_r \rtrue_r}
$$

Requiring the sequencing of translated derivations to take place as
depicted requires focusing reasoning beyond the scope of this note.
It's possible the reasoning could be simplified by directly defining
$\dia_1$ and $\dia_2$ as appropriate coalesced connectives in the adjoint logic.
\subsection{Intuitionistic Labelled Deduction}
Finally, consider a labelled deduction sequent calculus system
 with an entailment relation $\Gamma \prov A[p]$ where $\Gamma$
consists of a set hypotheses also of the form $A[p]$. The worlds $p$ 
are drawn from a set $M$.

All ordinary logical connectives such as $\land$ exist and have rules that
pass along the `world part' $[p]$ of the entailment unmolested, i.e.

$$\easyrule{\Gamma \prov A[p]\qquad \Gamma \prov B[p]}{\Gamma \prov A\land B[p]}\qquad
\easyrule{\Gamma, A[p], B[p]\prov C[r]}{\Gamma, A[p] \prov C[r]}$$

and it possesses a connective $@_p$ with rules

$$\easyrule{\Gamma \prov A[q]}{\Gamma \prov @_qA[p]}\qquad
\easyrule{\Gamma, A[q]\prov C[r]}{\Gamma, @_qA[p] \prov C[r]}$$ Then
this is just the special case of adjoint logic where the relation on
$M$ is entire, i.e. $p \le q$ for every $p, q$. The connective $@_p$
is equivalently translated (when `at world $q$') as $F_{p\ge q}$ or
$U_{p \le q}$. Since no pair of modes of truth fail to be connected,
no modal restriction obtains, and $@_p$ is ambipolar.

\bibliography{/home/jcreed/public/jcreed0.bib}
\end{document} 
