FitchStyle Modal Lambda Calculi
Abstract
Fitchstyle modal deduction, in which modalities are eliminated by opening a subordinate proof, and introduced by shutting one, were investigated in the 1990s as a basis for lambda calculi. We show that such calculi have good computational properties for a variety of intuitionistic modal logics. Semantics are given in cartesian closed categories equipped with an adjunction of endofunctors, with the necessity modality interpreted by the right adjoint. Where this functor is an idempotent comonad, a coherence result on the semantics allows us to present a calculus for intuitionistic S4 that is simpler than others in the literature. We show the calculi can be extended à la tense logic with the left adjoint of necessity, and are then complete for the categorical semantics.
Keywords
Intuitionistic modal logic Typed lambda calculi Categorical semantics1 Introduction
The CurryHoward propositionsastypes isomorphism [21, 39, 41] provides a correspondence between natural deduction and typed lambda calculus of interest to both logicians and computer scientists. For the logician, term assignment offers a convenient notation to express and reason about syntactic properties such as proof normalisation, and, especially in the presence of dependent types, allows proofs of nontrivial mathematical theorems to be checked by computer programs. For the computer scientist, logics have been repurposed as typing disciplines to address problems in computing in sometimes surprising ways. Following Lambek [25], categories form a third leg of the isomorphism. Categorical semantics can be used to prove the consistency of a calculus, and they are crucial if we wish to prove or program in some particular mathematical setting. For example, see the use of the topos of trees as a setting for both programming with guarded recursion, and proof by Löb induction, by Clouston et al. [11].
This work involved two functors, ‘later’ and ‘constant’. Where functors interact appropriately with finite products they correspond to necessity modalities in intuitionistic normal modal logic, usually written \(\square \). Such modalities have been extensively studied by logicians, and the corresponding typeformers are widely applicable in computing, for example to monads [32], staged programming [13], propositional truncation [2], and recent work in homotopy type theory [37]. There is hence a need to develop all sides of the CurryHowardLambek isomorphism for necessity modalities. Approaches to modal lambda calculi are diverse; see the survey by Kavvos [23], and remarks in the final section of this paper. This paper focuses on Fitchstyle modal lambda calculi as first proposed by Borghuis [9] and (as the “twodimensional” approach) by Martini and Masini [29].
Fitchstyle modal lambda calculi^{1} adapt the proof methods of Fitch [19] in which given a formula \(\square A\) we may open a ‘(strict) subordinate proof’ in which we eliminate the \(\square \) to get premise A. Such a subordinate proof with conclusion B can then be shut by introducing a \(\square \) to conclude \(\square B\). Different modal logics can be encoded by tweaking the open and shut rules; for example we could shut the proof to conclude merely B, if we had the T axiom \(\square B\rightarrow B\). Normal modal logics are usually understood with respect to Kripke’s possible worlds semantics (for the intuitionistic version, see e.g. Simpson [38, Sect. 3.3]). In this setting Fitch’s approach is highly intuitive, as opening a subordinate proof corresponds to travelling to a generic related world, while shutting corresponds to returning to the original world. See Fitting [20, Chap. 4] for a lengthier discussion of this approach to natural deduction.
Borghuis [9] kept track of subordinate proofs in a sequent presentation by introducing a new structural connective to the context when a \(\square \) is eliminated, and removing it from the context when one is introduced, in a style reminiscent of the treatment of modal logic in display calculus [42], or for that matter of the standard duality between implication and comma. To the category theorist, this suggests an operation on contexts left adjoint to \(\square \). This paper exploits this insight by presenting categorical semantics for Fitchstyle modal calculi for the first time, answering the challenge of de Paiva and Ritter [33, Sect. 4], by modelling necessity modalities as right adjoints. This is logically sound and complete, yet less general than modelling modalities as monoidal functors as done for example by Bellin et al. [4]. For example, truncation in sets is monoidal but has no right adjoint. Nonetheless adjunctions are ubiquitous, and in their presence we argue that the case for Fitchstyle calculi is compelling. Examples of right adoints of interest to type theorists include the aforementioned modalities of guarded recursion, the closure modalities of (differential) cohesive \(\infty \)toposes [36, Sect. 3], and atomabstraction in nominal sets [31].
In Sect. 2 we present Borghuis’s calculus for the logic Intuitionistic K, the most basic intuitionistic modal logic of necessity. To the results of confluence, subject reduction, and strong normalisation already shown by Borghuis we add canonicity and the subformula property, with the latter proof raising a subtle issue with sums not previously observed. We give categorical semantics for this style of calculus for the first time and prove soundness. In Sect. 3 we introduce the left adjoint as a firstclass type former à la intuitionistic tense logic [17], in which the “everywhere in the future” modality is paired with “somewhere in the past”. To our knowledge this is the first natural deduction calculus, let alone lambda calculus, for any notion of tense logic. It is not entirely satisfactory as it lacks the subformula property, but it does allow us to prove categorical completeness. In Sect. 4 we show how the basic techniques developed for Intuitionistic K extend to Intuitionistic S4, one of the moststudied intuitionistic modal logics. Instead of working with known Fitchstyle calculi for this logic [13, 34] we explore a new, particularly simple, calculus where the modality is idempotent, i.e. \(\square A\) and \(\square \square A\) are not merely logically equivalent, but isomorphic. Our semantics for this calculus rely on an unusual ‘coherence’ proof. In Sect. 5 we present a calculus corresponding to the logic Intuitionistic R. In Sect. 6 we conclude with a discussion of related and further work.
2 Intuitionistic K

K: \(\;\square (A\rightarrow B)\rightarrow \square A\rightarrow \square B\)

Necessitation: if A is a theorem, then so is \(\square A\).
2.1 Type System

\(\llbracket \cdot \vdash A\rrbracket = A\);

\(\llbracket B,\varGamma \vdash A\rrbracket = B\rightarrow \llbracket \varGamma \vdash A\rrbracket \);
This interpretation will suffice to confirm the soundness and completeness of our calculus, considered as a natural deduction calculus, with respect to IK. It is however not a satisfactory basis for a categorical semantics, because it does not interpret the context as an object. In Sect. 2.3 we shall see that Open image in new window may instead by interpreted as a left adjoint of \(\square \), applied to the context to its left.
Theorem 2.1
(Logical Soundness and Completeness). A formula is a theorem of IK if and only if it is an inhabited type in the empty context.
2.2 Computation
Lemma 2.2
(Variable Weakening). If \(\varGamma ,\varGamma '\vdash t:B\) then \(\varGamma ,x:A,\varGamma '\vdash t:B\).
Lemma 2.3
(Substitution). If \(\varGamma ,x:A,\varGamma '\vdash t:B\) and \(\varGamma \vdash u:A\) then \(\varGamma ,\varGamma '\vdash t[u/x]:B\).
Theorem 2.4
(Subject Reduction). If \(\varGamma \vdash t:A\) and \(t\mapsto u\) then \(\varGamma \vdash u:A\).
Proof
\(\beta \)reduction for \(\rightarrow \) requires Lemma 2.3, and for \(\square \) requires Lemma 2.2.
A term t is normalisable if there exists an integer \(\nu (t)\) bounding the length of any reduction sequence starting with t, and normal if \(\nu (t)\) is 0. By standard techniques we prove the following theorems:
Theorem 2.5
(Strong Normalisation). Given \(\varGamma \vdash t:A\), the term t is normalisable.
Theorem 2.6
(Canonicity). If \(\varGamma \) is a context containing no variable assignments, \(\varGamma \vdash t:A\), and t is normal, then the main termformer of t is the introduction for the main typeformer of A.
Concretely, if A is some base type then t is a value of that type.
Theorem 2.7
(Subformula Property). Given \(\varGamma \vdash t:A\) with t normal, all subterms of t have as their type in the derivation tree a subtype of A, or a subtype of a type assigned in \(\varGamma \).
2.3 Categorical Semantics
This section goes beyond Theorem 2.1 to establish the soundness of the type system with respect to a categorical semantics, in cartesian closed categories \(\mathcal {C}\) equipped with an endofunctor \(\square \) that has a left adjoint, which we write \(\blacklozenge \).

\(\llbracket \cdot \rrbracket \;\triangleq \; 1\);

\(\llbracket \varGamma ,x:A\rrbracket \;\triangleq \; \llbracket \varGamma \rrbracket \times A\);
We omit the brackets \(\llbracket \cdots \rrbracket \) where no confusion is possible, and usually abuse notation by omitting the leftmost ‘\(1\times \)’ where the left of the context is a variable.
We will also sometimes interpret contexts \(\varGamma \) as endofunctors, abusing notation to also write them as \(\llbracket \varGamma \rrbracket \), or merely \(\varGamma \), by taking \(\llbracket \cdot \rrbracket \) as the identity, \(\llbracket \varGamma ,x:A\rrbracket = \llbracket \varGamma \rrbracket \times A\), and Open image in new window .
We interpret \(\varGamma \vdash t:A\) as a \(\mathcal {C}\)arrow \(\llbracket \varGamma \vdash t:A\rrbracket :\llbracket \varGamma \rrbracket \rightarrow A\), often abbreviated to \(\llbracket t\rrbracket \), or merely t, by induction on the derivation of t as follows.
Standard constructions such as variables, abstraction and application are interpreted as usual. To interpret the rules for sums of Fig. 2 we use the fact that \(\blacklozenge \), as a left adjoint, preserves colimits.
\(\mathsf {shut}\): we simply apply the isomorphism \(\mathcal {C}(\blacklozenge \llbracket \varGamma \rrbracket ,A)\rightarrow \mathcal {C}(\llbracket \varGamma \rrbracket ,\square A)\) given by the \(\blacklozenge \dashv \square \) adjunction.
\(\mathsf {open}\): We apply the isomorphism \(\mathcal {C}(\llbracket \varGamma \rrbracket ,\square A)\rightarrow \mathcal {C}(\blacklozenge \llbracket \varGamma \rrbracket ,A)\) to the arrow interpreting the premise, then compose with the projection Open image in new window .
Theorem 2.8
(Categorical Soundness). If \(\varGamma \vdash t:A\) and \(t\mapsto t'\) then \(\llbracket t\rrbracket =\llbracket t'\rrbracket \).
We also have that \(\eta \)equivalent terms have the same denotation.
3 Left Adjoints and Categorical Completeness
In this section we extend the calculus to include the left adjoint \(\blacklozenge \) as a firstclass typeformer, and hence prove categorical completeness. The underlying logic is the fragment of intuitionistic tense logic [17] with just one pair of modalities, studied by Dzik et al. [15] as ‘intuitionistic logic with a Galois connection’; we use the name \(IK_{\blacklozenge }\). We have two new axioms
\(\eta ^m\): \(\;A\rightarrow \square \blacklozenge A\)
\(\varepsilon ^m\): \(\;\blacklozenge \square A\rightarrow A\)
We use the superscript m to identify these as the unit as the unit and counit of the modal adjunction \(\blacklozenge \dashv \square \), to differentiate them from other (co)units used elsewhere in the paper. We have one new inference rule:
Monotonicity: if \(A\rightarrow B\) is a theorem, then so is \(\blacklozenge A\rightarrow \blacklozenge B\).
3.1 Type System and Computation
This term is normal but evidently fails the subformula property. One might expect, as with sums, that a commuting conversion would save the day by reducing the term to \(\mathsf {let\,dia}\,y\,\mathsf {be}\,x\,\mathsf {in}\,((\lambda z.\mathsf {dia}\,y)x)\), but this term sees the free variable x appear in the second subterm of a \(\mathsf {let\,dia}\) expression, which is not permitted.
3.2 Categorical Semantics
We interpret the new termformers in the same categories as used in Sect. 2.3. For \(\mathsf {dia}\), given \(t:\varGamma \rightarrow A\) we compose \(\blacklozenge t\) with the projection Open image in new window . The denotation of \(\mathsf {let\,dia}\,x\,\mathsf {be}\,t\,\mathsf {in}\,u\) is simply \(u\circ t\). We may then confirm the soundness of \(\beta \)reduction, \(\eta \)equivalence, and associativity; we call these equivalences collectively definitional equivalence.
We extend standard techniques for proving completeness [25], constructing a term model, a category with types as objects and, as arrows \(A\rightarrow B\), terms of form \(x:A\vdash t:B\) modulo definitional equivalence. This is a category by taking identity as the term x and composition \(u\circ t\) as u[t / x]. It is a cartesian closed category using the type and termformers for products and function spaces.
The modalities \(\blacklozenge \) and \(\square \) act on types; they also act on terms by, for \(\blacklozenge \), the monotonicity construction, and for \(\square \), mapping \(x:A \vdash t:B\) to \(x:\square A\vdash \mathsf {shut}\,t[\mathsf {open}\,x/x]:\square B\). One can check these constructions are functorial, and that the terms for \(\eta ^m\) and \(\varepsilon ^m\) are natural and obey the triangle equalities for the adjunction \(\blacklozenge \vdash \square \).

\(c_{\cdot } \;\triangleq \; \langle \rangle \);

\(c_{\varGamma ,x:A} \;\triangleq \; \langle c_{\varGamma },x\rangle \);
Lemma 3.1
Given \(\varGamma \vdash t:A\), t is definitionally equal to \(\llbracket \varGamma \vdash t:A\rrbracket [c_{\varGamma }/x]\).
Theorem 3.2
(Categorical Completeness). If \(\varGamma \vdash t:A\) and \(\varGamma \vdash u:A\) are equal in all models then they are definitionally equal.
Proof
t and u have equal denotations in the term model, so their denotations are definitionally equal. Definitional equality is preserved by substitution, so \(\llbracket \varGamma \vdash t:A\rrbracket [c_{\varGamma }/x]=\llbracket \varGamma \vdash u:A\rrbracket [c_{\varGamma }/x]\), so by Lemma 3.1, \(t=u\).
4 Intuitionistic S4 for Idempotent Comonads
Intuitionistic S4 (IS4) is the extension of IK with the axioms
T: \(\;\square A\rightarrow A\)
4: \(\;\square A\rightarrow \square \square A\)
To the category theorist IS4 naturally suggests the notion of a comonad. IS4 is one of the most studied and widely applied intuitionistic modal logics; in particular there exist two Fitchstyle calculi [13, 34]. We conjecture that similar results to the previous sections could be developed for these calculi. Instead of pursuing such a result, we here show that a simpler calculus is possible if we restrict to idempotent comonads, where \(\square A\) and \(\square \square A\) are isomorphic. This restriction picks out an important class of examples – see for example the discussion of Rijke et al. [35] – and relies on a novel ‘coherence’ proof.
4.1 Type System and Computation
This confirms logical completeness; once can also easily check soundness.
Subject reduction for the \(\beta \)reduction \(\mathsf {open}\,\mathsf {shut}\,t\mapsto t\) requires a new lemma, proved by an easy induction on t:
Lemma 4.1
(Lock Replacement). If Open image in new window then \(\varGamma ,\varGamma ',\varGamma ''\vdash t:A\).
The key syntactic Theorems 2.5, 2.6, and 2.7 then follow easily.
4.2 Categorical Semantics
We give semantics to our type theory in a cartesian closed category with an adjunction of endofunctors \(\blacklozenge \dashv \square \) in which \(\square \) is a comonad. Equivalently [16, Sect. 3], \(\blacklozenge \) is a monad, equipped with a unit \(\eta \) and multiplication \(\mu \). To confirm the coherence of these semantics, discussed in the next subsection, and the soundness of \(\eta \)equivalence, we further require that \(\square \) is idempotent, or equivalently that all \(\mu _A:\blacklozenge \blacklozenge A\rightarrow \blacklozenge A\) are isomorphisms with inverses \(\eta _{\blacklozenge A}=\blacklozenge \eta _A\).

\(l_{\cdot }\) is the unit \(\eta \) of the monad;

\(l_{\varGamma ,x:A}\) is the projection composed with \(l_{\varGamma }\);

Open image in new window is \(\blacklozenge l_{\varGamma }\) composed with \(\mu \).
Note that Open image in new window is the identity by the monad laws.
We may now define the interpretation of \(\mathsf {open}\): given \(t:\varGamma \rightarrow \square A\) we apply the adjunction to get an arrow \(\blacklozenge \varGamma \rightarrow A\), then compose with Open image in new window .
Lemma 4.2
Proof
By induction on \(\varGamma _4\), with the base case following by induction on \(\varGamma _3\).
Lemma 4.3
Proof
By induction on the derivation of t.
Now \(\mathsf {open}\,\mathsf {shut}\,t\), where the \(\mathsf {open}\) has weakening \(\varGamma '\), has denotation \(\varepsilon ^{m}\circ \blacklozenge \square t\circ \blacklozenge \eta ^{m}\circ l_{\varGamma '}\), which is \(t\circ l_{\varGamma '}\) by the naturality of \(\varepsilon ^{m}\), and the adjunction. This is what is required by Lemma 4.3, so \(\beta \)reduction for \(\square \) is soundly modelled.
4.3 Coherence
The categorical semantics of the previous section is defined by induction on derivations, and so does not truly give semantics to terms unless any two trees with the same root must have the same denotation. In this section we show that this property, here called coherence, indeed holds. We make crucial use of the idempotence of the comonad \(\square \).
We first observe that if \(\varGamma ,\varGamma ',\varGamma ''\vdash t:A\) and all variables of \(\varGamma '\) are not free in t, then \(\varGamma ,\varGamma ''\vdash t:A\). The following lemma, proved by easy inductions, describes how the denotations of these derivations are related:
Lemma 4.4
 1.
If x is not free in t then \(\varGamma ,x:A,\varGamma '\vdash t:B\) has the same denotation as \(\varGamma ,\varGamma '\vdash t:B\circ \varGamma '(pr)\).
 2.
\(\varGamma ,\varGamma '\vdash t:B\) has denotation Open image in new window .
The technical lemma below is the only place where idempotence is used.
Lemma 4.5
Proof
By induction on \(\varGamma '\). The base case holds by the naturality of \(\eta \).
Lemma 4.6
Proof
By induction on \(\varGamma ''\). The base case follows by Lemma 4.5.
Lemma 4.7

\(\varGamma ,\varGamma ',\varGamma ''\vdash \mathsf {open}\,t:A\) where the weakening is \(\varGamma ''\);

obtaining an arrow \(\varGamma \rightarrow \square A\) via Lemma 4.4, then applying \(\mathsf {open}\) with weakening \(\varGamma ,\varGamma ''\).
Proof
Theorem 4.8
(Coherence). Given two different derivation trees of a term, their denotation is equal.
Proof
We can now demonstrate the soundness of \(\eta \)equivalence: given \(\varGamma \vdash t:\square A\) and \(\varGamma \vdash \mathsf {shut}\,\mathsf {open}\,t:\square A\) by any derivations, we can by coherence safely assume that \(\mathsf {open}\) used one lock only as its weakening, and so the arrows are equal by the \(\blacklozenge \dashv \square \) adjunction.
4.4 Left Adjoints and Categorical Completeness
to retain Lemma 4.1. The results of the previous sections, apart once more for the subformula property, still hold, where we define the denotation of \(\varGamma ,\varGamma '\vdash \mathsf {dia}\,t\) as \(\blacklozenge t\) composed with \(l_{\varGamma '}\). In particular, we must confirm that Lemma 3.1 extends to the new definitions of \(\mathsf {open}\) and \(\mathsf {dia}\), for which we need the lemma below:
Lemma 4.9
Given the term \(x:\llbracket \varGamma ,\varGamma '\rrbracket \vdash l_{\varGamma '}:\blacklozenge \llbracket \varGamma \rrbracket \) defined in the term model, \(l_{\varGamma '}[c_{\varGamma ,\varGamma '}/x]\) is definitionally equal to \(\mathsf {dia}\,c_{\varGamma }\).
Now \(\llbracket \mathsf {open}\,t\rrbracket [c_{\varGamma ,\varGamma '}/x]\) is \(\mathsf {let\,dia}\,x\,\mathsf {be}\,(\mathsf {let\,dia}\,x\,\mathsf {be}\,l_{\varGamma '} [c_{\varGamma ,\varGamma '}/x]\,\mathsf {in}\,\mathsf {dia}\llbracket t\rrbracket )\,\mathsf {in}\,\mathsf {open}\,x\), which by the lemma above is \(\mathsf {let\,dia}\,x\,\mathsf {be}\,(\mathsf {let\,dia}\,x\,\mathsf {be}\,\mathsf {dia}\,c_{\varGamma }\,\mathsf {in}\,\mathsf {dia}\llbracket t\rrbracket )\,\mathsf {in}\,\mathsf {open}\,x\mapsto \) \(\mathsf {open}\llbracket t\rrbracket [c_{\varGamma }/x]\), which equals \(\mathsf {open}\,t\) by induction. The proof for \(\mathsf {dia}\) is similar.
5 Intuitionistic R
One can readily imagine how the calculus for IS4 could be modified for logics with only one of the T and 4 axioms. In this section we instead illustrate the flexibility of Fitchstyle calculi by defining a calculus for the rather different logic Intuitionistic R (IR), which extends IK with the axiom
R: \(\;A\rightarrow \square A\)
This axiom was first studied for intuitionistic necessity modalities by Curry [12], along with the axiom M, \(\square \square A\rightarrow \square A\), to develop a logic for monads. The importance of the logic with R but without M was established by McBride and Paterson [30] who showed that it captured the useful programming abstraction of applicative functors. We take the name R for the axiom from Fairtlough and Mendler [18], and for the logic from Litak [28].
For substitution and subject reduction we require the following lemma, easily proved by induction on the derivation of t:
Lemma 5.1
(Lock Weakening). If \(\varGamma ,\varGamma '\vdash t:A\) then Open image in new window .
We can also observe that \(\eta \)equivalence preserves types in both directions.
We give semantics for this calculus in a cartesian closed category equipped with an adjunction of endofunctors \(\blacklozenge \dashv \square \) and a ‘point’ natural transformation \(r:Id\rightarrow \square \) preserved by \(\square \), i.e. \(\square r=r:\square A\rightarrow \square \square A\). This last property makes this model slightly less general than the notion of tensorial strength used for categorical semantics by McBride and Paterson [30], but is needed for coherence and the soundness of \(\eta \)equivalence. We will use the arrow \(\blacklozenge A\rightarrow A\) defined by applying the adjunction to r; we call this q and note the property:
Lemma 5.2
\(q=\blacklozenge q:\blacklozenge \blacklozenge A\rightarrow \blacklozenge A\).
The weakening natural transformation \(w_{\varGamma }:\varGamma \rightarrow Id\) is defined by induction on \(\varGamma \) via projection and q. Variables are then denoted by projection composed with weakening, and weakening is used similarly for \(\mathsf {open}\) and \(\mathsf {dia}\). We can hence show the soundness of \(\beta \)reduction for \(\square \) and \(\blacklozenge \). For the soundness of \(\eta \)equivalence for \(\square \) we need the following lemma:
Lemma 5.3
The denotation of Open image in new window is Open image in new window . By the above lemma we replace Open image in new window with Open image in new window , so by the naturality of \(\eta ^m\) we have Open image in new window , which is Open image in new window by the monad laws.
Moving finally to categorical completeness, in the term model \(\square t\circ r\) is \(\mathsf {shut}\,t[\mathsf {open}\,\mathsf {shut}\,x/x]\), which reduces to \(\mathsf {shut}\,t\), so r is natural. \(\square r:\square A\rightarrow \square \square A\) is \(\mathsf {shut}\,\mathsf {shut}\,\mathsf {open}\,x\), which is indeed \(\eta \)equal to \(\mathsf {shut}\,x\).
We finally need to update Lemma 3.1 for our new definitions. We do this via a lemma similar to Lemma 4.9:
Lemma 5.4
Given the term \(x:\llbracket \varGamma ,\varGamma '\rrbracket \vdash w_{\varGamma '}:\llbracket \varGamma \rrbracket \) defined in the term model, \(w_{\varGamma '}[c_{\varGamma ,\varGamma '}/x]\) is definitionally equal to \(c_{\varGamma }\).
Now the denotation of \(\varGamma ,x:A,\varGamma '\vdash x:A\) is \(\pi _2 w_{\varGamma '}\). Therefore we have \(\pi _2 w_{\varGamma '}[c_{\varGamma ,A,\varGamma '}/x]\), which is \(\pi _2 c_{\varGamma ,A}\) by the lemma above. This is \(\pi _2\langle c_{\varGamma },x \rangle \), which reduces to x.
The denotation of Open image in new window is \(\mathsf {let\,dia}\,x\,\mathsf {be}\,w_{\varGamma '}\,\mathsf {in}\,\mathsf {open}\llbracket t\rrbracket \). Applying the substitution Open image in new window along with the lemma above yields the term \(\mathsf {let\,dia}\,x\,\mathsf {be}\,\mathsf {dia}\,c_{\varGamma }\,\mathsf {in}\,\mathsf {open}\llbracket t\rrbracket \mapsto \mathsf {open}\llbracket t\rrbracket [c_{\varGamma }/x]\), and induction completes. The calculations for \(\mathsf {dia}\) follow similarly.
6 Related and Further Work
Conventional contexts. Lambda calculi with conventional contexts containing typed variables only have been proposed for the logic of monads [32], for IS4 [5], for IK [4], and for a logic with ‘Löb induction’ [6], from which one can extract a calculus for IR. In previous work [11] we developed the guarded lambda calculus featuring two modalities, where one (‘constant’) was an (idempotent) comonad, and the other (‘later’) supported a notion of guarded recursion corresponding to Löb induction. We therefore used the existing work [5, 6] ‘off the shelf’.
Problems arose when we attempted to extend our calculus with dependent types [7]. Neither of the calculi with conventional contexts we had used scaled well to this extension. The calculus for IS4 [5], whose terms involved explicit substitutions, turned out to require these substitutions on types also, which added a level of complexity that made it difficult to write even quite basic dependently typed programs. The constant modality was therefore jettisoned in favour of an approach based on clock quantification [1], of which more below. The calculus for later employed a connective \(\circledast \) (from McBride and Patterson [30]) which acted on function spaces under the modality. However with dependent types we need to act not merely on function spaces, but on \(\varPi \)types, and \(\circledast \) was unable to be used. Instead a novel notion of ‘delayed substitution’ was introduced. These were given an equational theory, but some of these equations could not be directed, so they did not give rise to a useful notion of computation.
Modalities as quantifiers. The suggestive but formally rather underdeveloped paper of De Queiroz and Gabbay [14] proposed that necessity modalities should be treated as universal quantifiers, inspired by the standard semantics of necessity as ‘for all possible worlds’. This is one way to understand the relationship between the constant modality and clock quantification [1]. However clock quantification is more general than a single constant modality because we can identify multiple free clock variables with multiple ‘dimensions’ in which a type may or may not be constant. This gap in generality can probably be bridged by using multiple independent constant modalities. More problematically, while it is clear what the denotational semantics of the constant modality are, the best model for clock quantifiers yet found [8] is rather complicated and still leaves open some problems with coherence in the presence of a universe.
Previous Fitchstyle calculi. The Fitchstyle approach was pioneered, apparently independently, by Martini and Masini [29] and Borghuis [9]. Martini and Masini’s work is rather notationally heavy, and weakening appears not to be admissible. Borghuis’s calculus for IK is excellent, but his calculi for stronger logics are not so compelling, as each different axiom is expressed with another version of the \(\mathsf {open}\) or \(\mathsf {shut}\) rules, not all of which compute when combined. The calculus for IS4 of Pfenning and Wong [34], refined by Davies and Pfenning [13, Sect. 4], provide the basis of the IS4 calculus of this paper, but involve some complications which appear to correlate to not assuming idempotence. We have extended this previous work by investigating the subformula property, introducing categorical semantics, and showing how left adjoints to necessity modalities à la tense logic can be used as types. Finally, the recent clocked type theory of Bahr et al. [3] independently gave a treatment of the later modality that on inspection is precisely Fitchstyle (albeit with named ‘locks’), and which has better computational properties than the delayed substitution approach.
Dual contexts. Davies and Pfenning [13] use a pair of contexts \(\varDelta ; \varGamma \) with intended meaning \(\square \varDelta \wedge \varGamma \). This is quite different from the semantics of Fitchstyle sequents, where structure in the context denotes the left adjoint of \(\square \). In recent work Kavvos [24] has shown that dual contexts may capture a number of different modal logics, and the approach has been used as a foundation for both penandpaper mathematics [37] and, via an Agda fork [40], formalisation [26]. We support this work but there is reason to explore other options. First, writing programs with dual context calculi was described by Davies and Pfenning themselves as ‘somewhat awkward’, and in the same paper they suggest the Fitchstyle approach as a less awkward alternative. Indeed, Fitch’s approach was exactly designed to capture ‘natural’ modal deduction. Second, any application with multiple interacting modalities is unlikely to be accommodated in a mere two zones; the mode theories of Licata et al. [27] extend the dual zone approach to a richer setting in which interacting modalities, substructural contexts, and even Fitchstyle natural deduction can be expressed^{2}, but the increase in complexity is considerable and much work remains to be done.
Further logics and algorithmic properties. We wish to bring more logics into the Fitchstyle framework, in particular the logic of the later modality, extending IR with the strong Löb axiom \((\square A\rightarrow A)\rightarrow A\). The obvious treatment of this axiom does not terminate. but Bahr et al. [3] suggest that this can be managed by giving names to locks. We would further like to develop calculi with multiple modalities. This is easy to do by assigning each modality its own lock; two IK modalities give exactly the intuitionistic tense logic of Goré et al. [22]. The situation is rather more interesting where the modalities interact, as with the later and constant modalities. Finally, we would like to further investigate algorithmic properties of Fitchstyle calculi such as type checking, type inference, and \(\eta \)expansion and other notions of computation. In particular, we wonder if a notion of commuting conversion can be defined so that the calculi with \(\blacklozenge \) enjoy the subformula property.
Footnotes
References
 1.Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: ICFP (2013)Google Scholar
 2.Awodey, S., Bauer, A.: Propositions as [types]. J. Log. Comput. 14(4), 447–471 (2004)MathSciNetCrossRefGoogle Scholar
 3.Bahr, P., Grathwohl, H.B., Møgelberg, R.E.: The clocks are ticking: no more delays! In: LICS, pp. 1–12 (2017)Google Scholar
 4.Bellin, G., De Paiva, V., Ritter, E.: Extended CurryHoward correspondence for a basic constructive modal logic. In: M4M (2001)Google Scholar
 5.Bierman, G.M., de Paiva, V.C.: On an intuitionistic modal logic. Stud. Logica. 65(3), 383–416 (2000)MathSciNetCrossRefGoogle Scholar
 6.Birkedal, L., Møgelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS (2013)Google Scholar
 7.Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 20–35. Springer, Heidelberg (2016). https://doi.org/10.1007/9783662496305_2CrossRefGoogle Scholar
 8.Bizjak, A., Møgelberg, R.E.: Denotational semantics for guarded dependent type theory. Math. Struct. Comput. Sci. (2018, to appear)Google Scholar
 9.Borghuis, V.A.J.: Coming to terms with modal logic: on the interpretation of modalities in typed lambdacalculus. Ph.D. thesis, Technische Universiteit Eindhoven (1994)Google Scholar
 10.Božić, M., Došen, K.: Models for normal intuitionistic modal logics. Stud. Logica. 43(3), 217–245 (1984)MathSciNetCrossRefGoogle Scholar
 11.Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: The guarded lambdacalculus: programming and reasoning with guarded recursion for coinductive types. LMCS 12(3) (2016). https://lmcs.episciences.org/2019
 12.Curry, H.B.: A Theory of Formal Deducibility. University of Notre Dame Press, Indiana (1957)Google Scholar
 13.Davies, R., Pfenning, F.: A modal analysis of staged computation. JACM 48(3), 555–604 (2001)MathSciNetCrossRefGoogle Scholar
 14.De Queiroz, R.J., Gabbay, D.M.: The functional interpretation of modal necessity. In: de Rijike, M. (eds.) Advances in Intensional Logic, pp. 61–91. Springer, Dordrecht (1997). https://doi.org/10.1007/9789401588799_3
 15.Dzik, W., Järvinen, J., Kondo, M.: Intuitionistic propositional logic with Galois connections. Log. J. IGPL 18(6), 837–858 (2009)MathSciNetCrossRefGoogle Scholar
 16.Eilenberg, S., Moore, J.C.: Adjoint functors and triples. Illinois J. Math. 9(3), 381–398 (1965)MathSciNetMATHGoogle Scholar
 17.Ewald, W.: Intuitionistic tense and modal logic. J. Symb. Log. 51(1), 166–179 (1986)MathSciNetCrossRefGoogle Scholar
 18.Fairtlough, M., Mendler, M.: Propositional lax logic. Inform. Comput. 137(1), 1–33 (1997)MathSciNetCrossRefGoogle Scholar
 19.Fitch, F.B.: Symbolic Logic, An Introduction. Ronald Press Co., New York (1952)MATHGoogle Scholar
 20.Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. D. Reidel Publishing Co., Dordrecht (1983)CrossRefGoogle Scholar
 21.Girard, J.Y., Taylor, P., Lafont, Y.: Proofs and Types. Cambridge University Press, Cambridge (1989)MATHGoogle Scholar
 22.Goré, R., Postniece, L., Tiu, A.: Cutelimination and proof search for biintuitionistic tense logic. In: AiML (2010)Google Scholar
 23.Kavvos, G.A.: The many worlds of modal \(\lambda \)calculi: I. CurryHoward for necessity, possibility and time. arXiv:1605.08106 (2016)
 24.Kavvos, G.: Dualcontext calculi for modal logic. In: LICS (2017)Google Scholar
 25.Lambek, J., Scott, P.J.: Introduction to HigherOrder Categorical Logic. Cambridge University Press, Cambridge (1986)MATHGoogle Scholar
 26.Licata, D.R., Orton, I., Pitts, A.M., Spitters, B.: Internal universes in models of homotopy type theory (2018, unpublished)Google Scholar
 27.Licata, D.R., Shulman, M., Riley, M.: A fibrational framework for substructural and modal logics. In: FSCD (2017)Google Scholar
 28.Litak, T.: Constructive modalities with provability smack. In: Bezhanishvili, G. (ed.) Leo Esakia on Duality in Modal and Intuitionistic Logics. OCL, vol. 4, pp. 187–216. Springer, Dordrecht (2014). https://doi.org/10.1007/9789401788601_8CrossRefGoogle Scholar
 29.Martini, S., Masini, A.: A computational interpretation of modal proofs. In: Wansing, H. (ed.) Proof Theory of Modal Logic, pp. 213–241. Springer, Dordrecht (1996). https://doi.org/10.1007/9789401727983_12Google Scholar
 30.McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008)CrossRefGoogle Scholar
 31.Menni, M.: About Open image in new windowquantifiers. Appl. Categ. Struct. 11(5), 421–445 (2003)Google Scholar
 32.Moggi, E.: Computational lambdacalculus and monads. In: LICS, pp. 14–23 (1989)Google Scholar
 33.de Paiva, V., Ritter, E.: Basic constructive modality. In: Logic without Frontiers: Festschrift for Walter Alexandre Carnielli on the occasion of his 60th Birthday, pp. 411–428. College Publication (2011)Google Scholar
 34.Pfenning, F., Wong, H.C.: On a modal \(\lambda \)calculus for S4. In: MFPS (1995)Google Scholar
 35.Rijke, E., Shulman, M., Spitters, B.: Modalities in homotopy type theory. arXiv:1706.07526 (2017)
 36.Schreiber, U.: Differential cohomology in a cohesive infinitytopos. arXiv:1310.7930 (2013)
 37.Shulman, M.: Brouwer’s fixedpoint theorem in realcohesive homotopy type theory. Math. Struct. Comput. Sci. (2017). https://www.cambridge.org/core/journals/mathematicalstructuresincomputerscience/article/brouwersfixedpointtheoreminrealcohesivehomotopytypetheory/8270C2EAC4EE5D5CDBA17EEB3FF6B19E
 38.Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh (1994)Google Scholar
 39.Sørensen, M.H., Urzyczyn, P.: Lectures on the CurryHoward Isomorphism. Elsevier, New York (2006)MATHGoogle Scholar
 40.Vezzosi, A.: Agdaflat (2017). https://github.com/agda/agda/tree/flat. GitHub repository
 41.Wadler, P.: Propositions as types. Commun. ACM 58(12), 75–84 (2015)CrossRefGoogle Scholar
 42.Wansing, H.: Sequent calculi for normal modal propositional logics. J. Log. Comput. 4(2), 125–142 (1994)MathSciNetCrossRefGoogle Scholar
 43.Yokota, S.: General characterization results on intuitionistic modal propositional logics. Commentarii Mathematici Universitatis Sancti Pauli 34(2), 177–199 (1985)MathSciNetMATHGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.