\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}