1 Introduction↩︎

Proof-theoretic Semantics (P-tS) is an alternative approach to semantics in which proof, rather than truth, takes a central role in conferring meaning to logical expressions. This can be seen as a mathematical realisation of the philosophical paradigm of Inferentialism; a position which seeks to determine the meanings of expressions through their use. In this realisation, the meanings of logical expressions are given through some notion of proof. This philosophical position has its origins in the works of Wittgenstein [1] in which he says that the meaning of a word should be determined by its use, though more recent works, such as those of Brandom [2]–[4] and Dummett [5] have also further explored this position.

Modern proof-theoretic semantics can be seen as having two main branches, both stemming from Prawitz’s original idea of a General Proof Theory² [7], [8]: The first, that of Proof-theoretic Validity (P-tV), concerns itself with the issue of what constitutes a valid proof. This approach to meaning can be seen as being closer to Prawitz’s General Proof Theory than the alternative we present here and has been explored by authors such as Dummett [5], Prawitz [9], Schroeder-Heister [10], [11] along with Piecha and de-Campos Sanz [12], [13]. The second, that of Base-extension Semantics (B-eS), concerns itself with the question of what constitutes a valid formula, and is the approach we will consider in this paper. This approach has been previously explored by Sandqvist [14], [15] and Schroeder-Heister, Piecha and de-Campos Sanz [13], [16]. Whilst Sandqvist gives a sound and complete B-eS for classical logic in his doctoral thesis [14], which he also later also discusses in [17], it was really his work on Intuitionistic Propositional Logic (IPL) [18] which cemented the importance of B-eS as a viable approach to P-tS. In particular, in this work, he develops the rather elegant completeness argument that forms the basis of our own in this paper, which we shall discuss below. For a good comparison of these two approaches to Pt-S (as well as a third approach that is similar to B-eS), the reader is referred to [19].

Sandqvist starts from the notion of an atomic rule \(\mathcal{R}\), which we write linearly as \((P_1\Rightarrow q_1,\dots,P_n\Rightarrow q_n)\Rightarrow r\) and defines a base \(\mathscr{B}\) to be a set of such rules. Such rules are to be considered as an instance of a valid inferential step that one can use in the justification of a particular atomic sentence. This is made precise through the definition of a derivability relation, \(\vdash_{\!\!\mathscr{B}}\), between bases, sets of atoms and individual atoms, as exemplified in Figure 1. One should understand \(\mathscr{B}\) as an \(\rm NJ\)-like object, whose elements are not schematic in nature. Consequently, just as how \(\rm NJ\) can be thought of as generating the consequence relation \(\vdash_{\rm NJ}\) for IPL, \(\mathscr{B}\) can be thought of as generating the consequence relation \(\vdash_{\!\!\mathscr{B}}\). Sandqvist uses this consequence relation to thus define a support relation \(\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\) on IPL sequents.

The need to consider base extensions in the semantics arises from the requirement that the meaning of a sentence should be given by some notion of a construction of it. In B-eS, one generally equates the concept of contruction of a sentence to that of the sentence satisfying the support relation relative to a base, with the base witnessing the construction of the sentence and thus, containing the “meaning” of the sentence³. With this in mind, it seems reasonable that, in the case of intuitionistic implication, a construction of \(\phi\supset\psi\), when combined with a construction of \(\phi\), should yield a construction of \(\psi\). Without the base extension, we would be required to accept that a construction of \(\psi\) may be obtained even without a construction of \(\phi\). This would follow vacuously as, were we to define \(\phi\supset\psi\) according to the clause \[\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\supset\psi\text{ iff }\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\Rightarrow \,\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\psi\] then we would have that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\supset\psi\) and \(\not\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\) imply \(\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\psi\); something that we find quite undesirable in our constructive world view. On the other hand, by considering base extensions, we lose Prawitz’s original idea, that bases are supposed to fix the meaning of sentences, as the meaning of sentences is now allowed to change. These issues are well discussed by Prawitz in [7] but again more recently by Sandqvist [14], [15], [20]. It is important to note that, in principle, the requirement for the extension is no different to the requirement that appears in Kripke semantics, where implication requires a condition on all accessible worlds⁴. It is with a support relation that one can give a semantics to the full logic. We briefly show how by giving an overview of the soundness and completeness arguments used by Sandqvist in [18].

As mentioned, the semantics in Figure 1 are sound and complete with respect to IPL. In this case, an IPL sequent \((\Gamma : \phi)\) is defined to be valid if and only if \(\Gamma\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\) for all bases \(\mathscr{B}\). We see this notion of validity is very similar to the usual conception of validity for Kripke semantics, where a formula \(\phi\) is considered to be valid if and only if for all models \(\mathcal{M}\), we have \(\mathcal{M}\vDash \phi\). This similarity is discussed in detail by Schroeder-Heister in [21]. Though we have, until now, emphasised the similarities between the usual Kripke semantics for IPL and the B-eS of Figure 1, it is imperative to note, however, that models and bases are not the same thing. A sceptic of this claim need only look at the form of the definitional clauses. Disjunction, for example, can be seen to be defined very closely to the interpretation one gives the disjunction elimination rule of \(\rm NJ\), in contrast to the usual meta-logical disjunction seen in the Kripke semantics. This seemingly contradicts the famous quote by Gentzen [22] that “the introductions present, so to speak, the ‘definitions’ of the symbols concerned". For details on why this definition of disjunction is necessary in B-eS, the reader is referred to [12], [18], [23], [24], Prawitz_NatDed_2006?.

Let us now sketch the arguments for soundness and completeness.

The proof of this theorem amounts to using the fact that derivations in \(\rm NJ\) are inductively defined and so it suffices to show that if the hypothesis of every rule of \(\rm NJ\) is valid then the conclusion also is. For example, in the case of \(\mathsf{\land}_\mathsf{I}\), we suppose that \(\Gamma\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\) and \(\Gamma\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\psi\) for all bases \(\mathscr{B}\) and show that therefore \(\Gamma\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\land\psi\) for all bases \(\mathscr{B}\), as required.

Since we start from the hypothesis that \(\Gamma\Vdash_{ \!\!\mathscr{B} }^{ \!\! }\phi\) holds in all \(\mathscr{B}\), we can therefore work in a tailor-made base, \(\mathscr{N}\), whose purpose will be to simulate the rules of \(\rm NJ\) in a particular way. Since bases cannot contain rule schemas⁵, we must therefore carefully pick atoms to represent all of the subformulae of the elements of the set \(\{\alpha\,|\,\alpha\in\Gamma\cup\phi\}\). After doing so, we construct \(\mathscr{N}\) to have all the rules of \(\rm NJ\) instantiated with our specially chosen atoms at all positions and show that each such atom is, in fact, inductively defined by atomised versions of the definitional clauses of the formulae being represented. It then follows that any \(\vdash_{\!\!\mathscr{N}}\) proof of any one of our specially chosen atoms corresponds to an \(\rm NJ\) proof of the formula it is representing, thus giving the completeness argument.

Intuitionistic linear logic (ILL) [25] is the intuitionistic fragment of Linear Logic [25], [26], a logic introduced by J.-Y. Girard. Linear logic is characterised by its feature that the general usage of the structural rules is strictly forbidden; their use instead being assigned to two “structural modalities”, both having structural rules on only one side of the sequent (and an S4-like Necessitation rule on the other). This restriction on the general use of structural rules leads to a splitting of the connectives of classical logic into additive and multiplicative parts. For example, the classical connective \(\land\) becomes split into the linear connectives \(\otimes\) and \(\mathbin{\&}\); the former governing multiplicative reasoning and the later additive. However, more importantly, since we cannot generally weaken or contract, the notion of reflexivity of the consequence relation of the logic is now sufficiently strict as to require that \(\Gamma\vdash\phi\) if and only if \(\Gamma=\{\phi\}\). Were \(\Gamma\) to contain any other formulae, this would amount to some measure of weakening. As a result, each formula can only be used once in a proof, unless there are multiple instances of it as hypothesis. This means that formulae in a proof act rather like resources that are being produced/consumed and that proofs keep track of which resources are needed to obtain what. This informal interpretation of proofs in linear logic is what has been dubbed the “resource interpretation" of linear logic and will play a key role in guiding our choices in the sequel. We, however, will be concerned with the intuitionistic fragment of linear logic, whose consequence relation can be understood, as normal, by taking the usual sequent calculus of linear logic [25] and restricting the succeedent to contain at most one formula. This restriction trivialises the additive disjunction, the modality which has its structural rules on the right and the unit of the additive disjunction. The resulting system, whilst losing the nice symmetry properties previously exhibited across all connectives, still retains the resource interpretation. It also now becomes easier to introduce a natural deduction system for linear logic as in [27]–[30].

The purpose of this paper will be to give a base-extension semantics for intuitionistic linear logic in a manner similar to that introduced by Sandqvist for IPL. Doing so, however, is not a trivial task. As noted, the consequence relation of ILL is much more “sensitive” to structurality. For example, whereas \(p\) is a consequence of the multiset \(\{p,q\}\) in IPL, the same does not hold true in ILL. Thus, it follows that any proposed support relation for ILL cannot validate intuitionistically valid sequents such as \((\{p,q\}:p)\). Therefore, the matter at hand is more complex than simply studying a larger set of connectives using the setup of Sandqvist for IPL. Indeed, we need to somehow redefine the support relation to prevent it from validating sequents of this form. To this end, we appeal to the semantics of Gheorghiu, Gu, and Pym [31] on the base-extension semantics for the Intuitionistic Multiplicative fragment of Linear Logic (IMLL). In this paper, the authors successfully redefine the support relation to correctly handle the issues around structurality discussed above. However, this isn’t the only modification they make. We summarise their semantics in Figure 2 and note another key difference; their interpretation of atomic rules is subtly, but crucially, different to that of Sandqvist’s for IPL. In the semantics for IMLL, we see that atomic rules, when interpreted by atomic derivability (that is, \(\vdash_{\!\!\mathscr{B}}\)) for IMLL, requires that each “branch” of an atomic rule “brings” its own multiset of open atomic assumptions, with the conclusion of the rule following as a consequence of the multiset union of all the multisets of open assumptions. That is to say, the \((\text{App}_{\mathcal{R}})\) clause differs considerably and meaningfully between the semantics for IMLL and IPL.

If one takes a look at the natural deduction system for IMLL, one sees that indeed, this is expected, for this is the interpretation we give to the rules. In fact, if we formally spell out this interpretation of derivability over the natural deduction system for IMLL, we obtain individual instances of something very similar to the (\(\text{App}_{\mathcal{R}}\)) clause in Figure 2, with the only differences being that we consider formulae and multisets thereof instead of just atoms. However, IMLL, being a purely multiplicative logic, has the obvious side effect that it doesn’t account for additive or modal behaviours. This is the situation we find ourselves in, for ILL has rules which are multiplicative, additive, contains elements of both, and has rules for a modality. Thus, it is to be expected that any proof-theoretic semantics for ILL, in the style we are interested in, must also modify its notion of atomic rule and atomic derivability, as compared to that of IMLL, lest it forgo completeness.

Thus, we are left with trying to develop a notion of atomic rule and application of such rules, that mimics that which we have in some natural deduction system for ILL. It is at this point that we are faced with a problem. What should the general form of an inference figure in a natural deduction system for ILL take? This is a serious problem which is, to the knowledge of the author, never adequately asked nor answered in the literature. In this paper, we additionally attempt to address this issue, though the solution is, unfortunately, somewhat convoluted.

Rules in natural deduction systems for ILL tend to be defined in a fairly ad-hoc manner. This is a completely acceptable approach to presenting such systems as, in reality, there are only a few number of rules in such systems and so, if one can provide a nice series of rule schemas, a few of which have side conditions to ensure that the rules are interpreted properly, then one can use these systems to study the proof-theoretic properties of such logics, taking care to ensure that the few side conditions are adhered to. These side conditions can be explicitly seen in systems such as those found in [28], [29], [32], to list a few. The main side condition we are talking of here is, of course, that of the interpretation of the contexts in the rules, particularly in the case of the rules governing the behaviour of the additive connectives. The side conditions tend to be justified by additionally giving a sequent-style presentation of the natural deduction figures, where multisets of open assumptions are baked into the notation using explicit schematic context metavariables. Indeed, there is nothing wrong with doing so and, in fact, we shall do something similar in Section 2. Nevertheless, we show that it is indeed possible to give a notion of derivability which handles additivity systematically, without side-conditions or appeal to explicit context metavariables, using a device which we call an additive box; a device which really acts as a scope delimiter for contexts (or more formally, multisets of open assumptions)⁶.

From the point of view of developing a B-eS for ILL, since we would like to develop a notion of atomic derivability that is as similar as possible to derivability in some natural deduction system for ILL, being able to eschew ourselves from using rules with context metavariables in the proof-theory is very desirable, as rules of inference in B-eS generally do not speak of sets of open assumptions. Doing so would effectively mean that certain inferences are “context specific”, resigning us to the position that such inferences can only be made given that we have a particular multiset of open assumptions. Given that ILL has no “context-specific” rules of this kind, as the context metavariables are always arbitrary multisets of formulae, it would be rather odd were our B-eS for ILL to require such constructions. Whilst it is plausible that for some logics this is indeed necessary, as we show in this paper, Intuitionistic Linear Logic is not one such logic.

However, expressing additivity systematically is not the only problem we have with natural deduction systems for ILL. Indeed, such systems tend to have rules with variably many minor premisses; something not usually seen in natural deduction. Such rules seem to be degenerating infinitely many rules into a single inference figure. This leads us to ask the question: Is an instance of such a rule a substitution instance of formulae and a number of premisses or just a substitution instance for formulae and any number of premisses? As we shall see in Section 2 (and also, as discussed by Negri in [32]), the variable number of minor premisses is really just a heavy handed way of saying that we require any arbitrary multiset of assumptions to hold at the hypothesis line. It turns out that additive boxes once again come to the rescue here, using the notion of an empty additive box, in all cases except for that of the promotion rule (c.f. Figure 3), where one has to define a special type of additive box that we call a modal box. The modal box internalises the additional side conditions that are required when treating the modality of ILL in natural deduction, at the cost of having to be treated as a separate type of assumption. Nevertheless, by abstracting these side conditions appropriately, using these “boxes”, one obtains a clean and systematic representation for the inference figures of the natural deduction system for ILL, where the answer to the question of what the general form of an inference figure in a natural deduction system for ILL is easily answerable. Thus, in Section 2, we spend considerable time developing this new language. One unfortunate side effect of this effort, however, is that we will require a somewhat complexly defined derivability relation on ILL sequents, to tell us how to interpret the rules. Nevertheless, as alluded to previously, a positive result of this effort will be that we develop a definition atomic derivability that is very similar to that for ILL; similar enough in fact, that the proof of completeness of the semantics should not be too complicated, as initially desired.

Before moving on, it is worth noting that whilst Gheorghiu, Gu, and Pym have extended their result to give a B-eS for the logic of Bunched Implications [33], at present, there is very little work done on understanding modalities from a base-extension semantics (or even more generally from the point of view of proof-theoretic semantics), and even less to understanding additivity. Some work in this direction has been undertaken by Gheorghiu, Gu, and Pym, with the goal to understand the role of resource from the perspective of base-extension semantics [34], [35]. Kürbis, for example, notes in his paper [36] some conditions in his view toward a theory of modalities from the point of view of proof-theoretic semantics. However the framework he considers is considerably different from that which we consider here. Nontheless, it is Eckhardt and Pym [37], [38] who first developed a base-extension semantics for the classical modal logics K, KT, K4, S4 and S5 in a manner closer to Sandqvist’s original work for classical logic, with Buzoku and Pym [39] having developed semantics for the intuitionistic modal logics defined by Simpson [40] in a style much closer to that which we are interested in here. Unfortunately, both of these approaches, in the opinion of the author, leave something to be desired. Whether it is due to the fact that modalities generally have poor proof-theoretic properties or simply that we are lacking some deep metaphysical insight into what it means for a word of a language to be modal, with this paper, it is hoped that we will be able to at least address the issues I feel are present in the approaches previously taken towards understanding modalities from the perspective of base-extension semantics. This will be done by taking a much more intrinsically proof-theoretic approach to understanding modality in the setting of Intuitionistic Linear Logic. Our paper thus goes as follows: We start by giving an overview and introducing a new syntax for natural deduction for Intuitionistic Linear Logic, in Section 2. We then introduce the key semantic structures, that of atomic derivability, in Section 3, and the support relation, in Section 4, and proceed to prove the necessary structural properties of both. We then have the key results of this paper, that of the soundness and completeness results, in Sections 5 and 6 respectively, before finally finishing with an overview of the results contained herein in Section [sec:Conc].

2 Intuitionistic Linear Logic↩︎

For the remainder of the paper we will assume a fixed set of propositional atoms \(\mathbb{A}\) that we refer to interchangeably as atoms or basic sentences. Unless stated otherwise, lowercase latin letters will be used to refer to atoms with uppercase latin letters being used to refer to finite multisets thereof. Similarly, lowercase greek letters will be used to represent individual formulae of Intuitionistic Linear Logic with uppercase letters being used to represent finite multisets thereof. We suppress set theoretic notation in the usual way, with the caveat that we write the multiset union of two multisets \(\Gamma\) and \(\Delta\) as \(\Gamma\msetsum\Delta\). That is to say, if \(\Gamma = \{a,a,b\}\) and \(\Delta = \{b,c,a\}\) then \(\Gamma\msetsum\Delta = \{a,a,a,b,b,c\}\). Finally, throughout this paper, the term “atomic multiset" is taken to mean multiset of propositional atoms.

We additionally may write \(\mathop{!}\Gamma\) to mean a multiset of ILL formulae where the top-level connective is \((\mathop{!})\); that is to say, for all \(\alpha\in\mathop{!}\Gamma\), there exists an ILL formula \(\gamma\), such that \(\alpha=\mathop{!}\gamma\).

As described, Figure 3 presents the natural deduction system \(\rm N_{ILL}\) in sequent style. A natural question to ask is whether it is possible to do so in a more traditional, Gentzen-Prawitz tree style? This issue is well covered in [28], but, as mentioned in the introduction, we wish to go further. If we consider the multiplicative fragment of ILL, then it is clear that we can always just consider all branches of an inference figure to be multiplicative with respect to each other (that is, that they have disjoint contexts) and so we naturally obtain such a calculus. Thus, an inference figure such as

\[\begin{array}{ccc} \infer[\mathsf{\otimes}_\mathsf{I}]{\Gamma\msetsum\Delta\vdash\phi\otimes\psi}{\Gamma\vdash\phi & \Delta\vdash\psi} & \text{ becomes } & \infer[\mathsf{\otimes}_\mathsf{I}]{\phi\otimes\psi}{\phi & \psi}\\[3mm] \end{array}\]

Such a system is used by the authors of [31] to give their base-extension semantics for the multiplicative fragment of ILL. If we include \((\mathop{!})\) to this fragment, to get the mutliplicative-exponential fragment, then we need to introduce the notion of strict derivations to correctly encode the Promotion rule. This is because in the rule \(\mathsf{Prom}\), there is the requirement that \(\mathop{!}\psi_1\msetsum\dots\mathop{!}\psi_n\vdash\phi\) occurs without any multiset of open assumptions, for all \(n\geq 0\). We show this requirement using semantic brackets to indicate that applying the rule requires a proof of \(\phi\) from the discharge set \(\mathop{!}\psi_1\msetsum\dots\mathop{!}\psi_n\). Thus, the tree-like inference figure for promotion becomes \[\infer[\mathsf{Prom}]{\mathop{!}\phi}{\mathop{!}\psi_1\,\dots\,\mathop{!}\psi_n & \deduce{\phi}{\llbracket \mathop{!}\psi_1\msetsum\dots\msetsum\mathop{!}\psi_n\rrbracket}}\]

A key point of note with regards to this rule however, is the presence of the \(n\) subscript. This \(n\) specifically requires that we are talking about any and all multisets of formulae prefixed with a (\(\mathop{!}\)) concurrently. An alternative, and more honest, way of writing this rule would be

\[\infer[\mathsf{Prom}]{\mathop{!}\phi}{\mathop{!}\Gamma & \deduce{\phi}{\llbracket \mathop{!}\Gamma\rrbracket}}\]

Thus becomes apparent the real meaning of this rule; that \(\phi\) must follow from a context of formulae with \((\mathop{!})\) as a top-level connective. This is nothing new, having been well investigated in [27], [28], but in short, the schematic setting that we are usually in when considering inferences in Natural Deduction systems means that this sort of rule is not problematic, since we can range \(\Gamma\) over all possible multisets and prefix each element of the context with a \((\mathop{!})\). Furthermore, we intuitively understand what it means to assert \(\mathop{!}\Gamma\) at the hypothesis line, but formally speaking, this would be inappropriate, thus leading to our initial characterisation of this rule. However, as discussed in the introduction, the inference figures we will be concerned with in the semantics are not schematic in nature and that can therefore only contain known propositional atoms; atoms which cannot have a \((\mathop{!})\) as a top level connective, as doing so would mean the are no longer atoms! Furthermore, they cannot have a variable number of premisses as it would no longer be a rule instance if they did. But individual instantiations of the promotion rule for any finite \(n\) are insufficient, since that would mean that you only consider contexts of certain sizes; something that clearly isn’t the case in the \(\mathsf{Prom}\) rule. These restrictions in the semantics mean that, when defining atomic derivability, our usual way of expressing the promotion rule is insufficient. We therefore need a different characterisation of the promotion rule. To this end, we redefine the meaning of the semantic bracket, and write the promotion rule now as follows:

\[\infer[\mathsf{Prom}]{\mathop{!}\phi}{\llbracket \phi\rrbracket}\]

We call the semantic bracket \(\llbracket\cdot\rrbracket\) here a modal box. This rule is to be operationally interpreted as saying:

1. If there is a derivation of \(\phi\) from some, possibly empty, multiset of formulae \(\{\alpha_1,\dots,\alpha_n\}\) i.e. \(\alpha_1\msetsum\dots\msetsum\alpha_n\vdash\phi\)

2. Each \(\alpha_i\) is a formula which is the conclusion of some instance of a rule with only modal boxes above the inference line

3. We have a derivation for each \(\alpha_i\), i.e. \(\Gamma_i\vdash\alpha_i\).

then it follows that \(\Gamma_1\msetsum\dots\msetsum\Gamma_n\vdash\mathop{!}\phi\). That is to say, the behavioural reading of the promotion rule is exactly as it was before, including the strict derivation (for a short discussion on why this is necessary, c.f. [28]), since the only rule which satisfies condition \((2)\) is \(\mathsf{Prom}\) and thus the only formulae which \(\alpha_i\) can be are formulae with \((\mathop{!})\) as a top-level connective. However, note that at no point did we define the multiset of formulae \(\{\alpha_1,\dots,\alpha_n\}\) as being a multiset of formulae with \((\mathop{!})\) as a top-level connective. This point is crucial, as we now have a characterisation of the \(\mathsf{Prom}\) rule that is not defined in terms of any connectives but in terms of some structural property of the rule itself. Note, that the operational reading of the rule is exactly the same as before, the only thing that has changed is the way we express this operation, as we shall see in Theorem 3 below.

So what of the additives? In this case, the author of [28] shows that to consider the additives, the language we have developed so far gets us close. For example, we may represent the additive conjunction as \[\infer[\mathsf{\mathbin{\&}}_\mathsf{I}]{\phi\mathbin{\&}\psi}{\chi_1\dots\chi_n & \deduce{\phi}{\llbracket\chi_1\msetsum\dots\msetsum\chi_n\rrbracket} & \deduce{\psi}{\llbracket\chi_1\msetsum\dots\msetsum\chi_n\rrbracket}}\] where the semantic brackets here mean that we discharge all assumptions at once (as in [28]) and that there are no other open assumptions on that branch, as in the original formulation of the \(\mathsf{Prom}\) rule. Our interpretation of this rule is that that we discharge both contexts \(\chi_1\msetsum\dots\msetsum\chi_n\) and re-introduce it but once. Whilst technically such a presentation is fine, it is at odds with our natural conception of additivity. Similarly, we can write this rule more honestly as \[\infer[\mathsf{\mathbin{\&}}_\mathsf{I}]{\phi\mathbin{\&}\psi}{\Gamma & \deduce{\phi}{\llbracket\Gamma\rrbracket} & \deduce{\psi}{\llbracket\Gamma\rrbracket}}\] We won’t go into details again but as in the case of the Promotion rule, we take problem with rules of this form as they require that we consider arbitrary contexts at the hypothesis line⁷. Indeed, the author of [28] instead opts to extend the proof-theory to include the concept of additive contexts. With additive contexts, the author is then able to represent inference rules which require context sharing derivations. They do so, effectively, by labelling each branch with a unique meta-variable which explicitly represents the context multiset used by those derivations. In this scheme, the \(\mathsf{\mathbin{\&}}_\mathsf{I}\) rule becomes \[\infer[\mathsf{\mathbin{\&}}_\mathsf{I}]{\phi\mathbin{\&}\psi}{\deduce{\phi}{\Gamma} & \deduce{\psi}{\Gamma}}\]

It is implicitly understood that the \(\Gamma\) in both branches is the same \(\Gamma\) ⁸ and that this is a context multiset. This notation, whilst clearly functional, is somewhat undesirable for it requires us to assign meta-variables to represent contexts when discussing inferences. Therein lies the problem; the rule requires that we talk about shared contexts in terms of derivations from arbitrary contexts \(\Gamma\). The problem here is the requirement of the \(\Gamma\) to represent an arbitrary context⁹. In a derivation, such \(\Gamma\)’s naturally accumulate and may be consumed through discharge. However, the rule uses these contexts effectively as labels. By doing so, we end up drawing vertical sequents and blur the lines between a pure rule of inference and its application. Since our rules are schematic in nature, this in itself isn’t problematic. However, as we shall see in Section 3 and beyond, if one were to consider a non-schematic system, this distinction becomes important. Of course, we could simply ignore this issue and use the initial method of encoding additivity. However, the problems initially identified remain. Thus, for the remainder of the paper, we sahll use the system shown in Figure 4 to better represent the rule schemas of \(\rm N_{ILL}\). That isn’t to say that this presentation of the rules constitutes a new calculus; this is simply a new way of systematically and uniformally representing the rules of the natural deduction system \(\rm N_{ILL}\).

In this presentation, no additional meta-variables are used to represent additive contexts. Instead, derivations are marked as being within “shared" contexts (demarcated by curly brackets), which we call additive boxes. This is what corresponds to an additive context in [28]. All derivations within an additive box must share the same multiset of open assumptions (i.e. must be”additive" with respect to each other) and, in the context of a rule, only one copy of the open assumptions from each additive box is understood to be necessary to obtain a derivation of the conclusion of a rule. If a rule has multiple additive boxes, then each additive box is understood to have disjoint contexts from every other additive box (i.e. the additive boxes are multiplicative with respect to each other). Thus, this syntaxt extends the tree like representation used for the purely multiplicative fragment of ILL, without the need for complex interpretation as in the case of the modal box. For example, the rule \[\begin{array}{ccc} \infer[\mathsf{\otimes}_\mathsf{I}]{\phi\otimes\psi}{\phi&\psi} & \text{ becomes } & \infer[\mathsf{\otimes}_\mathsf{I}]{\phi\otimes\psi}{\{\phi\}& \{\psi\}} \end{array}\]

To see how these brackets represent additivity, let us now consider some rules governing additive connectives. The case of \(\mathsf{\mathbin{\&}}_\mathsf{I}\) for example gives that \[\begin{array}{ccc} \infer[\mathsf{\mathbin{\&}}_\mathsf{I}]{\phi\mathbin{\&}\psi}{\deduce{\phi}{\Gamma} & \deduce{\psi}{\Gamma} } & \text{ becomes } & \infer[\mathsf{\mathbin{\&}}_\mathsf{I}]{\phi\mathbin{\&}\psi}{\{\phi& \psi\}} \end{array}\]

This notation is very flexible as it allows us to represent even \(\mathsf{\oplus}_\mathsf{E}\) very naturally as \[\infer[\mathsf{\oplus}_\mathsf{E}]{\chi}{\{\phi\oplus\psi\}& \left\{\raisebox{-0.5em}{ \deduce{\chi}{[\phi]} \quad \deduce{\chi}{[\psi]}} \right\}}\] We now give a formal definition of our characterisation of natural deduction for ILL using this new notation. Note that henceforth, the semantic brackets will be used to refer to modal boxes only. An important point to note is that, since this notation is nothing more than formalisation of the presentation of the system presented in Figure 3, the system we now formally define below continues to enjoy the exact same meta-logical properties of the system presented in Figure 3, that is, the system observes the subformula property and is strongly normalising (as shown in [28]); a fact that is a consequence of Theorem 3.

We now match the individual figures of Figure 4 with their rule schemas. :

• \(\mathsf{\multimap}_\mathsf{I}\) is written as \(\langle\{\phi\Rightarrow\psi\},\varnothing,\phi\multimap\psi\rangle\)

• \(\mathsf{\multimap}_\mathsf{E}\) is written as \(\langle\{\Rightarrow\phi\multimap\psi\}\msetsum\{\Rightarrow\phi\},\varnothing,\psi\rangle\)

• \(\mathsf{\otimes}_\mathsf{I}\) is written as \(\langle\{\Rightarrow\phi\}\msetsum\{\Rightarrow\psi\},\varnothing,\phi\otimes\psi\rangle\)

• \(\mathsf{\otimes}_\mathsf{E}\) is written as \(\langle\{\Rightarrow\phi\otimes\psi\}\msetsum\{\phi\msetsum\psi\Rightarrow\chi\},\varnothing,\chi\rangle\)

• \(\mathsf{1}_\mathsf{I}\) is written as \(\langle\varnothing,\varnothing,1\rangle\)

• \(\mathsf{1}_\mathsf{E}\) is written as \(\langle\{\Rightarrow1\}\msetsum\{\Rightarrow\chi\},\varnothing,\chi\rangle\)

• \(\mathsf{\mathbin{\&}}_\mathsf{I}\) is written as \(\langle\{\Rightarrow\phi\msetsum\,\Rightarrow\psi\},\varnothing,\phi\mathbin{\&}\psi\rangle\)

• \(\mathsf{\mathbin{\&}}_\mathsf{E}\) is written as \(\langle\{\Rightarrow\phi\mathbin{\&}\psi\},\varnothing,\phi\rangle\) and \(\langle\{\Rightarrow\phi\mathbin{\&}\psi\},\varnothing,\psi\rangle\)

• Both \(\mathsf{\oplus}_\mathsf{I}\) rules are written as \(\langle\{\Rightarrow\phi\},\varnothing,\phi\oplus\psi\rangle\) and \(\langle\{\Rightarrow\psi\},\varnothing,\phi\oplus\psi\rangle\)

• \(\mathsf{\oplus}_\mathsf{E}\) is written as \(\langle\{\Rightarrow\phi\oplus\psi\}\msetsum\{\phi\Rightarrow\chi\msetsum\psi\Rightarrow\chi\},\varnothing,\chi\rangle\)

• \(\mathsf{\top}_\mathsf{I}\) is written as \(\langle\{\varnothing\},\varnothing,\top\rangle\), for all \(n\geq0\)

• \(\mathsf{0}_\mathsf{E}\) is written as \(\langle\{\varnothing\}\msetsum\{\Rightarrow0\},\varnothing,\chi\rangle\), for all \(n\geq0\)

• \(\mathsf{Prom}\) is written as \(\langle\varnothing,\Rightarrow\phi,\mathop{!}\phi\rangle\)

• \(\mathsf{Der}\) is written as \(\langle\{\Rightarrow\mathop{!}\phi\}\msetsum\{\phi\Rightarrow\psi\},\varnothing,\psi\rangle\)

• \(\mathsf{Wk}\) is written as \(\langle\{\Rightarrow\mathop{!}\phi\}\msetsum\{\Rightarrow\psi\},\varnothing,\psi\rangle\)

• \(\mathsf{Ctr}\) is written as \(\langle\{\Rightarrow\mathop{!}\phi\}\msetsum\{\mathop{!}\phi\msetsum\mathop{!}\phi\Rightarrow\psi\},\varnothing,\psi\rangle\)

We call the set of these rule schemas, \(\mathfrak{N}\).

It is important to note the presence of the empty additive boxes in the rules \(\mathsf{\top}_\mathsf{I}\) and \(\mathsf{0}_\mathsf{E}\), something seemingly completely new and very different from the previous presentation of a natural deduction system for ILL in Definition 3. In the presence of the (App) clause, we observe that these empty additive boxes are nothing more than a formalisation of the requirement that we have in Definition 3, that the conclusion of \(\mathsf{\top}_\mathsf{I}\) and \(\mathsf{0}_\mathsf{E}\) follows from arbitrary many formulae in disjoint contexts. In other words, we see that this means nothing more than having an arbitrary multiset at the hypothesis line, something we have previously discussed as undesirable for our requirements, but something that exists in the literature, as in the case of the natural deduction figures of Negri for these rules in [32]. By having empty additive boxes instead, the rules now express that there are no conditions on what needs to hold for the conclusion of the rule to hold in the presence of an arbitrary multiset of formulae, without specifying the multiset itself. This, in the opinion of the author, is much neater than the presentation of Definition 3 and removes the question of what, in fact, is an instance of the rules \(\mathsf{\top}_\mathsf{I}\) and \(\mathsf{0}_\mathsf{E}\). This also makes abundantly clear an important point: The context in which the conclusion of a rule follows from in ILL is connected to the additive boxes above the hypothesis line in the rule and not the branches themselves. As previously mentioned, it is really important to note that this notion of derivability is still nothing more than what was available before.

Thus, we see that what we have introduced with Figure 4, under the interpretation of Definition 6, is really nothing more than a more rigourous and uniform representation of the rules of \(\rm N_{ILL}\), under the interpretation of Definition 3. The underlying notion of derivability in the two systems remains exactly the same. However, the new notation allows us to write our inference figures in such a way that they are totally abstracted from the derivations in which they will be used, something which will be important in the remainder of this paper. As a result, for the remainder of this paper, when talking of individual inference rules (or rule schemes in the context of \(\rm N_{ILL}\)) we will use our Gentzen-Prawitz tree notation extended with additive and modal boxes as in Figure 4 and stick to using sequent style inference figures to represent actual rule applications and derivations as a whole.

Before moving on, we make clear the point that, henceforth, when we write \(\vdash\), we mean the derivability relation that has hitherto been written as \(\vdash^*\). We do so, as the two notions of derivability discussed in this section are, as a consequence of Theorem 3, equivalent. As a result of this, we choose the new derivability relation to be the “standard” for the rest of the paper, for the reasons mentioned previously but also, as the notion of atomic derivability we will introduce in the next section will be, purposefully, very similar to Definition 6. As mentioned previously, a consequence of this is that completeness will be much easier to prove.

3 Substructural Basic Derivability↩︎

We now begin our discussion of the semantics we will develop in this paper for ILL. We start by introducing the notions of an atomic rule and basic derivability which will form the core of our semantic theory.

We use the notation \(\{P\Rightarrow p, Q\Rightarrow q \}\) to mean the atomic additive box with the two atomic sequents \(P\Rightarrow p\) and \(Q\Rightarrow q\). The length of an atomic additive box is understood to mean the number of elements it contains. We conventionally write this as \(l\), or possibly \(l_{\mathbf{S}}\), if the atomic additive box is called \(\mathbf{S}\).

Atomic rules are meant to be structurally very similar to the rule schemas of natural deduction. We shall sometimes write them graphically in a similar way too, using a tree-like notion to represent the rules. We do so as follows:
Given the atomic rule \(\mathcal{R}=\langle\mathbf{A},\mathbf{S},p\rangle\), where \(\mathbf{A}=\{\{Q^1_1\Rightarrow q^1_1, \dots, Q^1_{l_1}\Rightarrow q^1_{l_1}\},\dots,\{Q^1_1\Rightarrow q^1_1, \dots, Q^n_{l_n} \Rightarrow q^n_{l_n} \}\}\) and \(\mathbf{S} = \{U_1\Rightarrow v_1, \dots, U_m\Rightarrow v_m\}\), then the graphical form of this rule is given as: \[\infer[\mathcal{R}]{p}{\left\{\raisebox{-0.9em}{ \deduce{q^1_1}{[Q^1_1]}\,\dots \, \deduce{q^1_{l_1}}{[Q^1_{l_1}]}} \right\}\raisebox{-0.9em}{\,\dots\,} \left\{\raisebox{-0.9em}{ \deduce{q^n_1}{[Q^n_1]} \,\dots \, \deduce{q^n_{l_n}}{[Q^n_{l_n}]}} \right\} \quad\left\llbracket\raisebox{-0.9em}{\deduce{v_1}{[U_1]}\,\dots\,\deduce{v_m}{[U_m]}}\right\rrbracket}\]

When the base in question is clear, we will simply call such atoms persistent. We see that for an atom to be deemed persistent, the base in question must contain a rule whose shape closely mirrors the promotion rule in \(\mathfrak{N}\). In fact, the following definition shows us that, relative to our notion of derivability in a base, persistent atoms play a role that is very similar to the role played by formulae of the shape \(\mathop{!}\phi\) in the definition of \(\vdash\). This correspondence is important and we will use this fact in the proof of completeness of the semantics in Section 6.

When \(L\vdash_{\!\!\mathscr{B}}p\) holds, we say that \(p\) follows (or is derivable) from \(L\) in base \(\mathscr{B}\). The multiset \(L\) is called the multiset of hypotheses (or sometimes hypothesis multiset) of the derivation. As a result of the similarity between the notion of derivation in a base and that of \(\vdash\), we can, in fact, graphically represent derivations in a base using a sequent-like notation very similar to that shown in Figure 3. This graphical notation proves very useful when considering explicit and long atomic derivations, though we will not be making use of it in this work.

4 Base-extention Semantics↩︎

We are now ready to introduce the support relation, as mentioned in the introduction, the relation at the heart of the semantics we define in this paper .

That the inductive definition of \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\) is well-founded may not be immediately clear. To show this, we define the following notion of the degree of a formula:

• To atoms \(p\), we assign a degree of \(1\).

• To the constants \(\top\), \(1\) and \(0\) assign a degree of \(2\).

• To each formula \(\phi\multimap\psi\), \(\phi\otimes\psi\), \(\phi\mathbin{\&}\psi\) and \(\phi\oplus\psi\), assign the degree the sum of the degrees of \(\phi\) and \(\psi\) plus \(1\).

• To \(\mathop{!}\phi\), assign the degree of \(\phi\) plus \(1\).

For all the definitional clauses in Definition 8 we have that the formula being defined is always of greater degree than any formula in its definition, thus verifying the claim.

An important consequence of this theorem is that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\) makes for a conservative extension of \(L\vdash_{\!\!\mathscr{B}}\) to the whole language of Intuitionistic linear logic (that is, \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }p\) if and only if \(L\vdash_{\!\!\mathscr{B}}p\)). As a result, it should be the case that we retain montonicity in the base, as follows.

The proof follows immediately from Lemma 9 and the inductive clauses of Definition 8. Note however, that the support relation is monotone only with respect to the base, not with respect to the context. For example, we see that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!p }p\) holds in all bases \(\mathscr{B}\), but \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!p\msetsum p } p\) does not necessarily hold in all bases \(\mathscr{B}\). Were it to be the case that the support relation was monotone with respect to the context as well it would result in us having unrestricted weakening and contraction in the context; something which, as we shall see, is undesirable for the semantics we have set up. The fact that that the support relation is monotone with respect to the base, however, is useful and in fact, allows us to give us a simpler characterisation of validity.

Thus, we can justifiably write the valid sequent \((\Gamma:\phi)\) as \(\Gamma\Vdash_{ \!\! }^{ \!\! }\phi\). Before moving on, it is worth nothing that the clause for (\(\mathop{!}\)), can be simplified to \[\begin{align} \Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi&\text{ iff for all bases }\mathscr{C}\supseteq\mathscr{B}\text{, atomic multisets } K \text{ and } p\in\mathbb{A},\\ &\text{ if }\mathop{!}\phi\Vdash_{ \!\!\mathscr{B} }^{ \!\!K }p\text{ then } \Vdash_{ \!\!\mathscr{B} }^{ \!\!L\msetsum K }p \end{align}\] That this holds is an immediate consequence of our (Inf) clause and we make use of this form of the definition for the remainder of this paper. We now make note of three interesting structural properties of \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\), the proofs of which we defer to Appendix 8.

Of more interest to us is the interaction of \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\) with formulae \((\mathop{!})\) as a top-level connective. Let us prove some structural results about these formulae.

The question “Does the deduction theorem hold in modal logics?" has long been a problematic issue in the literature of modal logic [41]. These historical issues seem to be being reflected in our definition of [BeS:ILL:inf], which seems to suggest, somewhat in line with the reasoning of Fagin et al. in [42] for Epistemic Logic and Chagrov and Zakharyaschev [43] for normal modal logics, that modal formulae (that is, for us, formulae of the form \(\mathop{!}\phi\)) need to be treated differently as hypothesis. This is troublesome for the linear logician as there are many formulae which are logically equivalent to a”modal" formula but do not have the \((\mathop{!})\) as a top-level connective. An example of this are the formulae \[\mathop{!}(\phi\mathbin{\&}\psi)and(\mathop{!}\phi)\otimes(\mathop{!}\psi)\] Our desire to treat formulae of the form \(\mathop{!}\phi\) differently as hypothesis comes from the observation that the sequent \[\mathop{!}\phi\Rightarrow\phi\otimes\dots\otimes\phi\] is meant to be valid for any number of \(\phi\)’s in the right-hand side. Thus, it should be the case that for any number of \(\phi\), we have that \[\mathop{!}\phi\Vdash_{ \!\! }^{ \!\! }\phi\otimes\dots\otimes\phi\] However, according to the resource interpretation of this support judgement, a “normal", resourceful, reading of \(\mathop{!}\phi\) on the left-hand side would seemingly lead to a contradiction to the fact that our sequent is valid for any number of \(\phi\) on the right. Spelt out, a”normal" style \((Inf)\) clause would say that \[\begin{align} \mathop{!}\phi\Vdash_{ \!\! }^{ \!\! }\phi\otimes\dots\otimes\phi& iff for all\mathscr{B},atomic multisetsLand atomsp,\\ & if\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi,then\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\phi\otimes\dots\otimes\phi \end{align}\] Since \(L\) must be finite, it seems preposterous that such a judgement would hold for arbitrary many \(\phi\). Nevertheless, this indeed turns out to be the case. In fact, we dedicate the remainder of this section to showing that the “normal" style \((Inf)\) clause is equivalent to our [BeS:ILL:inf] clause. That is, we will prove the following statement: \[\Gamma\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\phi\text{ iff for all }\mathscr{C}\supseteq\mathscr{B}\text{ and atomic multisets }K,\, \Vdash_{ \!\!\mathscr{C} }^{ \!\!K }\Gamma\text{ implies }\Vdash_{ \!\!\mathscr{C} }^{ \!\!L\msetsum K }\phi\]

We call this clause \((Gen-Inf)\), in line with [34]. Thus, the goal for the remainder of this section is to show that [BeS:ILL:gen-inf] indeed holds. An interesting point to note is that, as a result of the soundness and completeness of the semantics, one can view the proof of this statement as a semantic argument for the deduction theorem in ILL. Before continuing, since [BeS:ILL:gen-inf] holds (and thus there is no need for a special [BeS:ILL:inf] clause), it is worth explaining the reasoning behind sticking with such an [BeS:ILL:inf] clause: Firstly, working with such a form of the [BeS:ILL:inf] clause gives us a new way of looking at an aspect of base-extension semantics that has, so far in the literature, never needed to be investigated further. Secondly, and perhaps more pragmatically, it makes the mathematics simpler. Whether making such a choice for simplicity alone is a discussion unto itself, which we shall not be continuing here. In any case, we proceed to show that [BeS:ILL:gen-inf] is indeed equivalent to [BeS:ILL:inf].

This corollary is an immediate consequence of Lemma 10.

Finally, it is worth mentioning the following points related to the multiplicative unit. These are to be expected. We won’t make much use of these results in what follows, except for the second point, as this allows us to prove soundness of the weakening rule, though they are nice sanity checks:

• By expanding the definition of \(1\), one sees that \(\Vdash_{ \!\!\varnothing }^{ \!\!\varnothing }1\) is valid.

• Consequently, it is the case that for any \(\phi\), we have that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\phi\text{ iff } 1\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\phi\). Going right to left, it holds by Lemma 6. Going right to left, it holds immediately since we cut with \(\Vdash_{ \!\!\varnothing }^{ \!\!\varnothing }1\).

• Finally, we have that if \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }1\) and \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!K }1\) hold, then \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L\msetsum K }1\) also holds, again by cut.

We finish this section with following lemma which relates derivations of (\(\mathop{!}\)) to derivations of (\(1\)).

We are now ready to prove the main results of this paper, that this semantics is indeed sound and complete for ILL.

5 Soundness↩︎

6 Completeness↩︎

We now show that, given an arbitrary valid sequent \((\Gamma : \phi)\) in our semantics, there exists a valid \(\rm N_{ILL}\) proof of it. To this end, we will construct a special base, called \(\mathscr{N}\), whose rules will mimic the rules of the natural deduction system \(\rm N_{ILL}\), with basic sentences “simulating” the subformulae of the arbitrary valid sequent. The key step will be to then show that derivations in \(\mathscr{N}\) directly correspond to natural deduction derivations of the formulae being simulated. Thus, we show that \((\Gamma : \phi)\) is provable in \(\rm N_{ILL}\) by, effectively, constructing the proof.

Let us begin by fixing an arbitrary sequent \(\mathfrak{S}=(\Gamma:\phi)\) and let \(\Xi\) be the set of subformulae of the sequent \(\mathfrak{S}\). That is to say, \(\Xi\) is the union of the subformulae of each element of \(\Gamma\) and \(\phi\). We additionally fix an injection \({(\cdot)}^{\flat}:\Xi\rightarrow\mathbb{A}\), called the flattening map, such that:

• It is the identity map on atoms and the units \(\top\), \(0\) and \(1\).

• For non-atomic formulae, \(\phi\), it assigns an atom \(p\) where \(p\notin\Xi\) and for all \(\alpha,\beta\in \Xi\), if \(\alpha\neq\beta\) then \({\alpha}^{\flat}\neq{\beta}^{\flat}\).

Such a map has a left inverse, \({(\cdot)}^{\natural}\) defined similarly as:

• The identity map on the units \(\top\), \(0\) and \(1\) and on atoms not in the image of \({(\cdot)}^{\flat}\).

• The original formula, i.e. \({({(\phi)}^{\flat})}^{\natural} = \phi\).

We further define these functions to be distributing over mulitsets; that is, given multisets \(\Gamma=\{\gamma_1,\dots,\gamma_n\}\) and \(P=\{p_1,\dots,p_n\}\) then \({\Gamma}^{\flat} = \{{\gamma_1}^{\flat},\dots,{\gamma_n}^{\flat}\}\) and \({P}^{\natural} = \{{p_1}^{\natural},\dots,{p_n}^{\natural}\}\). We now define the simulation base \(\mathscr{N}\) relative to \(\Xi\) and \({(\cdot)}^{\flat}\) according to the rules of Figure 6 where \(\phi\) and \(\psi\) range over all elements of \(\Xi\) and \(p\) ranges over all atoms \(\mathbb{A}\).

As a result of our definition of \(\mathscr{N}\), we note that the only persistent atoms of \(\mathscr{N}\) are those atoms \({(\mathop{!}\phi)}^{\flat}\) where \(\mathop{!}\phi\in\Xi\). We now begin by proving completeness, making use of lemmas that we will prove later in this section.

It is important to note that the final rule application works because the multiset \({(\mathop{!}\phi)}^{\flat}\msetsum D\) is still a multiset of persistent atoms. To apply the rule \(\mathcal{R}\), we need, amongst other details, to have a derivation of every element of this multiset as the union of the hypotheses of each derivation forms the context of the conclusion of the rule. Indeed we have that \({(\mathop{!}\phi)}^{\flat}\msetsum K_{m+i}\vdash_{\!\!\mathscr{B}}d_{m+i}\) for all \(i\in[1,n-m]\) but also that by [eq:derive-ref] that \({(\mathop{!}\phi)}^{\flat}\vdash_{\!\!\mathscr{B}}{(\mathop{!}\phi)}^{\flat}\). Thus, the rule application results in \(({(\mathop{!}\phi)}^{\flat})^{n+1}\msetsum K\vdash_{\!\!\mathscr{B}}p\) where the extra \({(\mathop{!}\phi)}^{\flat}\) arises as a result of this extra element of the multiset of persistent atoms.

7 Comments on the semantics↩︎

As mentioned in the introduction, the work herein uses the solid framework set up by Gheorghiu, Gu, and Pym in [31] to help us capture substructurality. However, extending to the additives and including the modality required quite some additional mathematical machinery. Whilst the modification to [BeS:ILL:inf] was previously discussed in Section 4, what is not perhaps clear is the origins of the clause for [BeS:ILL:bang]. A naïve but not incorrect view of the clause is that we simply put things in the right places to obtain an inductive definition that we can “cut" resources on. This argument can be further justified if one makes use of the identities \(\mathop{!}\top \equiv 1\) and \(\mathop{!}(\phi\mathbin{\&}\psi)\equiv(\mathop{!}\phi)\otimes(\mathop{!}\psi)\), where \(\equiv\) represents logical equivalence. Supposing we accept these equivalences and the argument provided in Section 4 for the modified [BeS:ILL:inf] clause, we can derive the clause for (\(\mathop{!}\)) as follows:

1. Start with the fact that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}(\phi\mathbin{\&}\psi)\) iff \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }(\mathop{!}\phi)\otimes(\mathop{!}\psi)\).

2. Let \(\psi = \top\). Thus, we have that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}(\phi\mathbin{\&}\top)\) iff \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }(\mathop{!}\phi)\otimes(\mathop{!}\top)\).

3. Since \(\phi\mathbin{\&}\top \equiv \phi\) and \(\mathop{!}\top \equiv 1\), we therefore have that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}(\phi)\) iff \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }(\mathop{!}\phi)\otimes1\).

4. By [BeS:ILL:mand], the right hand side becomes \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi\) iff for all \(\mathscr{C}\supseteq\mathscr{B}\), atomic multisets \(K\) and atoms \(p\), if \(\phi\msetsum1\Vdash_{ \!\!\mathscr{C} }^{ \!\!K }p\), then \(\Vdash_{ \!\!\mathscr{C} }^{ \!\!L\msetsum K }p\).

5. Since \(\phi\msetsum1\Vdash_{ \!\!\mathscr{X} }^{ \!\!M }\psi\) iff \(\phi\Vdash_{ \!\!\mathscr{X} }^{ \!\!M }\psi\), our equivalence becomes \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi\) iff for all \(\mathscr{C}\supseteq\mathscr{B}\), atomic multisets \(K\) and atoms \(p\), if \(\mathop{!}\phi\Vdash_{ \!\!\mathscr{C} }^{ \!\!K }p\), then \(\Vdash_{ \!\!\mathscr{C} }^{ \!\!L\msetsum K }p\).

6. Finally, by [BeS:ILL:inf], we have that \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi\) iff for all \(\mathscr{C}\supseteq\mathscr{B}\), atomic multisets \(K\) and atoms \(p\), if, for all \(\mathscr{D}\supseteq\mathscr{C}\) such that \(\Vdash_{ \!\!\mathscr{D} }^{ \!\!\varnothing }\mathop{!}\phi\) implies \(\Vdash_{ \!\!\mathscr{D} }^{ \!\!K }p\), then \(\Vdash_{ \!\!\mathscr{C} }^{ \!\!L\msetsum K }p\).

This line of reasoning allows one to correctly deduce a clause for [BeS:ILL:bang] with the right formulaic equivalences, such that the formulae on the right-hand side of the clause are of strictly lower weight than on the left-hand side, as discussed in Section 4. However, doing so seems to suggest that the meaning of [BeS:ILL:bang] comes from the [BeS:ILL:inf] clause, which is at odds with the purpose of the [BeS:ILL:bang] clause. In this case, we observe that Theorem 10 puts this issue to rest, as regardless of whether one uses [BeS:ILL:gen-inf] or [BeS:ILL:inf], we can use the [BeS:ILL:bang] clause without modification. Nevertheless, one might note that the core of the definition of [BeS:ILL:bang] exactly meets the criterion for formulae with [BeS:ILL:bang] as a top-level connective on the left-hand side of a sequent in the [BeS:ILL:inf]; that is, the requirement for an object of the form \(\Vdash_{ \!\!\mathscr{X} }^{ \!\!\varnothing }\phi\). So the question arises, should it not be possible to define [BeS:ILL:bang] as something along the lines of \[\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi\text{ iff } \Vdash_{ \!\!\mathscr{B} }^{ \!\!\varnothing }\phi\text{ and }L = ?\] where \(L=?\) is to mean that the condition on \(L\) is unclear. If one takes \(L=\varnothing\) then such a clause fails to be both sound and complete as the requirement that \(L\) be empty cannot be enforced prima facie. However, the clause [BeS:ILL:bang] can be viewed as a reflection (in a sense related to the works of Hallnäs and Schroeder-Heister [11], [44], [45] and the work of Gheorghiu, Gu and Pym [31]) of the expression above with \(L=\varnothing\).

The connection between the [BeS:ILL:bang] clause and the condition \(L=\varnothing\) is perhaps best understood in the context of the works of Wadler [46] and Pfenning et al. [47], [48] and Dual Intuitionistic Linear Logic of Barber [49] where, following Andreolli [50], we represent sequents

\[\Gamma\Rightarrow\phi\text{ as } \Theta;\Delta\Rightarrow\phi\]

where the \(;\) is meant to represent a separation of “types" of hypotheses. Following Pfenning et al., elements of \(\Theta\) obtain the interpretation that they are in some sense”valid" assumptions, whereas elements of \(\Delta\) are as before. As shown in [47], [48], the elements of \(\Delta\) contain formulae which we can move into \(\Theta\). However, when we do so, we prepend each such formula with a \((\mathop{!})\). Similarly, if we move a formula from \(\Delta\) to \(\Theta\), it must first have a \((\mathop{!})\) as top-level connection and we strip it away when moving it over. If we were to setup a semantic theory along judgements of this form, one would give a clause for [BeS:ILL:bang] along the lines of \[\begin{align} \Vdash_{ \!\!\mathscr{B} }^{{ \!\!G };{ \!\!L }}\mathop{!}\phi& iff for all\mathscr{C}\supseteq\mathscr{B},atomic multisetsKand atomsp,\\ & if\phi;\varnothing\Vdash_{ \!\!\mathscr{C} }^{{ \!\!G };{ \!\!K }}p,then\Vdash_{ \!\!\mathscr{C} }^{{ \!\!G };{ \!\!L,K }}p \end{align}\]

Under the interpretation of Pfenning et al. we see that the real meaning of \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi\) is given by what one can do with it if one assumes \(\phi\) to be valid¹⁰. Returning to the semantics presented in this paper, we see that the interpretation of \(\Vdash_{ \!\!\mathscr{B} }^{ \!\!L }\mathop{!}\phi\) expresses this assumed validity by saying that for all \(\mathscr{C}\supseteq\mathscr{B}\), atomic multisets \(K\) and atoms \(p\), if for all \(\mathscr{D}\supseteq\mathscr{C}\, \Vdash_{ \!\!\mathscr{D} }^{ \!\!\varnothing }\phi\) implies \(\Vdash_{ \!\!\mathscr{D} }^{ \!\!K }p\), then \(\Vdash_{ \!\!\mathscr{C} }^{ \!\!L\msetsum K }p\). The validity of \(\phi\) is perfectly captured by this clause with the expression that we consider all extensions \(\mathscr{D}\) of the base \(\mathscr{C}\) where \(\phi\) is a “theorem" of the base, with modal-like behaviour. This isn’t to say that \(\phi\) is necessarily a theorem of \(\mathscr{C}\) but we consider all extensions where it is. If anything follows from such an assumption, then it is as if we have the assumption that \(\mathop{!}\phi\) is on the left-hand side of the support judgement and thus we indeed can cut on it. Furthermore, as a result of the fact that \(\phi\) is a theorem, we have the requirement of before that the assumption of a \(\mathop{!}\phi\), that is, the assumption that \(\phi\) is a theorem, allows us to deduce as many copies of \(\phi\) as we need, i.e. such formulae are structural in nature. Similarly, a reverse reading shows that indeed we are necessitating if we are to conclude \(\mathop{!}\phi\), i.e. capturing the modal-like behaviour previously mentioned. Thus, it should be understood that this clause really is intrinsically capturing the definition of [BeS:ILL:bang]. Thus, the role of the persistent atoms, as defined in Section 3 should perhaps be clearer. Such atoms are those which may be considered theorems of the base, but more importantly, they are the atoms whose behaviour is modal in nature. This distinction is important because we do not wish to consider all theorems and axioms of the base when working with persistent atoms, only that subset which has modal-like behaviour, which for us means, can be introduced using promotion-like reasoning. This is, of course, necessary for our completeness argument. Note, importantly, that the definition of a persistent atom does not require that the atom is structural in any way. This is perhaps surprising as it says that as far as the semantics is concerned, modal behaviour is still restricted to what it has always been: promotion (or in other words, necessitation).

To conclude, I would like to discuss the prospects for the embedding of the semantics for IPL in our semantics for ILL. We know from [25], [26], [28] that there are many possible translations of formulae from IPL to ILL, called Girard translations. We present a particular one below:

Girard, in [26], says that the crux of the translation is the following: \((\Gamma:\phi)_{\text{IPL}}\) is intuitionistically provable if and only if \((\mathop{!}(\Gamma)^\star:(\phi)^\star)_{\text{ILL}}\) is linearly provable, a relevant proof of which can be found in [28]. This translation ties in to our intuition that structurality in the hypothesis of a sequent is really properly represented by our treatment of (\(\mathop{!}\)) in (Inf). Since we have a sound and complete P-tS for IPL and now a sound and complete P-tS for ILL, we therefore know that we can always map any valid IPL sequent \(\Gamma\Vdash_{ \!\!\varnothing }^{\!\!\mathfrak{S}}\phi\) (using \(\Vdash_{ \!\!\mathscr{X} }^{\!\!\mathfrak{S}}\) for the support relation of Sandqvist’s semantics in [18]) to a valid sequent in ILL of the form \(\mathop{!}(\Gamma)^\star\Vdash_{ \!\!\varnothing }^{ \!\!\varnothing }(\phi)^\star\), and vice-versa. This result is interesting as it gives a way of analysing valid sequents of IPL in the framework we have setup for ILL which is certainly not without its quirks (for example, consider how disjunction maps over!). However, a natural question to ask would be how may one generalise this mapping? What if we were given a formula and base in which inference of the formula is supported i.e. \(\Vdash_{ \!\!\mathscr{B} }^{\!\!\mathfrak{S}}\phi\), and wanted to try and understand it in the linear setting, i.e. to find a multiset \(L\) and a base \((\mathscr{B})^\star\) such that the support relation \(\Vdash_{ \!\!(\mathscr{B})^\star }^{ \!\!L }(\phi)^\star\) now holds? Whilst it is obvious that the formula is mappable directly, we are then stuck with how to obtain \(L\) and \((\mathscr{B})^\star\), as rules and atomic derivability in the two semantics are quite differently behaved. At present, it is not clear to me how this mapping should be done, though I do believe such a mapping between the semantics of Sandqvist and ours for ILL is possible. However, I believe that instead, the correct approach to take if we are committed to this line of investigation, is to define a support relation for IPL that is in some sense much closer to ours for ILL, whose treatment of formulae is closer to our own and whose atomic derivability relation mirrors ours in how it uses rules of the base, and whose base rules may also include the additional structure that ours do. Whilst it can easily be shown that one can have a sound and complete P-tS for IPL which keeps track of atoms in much the same way as ours for ILL does, I have had no luck in finding a way of constructing such a mapping. I thus leave this problem open for further study.

Acknowledgements↩︎

I would like to thank Timo Eckhardt, Alex Gheorghiu, Tao Gu, Victor Nascimento, Elaine Pimentel and David Pym for our many discussions on base-extension semantics. In particular, I would also like to thank Katya Piotrovskaya for finding a bug in a previous version of this manuscript. I would like to further thank the anonymous reviewers for their extensive and incredibly helpful comments on earlier drafts of this manuscript.

References↩︎