UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC

Abstract

We present a proof system for a multimode and multimodal logic, which is based on our previous work on modal Martin-Löf type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e., a small 2-category. The logic is extended to a lambda calculus, establishing a Curry–Howard correspondence.

1 Introduction

Many-dimensional [13], multimodal [7], or poly-modal [2] logics have found a number of successful applications. To name but a few:

The majority of work on the aforementioned logics has a number of common features:

• • The propositional substrate is almost always classical. While a classical approach is more than sufficient for modelling knowledge and computational systems, it precludes the making of a close connection with categorical logic, where the internal language of many categories is intuitionistic [35].

• • The modal fragment is almost always inspired by a Kripke semantics, and lacks a proof system. The Kripke semantics usually model some intensional aspect of interest, such as states of knowledge and the execution trace of a machine. While this is indeed more than adequate for modelling purposes, it precludes the immediate formulation of a well-behaved, computational theory for these logics under the Curry–Howard correspondence [16, 41].

• • There is no cohesive, unifying account. While there have been a few attempts at building a framework [7, Section 8], as well as a host of results on combining simpler modal logics using product and fusion operators [13, Sections 3 and 4], we have yet to obtain a unifying account of logics with multiple interacting modalities.

In this paper we present a new modal logic. Unlike previous work, this logic fixes neither the number nor the interactions of modalities in advance. Instead, it is given parametrically in a specification of the modalities and their interrelations, which is called the mode theory.

Moreover, this new logic is not just multimodal—in that it sports multiple modalities—but also multimode. This is a new concept in modal logic. Traditionally, a modal operator $\Box $ is an operator that takes a formula $\varphi $ to a formula $\Box \varphi $ . Crucially, the formula $\Box \varphi $ is in the same syntactic category as $\varphi $ . The logic in this paper will conceive of modal operators as transporting formulas between multiple syntactic categories. We will call these syntactic categories modes, and modalities will map formulas of one mode to formulas in another. Modes can be conceived of as ‘possible universes of discourse’ in which we can make various logical statements. Modalities will then allow formulas in one mode to appear in another—not directly, but as spectres under a modality. All the modal operators in the logic will preserve conjunction. Thus, their essence is one of a necessity modality. Extending the present approach to possibility-like modalities is an open problem.

Instead of originating from a Kripke semantics of computational interest, our logic comes from categorical logic. In fact, it is the logical isolate of a multimodal Martin-Löf Type Theory [30] called MTT [18, 19]. Hence, it is presented as a proof system in the style of Gentzen’s natural deduction [36, 37]. Due to a lack of a double-negation elimination rule the resultant logic is intuitionistic. The formulation of a classical version of this logic as well as an associated Kripke semantics for it remains an open problem.

2 Mode theories

2.1 Modes

To begin presenting the logic we must presuppose a set ${\mathcal {M}}$ of modes, with typical members $m, n, \ldots \in {\mathcal {M}}$ . Each of these modes corresponds to a syntactic category, thus partitioning the formulas of the logic. We will write

to mean that $\varphi $ is a formula at mode m.

2.2 Modalities

Modalities are traditionally endoöperators of the logic: a modality $\Box $ maps a formula to a formula at the same mode. Our logic breaks with tradition by featuring modalities which map formulas to different modes. Thus, a modality indexed by $\mu $ applied to a formula at mode n may yield a formula at some other mode m. We will also break with tradition by writing $\langle {\mu }\mid {\varphi }\rangle $ for the application of the modality indexed by $\mu $ to $\varphi $ , instead of the more common notation $\Box _\mu \,\varphi $ .

We will specify the fact that implies by writing

$$ \begin{align*} \mu : n \to m. \end{align*} $$

This notation says that $\mu $ is a modality from mode n to mode m. We are likely to call m and n the boundary of the modality. ¹

One may wonder how modal operators are to be combined. Indeed, standard treatments of modal logic define a modality to be a composite of modal operators, and demonstrate various ‘reduction laws’ that simplify such composites (see, e.g., [24, Section 3]). In our case, if we have two modalities $\nu : o \to n$ and $\mu : n \to m$ , and a formula

we see that

In a more traditional system of modal logic we might have tried to prove that such a formula is equivalent to a simpler formula

for some modality $\xi : o \to m$ . We will once more break with tradition by presuming that such a modality always exists. In other words, we will assume that for any two modalities $\nu : o \to n$ and $\mu : n \to m$ there exists a composite modality $\mu \circ \nu : o \to m$ . The rules of our logic will eventually allow us to prove for any formula

a logical equivalence

In order to ensure that the composition of modalities behaves well we must assume that it is governed by some algebraic laws. In particular, we will assume that it is associative: for any three composable modalities $\xi : p \to o$ , $\nu : o \to n$ , and $\mu : n \to m$ we must have

$$ \begin{align*} (\mu \circ \nu) \circ \xi = \mu \circ (\nu \circ \xi) : p \to m. \end{align*} $$

Thus, a string of modalities will compose to a unique result. Moreover, we will assume for each mode $m \in {\mathcal {M}}$ an identity modality

$$ \begin{align*} 1_m : m \to m, \end{align*} $$

which will be an identity element for the composition operator $\circ $ , so that for each $\mu : \nu \to \mu $ it is the case that $1_m \circ \mu = \mu = \mu \circ 1_n$ . We will later be able to prove a logical equivalence

for any

.

Readers that have encountered category theory before will immediately recognise that we have assumed that ${\mathcal {M}}$ is not just a set, but a category. Between any two modes $m, n \in {\mathcal {M}}$ (the objects of the category) we are given a set $\mathrm {Hom}_{\mathcal {M}}({m}, {n})$ of modalities from m to n (the morphisms of the category with source m and target n). Moreover, for any three modes $m, n, o \in {\mathcal {M}}$ we are given an indexed binary operation

$$ \begin{align*} \circ_{m, n, o} : \mathrm{Hom}_{\mathcal{M}}({n}, {m}) \times \mathrm{Hom}_{\mathcal{M}}({o}, {n}) \to \mathrm{Hom}_{\mathcal{M}}({o}, {m}), \end{align*} $$

which is associative and has ‘indexed’ identity elements $1_m \in \mathrm {Hom}_{\mathcal {M}}({m}, {m})$ . Thus, modes and modalities form a category, i.e., a ‘typed’ monoid, whose elements (morphisms) have a ‘source’ and ‘target’ type, and where monoid multiplication (composition) can only happen when these types align. The structure of a category underlies a large part of modern algebra and mathematics. For an introduction we refer the reader to books by Awodey [1] and Mac Lane [28].

It is instructive to try to encode a very simple modal syntax as a mode theory. Recall that traditional modal logics assume a single-mode syntax. Thus, we define the set $\mathcal {M}_{{\textbf {K}}} = \{\bullet \}$ to consist of a unique mode $\bullet $ . Next, we can generate the morphisms by stipulating that $\Box : \bullet \to \bullet $ is an endomodality on that unique mode. We can then generate the free category based on these data. This is essentially the free monoid on a set of generating morphisms, subject to the restriction that in any string of morphisms the target of a morphism always matches the source of the next. As this happens trivially in our case (we have a unique mode), the set of morphisms is exactly the free monoid on one generator: its elements consist of the modalities $\Box ^n : \bullet \to \bullet $ for each $n \in \mathbb {N}$ . The composite of two morphisms is

$$ \begin{align*} \Box^a \circ \Box^b = \Box^{a + b}. \end{align*} $$

Finally, the identity morphism for this operation is $\Box ^0$ .

This generates a syntax with an infinite set of modalities: if

then

are all well-formed formulas at mode $\bullet $ . We will see later that the logic generated here is essentially (an intuitionistic variant of) the smallest normal modal logic K [5, Section 1.6].

2.3 Transformations between modalities

This technology does not suffice to encode richer settings. For example, the 4 axiom

$$ \begin{align*} \Box \phi \to \Box \Box \phi \end{align*} $$

is one of the two characteristic axioms of the modal logic S4 [24, Section 3]. We would ideally like to be able to encode this as part of the structure of the mode theory ${\mathcal {M}}$ . However, none of the ‘moving parts’ of ${\mathcal {M}}$ allows the representation of such information.

Consequently, to encode implications such as the above we will need to add another layer to the mode theory ${\mathcal {M}}$ . We will postulate that between any two ‘parallel’ modalities $\mu , \nu : n \to m$ with the same source and target mode there exists a set of transformations

$$ \begin{align*} \alpha : \mu {\mathop{{}\Rightarrow}{}} \nu. \end{align*} $$

These transformations—typically denoted by the letters $\alpha $ , $\beta $ , …—encode implications between modalities. They may be illustrated pictorially this way:

This shape is often called a globe. We can imagine $\alpha $ as ‘inhabiting’ this globe. Due to this shape we are likely to collectively call the modes m and n and the modalities $\mu $ and $\nu $ the boundary of $\alpha $ .

The presence of such a transformation in ${\mathcal {M}}$ will allow us to prove the formula

in the logic, for any formula

. For example, if in $\mathcal {M}_{{\textbf {K}}{}}$ we postulate a transformation

$$ \begin{align*} {4} : \Box {\mathop{{}\Rightarrow}{}} \Box^2 \end{align*} $$

which corresponds to the 4 axiom, then in the logic we will be able to prove the implication

Combined with the equivalence

this implication enables a proof of a formula that looks like axiom 4 within the logic.

The addition of 4 to a modal logic may have far-reaching implications. For example, when combined with the ${K}$ axiom it allows us to prove the implication $\Box \Box A \to \Box \Box \Box A$ . Thus, there should be a minimum amount of algebra on transformations that generates these consequences. To start, given three parallel modalities $\mu , \nu , \xi : n \to m$ and a formula

, the desired hypothetical syllogism

can be indirectly encoded by the existence of a composition operation on transformations: if $\alpha : \mu {\mathop{{}\Rightarrow}{}} \nu $ and $\beta : \nu {\mathop{{}\Rightarrow}{}} \xi $ then there should exist a composite transformation

$$ \begin{align*} \beta \circ \alpha : \mu {\mathop{{}\Rightarrow}{}} \xi. \end{align*} $$

This may be illustrated pictorially by placing two globes on top of each other:

This composition should also be subject to associativity. Moreover, there should be an identity transformation $1_\mu : \mu {\mathop{{}\Rightarrow}{}} \mu $ for every modality $\mu : n \to m$ . Note that we abuse the notations for composition and identities, using them for both modalities and their transformations.

This vertical composition of transformations is not sufficient to construct $\Box \Box \varphi \to \Box \Box \Box \varphi $ from the 4 axiom $\Box \varphi \to \Box \Box \varphi $ . What is needed instead is a form of horizontal composition. Suppose that we have four modalities $\mu , \nu : n \to m$ and $\theta , \xi : o \to n$ , and transformations $\beta : \theta {\mathop{{}\Rightarrow}{}} \xi $ and $\alpha : \mu {\mathop{{}\Rightarrow}{}} \nu $ . This may be illustrated pictorially by placing two globes one next to the other:

The horizontal composition of the transformations $\alpha $ and $\beta $ is a transformation

$$ \begin{align*} \alpha \ast \beta : \mu \circ \theta {\mathop{{}\Rightarrow}{}} \nu \circ \xi, \end{align*} $$

which transforms the composite modality $\mu \circ \theta $ to the composite modality $\nu \circ \xi $ .

If one of the two transformations is the identity then the horizontal composites are

$$ \begin{align*} 1_\mu \ast \beta : \mu \circ \theta {\mathop{{}\Rightarrow}{}} \mu \circ \xi && \alpha \ast 1_\theta : \mu \circ \theta {\mathop{{}\Rightarrow}{}} \nu \circ \theta. \end{align*} $$

This special case is sometimes called whiskering, because its pictorial representation resembles the adding of a cat’s whisker to a transformation:

Picking

and

we obtain a transformation

$$ \begin{align*} {4} \ast 1_\Box : \Box^2 {\mathop{{}\Rightarrow}{}} \Box^3, \end{align*} $$

which, modulo isomorphisms, is the desired conclusion $\Box \Box \varphi \to \Box \Box \Box \varphi $ . Thus, transformations of modalities along with their vertical and horizontal compositions can be used to systematically encode various interaction laws between modalities.

It may not come as a surprise that this type of structure is already well-known: the ingredients used above are precisely the components of a (strict) 2-category, i.e., a category which is also equipped with morphisms between morphisms, which can be composed vertically (i.e., in the same hom-set) as well as horizontally (between hom-sets whose source and targets match). To have the structure of a 2-category these two compositions need to be compatible, i.e., to obey the interchange law: for any modalities and transformations fitting into the diagram

we must have that no matter which direction we compose in first, the result should be the same:

$$ \begin{align*} (\delta \circ \alpha) \ast (\gamma \circ \beta) = (\alpha \ast \beta) \circ (\delta \ast \alpha). \end{align*} $$

The structure of 2-categories is rich, and of foundational interest to category theory. Of course, the terminology is different: higher category theorists do not speak of modes, modalities, and transformations, but of morphisms and n-cells. The correspondence of terms between 2-categories and our multimodal logic can be summarised as follows:

$$ \begin{align*} \text{object} &\sim \text{mode} \\ \text{morphism (1-cell)} &\sim \text{modality} \\ \text{2-cell} &\sim \text{transformation (natural map between modalities).} \end{align*} $$

In this manner we are able to give a very precise definition of a mode theory:

Definition 2.1. A mode theory is a (strict) 2-category.

Unfortunately, we cannot expand on the subject any further in this paper. For introductory treatments of 2-categories we refer the reader to books by Mac Lane [28, Section XII.3] and Borceux [6, Section 7].

3 Formulas and judgements

Having sketched how mode theories can be used to encode the modal structure of a modal logic, we now turn to defining the formulas of our logic as well as its proof system.

Owing to the roots of our work in Martin-Löf type theory, almost all our definitions will be given using Martin-Löf’s methodology of judgements [29]. This amounts to a universal use of positive statements which are inductively justified by evidence. The canonical examples of this methodology are the proof systems of natural deduction and sequent calculus: each sequent is a judgement, and the evidence that a judgement holds is a proof tree with that conclusion. This methodology is very common in the parts of Computer Science that are influenced by type theory (see, e.g., the book of Robert Harper on the foundations of programming languages [22]). It has also been particularly influential in treatments of the Curry–Howard correspondence for modal logic (see, e.g., Pfenning and Davies [34]).

3.1 Formulas

The majority of presentations of modal logic assume a propositional syntax that has been augmented by a set of endomodalities—usually $\Box $ and $\diamond $ , or an indexed version of them in the multimodal case. We will enrich this by including a modal operator $\langle {\mu }\mid {-}\rangle $ for every modality $\mu : n \to m$ in the mode theory ${\mathcal {M}}$ . However, modalities transport formulas between modes, so we have to ensure that every formula is well-formed. We first define a grammar of pre-formulas. Then, we introduce a judgement

which states that the pre-formula $\varphi $ is well-formed with respect to the mode theory ${\mathcal {M}}$ . Thus, the well-formed formulas of the logic are a subset of the pre-formulas.

The pre-formulas of are generated by the grammar

where $\mu $ is a modality in ${\mathcal {M}}$ . These are mostly standard. Each $p_i$ is a propositional variable, and we have the usual propositional connectives. As is usual in intuitionistic logic, we define

. The only deviant is the implication $(\mu \mid {\varphi })\to {\psi }$ , whose antecedent carries a modality $\mu $ . Written in terms of the modal operator and the traditional connective of implication, this is essentially $\langle \mu \mid {\phi }\rangle \to \psi $ . However, there are technical advantages in having this compound version of implication in the logic: many proofs become significantly shorter, and the relevant ‘modal modus ponens’ rule is interesting from a modal perspective. We write the usual implication $\varphi \to \psi $ as shorthand for $(1\mid {\varphi })\to {\psi }$ .

The well-formed formulas (wffs) are generated by the following inductive definition:

With the exception of the implication and the modal operator, the rest of the rules all refer to a single mode m, in which they are parametric. Thus, most of the connectives are mode-local: they construct propositions that remain in a single mode. In contrast, both the rules for the modal operator and the implication rules reach across modes. In the first case, a formula that is well-formed at n may appear in mode m, but only under a modality $\mu : n \to m$ . In the second case, the antecedent of an implication should be well-formed under the appropriate modality, in a similar manner.

3.2 Judgments and contexts

A judgement of the multimodal logic has the form

where $\Gamma $ is a context (at mode m), and $\varphi $ is a well-formed formula (at mode m).

Traditionally, contexts in natural deduction consist of a list of assumptions $\phi _1, \dots , \phi _n$ . However, in order to accommodate modal reasoning, ours will feature two additional gadgets: tags and locks. Each of these gadgets complements the other.

Each assumption in the context will be tagged with a modality. Hence, the assumption

$$ \begin{align*} (\mu\mid\varphi) \end{align*} $$

is meant to be read as ‘the formula $\varphi $ under modality $\mu $ ’. In broad strokes this is logically equivalent to the assumption $\langle {\mu }\mid {\varphi }\rangle $ . When we come to define contexts we must remember to ensure that $\varphi $ be well-formed under $\mu $ .

The other side of the coin is the appearance of locks in contexts. Unlike tags, locks are operators that act on entire contexts, and are annotated by a modality. If $\mu : n \to m$ is a modality and $\Gamma $ is a context at the appropriate mode, then

will also be a context, also at an appropriate mode. We use postfix notation for reasons that will be revealed shortly. Finally, it should be stressed that locks are formal operations that act on the entire context; it might perhaps be more apt to think of

as

.

As is suggested by the notation, locks restrict access to the assumptions they enclose: whether an assumption $(\nu \mid \phi )$ found in shall be accessible will depend on the transformations between modalities $\mu $ and $\nu $ . For this reason, it is important that contexts are understood as structures generated by a certain grammar, and not as lists or multisets of assumptions.

In summary, the pre-contexts are generated by the grammar

where ${\cdot }$ is the empty context, $\varphi $ is a pre-formula, and $\mu $ is modality in ${\mathcal {M}}$ .

The (well-formed) contexts are isolated by a judgement

which is generated by the following rules:

Perhaps the only unexpected detail here is that locks transport contexts backwards along modalities: if and $\mu : n \to m$ , then . In categorical language we would say that the lock operation is contravariant in the modality $\mu $ . The reason for this will become clear when we introduce the modal rules. The categorical essence of it is that is in some sense a left adjoint to the modal operator $\langle {\mu }\mid {-}\rangle $ , and thus must have the opposite variance to make sense.

Finally, it is important to determine how the lock operators should interact with the composition of modalities. Suppose that we have

The rules then allow us to construct the following context:

However, the mode theory also provides a composite modality $\mu \circ \nu : o \to m$ . With respect to that modality the rules then allow us to construct the following context:

We will quotient the set of contexts, so that these two constructions will be understood to be identical. The rationale for this choice has to do with our earlier discussion about the equivalence between the formulas

for any

. The proof of this equivalence will be enabled by the fact these two contexts are syntactically interchangeable.

Hence, for any , $\nu : o \to n$ , $\mu : n \to m$ , and , we stipulate that

(1)

(2)

This last equation also reveals the reason that is best written as a postfix operator: as it is contravariant, writing it at the end preserves the order of symbols when composing modalities.

Figure 1 Rules of multimodal logic.

3.3 Rules

We are now able to introduce the logical rules of the system. The complete list is given in Figure 1.

3.3.1 Propositional connectives

The rules for the propositional constants and connectives $\top $ , $\bot $ , $\land $ , and $\lor $ are the standard rules of natural deduction. The only difference is that they have become parametric in the mode , which they carry from premise to conclusion. In the case of $\lor $ , the elimination rule creates ‘local assumptions’ as usual; but because of the structure of contexts these need to be tagged with a modality. We pick the identity modality $1$ , so that the rule remains completely mode-local. Therefore, the rules for all but one of the usual propositional connectives apply in an unchanged form within a single mode. The only exception is the compound modal implication.

3.3.2 Using assumptions

The usual variable rule of natural deduction

allows us to prove a conclusion if we have already assumed it in the context.

This rule does not immediately adapt to our multimodal system. There is a sense in which modal reasoning is largely about the control of assumptions. The rôle of modalities very often seems to amount to a specification of who or which state of the world ‘owns’ an assumption, and when we should be able to use it. In this particular setting, the logical power of an assumption is attenuated by the presence of a lock operator . The lock stops us from using the assumptions that it guards—unless there is a transformation that explicitly allows it.

There are three principles that determine the behaviour of locks.

Principle 1. A $\mu $ -variable can escape the hold of a $\mu $ -lock.

In symbols, this implies that the variable rule at the very least admits the inference

where for $\mu : n \to m$ the formation of the context presupposes that

If we view a lock

as a protector of variables, we see that it acts as a $\mu $ -firewall that only authorises $\mu $ -assumptions to escape its hold. In another interpretation, the appearance of a lock at the end of a context signifies that we are currently reasoning in a $\mu $ -protected environment, so we are entitled to access $\mu $ -classified information.

As we have quotiented our contexts up to Equations (1) and (2), this ability of a $\mu $ -assumption to escape a $\mu $ -lock should be retained even when the locks match only up to composition. For example, given $\nu : o \to n$ and

we should also be able to use the variable rule to infer

precisely because

.

The second principle allows us to weaken the requirement for an exact match between the modality and the lock:

Principle 2. The transformations of ${\mathcal {M}}$ are ‘keys’ for the lock.

In other words, suppose that for modalities $\mu , \nu : n \to m$ we have a transformation

$$ \begin{align*} \alpha : \nu {\mathop{{}\Rightarrow}{}} \mu \end{align*} $$

in ${\mathcal {M}}$ . If we interpret this to mean that the modality $\nu $ implies (or is stronger than) the modality $\mu $ , then intuition has it that $\nu $ -modal assumptions should be able to ‘unlock’ a $\mu $ -lock. In symbols:

The final principle is already well-known:

Principle 3. The variable rule should be stable under weakening.

The idea here is that weakening should be admissible independently of the position of locks: if we have an inference in context we should also be able to admit it in either or for appropriately-typed modalities $\nu $ and $\nu '$ . Moreover, this should only apply to tagged assumptions: introducing a new lock should by no means be admissible! That is, if we have an inference in context $\Gamma $ , it should not in general be possible to also have it in , as might protect some of the assumptions in $\Gamma $ by prohibiting their use.

Combining those three principles we see that the assumption rule should more or less function in the following manner:

1. 1. It should gather all the locks to the right of the relevant assumption.

2. 2. It should compose the modalities associated with each one of these locks.

3. 3. It should allow the use of an assumption whenever its tag is stronger than the locks that protect it, i.e., the locks to its right.

In symbols we write

where the function ${\mathsf {locks}(-)}$ is defined by the following inductive clauses:

It is evident that this function is well-defined on contexts, for it respects Equations (1) and (2).

3.3.3 Locks vs. modalities

The modal rules of the system reveal the close interaction between locks and modal operators.

Broadly speaking, the lock operators

are used to ‘filter’ the assumptions in the context, keeping only those that are allowed in a proof of a formula under the modality $\langle {\mu }\mid {-}\rangle $ . This is encoded in the introduction rule, viz.

which allows us to prove the modal formula $\langle {\mu }\mid {\varphi }\rangle $ from the context $\Gamma $ exactly whenever we can prove $\phi $ from a $\mu $ -locked $\Gamma $ . Thus, when trying to prove $\langle {\mu }\mid {\varphi }\rangle $ it suffices to prove $\varphi $ , but with restrictions on the proof. More precisely, we are able to use only those assumptions whose modal tag is at least as strong as $\mu $ .

The modal elimination rule

is the most complicated rule of the system. Its major premise (i.e., the premise whose connective is being eliminated) is

. Notice that this judgement could be turned into

by applying the introduction rule. Putting the transformed major premise and the minor premise side-by-side

we see that this elimination rule is almost a cut rule! This is particularly evident if we recall that $\langle \mu \mid \langle \nu \mid {\varphi }\rangle \rangle $ is supposed to be logically equivalent to $\langle \mu \circ \nu \mid {\varphi }\rangle $ , which is also supposed to be equivalent to the tagged assumption $(\mu \circ \nu \mid {\varphi })$ .

Despite appearances, this elimination rule is subtle: it allows the prover to ‘split’ a composite modality $\mu \circ \nu $ into its constituent parts, keeping the second half $\mu $ as a lock in the context of the major premise, and eliminating only the first half $\nu $ . In fact, we will see in Section 4 that the modal elimination rule is the central device that allows highly non-trivial interactions between modalities to appear as reasoning principles in the logic.

3.3.4 Implication

As is usual in natural deduction, the implication introduction rule

internalises the usual deduction theorem as a rule of the proof system, by allowing the prover to discharge an assumption. This is exactly why the compound implication $(\mu \mid {\varphi })\to {\psi }$ is a natural connective in this logic: its antecedent mirrors the structure of assumptions in the proof system.

The elimination rule is a form of modal modus ponens:

If we can prove the implication $(\mu \mid {\varphi })\to {\psi }$ then proving $\varphi $ in a $\mu $ -locked context suffices to obtain $\psi $ . Notice once more that the minor premise can be transformed into

by one application of the modal introduction rule. Thus, if we consider the assumption $(\mu \mid {\varphi })$ and the formula $\langle {\mu }\mid {\varphi }\rangle $ to be equivalent, this rule is simply modus ponens, but a little bit more accommodating towards the structure of locks.

3.4 Metatheory

The system satisfies a number of the usual metatheorems. First, one is able to show the admissibility of the usual structural rules of weakening and exchange. Some additional care is needed in the case of weakening to ensure that the weakened context is well-formed.

Theorem 3.1 (Structural rules).

The following rules are admissible:

We cannot in general weaken a context by adding a lock. In fact, locks transport contexts between modes, so adding arbitrary locks to a context may well map a well-formed context to one that is not well-formed. However, we can ‘weaken a $\mu $ -lock’ by replacing it with one corresponding to a $\nu $ -lock for a ‘weaker’ $\nu $ , i.e., a modality with the same boundary (source and target modes) for which there exists some $\alpha : \mu {\mathop{{}\Rightarrow}{}} \nu $ .

Theorem 3.2 (Lock weakening).

The following rule is admissible:

Finally, we can prove that a modal version of the cut rule is admissible.

Theorem 3.3 (Cut).

The following rule is admissible:

These metatheorems will follow as corollaries of theorems in section (5).

4 Examples

In this section we demonstrate modal reasoning using our proof system.

Recall that

. The usual modus ponens is then a derived rule:

This follows from the elimination rule, as by Equation (1) we have

.

4.0.1 Some general theorems about modal formulas

We begin by showing some theorems that hold irrespective of the choice of mode theory. This determines the nature of our modalities—which are shown to automatically preserve conjunctions—and showcases the various rules in action.

First, we can show that a modal antecedent $(\mu \mid {\varphi })$ implies its corresponding modal formula. For any $\mu : n \to m$ and

we have

This proves one half of the claim that $(\mu \mid {\varphi })$ and $\langle \mu \mid {\varphi }\rangle $ are equivalent. The other half cannot be shown as a theorem, as an implication cannot have $(\mu \mid {\varphi })$ as a conclusion. However, the following special case of the modal elimination rule for

(which follows because

by Equation (1)) shows how we can ‘promote’ a modal formula $\langle \mu \mid {\varphi }\rangle $ and use it as an assumption $(\mu \mid {\varphi })$ in the context of another proof. This can be thought as a converse to above proof.

One can also show a version of the K axiom $\Box (\varphi \to \psi ) \to \Box \varphi \to \Box \psi $ , where the $\Box $ in the conclusion is replaced by a $\langle {\mu }\mid {-}\rangle $ , and the two antecedents are tagged:

Consequently all the modalities in our system are necessity-type modalities.

It is interesting to ask how one can handle this type of reasoning without using modal antecedents in implications, i.e., replacing antecedents $(\mu \mid {\varphi })$ with antecedents $(1\mid {\langle \mu \mid {\varphi }\rangle })$ with a trivial modal tag and a modal formula. Navigating the difference between $(\mu \mid {\varphi })$ and $\langle \mu \mid {\varphi }\rangle $ is the domain of the modal elimination rule. For example, we can prove that we can eliminate conjunctions under modalities. Given

and writing

we have

Notice that the modal elimination rule is used to turn the modal formula $\langle \mu \mid \varphi \land \psi \rangle $ into an assumption $(\mu \mid \varphi \land \psi )$ which overpowers the $\mu $ -lock. One can also prove the following theorems in a similar manner:

(3)

Both of these are versions of the K axiom.

4.0.2 Normality

Most modal logics are single-mode, single-modal-operator logics. Following our approach in Equation (2) we want to construct a mode theory consisting of a single object $\bullet $ . The axioms of 2-categories then dictate that we define a category $\mathrm {Hom}_{\mathcal {M}}({\bullet }, {\bullet })$ of modalities and their transformations. The objects of this category are the modalities, and the morphisms are the transformations between them. There also needs to be a composition functor

$$ \begin{align*} \circ : \mathrm{Hom}_{\mathcal{M}}({\bullet}, {\bullet}) \times \mathrm{Hom}_{\mathcal{M}}({\bullet}, {\bullet}) \to \mathrm{Hom}_{\mathcal{M}}({\bullet}, {\bullet}). \end{align*} $$

On objects this functor maps any two modalities to their composite; on morphisms it maps two transformations of modalities to their horizontal composite.

Suppose that, as in Section 2, we define $\mathcal {M}_{{\textbf {K}}{}}$ to be the free category on one generator, so that $\mathrm {Hom}_{\mathcal {M}}({\bullet }, {\bullet })$ is the set consisting of the modalities $\Box ^n : \bullet \to \bullet $ for each $n \in \mathbb {N}$ . Defining

the proofs of Equation (3) read

Thus the ‘simplest’ mode theory $\mathcal {M}_{{\textbf {K}}{}}$ generates a logic that is a lot like K.

4.0.3 Axioms as transformations

We will now demonstrate how the transformations of the mode theory gives rise to theorems that are usually axioms of normal modal logics.

To add axioms to the logic we can then promote the set $\mathrm {Hom}_{\mathcal {M}}({\bullet }, {\bullet })$ itself to be the free category on additional transformations. If we also freely add horizontal composites we get a free 2-category. For example, if as in Section 2 we generate the free 2-category on

$$ \begin{align*} {4} : \Box {\mathop{{}\Rightarrow}{}} \Box^2, \end{align*} $$

then we get a category with an infinite number of transformations, e.g.,

$$ \begin{align*} \begin{array}{lcl} {4} &:& \Box {\mathop{{}\Rightarrow}{}} \Box^2 \\ 1_\Box \ast {4} &:& \Box^2 {\mathop{{}\Rightarrow}{}} \Box^3 \\ 1_\Box \ast 1_\Box \ast {4} &:& \Box^4 {\mathop{{}\Rightarrow}{}} \Box^5 \\ &\vdots& \end{array} \end{align*} $$

Axiom 4 then appears in the logic through the following proof: for any

,

Similarly, we could have added an axiom

$$ \begin{align*} {T} : \Box^1 {\mathop{{}\Rightarrow}{}} \Box^0, \end{align*} $$

which leads to the modal logic T.

We would expect that combining axioms 4 and ${T}$ generates the modal logic S4. We can indeed generate a free category out of these two generating transformations, but there is more subtlety involved. The reason is that our mode theory reifies axioms as transformations—actual objects that can be composed in more than one way. For example, we can immediately find three transformations $\alpha : \Box {\mathop{{}\Rightarrow}{}} \Box $ . One is simply the identity $1_\Box : \Box {\mathop{{}\Rightarrow}{}} \Box $ . But there are also two more, which combine the ${T}$ and 4 axioms:

$$ \begin{align*} &({T} \ast 1_\Box) \circ {4} : \Box {\mathop{{}\Rightarrow}{}} \Box, \\ &(1_\Box \ast {T}) \circ {4} : \Box {\mathop{{}\Rightarrow}{}} \Box. \end{align*} $$

Moreover, there are two ways to construct a transformation $\Box {\mathop{{}\Rightarrow}{}} \Box ^3$ :

$$ \begin{align*} &({4} \ast 1_\Box) \circ {4} : \Box {\mathop{{}\Rightarrow}{}} \Box^3, \\ &(1_\Box \ast {4}) \circ {4} : \Box {\mathop{{}\Rightarrow}{}} \Box^3. \end{align*} $$

It is not unreasonable to postulate that these different ways of constructing the same transformation are equal, i.e., that

(4) $$ \begin{align} ({T} \ast 1_\Box) \circ {4} = 1_\Box = (1_\Box \ast {T}) \circ {4}, \end{align} $$

(5) $$ \begin{align} ({4} \ast 1_\Box) \circ {4} = (1_\Box \ast {4}) \circ {4}. \end{align} $$

In category theory such equations are called coherence equations: they state that multiple ways of performing a certain transformation are in fact identical in their effect (coherent). The addition of coherence equations means that a category is no longer freely generated.

A mode theory that satisfies these equations can be constructed explicitly: its modalities are of the form $\Box ^n$ for $n \in \mathbb {N}$ ; a transformation $\alpha : \Box ^n {\mathop{{}\Rightarrow}{}} \Box ^m$ is just an order preserving function $\alpha : [m] \to [n]$ where ; and composition of modalities is just their sum [39]. Category theorists will recognise this as the walking comonad, i.e., a tiny 2-category $\mathbf {Comnd}$ such that 2-functors $\mathbf {Comnd} \longrightarrow \mathbf {Cat}$ classify all categories equipped with a specific comonad. The fact that this kind of object occurs in category theory provides external justification for why the above list of equations might be seen as exhaustive.

Of course, this could be seen as being far more work than necessary. We could have constructed a mode theory $\mathcal {M}_{\mathbf {K4}}^{\text {idem}}$ with one mode $\bullet $ , and one modality $\Box : \bullet \to \bullet $ that satisfies the equation

$$ \begin{align*} \Box \circ \Box = \Box \end{align*} $$

and no non-identity transformations. In this mode theory there is a unique transformation $\alpha : \Box {\mathop{{}\Rightarrow}{}} \Box \circ \Box $ : because the boundaries of this transformation are equal, it is just the identity transformation $1_\Box $ on $\Box $ . With this mode theory we can prove a theorem corresponding to 4:

where the leaf on the right branch works exactly because $\Box \circ \Box = \Box $ . This mode theory generates a version of the logic K4, which combines the ${K}$ and 4 axioms. We can also scale it to S4 by adding a transformation $\varepsilon : \Box {\mathop{{}\Rightarrow}{}} 1_\bullet $ from the $\Box $ modality to the identity modality. This leads to the mode theory $\mathcal {M}_{{\mathbf {S4}}}^{\text {idem}}$ , a more explicit description of which is the following: there is one mode $\bullet $ , and the hom-category $\mathrm {Hom}_{\mathcal {M}}({\bullet }, {\bullet })$ consists of two objects $\Box $ and $1_\bullet $ with a single morphism $\epsilon : \Box {\mathop{{}\Rightarrow}{}} 1_\bullet $ between them.

At this point it still appears as if the mode theory $\mathcal {M}_{{\mathbf {S4}}}$ generates almost exactly the same logic as the appreciably simpler mode theory $\mathcal {M}_{{\textbf {S4}}}^{\text {idem}}$ . Modulo syntactic differences—e.g., that $\langle \Box ^2\mid {\varphi }\rangle $ is the same as $\langle \Box \mid {\varphi }\rangle $ —this is true up to provability of formulas: the logic generated by this mode theory is indeed equivalent to (an intuitionistic variant of) S4 at the level of provable theorems. However, at the level of proofs, the logics generated by $\mathcal {M}_{{\mathbf {S4}}}$ and $\mathcal {M}_{{\mathbf {S4}}}^{\text {idem}}$ are rather different! The reasons for that are easily understood only when we use the proofs-as-programs perspective of the Curry–Howard correspondence to study the dynamic behaviour of proofs. For category theorists we will simply mention that whereas $\mathcal {M}_{{\mathbf {S4}}}$ generates a logic whose modality can be interpreted by any comonad with a left adjoint, the mode theory $\mathcal {M}_{{\mathbf {S4}}}^{\text {idem}}$ additionally requires that the said comonad be idempotent.

4.0.4 Encoding multimodal logics

The flexibility afforded by the mode theory means that we can encode multimodal logics in our system. For example, we can encode a simple epistemic logic: if we start with a set of agents $\mathbb {I}$ , we can generate a mode theory with a single mode $\bullet $ and an epistemic modality $K_i : \bullet \to \bullet $ for each $i \in \mathbb {I}$ (read as ‘agent i knows’) [2, Section 12]. If we then add enough transformations—as above—we can capture two of the most popular axioms of epistemic logic:

$$ \begin{align*} &K_i \varphi \to \varphi &&\text{veridicality,} \\ &K_i \varphi \to K_i (K_i \varphi) &&\text{positive introspection.} \end{align*} $$

The axiom $\lnot K_i \varphi \to K_i \lnot K_i \varphi $ of negative introspection cannot be captured as negation is not a modality in our system (it cannot be: modalities preserve conjunctions).

To capture a basic doxastic logic [2, Section 13] we could also add endomodalities $B_i$ (read ‘agent i believes’) along with a transformation

$$ \begin{align*} \mathsf{Aristotle} : K_i {\mathop{{}\Rightarrow}{}} {B_i}, \end{align*} $$

which states that knowledge implies belief. We could also add a strong introspection transformation, that states that an agent knows what they believe:

$$ \begin{align*} \mathsf{Introsp} : B_i {\mathop{{}\Rightarrow}{}} K_i \circ {B_i}. \end{align*} $$

Whether any coherence laws naturally arise in this setting is yet to be determined.

4.0.5 A multimode logic

Our discussion would not be complete without including a bona fide multimode logic. To the best of our knowledge no such logics have appeared before. However, in our work on multimodal Martin-Löf type theory we have found multimode settings extremely useful, especially when there are two distinct ‘universes of discourse’ that we are trying to model. The scenario usually involves a universe of discourse in which some particular principle holds (e.g., some axiom or induction principle), and another in which it does not. These are related by modalities, so that the formulas in one are available in the other under a modality, and can also be related to the formulas of another mode.

We wish illustrate that perspective in the simplest possible way. Consider the mode theory consisting of two objects, ${\mathsf {int}}$ and ${\mathsf {cl}}$ , and a single modality

$$ \begin{align*} {\mathbf{P}}{} : {\mathsf{int}} \to {\mathsf{cl}}. \end{align*} $$

The idea is that the mode ${\mathsf {cl}}$ corresponds to classical logic, and the mode ${\mathsf {int}}$ corresponds to intuitionistic logic. In this setup we are able to add the excluded middle axiom to the rules of the classical mode:

We do not include this rule in the logic of the intuitionistic mode ${\mathsf {int}}$ . If we can prove

then we know that $\varphi $ is a theorem of intuitionistic propositional logic. Thus, only the theorems of intuitionistic logic are available under the modality ${\mathbf {P}}{}$ .

Notice that this modality ${\mathbf {P}}{}$ is not really an ‘inclusion’. For example, we are not able to prove . In fact, this formula need not even be well-formed! To form we must have that , and concluding that from that assumption is a non-trivial metatheorem about the logic.

In the classical mode we may infer that

That is: in the classical mode we can infer that it is either true or false that $\phi $ is intuitionistically true or false. Thus, the classical mode of this logic can be seen as a place where one may reason about truth in intuitionistic logic! Alternatively, the modality $\langle {\mathbf {P}}\mid {-}\rangle $ can be seen as internalising some metatheoretic notion of provability, or even a translation from intuitionistic to classical logic.

5 A Multimodal $\lambda $ -calculus

In this section we establish a Curry–Howard correspondence [14, 16, 23, 41] for multimodal logic. Curry–Howard correspondences are traditionally achieved as follows. Beginning with a natural deduction system, we associate variables with assumptions of the logic. Then, we assign a term to each derivation. The terms themselves are linearly written representations of proof trees, to which they correspond bijectively. This process is sometimes called term assignment.

If we annotate proof trees with terms, then we can view:

• • terms as computer programs,

• • formulas as the types of programs,

• • proof reduction as computation.

In this setting the introduction and elimination rules for implication strongly resemble functional abstraction and function application. Thus, the system of proof terms is often a $\lambda $ -calculus, and proof simplification can be seen as a dynamics of these proofs.

First, we describe the types of our system. These are exactly the same as the formulas, but we consistently replace $\varphi , \psi , \dots $ with $A, B, \dots $ , $\land $ with $\times $ , and $\lor $ with $+$ . The pre-types of are generated by

The types are generated by the following judgement:

Second, we need to describe the contexts of the type system. These are again the same as the natural deduction system, but with the addition of a unique variable for each assumption. Contexts are generated by the rules

considered as before subject to Equations (1) and (2). A point of order: when we add a new binding to a context, we assume that no other assumption uses the same variable. This allows us to uniquely identify which assumption is being used in a proof term without any confusion.

We extend the definition of ${\mathsf {locks}(-)}$ to cover variables in the obvious way:

This operation clearly preserves Equations (1) and (2), and is hence well-defined on contexts. One can show by induction on pre-contexts that this operation is a homomorphism with respect to concatenation, i.e., that

$$ \begin{align*} {\mathsf{locks}(\Gamma, \Delta)} = {\mathsf{locks}(\Gamma)} \circ {\mathsf{locks}(\Delta)} \end{align*} $$

when both sides are defined. ²

The term assignment system for multimodal logic is given in Figure 2. The basic judgement is of the form , which means that M is a term of type A under the context $\Gamma $ , in mode m.

Figure 2 Terms of multimodal logic.

The typing rules closely correspond to the rules of the logic in Figure 1. For example, we have replaced conjuction $\land $ by the Cartesian product $\times $ . We may construct a proof of $A \times B$ by pairing together a proof of A and of B. Hence, the Curry–Howard correspondence is readily apparent.

One subtle point is that the terms for the introduction of an implication, the elimination of a disjunction, and the elimination of modal term all create bound variables. For example, the variable is bound in the subterm within . Similarly, the variable is bound in within . Thus, the usual rules of capture avoidance need to be employed.

5.1 Metatheory

We have the following metatheoretic results on the term assignment system. The proofs of these are ordinary inductions, but require care in propagating the various modal contraptions within terms.

It is also worth noting that any metatheorem we establish about this system is also a metatheorem about the logic given in Figure 1: all we have to do is erase the new ingredients (terms, variables, and so on). Thus, the theorems established in this section directly correspond to the claims in Section 3.4.

Theorem 5.1 (Structural rules).

The following rules are admissible:

As discussed in Section 3.4, we cannot be cavalier with adding locks to the context. The following rule describes how to weaken already extant locks. Given a $2$ -cell $\alpha $ and two (disjoint) pre-contexts $\Gamma $ and $\Delta $ , we define the partial metatheoretic operation

by the following clauses:

Theorem 5.2 (Lock weakening).

In the following rule the term in the conclusion is well-defined when the premises hold, and the rule itself is admissible.

With lock weakening at hand, we define a metatheoretic operation

which stands for the substitution of M for the variable x under context $\Gamma $ . In most cases this operation simply recurses appropriately through the structure of the term. The novel clauses are

The rest are according to custom. Notice that $\Gamma $ is a global parameter to this definition, and is only used in the base case in order to effect lock weakening.

Theorem 5.3 (Cut).

The following rule is admissible:

5.1.1 Equational theory

With the preceding metatheorems in hand we are now able to formulate an equational theory of terms for this system. The equational theory specifies a minimal set of equations between proofs of a certain formula/type. In particular, the cut elimination theorem suggests the following two $\beta $ -rules:

A very similar equational theory was developed by Gratzer, Kavvos, Nuyts, and Birkedal [18, 19], but for an algebraically-specified system of dependent types.

Finally, we could also make these equations directed, and consider them as reductions from one term to another. That way we could see this system as a programming language that is equipped with an operational semantics.

6 Related work

Multimode logics were inspired by the decomposition of the $!$ modality of Linear Logic [15] into two adjoint functors/modalities. This was used by Benton [3] to present Linear Logic through the LNL (linear-non-linear) calculus, which had two modes: linear and intuitionistic. Many years later this pattern was used by Reed [38] in an unpublished manuscript which presented adjoint logic, the first multimode and multimodal logic. The modes and modalities of the Reed’s logic were presented through a mode theory that was a preorder; in our terminology this means that the 2-category had no transformations, and between two modes there was at most one modality.

The 2-categorical specification of mode theories was introduced by Licata and Shulman [26], who presented a single-premise, single-conclusion, multimodal sequent calculus with adjoint modalities. This was later refined by Licata, Shulman, and Riley [27] into a multimode and multimodal framework that also subsumes a number of substructural logics. While much of work of Reed, Licata, and collaborators concerned sequent calculi, they did also present a natural deduction framework for a general modal type theory. Unfortunately, the generality of the theory meant that the rules were rather complex and involved ubiquitous annotation by modal and substructural information. This precluded their immediate generalization to practicable modal type theories.

A decisive step towards that direction happened with the re-introduction of Fitch-style modal $\lambda $ -calculi by Clouston [8]. The Fitch style of natural deduction, which mirrors the classic opening and closing of proof boxes at the level of proof terms, was adapted to formulate two modal Martin-Löf type theories, one by Birkedal, Clouston, Mannaa, Møgelberg, Pitts, and Spitters [4] and one by Gratzer, Sterling, and Birkedal [20]. These arise from a Fitch-style formulation of K and S4 respectively.

The next step, which was that of generalising modal Martin-Löf type theories to a multimode, multimodal setting, proved more challenging. In particular, generalizing the elimination rule proved to be problematic. Later work would show that the good behaviour of these elimination rules relied on additional structure [17]. In the case of a single modality, this additional structure was often admissible, but for multiple modalities it was necessary to manually postulate. However, adding such structure explicitly imposed further restrictions on which modalities could be incorporated into the logic, making the elimination rule less desirable as a basis for a general framework.

A solution was given by Gratzer, Kavvos, Nuyts, and Birkedal [18, 19], who combined Reed’s mode theories with a Fitch-style ‘lock’ operation on contexts, and an elimination rule the dual-context style of Davies and Pfenning [9, 25, 34]. This particular combination proved to work well in practice, leading to many examples of multimodal type-theoretic reasoning. This type of theory directly inspired the logic and modal $\lambda $ -calculus in this paper. Unlike op. cit. we present the calculus in elementary terms, i.e., without using the machinery of generalised algebraic theories.

Before the work by Gratzer, Kavvos, Nuyts, and Birkedal [18, 19] there were a limited number of type theories with multiple modalities. These were usually ad hoc, as the approach was almost always guided by special properties of the modalities of interest. With no claims to completeness we mention the work of Pfenning [33], Shulman [40], Nuyts, Vezzosi, and Devriese [32], and Nuyts and Devriese [31].