# Looking for papers and articles on higher-order sequent systems

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?

• 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 Apr 1 '11 at 14:51
• 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 Apr 1 '11 at 20:57

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, as well as Constructive provability logic by Rob Simmons and Bernardo Toninho.

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".

• 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 Apr 1 '11 at 21:16
• @Rob: have you seen Greg Restall's paper, "Comparing Modal Sequent Systems" (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 Apr 2 '11 at 8:41
• I have seen that as well. I wrote a thesis on translating between hypersequents and labelled systems hdl.handle.net/10023/1350 - I am looking to extend some of this work to higher-order sequents. – Rob Apr 2 '11 at 11:22

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.

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

• That looks interesting, but does it add anything new about higher-order sequents that are not already in the literature? – Rob Apr 15 '11 at 13:03
• @Rob: No, but it was the broadest survey of proof systems. – Charles Stewart Apr 15 '11 at 15:53