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).

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.

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.

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

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

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.

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.

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:

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

• for
• for

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 .

• 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