<p>I know this is a bit late, but perhaps it is still of interest.</p>

<p>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:</p>

<ul>
<li><p>The paper <a href="http://link.springer.com/chapter/10.1007/978-3-642-29822-6_14" rel="nofollow">A Lambda Calculus for Goedel-Dummett Logic Capturing Watifreedom</a> by Yoichi Hirai gives a lambda calculus based on a hypersequent calculus for that logic.</p></li>
<li><p>The paper <a href="http://www.logic.at/staff/agata/librotonino.ps" rel="nofollow">A Natural Deduction System for Intuitionistic Fuzzy Logic</a> 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.</p></li>
</ul>

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

CC BY-SA 3.0
2015-03-12T09:46:32.310Z
Thanks! Hirai's paper is especially interesting to me, since I've been looking at the connections between reactive programming and concurrency.
Neel Krishnaswami
CC BY-SA 3.0
2015-03-13T07:58:24.167Z
No problem. You might also be interested in his [thesis](https://yoichihirai.com/hirai-thesis.pdf), then.
Björn
CC BY-SA 3.0
2015-03-12T07:56:47.350Z
2015-03-12T07:56:47.350Z
Björn
<p>I've been looking at a modal logic with the axiom </p>

<p>$$
(\Diamond A \land \Diamond B) \to \Diamond((A \land \Diamond B) \vee (A \land B) \vee (A \land \Diamond B))
$$</p>

<p>Roughly, this says that the accessibility relation is linear. </p>

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

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

<p>Any pointers?</p>

<lo.logic><pl.programming-languages><proof-theory>
Hypersequents: proof term assigments or translations to hybrid logic
Neel Krishnaswami
# Hypersequents: proof term assigments or translations to hybrid logic

(Asked by: username_0 on 2014-07-11)

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?

**Tags:** lo.logic, pl.programming-languages, proof-theory

---

## 1 answers

### Answer by username_1 on 2015-03-12. Score: 3 | Accepted answer

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](http://link.springer.com/chapter/10.1007/978-3-642-29822-6_14) 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](http://www.logic.at/staff/agata/librotonino.ps) 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.

> **Comments:**
> **username_0**: Thanks! Hirai's paper is especially interesting to me, since I've been looking at the connections between reactive programming and concurrency.  
> **username_1**: No problem. You might also be interested in his [thesis](https://yoichihirai.com/hirai-thesis.pdf), then.  

---

