Linear/Non-Linear Contextual Modal Logic

This document is the miniproject for the course Substructural Logics (15-836, https://www.cs.cmu.edu/~fp/courses/15836-f23).

1. Introduction

In logic, we consider hypothetical judgments and usually take them to mean “if every assumption in is true, then is true”. Nanevski et al. [5] introduced ICML, Intuitionistic Contextual Modal Logic. In ICML, is a proposition standing for the hypothetical judgment . So is true when the truth of all assumptions in implies truth of . In this way, ICML internalizes hypothetical truth in any context. Nanevski and coauthors find to be a modal operator validating S4 axioms. Unfortunately, ICML is a structural logic.

In a different development, Girard introduced linear logic [4] in which weakening and contraction are not available. This enables tracking the exact multiset of assumptions (resources) required to prove a statement (make a construction). Linear logic is more general than structural logic: Girard and Lafont [3] showed that intuitionistic structural logic (IL) can be soundly embedded into intuitionistic linear logic (ILL) by means of an ‘of course’ operator that does admit weakeaning and contraction:

In fact, ‘of course’ also satisfies the axioms of an S4 modality.

Andreoli [1] gave a dyadic presentation of ILL, meaning that the basic hypothetical judgment assumes two contexts. It is written (in our presentation) and read as “if the structural assumptions in are valid, and the linear assumptions in are true, then the linear succedent is true”. In this presentation, ‘of course’ can be seen to internalize hypothetical truth with no linear assumptions (a construction that requires no resources):

This brings forward the connection of ILL to ICML: we conjecture that should make sense somehow.

The ‘of course’ point of view treats ILL as prior, and IL as something that embeds into it. Benton [2] proposed an alternative perspective: IL and ILL can be put on equal footing in a combined system of linear/non-linear logic (LNL) that includes two layers of propositions – the structural ones and the linear ones – that interact by means of up- and down-shift modalities . In LNL, .

In this project we investigate how to combine these developments by first making ICML linear and then splitting the modality into a contextual upshift , and a standard downshift in the style of LNL. We conjecture that , similarly to .

The choice to generalize only the upshift, and not the downshift, is motivated by the observation that this seems to suffice to internalize hypothetical judgments with respect to the linear context. However, other phenomena may not be captured. We consider possible extensions in Section 5.

2. Development of the logical calculus

Nanevski and coauthors presented ICML as a system of natural deduction, and an equivalent sequent calculus. They provided an operational interpretation for the former in the form of a type theory. We present only a sequent calculus, which will later be operationalized.

2.1. The right left rule for

We start from Benton’s LNL, presented as in lecture 10. We have two basic judgments and . The shift rules are as follows:

Figure 1: Shift rules

As mentioned earlier, we do not generalize the downshift. So nothing will change in the downshift rules apart from the intended interpretation of the symbols.

The remaining task is to generalize the upshift. The right rule says that to prove , it suffices to prove in an empty linear context. It is clear how to make the linear context arbitrary:

The left rule is not so easy: at least syntactically, there doesn’t seem to be an empty context anywhere that we could generalize.

One way of proceeding is to think of the rule as a sort of cut: we have the structural assumption which means that we are assuming that is provable from no linear assumptions. Now the context is the same as , and the rule is cutting in for . One possible generalization would consequently be to cut in for some context :

Unfortunately this does not admit cut elimination, for essentially the same reason that

does not admit cut elimination in ILL. In ILL with the above as the left rule for , has no cut-free proof because no rule applies. This sequent is, however, provable with cut. The reason is that the input to may not be directly available as an assumption but rather only be provable from a subcontext of . To remedy this, in ILL we must use

Similarly in our system with , where is a propositional atom has no cut-free proof, but is provable with cut. To make the ILL remedy work, we must express somehow that all propositions in the context are provable. We take a page from Nanevski and coauthors and add a judgment where the succedent is a linear context derivable by

This extra gadget allows us to express the correct left rule

2.2. Rules

In summary, the rules of our system are those of LNL extended by a concludes-context judgment derivable by

and with the upshift rules replaced by

We also note some essential properties of and :

is invertible on the right, hence negative.
is invertible on the left, hence positive.

3. Identity and cut elimination

We will show that the following rules of identity and cut are admissible in a version of our system without cut, and with identites restricted to atomic propositions. We will rely on the fact that the system we adapted, LNL, has these properties.

Figure 2: Identity rules

Figure 3: Cut rules

Lemma 3.1 (Identity for contexts).

If is derivable for every , then

is derivable.

Lemma (..) => ..(..) => ..: Identity for contexts

Proof. Let . Then

Theorem 3.2 (Admissibility of Identity). The rules of identity and are admissible in the system where identities are restricted to atomic propositions.

Theorem (..) => ..(..) => ..: Admissibility of Identity

Proof. By simultaneous structural induction on and . The cases except for are the same as in LNL, so need not be re-checked. The new case of follows by since all propositions in are subformulas of .

Lemma 3.3 (Cut for contexts).

If with and any subderivation of as premises is admissible, then

is derivable. Similarly if with and any subderivation of as premises is admissible, then

is derivable. Furthermore if with any subderivation of as the left permise is admissible, then for all

is derivable.

Lemma (..) => ..(..) => ..: Cut for contexts

Proof. (). Let . By inversion on (which was derived by ), there are contexts such that , and are all derivable. Thus

(). Let . By inversion on , there are contexts such that , and are all derivable. Let be the context that contains . We now have

(). Let . By inversion on , there are contexts such that and are all derivable. We now have

⁠

Theorem 3.4 (Admissibility of Cut). The three rules of cut are admissible in the system without cut.

Theorem (..) => ..(..) => ..: Admissibility of Cut

Proof. By simultaneous nested induction on all three forms of cut, first on the cut proposition or , and second on the first and second given derivation. Both LNL without cut and our system without cut have the subformula property. Thus, cut-free proofs of connectives other than cannot refer to . Consequently the cases of cut elimination for these connectives are the same as in the proof for LNL and need not be re-checked.

We only need to check cases with the modified connective. We only consider principal and commuting cases.

The principal case of is

and eliminates to

where , and is

Note that the use of on is justified because all formulas in are subformulas of , and the use of is justified because is a smaller derivation.

The commuting case of with is

This eliminates to

The commuting case of with is

This eliminates to

The commuting case of with is

and eliminates to

Finally, with has two commuting cases depending on which branch uses . The first is

We first do a sub-cut to obtain derivation :

The use of is justified here because is a smaller derivation. Then we can eliminate to

The second is

We first obtain :

And then produce the new proof:

⁠

4. Operational interpretation

We extend the operational interpretation of LNL proofs as message passing programs to our system.

The program terms for LNL rules are as before. A provider of generalized upshift type provides a structural channel that expects to receive the resources and continues by providing a channel of type . In essence, it is like a global MPass function (registered with procproc) that can be called arbitrarily many times, but now existing dynamically as a channel.

Writing for an arbitrary list of terms , our program terms written in send-receive style are:

Figure 4: Upshift program terms

We could alternatively use a syntax closer to the one in MPass by writing:

although the analogy is not exact: e.g. the argument to is a program term that writes into a freshly bound channel rather than necessarily being a variable as in the original syntax.

The dynamic behaviour inspired by the principal case of cut elimination for is:

Insofar as the operation consists of the persistent provider receiving several channels at once, we may need to adjust the message grammar to .

5. Further questions

We chose to generalize to . Alternatively, we could also capture the structural context as in with the right rule

This formulation would more clearly include the structural ICML in its structural fragment; our current version seems to include something like a linear version of ICML in its linear fragment instead.
Can be contextified, too, and how? Does it have anything to do with existential quantification or parametric abstraction?
How does any of this generalize to a full adjoint logic?
Can our additions be reflected in the categorical semantics of LNL [2] without modifying the notion of model? In other words, is the extension conservative?

Bibliography

[1] Jean-Marc Andreoli. 1992. Logic Programming with Focusing Proofs in Linear Logic. Journal Logic and Computation 2, (1992), 297–347. Retrieved from https://api.semanticscholar.org/CorpusID:205204264
[2] P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers (Lecture Notes in Computer Science), 1994. Springer, 121–135. https://doi.org/10.1007/BFB0022251
[3] Jean-Yves Girard and Yves Lafont. 1987. Linear Logic and Lazy Computation. In TAPSOFT'87: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Pisa, Italy, March 23-27, 1987, Volume 2: Advanced Seminar on Foundations of Innovative Software Development II and Colloquium on Functional and Logic Programming and Specifications (CFLP) (Lecture Notes in Computer Science), 1987. Springer, 52–66. https://doi.org/10.1007/BFB0014972
[4] Jean-Yves Girard. 1987. Linear logic. Theoretical Computer Science 50, 1 (1987), 1–101. https://doi.org/10.1016/0304-3975(87)90045-4
[5] Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual modal type theory. ACM Transactions on Computational Logic 9, 3 (2008), 23:1–23:49. https://doi.org/10.1145/1352582.1352591