<p>Again I'm not exactly sure what you are looking for because there are potentially many "similar" systems, but for recent work that I think is very related you can read Part II ("Mixing Derivability and Admissibility") of <a href="http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf" rel="nofollow">Dan Licata's thesis</a>, as well as <a href="https://bitbucket.org/robsimmons/constructive-provability-logic/downloads/imla11.pdf" rel="nofollow">Constructive provability logic</a> by Rob Simmons and Bernardo Toninho.</p>

CC BY-SA 2.5
2011-04-02T08:31:40.340Z
2011-04-02T08:31:40.340Z
Noam Zeilberger
<p>Look at the survey of proof calculi for modal logic in chapter 3 of Phiniki Stouppa's MSc thesis <a href="http://www.wv.inf.tu-dresden.de/Publications/Diploma/diplom_stouppa.pdf" rel="nofollow">The Design of Modal Proof Theories:
The case of S5</a>.</p>

<p>IIRC, she discussed how 11 systems handled the formalisation of S5.</p>

CC BY-SA 3.0
2011-04-15T13:03:31.063Z
That looks interesting, but does it add anything new about higher-order sequents that are not already in the literature?
Rob
CC BY-SA 3.0
2011-04-15T15:53:17.893Z
@Rob: No, but it was the broadest survey of proof systems.
Charles Stewart
CC BY-SA 3.0
2011-04-14T07:49:33.433Z
2011-04-14T07:49:33.433Z
Charles Stewart
<p>I can't find the paper online, but guessing based on the references to it, Dosen's system changes the context from a sequence or multiset into a more general graph structure. This is reminiscent of several things. </p>

<ol>
<li><p>Belnap's display logic, in which many connectives (and not just conjunction/disjunction) are internalized into the sequent structure.</p></li>
<li><p>It is also reminiscent of labelled deduction, in which graph structure is simulated by adding labels to hypotheses and judgments, and requiring agreement between the two to discharge a hypothesis. Alex Simpson's PhD thesis investigates applications of these systems to modal logic. </p></li>
<li><p>Noam Zeilberger has investigated interpretations of Buchholz's omega-rule (and generalizations of it) as a literally higher-order rule of inference, in which the premise of a rule becomes a function (ie, a higher-order object) generating the premises. See his POPL 2008 paper "Focusing and Higher-order Abstract Syntax".</p></li>
</ol>

CC BY-SA 2.5
2011-04-01T21:16:47.647Z
I'm aware of display logic, but that's not the same. Dosen's systems are sequents of sequents (ad infinitum, if needed). Nor are hypersequents and labelled deduction "the same". Thanks, though. I'll look for the Zeilberger paper.
Rob
CC BY-SA 2.5
2011-04-02T08:41:09.203Z
@Rob: have you seen Greg Restall's paper, "Comparing Modal Sequent Systems" (http://consequently.org/papers/comparingmodal.pdf)? He explains how to "delabel" labelled deduction into a graph structure on sequents (e.g., as a special case deriving the hypersequent calculus for S5 from its labelled deduction formulation).
Noam Zeilberger
CC BY-SA 2.5
2011-04-02T11:22:16.847Z
I have seen that as well. I wrote a thesis on translating between hypersequents and labelled systems http://hdl.handle.net/10023/1350 - I am looking to extend some of this work to higher-order sequents.
Rob
CC BY-SA 2.5
2011-04-01T13:08:57.023Z
2011-04-01T13:08:57.023Z
Neel Krishnaswami
<p>I am looking for work on systems that are similar to K. Dosen's higher-order sequents ("Sequent Systems for Modal Logic", <em>JSL 50</em>).  The only work that I am aware of is recent work by Iemhoff and Metcalfe ("Proof theory for admissible rules", <em>Annals of Pure and Applied Logic 159</em> (1-2), 2009).</p>

<p>Are there other papers on such systems?</p>

CC BY-SA 2.5
2011-04-01T14:51:42.693Z
what do you mean by "similar", i.e., what sort of properties are you interested in?  I can give you a lot of references to things which are related if you squint hard enough (e.g., ancient work on the $\omega$-rule, and very old work on iterated inductive definitions).
Noam Zeilberger
CC BY-SA 2.5
2011-04-01T20:57:46.810Z
IIRC Greg Kriesel and some of his students and collaborators have worked on related stuff. There is also Girard's work (old stuff: p-tykes, dilators, $\Pi^1_2$-logic, ... check his old book; new stuff: check his recent book, draft of English translation is available on his webpage).
Kaveh
<reference-request><lo.logic><proof-theory>
Looking for papers and articles on higher-order sequent systems
Rob
# Looking for papers and articles on higher-order sequent systems

(Asked by: username_0 on 2011-04-01)

I am looking for work on systems that are similar to K. Dosen's higher-order sequents ("Sequent Systems for Modal Logic", *JSL 50*). The only work that I am aware of is recent work by Iemhoff and Metcalfe ("Proof theory for admissible rules", *Annals of Pure and Applied Logic 159* (1-2), 2009).

Are there other papers on such systems?

**Tags:** reference-request, lo.logic, proof-theory
> **Comments:**
> **username_1**: what do you mean by "similar", i.e., what sort of properties are you interested in?  I can give you a lot of references to things which are related if you squint hard enough (e.g., ancient work on the $\omega$-rule, and very old work on iterated inductive definitions).  
> **username_2**: IIRC Greg Kriesel and some of his students and collaborators have worked on related stuff. There is also Girard's work (old stuff: p-tykes, dilators, $\Pi^1_2$-logic, ... check his old book; new stuff: check his recent book, draft of English translation is available on his webpage).  

---

## 3 answers

### Answer by username_1 on 2011-04-02. Score: 6

Again I'm not exactly sure what you are looking for because there are potentially many "similar" systems, but for recent work that I think is very related you can read Part II ("Mixing Derivability and Admissibility") of [Dan Licata's thesis](http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf), as well as [Constructive provability logic](https://bitbucket.org/robsimmons/constructive-provability-logic/downloads/imla11.pdf) by Rob Simmons and Bernardo Toninho.


---

### Answer by username_3 on 2011-04-14. Score: 5

Look at the survey of proof calculi for modal logic in chapter 3 of Phiniki Stouppa's MSc thesis [The Design of Modal Proof Theories:
The case of S5](http://www.wv.inf.tu-dresden.de/Publications/Diploma/diplom_stouppa.pdf).

IIRC, she discussed how 11 systems handled the formalisation of S5.

> **Comments:**
> **username_0**: That looks interesting, but does it add anything new about higher-order sequents that are not already in the literature?  
> **username_3**: @Rob: No, but it was the broadest survey of proof systems.  

---

### Answer by username_4 on 2011-04-01. Score: 5

I can't find the paper online, but guessing based on the references to it, Dosen's system changes the context from a sequence or multiset into a more general graph structure. This is reminiscent of several things.

1. Belnap's display logic, in which many connectives (and not just conjunction/disjunction) are internalized into the sequent structure.
2. It is also reminiscent of labelled deduction, in which graph structure is simulated by adding labels to hypotheses and judgments, and requiring agreement between the two to discharge a hypothesis. Alex Simpson's PhD thesis investigates applications of these systems to modal logic.
3. Noam Zeilberger has investigated interpretations of Buchholz's omega-rule (and generalizations of it) as a literally higher-order rule of inference, in which the premise of a rule becomes a function (ie, a higher-order object) generating the premises. See his POPL 2008 paper "Focusing and Higher-order Abstract Syntax".

> **Comments:**
> **username_0**: I'm aware of display logic, but that's not the same. Dosen's systems are sequents of sequents (ad infinitum, if needed). Nor are hypersequents and labelled deduction "the same". Thanks, though. I'll look for the Zeilberger paper.  
> **username_1**: @Rob: have you seen Greg Restall's paper, "Comparing Modal Sequent Systems" (http://consequently.org/papers/comparingmodal.pdf)? He explains how to "delabel" labelled deduction into a graph structure on sequents (e.g., as a special case deriving the hypersequent calculus for S5 from its labelled deduction formulation).  
> **username_0**: I have seen that as well. I wrote a thesis on translating between hypersequents and labelled systems http://hdl.handle.net/10023/1350 - I am looking to extend some of this work to higher-order sequents.  

---

