15
$\begingroup$

I am looking for papers and articles on modal substructural logics-- not on the semantics of linear logic modalities, but on substructural logics augmented with standard modal operators, e.g. substructural K (something like MALL with box operator, necessitation and K rules).

Improve this question
$\endgroup$

5 Answers 5

Reset to default
13
$\begingroup$

I know of work adding temporal modalities to linear logic to produce what has been called temporal linear logic (in contrast to LTL = linear-time temporal logic). This is quite interesting: a formula (without a modality) is interpreted as resources being available now. The next time modality $\bigcirc-$ is interpreted as resources being available in the next time step. The box modality $\Box-$ means that the resources can be consumed at any point in the future, determined by the holder of the resources, whereas $\lozenge-$ means that the resources can be consumed at any point in time determined by the system. Notice the duality between the holder of the resource and the system.

There are a few papers adding all sorts of modalities to linear and affine logic:

The work on temporal linear logic has been applied in agent-oriented programming and coordination, making essential use of the interpretation of the modalities described above:

Improve this answer
$\endgroup$
0
8
$\begingroup$

These kind of logics are considered in linguistics: you can have a look at Michael Moortgat's article, Categorial Type Logic.

Improve this answer
$\endgroup$
8
$\begingroup$

The !A modality of linear logic is a box operator satisfying the S4 axioms.

It's well-known that the uniqueness of !A is not derivable -- that is, if you have a red bang and a blue bang, both of which separately satisfy the rules for bang, you can't prove that they are equivalent. I don't recall offhand where this result can be found, but it's probably in Girard's 1987 paper on linear logic.

EDIT: I asked Jason Reed, whose thesis was about encodings of linear logic into hybrid logic, and he pointed me at the following paper by Chaudhuri and Despeyroux, "A Logic for Constrained Process Calculi with Applications to Molecular Biology". They extend intuitionistic linear logic with hybrid annotations intended to mirror temporal logic, and they did a very clean job of it -- they prove not just have cut-elimination, but also focalization. So it looks like it should be straightforward to simplify their calculus to get modal K a la Simpson.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ I'm looking for something weaker, that corresponds to K rather than S4. $\endgroup$
    – Rob
    Apr 1, 2011 at 10:44
  • 1
    $\begingroup$ @Rob: some weaker modalities for linear logic are studied in light linear logic. I've seen a paper outlining the relationship between three LLLs and standard Kripkean modal logics, but I forget which and whether K was among them. $\endgroup$
    – Charles Stewart
    Apr 14, 2011 at 6:38
  • $\begingroup$ @Charles: do you have the reference for that paper? $\endgroup$
    – Rob
    May 4, 2011 at 8:48
  • 1
    $\begingroup$ @Rob: No, I'm afraid. It occurs to me that it might have been a workshop paper that wasn't written up. There's a paper by Danos & Joinet (2001) that lists some weak linear logics, Linear Logic & Elementary Time, and you might figure out the axiomatics from that: it should follow by looking to see which are the theorems of the form Lp -> Rp, where L&R any any string of modal operators, and see which similar theorems of regular modal logic they match. $\endgroup$
    – Charles Stewart
    May 4, 2011 at 10:29
  • $\begingroup$ @Charles - thanks! I will take a look at it. $\endgroup$
    – Rob
    May 6, 2011 at 18:13
7
$\begingroup$

Currently, the most systematic proof theory that allows many modal logics to be layered upon many substructural logics is Belnap's display logic, which has received a decent treatment at the hands of Marcus Kracht —see in particular his Power and Weakness of the Modal Display Logic, 1996— and Heinrich Wansing, Displaying Modal Logic, 1998.

Display logic has problems handling noncommutative logic, which was one of the motivations behind a couple of MSc theses I supervised some years back, to apply some ideas about representing modalities in the Calculus of Structures, which is very powerful for representing substructural logics, but ran into problems because of the unusual way cut-elimination is proven in that setting. Robert Hein's work on generating rules for modal logics from families of axioms, summarised in Purity through Unravelling, 2005, covers most of the usual logics (the most important axioms not covered are B, CR, and L), and there is fairly strong circumstantial evidence to believe the cut-elimination conjecture. None of this work actually treats substructural logic, but if a stronger kind of cut-elimination theorem were proven for these modalities, the so-called splitting lemma, this would make the logic very modular and cut-elimination should follow easily for all ways of gluing together the logics.

Substructural logic doesn't really have a uniform notion of semantics, but for modal substructural logic we do have a kind of recipe for turning semantics of the base logic into semantics of matching modal logics, by extending a trace-like semantics with a notion of frame or an algebraic/categorical semantics with a notion of operator. Kracht and Wansing do some work in both of these directions.

Improve this answer
$\endgroup$
6
$\begingroup$

I've been skimming Norihiro Kamide, "Kripke Semantics for Modal Substructural Logics", Journal of Logic, Language and Information 11 (4), 2002, which isn't quite what I wanted, but the references cite Marcello D'Agostino and Dov M. Gabbay and Alessandra Russo, "Grafting Modalities onto substructural implication systems", Studia Logica 59, 1996, which seems to be what I am looking for. It is on CiteSeer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.53.5719

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.