Intuitionistic Necessity Revisited (Extended Abstract)

Gavin Bierman M. Claudia Meré^{∗} Valeria de Paiva

Computer Laboratory University of Cambridge

October 27, 1992

1 Introduction

In this note we shall study a specific intuitionistic, propositional modal logic, namely S4 [10, 4, 11]. More specifically we shall only consider the necessity modality.

Here (as well as elsewhere [3]) we advocate the view that for a given logical system we must be able to give all of the following:

• A Sequent Calculus Formulation

• A Natural Deduction Formulation

• An Axiomatic Presentation^{1}

• A (Categorical) Semantics

In particular we are interested in term assignment systems. These follow from the sequent calculus and natural deduction formulations by the well known Curry-Howard Correspondence [8]. Such systems open up the study of logics to the world of functional programming.

It is our belief that our approach can be used to study a family of modal logics; this note serves as an example. In particular we give a simpler natural deduction formulation than previous attempts, and also a significantly more elegant categorical treatment.

2 A Sequent Calculus Formulation of S4

We start by recalling a sequent calculus formulation for Intuitionistic Modal Logic S4 as presented by Curry [4]. We add the rules for the necessity modality, □, to Gentzen’s original system LJ for Intuitionistic Logic. The rules are presented in Figure 1.

∗Now at Departamento de Informática, PUC - Rio de Janeiro, Brazil.

1We shall omit the well known axiomatic presentation in this note.

\begin{aligned}& Axiom \\ A ⊢ A \end{aligned}

Γ ⊢ B B, Δ ⊢ C
Cut

Γ, Δ ⊢ C

Γ, A, B, Δ ⊢ C

\overline{Exchange}

Γ, B, A, Δ ⊢ C

\begin{aligned}& (⊥_{L}) \\ Γ, ⊥ ⊢ A \end{aligned}

Γ ⊢ C ; \overline{Weakening} ; Γ, A ⊢ C  Γ, A, A ⊢ C ; \overline{Contraction} ; Γ, A ⊢ C

Γ, A ⊢ C Δ, B ⊢ C ; (∨_{L}) ; Γ, Δ, A ∨ B ⊢ C Γ ⊢ A ; (∨_{R}) ; Γ ⊢ A ∨ B Γ ⊢ B ; (∨_{R}) ; Γ ⊢ A ∨ B

Γ, A, B ⊢ C ; (∧_{L}) ; Γ, A ∧ B ⊢ C  Γ ⊢ A  Δ ⊢ B ; (∧_{R}) ; Γ, Δ ⊢ A ∧ B

Γ ⊢ A  Δ, B ⊢ C ; (→_{L}) ; Γ, Δ, A → B ⊢ C  Γ, A ⊢ B ; (→_{R}) ; Γ ⊢ A → B

Γ, A ⊢ B ; (□_{L}) ; Γ, □A ⊢ B  □Γ ⊢ A ; (□_{R}) ; □Γ ⊢ □A

Figure 1: Sequent Calculus formulation of Intuitionistic S4

We use Γ, Δ to represent sequences of formulae and A, B for single formulae. The Exchange rule simply allows the permutation of assumptions. The Weakening rule permits assumptions to be discarded and the Contraction rule allows an assumption to be duplicated. In what follows we shall consider the Exchange rule to be implicit, whence the convention that Γ, Δ denote multisets of assumptions. Negation is defined, as usual, as

¬A ::= A → ⊥

In classical modal logic the possibility modality, ⋄A, can be defined as ¬□¬A, but intuitionistically the situation is more complex. Following Curry we shall not consider this modality in this note.

3 Natural Deduction for S4

In the natural deduction system, due to Gentzen [14], but expounded by Prawitz [11], a deduction is a derivation of a proposition from a finite set of assumption packets, using some predefined set of inference rules. Within a deduction, we may ‘discharge’ any number of assumption packets. Assumption packets can be given natural number labels and applications of inference rules can be annotated with the labels of those packets which it discharges.

We give the inference rules in Figure 2. Our presentation differs from others only in its (simpler) treatment of the modality.

\begin{matrix}· \\ · \\ · \end{matrix} ; ⊥ ; (⊥_{E}) ; A ; \begin{matrix}[A^{x}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B ; (→_{I}) ; A → B & \begin{aligned}\begin{matrix}· \\ · \\ · \end{matrix} ; A → B & \begin{matrix}· \\ · \\ · \end{matrix} ; A \\ & & (→_{E}) \\ B \end{aligned} \\ \begin{aligned}\begin{matrix}· \\ · \\ · \end{matrix} ; A & \begin{matrix}· \\ · \\ · \end{matrix} ; B \\ & (∧_{I}) \\ A ∧ B \end{aligned} & \begin{matrix}· \\ · \\ · \end{matrix} ; A ∧ B ; (∧_{E}) ; A \begin{matrix}· \\ · \\ · \end{matrix} ; A ∧ B ; (∧_{E}) ; B \\ \begin{matrix}· \\ · \\ · \end{matrix} ; A ; (∨_{I}) ; A ∨ B \begin{matrix}· \\ · \\ · \end{matrix} ; B ; (∨_{I}) ; A ∨ B & \begin{aligned}\begin{matrix}· \\ · \\ · \end{matrix} ; A ∨ B & [A] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C & [B] ; \begin{matrix}· \\ · \\ · \end{matrix} ; C \\ & & & (∨_{E}) \\ & C \end{aligned} \\ \begin{matrix}· \\ · \\ · \end{matrix} ; □B ; (□_{E}) ; B & \begin{aligned}\begin{matrix}· \\ · \\ · \end{matrix} ; □A_{1} & … & \begin{matrix}· \\ · \\ · \end{matrix} ; □A_{n} & [□A_{1}^{x_{1}} ⋯ □A_{n}^{x_{n}}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B \\ & & & (□_{I}) \\ & & □B \end{aligned} \end{matrix}

Figure 2: Natural Deduction Formulation of S4

The usual introduction rule for □ insists that all of the undischarged assumptions at the time of application are modal, i.e. they are all of the form □A_{i}. However, an additional fundamental feature of natural deduction is that it is closed under substitution. One might be tempted to give the rule for (□_{I}) as

□A_{1} ⋯ □A_{n} ; \begin{matrix}· \\ · \\ · \end{matrix} ; B

(□_{I})
□B

but clearly this rule is not closed under substitution. For example, substituting for □A_{1}, the deduction

C → □A_{1} C
(→_{E})
□A_{1}

we get the following deduction

C → □A_{1} C ; (→_{E}) ; □A_{1} ⋯ □A_{n}

\begin{matrix}· \\ · \\ · \end{matrix}

B

(□_{I}) □B

which is no longer a valid deduction (the assumptions are not all modal). We conclude that (□_{I}) must be formulated as in Figure 2, where the substitutions are given explicitly.

It is possible to present natural deduction rules in a ‘sequent-style’, where given a sequent Γ ⊢ A, Γ represents all the undischarged propositions so far in the deduction, and A represents the conclusion of the deduction. This formulation should not be confused with the sequent calculus formulation, which differs by having operations which act on the left and right of the turnstile, rather than rules for the introduction and elimination of logical operators. The ‘sequent-style’ formulation of natural deduction for S4 is given in Figure 3.

A ⊢ A

Γ ⊢ ⊥ ; (⊥_{E}) ; Γ ⊢ A

Γ, A ⊢ B ; (→_{I}) ; Γ ⊢ A → B  Γ ⊢ A → B  Δ ⊢ A ; (→_{E}) ; Γ, Δ ⊢ B

Γ ⊢ A  Δ ⊢ B ; (∧_{I}) ; Γ, Δ ⊢ A ∧ B  Γ ⊢ A ∧ B ; (∧_{E}) ; Γ ⊢ A Γ ⊢ A ∧ B ; (∧_{E}) ; Γ ⊢ B

Γ ⊢ A ; (∨_{I}) ; Γ ⊢ A ∨ B Γ ⊢ B ; (∨_{I}) ; Γ ⊢ A ∨ B Γ ⊢ A ∨ B  Δ, A ⊢ C  Δ, B ⊢ C ; (∨_{E}) ; Γ, Δ ⊢ C

Δ_{1} ⊢ □A_{1} ⋯ Δ_{n} ⊢ □A_{n} □A_{1}, …, □A_{n} ⊢ B

(□_{I})

Δ_{1}, …, Δ_{n} ⊢ □B

Γ ⊢ □A ; (□_{E}) ; Γ ⊢ A

Figure 3: Sequent formulation of S4 natural deduction

The Curry-Howard Correspondence [8] relates typed calculi to constructive logics. It essentially annotates each stage of a deduction with a ‘term’, which is an encoding of the construction of the deduction so far. Consequently a logic can be viewed as a type system for a term assignment system. The Correspondence also links proof normalisation to term reduction.

We can use the Curry-Howard Correspondence to obtain the term assignment system given in Figure 4. We should point out that the unique natural number labels mentioned above, are replaced by (the more familiar) unique variable names.

x : A ⊢ x : A
Γ ⊢ e : ⊥
(⊥_{E})
Γ ⊢ ∇_{A}(e) : A
Γ, x : A ⊢ e : B ; (→_{I}) ; Γ ⊢ λx.e : A → B  Γ ⊢ e : A → B  Δ ⊢ f : A ; (→_{E}) ; Γ, Δ ⊢ ef : B

Γ ⊢ e : A  Δ ⊢ f : B ; (∧_{I}) ; Γ, Δ ⊢ ⟨e, f⟩ : A ∧ B Γ ⊢ e : A ∧ B ; (∧_{E}) ; Γ ⊢ fst(e) : A Γ ⊢ f : A ∧ B ; (∧_{E}) ; Γ ⊢ snd(f) : B

Γ ⊢ e : A ; (∨_{I}) ; Γ ⊢ inl(e) : A ∨ B  Γ ⊢ e : B ; (∨_{I}) ; Γ ⊢ inr(e) : A ∨ B
Γ ⊢ e : A ∨ B  Δ, x : A ⊢ f : C  Δ, y : B ⊢ g : C
(∨_{E})

Γ, Δ ⊢ case e of inl(x) →f∥ inr(y)→g : C

Δ_{1} ⊢ e_{1} : □A_{1} ⋯ Δ_{n} ⊢ e_{n} : □A_{n} x_{1} : □A_{1}, …, x_{n} : □A_{n} ⊢ f : B
(□_{I})
Δ_{1}, …, Δ_{n} ⊢ box f with e_{1}, …, e_{n} for x_{1}, …, x_{n} : □B
Γ ⊢ e : □A
(□_{E})
Γ ⊢ unbox(e) : A

Figure 4: Term Assignment System for S4

We could have used more traditional pattern matching term constructors in the last two rules but we have chosen ‘box’ and ‘unbox’ as we feel they are more instructive.

We note at once a significant property of the term assignment system for S4. Essentially the terms code the derivation trees so that any valid term assignment has a unique derivation.

Theorem 1 (Unique Derivation) For any term t and proposition A, if there is a valid derivation of the form Γ ⊢ t : A, then (Γ is uniquely determined by t and A) and there is a unique derivation of Γ ⊢ t : A.

Proof. By induction on the structure of t. □

We shall see that the term assignment system we derive in Section 5 from semantical considerations is equivalent to the term assignment system based on our analysis of natural deduction. For our system, the substitution property holds.

Theorem 2 (Substitution) If Γ ⊢ a : A and Δ, x : A ⊢ b : B then Γ, Δ ⊢ b[a/x] : B

Proof. By induction on the derivation Δ, x : A ⊢ b : B □

Before we continue, a quick word concerning the (□_{I}) rule. At first sight this seems to imply an ordering of the e_{i} and x_{i} subterms. However, the Exchange rule (which does not introduce any additional syntax) tells us that any such order is really just the effect of writing terms in a sequential manner on the page. (As we shall see, the naturality equations derived from the categorical model have similar consequences.)

Comparison with Prawitz’s Formulation

Prawitz [11] also noticed the problem of closure under substitution, but his solution involves a new notion of “essentially modal” formulae and also the tracing of assumptions. We feel that our solution is conceptually simpler.

Consider the case of normalisation. In natural deduction, normalisation steps occur when a formula is introduced only to be immediately eliminated. In this case we say that a detour (redex) exists in the derivation (term). Normalisation is the process of eliminating all detours (redexes). For our formulation we can easily derive the normalisation step for the modal operator—Prawitz has much more difficulty.

In our formulation, the derivation where (□_{I}) is followed by (□_{E})

\begin{matrix}· \\ · \\ · \end{matrix} ; □A_{1} … \begin{matrix}· \\ · \\ · \end{matrix} ; □A_{n} [□A_{1}] … [□A_{n}] ; \begin{matrix}· \\ · \\ · \end{matrix} ; B
(□_{I})
□B
(□_{E})
B

normalises to

\begin{matrix}· \\ · \\ · \end{matrix} ; [□A_{1}] … \begin{matrix}· \\ · \\ · \end{matrix} ; [□A_{n}]

\begin{matrix}· \\ · \\ · \end{matrix}

B

4 The Categorical Model

The fundamental idea of the categorical treatment of proof theory is that propositions should be interpreted as the objects of a category (or multicategory, or polycategory) and proofs should be interpreted as maps; operations transforming proofs into proofs then correspond (if possible) to natural transformations (between appropriate hom-functors) in the categorical sense. The maps modelling proofs are built up using these categorical operations and so the problem of providing a categorical model is essentially the problem of providing the natural operations. Here we carry out this programme for S4.

Observe that versions of this programme have been carried out by other people, notably Flagg [6]; Meloni and Ghilardi [7] and Reyes and Zolfaghari [12]. Flagg considered the case of posets (as special kinds of categories) and other researchers have worked with toposes, a framework much more expressive than is necessary for our purposes. Our work is different as it is based on producing in parallel to the categorical model, a term assignment system for the logic and it arises from our work on Intuitionistic Linear Logic [3].

With a view to understanding what is involved here, let us consider the traditional analysis of the proof theory of some basic intuitionistic logic via the notion of a cartesian closed category. (Lambek and Scott [9] is a good source for this material.) In that case, the basic normalization process gives rise to β-equality on the terms of the typed λ-calculus. The β-equality rule is valid in any cartesian closed category, but the attractive categorical assumption of being cartesian closed amounts to requiring βη-equality, that is, to a further ‘extensionality’ assumption. Thus one way to understand what we do is that we make a minimal number of attractive simplifying assumptions about a basic categorical set up which at least entail the (desired) equalities between proofs. (Of course we would like the equalities to make some kind of sense!) In this section we simply discuss the categorical assumptions we make.

Since we are dealing with sequents Γ ⊢ A, in principle we should deal with multicategories. However it simplifies things to assume at once that the multicategorical structure is represented by a tensor product •, so that we are dealing with a monoidal category. We shall write ⟨⟩ for the unit of this tensor product. To simplify the presentation we use the same symbols both for propositions of modal logic and for their denotations in our monoidal category. The idea then is that a sequent of form

C_{1}, C_{2}, …, C_{n} ⊢ A

will be interpreted as a map C_{1} • C_{2} • … • C_{n} → A, i.e. from the product of the C_{i} to A. (Thus a coherence result is assumed.) When Γ is the sequence C_{1}, C_{2}, …, C_{n}, we write Γ → A for this map.

The whole process is based upon some simple assumptions about the interpretation of the basic structural rules, and a simple procedure for dealing with the logical rules, which we describe in turn.

4.1 Structural Rules

The sequent representing the Identity rule is interpreted as the (canonical) identity arrow A ⟶^{1_{A}} A from A to A. The rule of Exchange we interpret by assuming that we have a symmetry for the product • (making our model a symmetric monoidal category). We henceforth suppress Exchange and the corresponding symmetry; thus we really consider multisets of formulae.

The Cut rule

Γ ⊢ A A, Δ ⊢ B

\overline{Cut}

Γ, Δ ⊢ B

is then interpreted as a generalized form of composition: if the maps Γ ⟶^{f} A and A • Δ ⟶^{g} B are the interpretations of hypotheses of the rule, then the composite

Γ • Δ −f • 1_{Δ} ; \begin{matrix}− \\ − \\ − \\ − \\ − \\ − \end{matrix}⟶ A • Δ − g ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ B

is the interpretation of the conclusion.

The Contraction and Weakening rules amount to requiring diagonals and projections respectively for the monoidal structure. We shall make the (traditional) simplifying assumption that our categories are cartesian.

4.2 Logical rules

We shall make the assumption that any logical rule corresponds to an operation on maps of the category which is natural in (the interpretations of) the components of the sequents which remain unchanged during the application of a rule. Composition corresponds to Cut so clearly the logical significance is that we are assuming that our operations commute (where appropriate) with Cut.

Since the correspondence between the (intuitionistic) logical connectives of conjunction, disjunction and implication and cartesian products, coproducts and function-spaces in a cartesian closed category is well-known we proceed directly to the modality rules.

Logical rules for the modality ‘□’

Consider the (□_{L}) rule

Γ, A ⊢ B ; (□_{L}) ; Γ, □A ⊢ B

It gives an operation taking an arrow Γ • A → B to an arrow Γ • □A → B, however it is a consequence of naturality that this operation is determined by its effect on identity arrows, thus it is enough to give a map □A ⟶^{ε} A. Then given an arrow f: Γ • A → B, the required arrow Γ • □A → B is the composite

Γ • □A −1 • ε ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ Γ • A −f ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ B

Now consider the problematic (□_{R}) rule

□Γ ⊢ A ; (□_{R}) ; □Γ ⊢ □A

This gives an operation taking an arrow □Γ → A to an arrow □Γ → □A. Firstly let us consider the derivation where we apply the (□_{R}) rule to the axiom □A ⊢ □A to obtain the derivation

□A ⊢ □A ; (□_{R}) ; □A ⊢ □□A

In other words, from an identity arrow □A ⟶ □A we can get a canonical arrow δ_{A}: □A → □□A.

We shall assume that □ is a functor, thus it takes an arrow f: A → B to □f: □A → □B. Consequently the process described above of taking an arrow g : □Γ → A to an arrow □Γ → □A is (approximately) the composition of the map δ_{Γ}: □Γ → □□Γ with the map □□Γ → □A arising from an application of the functor □ to the arrow g. We shall consider this in more detail later.

Summarizing the contents of this section we have as a first approximation of a categorical model of S4 as a cartesian closed category together with an endofunctor □ and maps ε and δ. We stress that rather elementary assumptions and unsophisticated categorical observations have been used in this analysis. However this analysis can lead us to a term assignment system in a very straightforward way, as we can see in the next section.

5 Categorical considerations and term assignment

The sequent calculus is best thought of as providing not proofs themselves, but a metatheory concerning proofs. Hence a formulation in these terms does not always provide clear clues as to how it should be enriched to a term assignment system. Fortunately we can use the general form of a categorical model (of the proof theory) of the logic to derive an appropriate term assignment system for the sequent calculus formulation of this logic. The idea is to enrich any sequent judgement to a term assignment judgement of the form

x_{1}: C_{1}, x_{2}: C_{2}, …, x_{n}: C_{n} ⊢ e: A

where the x_{i} are distinct variables and e is a term; usually we suppress (irrelevant) variables and write Γ ⊢ e: A for this term assignment. The whole process is based on simple assumptions about the (categorical) interpretation of the logical rules.

Deriving the term formation rules

The terms associated with the structural rules and (usual) logical connective rules are standard. We shall proceed directly to the terms associated with the □ rules.

Logical rules for the connective ‘□’

Consider the (□_{L}) rule

Γ, A ⊢ B ; (□_{E}) ; Γ, □A ⊢ B

Since it gives an operation taking an arrow Γ • A → B to an arrow Γ • □A → B, an appropriate syntax is

Γ, x : A ⊢ e : B

\overline{Dereliction}

Γ, z : □A ⊢ let z be □x in e : B

and indeed this is the syntax given by Abramsky [1] for a similar situation in Intuitionistic Linear Logic. With this formulation naturality in B gives rise to an equation

f[let z be □x in e/y] = let z be □x in f[e/y]

However as we have mentioned before this operation is determined by its effect on identity arrows, thus an appropriate syntax (and the one we shall use in what follows) is

Γ, x : A ⊢ e : B

(□_{L})
Γ, z : □A ⊢ e[unbox(z)/x] : B

Consider the (□_{R}) rule again

□Γ ⊢ A ; (□_{R}) ; □Γ ⊢ □A

This gives an operation taking an arrow □Γ → A to an arrow □Γ → □A. The important point to realize is that if the operation is not natural in □Γ, then the operation should not preserve substitution for the free variables implicitly declared in □Γ. Hence we are restricted to giving an operation on ‘higher-order’ terms, where the variables which appear initially must be bound and fresh variables introduced. These considerations lead to the term assignment rule

\overline{x} : □Γ ⊢ e : A

\overline{Promotion}

\overline{y} : □Γ ⊢ box e with \overline{y} for \overline{x} : □A

This concludes our derivation of a term assignment system for S4 from general considerations of the form of a categorical model. We display this system of term assignment in Figure 5.

x : A ⊢ x : A

Γ ⊢ e : A Δ, x : A ⊢ f : B

Cut

Γ, Δ ⊢ f[e/x] : B

\begin{aligned}& (⊥_{L}) \\ Γ, x : ⊥ ⊢ ∇_{A}(x) : A \end{aligned}

Γ, x : A ⊢ e : C Δ, y : B ⊢ f : C
(∨_{L})
Γ, Δ, z : A ∨ B ⊢ case z of inl(x) →e∥ inl(y)→f : C
Γ ⊢ e : A ; (∨_{R}) ; Γ ⊢ inl(e) : A ∨ B  Γ ⊢ e : B ; (∨_{R}) ; Γ ⊢ inr(e) : A ∨ B

Γ ⊢ e : A  Δ, x : B ⊢ f : C ; (→_{L}) ; Γ, g : A → B, Δ ⊢ f[(ge)/x] : C  Γ, x : A ⊢ e : B ; (→_{R}) ; Γ ⊢ λx.e : A → B
Δ, x : A, y : B ⊢ f : C
(∧_{L})

Δ, z : A ∧ B ⊢ f[fst(z)/x, snd(z)/y] : C

Γ ⊢ e : A Δ ⊢ f : B ; (∧_{R}) ; Γ, Δ ⊢ ⟨e, f⟩ : A ∧ B

Γ, x : A ⊢ e : B
(□_{L})
Γ, z : □A ⊢ unbox z for x in e : B

\overline{x} : □Γ ⊢ e : A

\overline{Promotion}

\overline{y} : □Γ ⊢ box e with \overline{y} for \overline{x} : □A

Figure 5: Term Assignment System for sequent calculus

6 Equalities and Reductions

Our analysis has not only led us to a term assignment system, but has uncovered a series of naturality equations. We could, as we have done elsewhere [3], discuss at length a series of equations corresponding to the process of normalization in Natural Deduction and/or cut elimination in the sequent calculus, using simple proof-theoretic methods. These equations can be read (from left-to-right) as reductions in the term assignment system. Instead of deriving all the equalities/reductions arising from the principal cuts (or normalization) we simply display them in Figure 6.

7 The Categorical Model Revisited

Now we consider the meaning of the β-rule for □ involving (□_{L}). The categorical import of this rule is that any map □Γ → A factors in a canonical way as a composite

□Γ −\begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ □A −ε_{A} ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ A

where □A ⟶^{ε_{A}} A is the canonical map obtained by (□_{L}) from the identity. Given any proof Γ ⊢ B there is obviously a canonical two-step process that transforms it into a proof

fst(⟨e, f⟩)  →_{β} e
snd(⟨e, f⟩)  →_{β} f
case inl(e) of inl(x) →f∥ inr(y)→g  →_{β} f[e/x]
case inr(e) of inl(x) →f∥ inr(y)→g  →_{β} g[e/y]
h[(λx.f)g/y]  →_{β} h[f[g/x]/y]
(f[unbox(q)/p])[box e with y_{i} for x_{i}/q] →_{β} f[e/p]

Figure 6: Principal reduction rules

□Γ ⊢ □B by applying the (□_{L}) rule (several times) followed by (□_{R}).

\begin{aligned}Γ ⊢ B \\ & (□_{L}) \\ □Γ ⊢ B \end{aligned} ; (□_{R}) ; □Γ ⊢ □B

If f : Γ ⟶ B interprets the original proof, we write the resulting arrow as □f: □Γ ⟶ □B. As a preliminary simplification, we assume that this definition gives the extension of □ to a multicategorical functor. This amounts to the assumption that □ is a monoidal functor; that is, the functor □ comes equipped with a natural transformation

m_{A,B}: □A × □B → □(A × B)

(natural in A and B) and a morphism m_{I}: I → □I making a standard collection of diagrams commute. (The definition is given in Eilenberg and Kelly [5].)

Note that the β-rule for (□_{L}) certainly implies that for any f: Γ → A, the following equation holds.

□f; ε_{A} = ε_{Γ}; f

Either composite gives the effect of (□_{L}) on f. This shows that ε: □ → Id will be a multicategorical natural transformation and so a monoidal natural transformation.

With the equations to hand we know rather little about the other map, δ. One can easily check that the composite

□A −δ_{A} ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ □□A − ε ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ □A

is the identity on □A, and that is one of the triangle identities for a comonad, but that is about it. However it is tempting to add to our preliminary assumption that □ is a monoidal functor, the assumption that δ (as well as ε) is a monoidal natural transformation and that (□, ε, δ) forms a comonad on our category. These assumptions are quite natural in the context of the 2-category of monoidal categories, monoidal functors and monoidal natural transformations. (The basic notions are again due to Eilenberg and Kelly [5].) Note that given a monoidal comonad (□, ε, δ), the (□_{R}) rule can be interpreted as follows: given a map f: □C_{1} × … × □C_{n} ⟶ A we obtain the ‘boxed’ map as the composite

□C_{1} × … × □C_{n} − δ ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ □□C_{1} × … × □□C_{n} −m ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ □(□C_{1} × … × □C_{n}) −□f ; \begin{matrix}− \\ − \\ − \\ − \end{matrix}⟶ □A

We can formulate the conditions that (□, ε, δ) be a monoidal comonad directly in terms of the basic operations given by the logic. In addition to the β-equality we obtain:

box (unbox(x)) with z for x = z  (1)
box g with (box f with z_{i} for x_{i}), w_{j} for y, y_{j} =
box (g[box f with z′_{i} for x_{i}/y]) with z_{i}, w_{j} for z′_{i}, y_{j}.  (2)

Equation (1) can be thought of as an η-rule, as it provides a kind of uniqueness of the factorization mentioned above; equation (2) expresses an appropriate form of naturality of the operation given by (□_{R}).

We summarize some of the discussion in this section in the following definition.

Definition 1 A categorical model for S4 consists of a cartesian closed category together with a monoidal comonad (□, ε, δ).

We have indicated in the text above some of the equations in our term assignment system corresponding to our notion of categorical model. (These equations can be read (from left-to-right) as reductions in the term assignment system). Instead of deriving all the equalities/reductions we simply display these in Figure 7. These rules are sound and complete for our notion of a model. Further details of this point will appear in an expanded paper.

Theorem 3

1. (Soundness) For any signature and interpretation of the corresponding system in a categorical model for S4 (all the equational consequences of) the typed equations in Figure 7 hold in the sense that the interpretations of either term gives the same map in the category.

2. (Completeness) For any signature there is a categorical model for S4 and an interpretation of the system in it with the following property:

• If Γ ⊢ t: A and Γ ⊢ s: A are derivable in the system then t and s are interpreted as the same map Γ → A just when t = s: A is provable from the equations in Figure 7 (in typed equational logic).

Proof. The proof of soundness involves labouriously checking for each rule that a relevant diagram commutes in the category. Details can be found in the full paper.

The proof of completeness is by the usual categorical term model construction and is omitted. □

fst(⟨e, f⟩)  = e
snd(⟨e, f⟩)  = f
⟨fst(e), snd(e)⟩  = e
case inl(e) of inl(x) →f∥ inr(y)→g  = f[e/x]
case inr(e) of inl(x) →f∥ inr(y)→g  = g[e/y]
(λx.t)e  = t[e/x]
λx.tx  = t
unbox(box t with e_{i} for x_{i})  = t[e_{i}/x_{i}]
box unbox(x) with z for x  = z
box g with (box f with z_{i} for x_{i}), w_{j} for y, y_{j} = box
with z_{i}, w_{j} for z′_{i}, y_{j}  (g[box f with z′_{i} for x_{i}/y])

Figure 7: Categorical equalities

8 Conclusions

In this paper we have considered the propositional, intuitionistic modal logic S4, and have given a sequent calculus formulation, a natural deduction formulation, the corresponding term assignment systems as well as a general categorical model.

Prawitz gave a natural deduction formulation of S4 (and S5) in his monograph, although it required extra machinery specifically for these modal logics. Indeed it has proved difficult to extend his sort of analysis to other systems of modal logics. Segerberg [13, pages 29–30] has also given a natural deduction formulation although he introduces the notion of an indexed modality. More recently, Benevides and Maibaum [2] have presented a natural deduction formulation of S4 inspired by the observation of Hacking that modal logic is in some sense metalogical. This metalogical viewpoint is entwinned within the formulation.

Categorical notions of S4 modalities were considered by Flagg [6] although he only worked within the framework of posets. Other categorical investigations of S4 have been performed within the framework of Toposes, notably by Ghilardi and Meloni [7] and Reyes and Zolfaghari [12]. Although our approach is somewhat different we emphasize again our resulting simpler categorical framework.

It is our hope that our approach will shed light on the problem of quantification in modal logics. This is future work. We should also like to consider other modal logics within our framework. We should like to investigate the effect of our term assignment on the problem of proof search in modal logic. Finally we should like to consider our term assignment within the world of functional programming.

Acknowledgements

We should like to thank Martin Hyland for his guidance with this work.

References

[1] Samson Abramsky. Computational interpretations of linear logic. Technical Report 90/20, Department of Computing, Imperial College, London, October 1990.

[2] Mario Benevides and Thomas Maibaum. A constructive presentation for the modal connective of necessity. Journal of Logic and Computation, 2(1):31–50, 1992.

[3] Nick Benton, Gavin Bierman, Valeria de Paiva, and Martin Hyland. Term assignment for intuitionistic linear logic. Technical Report 262, Computer Laboratory, University of Cambridge, August 1992.

[4] Haskell B. Curry. Foundations of Mathematical Logic. Dover, 1976.

[5] S. Eilenberg and G.M. Kelly. Closed categories. In Proceedings of Conference on Categorical Algebra, La Jolla, 1966.

[6] Robert C. Flagg. Church’s thesis is consistent with epistemic arithmetic. In Intensional Mathematics, 1985.

[7] S. Ghilardi and G. Meloni. Modal and tense predicate logic: models in presheaves and categorical conceptualization. In Categorical Algebra and its Applications, volume 1348 of Lecture Notes in Mathematics, pages 130–142, 1988.

[8] W.A. Howard. The formulae-as-types notion of construction. In J.R. Hindley and J.P. Seldin, editors, To H.B. Curry: Essays on combinatory logic, lambda calculus and formalism. Academic Press, 1980.

[9] J.Lambek and P.J.Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1987.

[10] C.I. Lewis. A Survey of Symbolic Logic: the classic algebra of logic. Dover, 1960.

[11] Dag Prawitz. Natural Deduction, volume 3 of Stockholm Studies in Philosophy. Almqvist and Wiksell, 1965.

[12] G.E. Reyes and H. Zolfaghari. Topos-theoretic approaches to modalities. Technical Report 911-8, Université de Montréal, Québec, 1991.

[13] K. Segerberg and R. Bull. Basic modal logic. In Handbook of Philosophical Logic, pages 1–89. D. Reidel, 1984.

[14] M.E. Szabo, editor. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, 1969.