I've been looking at a modal logic with the axiom

$$ (\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B)) $$

Roughly, this says that the accessibility relation is linear.

It seems like you can give a proof theory for this language using hypersequents (see Andrzej Indrzejczak's Cut-Free Hypersequent Calculus for S4.3), and I was wondering if anyone has investigated giving proof term assignments to hypersequent calculi.

Alternatively, I'd be just as happy if someone had shown how to translate hypersequent calculi into hybrid logics.

Any pointers?


1 Answer 1


I know this is a bit late, but perhaps it is still of interest.

While not exactly the logic you are interested in, Gödel-Dummett logic, the intermediate logic characterised by linear Kripke-frames, is closely related to S4.3, and for this logic people have looked into similar questions:

Also, you might be interested in the paper From Frame Properties to Hypersequent Rules in Modal Logics by Ori Lahav, which includes an alternative hypersequent calculus for S4.3.

  • $\begingroup$ Thanks! Hirai's paper is especially interesting to me, since I've been looking at the connections between reactive programming and concurrency. $\endgroup$ Mar 12, 2015 at 9:46
  • $\begingroup$ No problem. You might also be interested in his thesis, then. $\endgroup$
    – Björn
    Mar 13, 2015 at 7:58

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.