Hypersequents: proof term assigments or translations to hybrid logic

Question

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?

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:

• The paper A Lambda Calculus for Goedel-Dummett Logic Capturing Watifreedom by Yoichi Hirai gives a lambda calculus based on a hypersequent calculus for that logic.

• The paper A Natural Deduction System for Intuitionistic Fuzzy Logic by Matthias Baaz, Agata Ciabattoni and Christian Fermüller gives a natural deduction system for the same logic, which might be used to give proof term assignments.

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.