Studia Logica

, Volume 107, Issue 2, pp 247–282 | Cite as

Intermediate Logics Admitting a Structural Hypersequent Calculus

  • Frederik M. LauridsenEmail author
Open Access


We characterise the intermediate logics which admit a cut-free hypersequent calculus of the form \(\mathbf {HLJ} + \mathscr {R}\), where \(\mathbf {HLJ}\) is the hypersequent counterpart of the sequent calculus \(\mathbf {LJ}\) for propositional intuitionistic logic, and \(\mathscr {R}\) is a set of so-called structural hypersequent rules, i.e., rules not involving any logical connectives. The characterisation of this class of intermediate logics is presented both in terms of the algebraic and the relational semantics for intermediate logics. We discuss various—positive as well as negative—consequences of this characterisation.


Intermediate logics Hypersequent calculi Algebraic proof theory Heyting algebras 


  1. 1.
    Ackermann, W., Untersuchung über das Eliminationsproblem der Mathematischen Logic, Mathematische Annalen 110(1):390–413, 1935.CrossRefGoogle Scholar
  2. 2.
    Avellone, A., M. Ferrari, and P. Miglioli, Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics, Logic Journal of the IGPL 7(4):447–480, 1999.CrossRefGoogle Scholar
  3. 3.
    Avron, A., A constructive analysis of RM, Journal of Symbolic Logic 52(4):939–951, 1987.CrossRefGoogle Scholar
  4. 4.
    Avron, A., The method of hypersequents in the proof theory of propositional non-classical logics, in W. Hodges et al., (eds.), Logic: From Foundations to Applications, Oxford University Press, Oxford, 1996, pp. 1–32.Google Scholar
  5. 5.
    Balbes, R., and P. Dwinger, Distributive Lattices, University of Missouri Press, Columbia, 1974.Google Scholar
  6. 6.
    Balbes, R., and A. Horn, Projective distributive lattices, Pacific Journal of Mathematics 33:273–279, 1970.CrossRefGoogle Scholar
  7. 7.
    Bezhanishvili, G., and N. Bezhanishvili, Locally finite reducts of Heyting algebras and canonical formulas, Notre Dame Journal of Formal Logic 58(1):21–45, 2017.CrossRefGoogle Scholar
  8. 8.
    Bezhanishvili, G., N. Bezhanishvili, and R. Iemhoff, Stable canonical rules, Journal of Symbolic Logic 81(1):284–315, 2016.CrossRefGoogle Scholar
  9. 9.
    Bezhanishvili, G., N. Bezhanishvili, and J. Ilin, Stable modal logics, Review of Symbolic Logic. To appear. Available as ILLC Prepublication Series Report PP-2016-11.Google Scholar
  10. 10.
    Bezhanishvili, G., N. Bezhanishvili, and J. Ilin, Cofinal stable logics, Studia Logica 104(6):1287–1317, 2016.CrossRefGoogle Scholar
  11. 11.
    Bezhanishvili, G., and R. Jansana, Priestley style duality for distributive meet-semilattices, Studia Logica 98(1-2):83–122, 2011.CrossRefGoogle Scholar
  12. 12.
    Bezhanishvili, N., Lattices of Intermediate and Cylindric Modal Logics, Ph.D. thesis, University of Amsterdam, 2006.Google Scholar
  13. 13.
    Bezhanishvili, N., and D. de Jongh, Stable formulas in intuitionistic logic, Notre Dame Journal of Formal Logic. To appear. Available as ILLC Prepublication Series Report PP-2014-19.Google Scholar
  14. 14.
    Bezhanishvili, N., N. Galatos, and L. Spada, Canonical formulas for k-potent commutative, integral residuated lattices, Algebra Universalis 77(3):321–343, 2017.CrossRefGoogle Scholar
  15. 15.
    Bezhanishvili, N., and S. Ghilardi, Multiple-conclusion rules, hypersequents syntax and step frames, in R. Goré et al., (eds.), Advances in Modal Logic 10. College Publications, 2014, pp. 54–73.Google Scholar
  16. 16.
    Bezhanishvili, N., S. Ghilardi, and F. M. Lauridsen, One-step Heyting algebras and hypersequent calculi with the bounded proof property, Journal of Logic and Computation 27(7):2135–2169, 2017.Google Scholar
  17. 17.
    Burris, S., and H. P. Sankappanavar, A Course in Universal Algebra. Graduate Texts in Mathematics, Springer, 1981.CrossRefGoogle Scholar
  18. 18.
    Chagrov, A. V., and M. Zakharyaschev, Modal Logic, volume 35 of Oxford logic guides, Clarendon Press, 1997.Google Scholar
  19. 19.
    Ciabattoni, A., and M. Ferrari, Hypertableau and path-hypertableau calculi for some families of intermediate logics, in R. Dyckhoff, (ed.), TABLEAUX 2000, Proceedings, volume 1847 of Lecture Notes in Computer Science, Springer, 2000, pp. 160–174.Google Scholar
  20. 20.
    Ciabattoni, A., and M. Ferrari, Hypersequent calculi for some intermediate logics with bounded Kripke models, Journal of Logic and Computation 11(2):283–294, 2001.CrossRefGoogle Scholar
  21. 21.
    Ciabattoni, A., D. M. Gabbay, and N. Olivetti, Cut-free proof systems for logics of weak excluded middle, Soft Computing 2(4):147–156, 1998.CrossRefGoogle Scholar
  22. 22.
    Ciabattoni, A., N. Galatos, and K. Terui, From axioms to analytic rules in nonclassical logics, in Proceedings of 23th Annual IEEE Symposium on Logic in Computer Science, LICS 2008, IEEE Computer Society, 2008, pp. 229–240.Google Scholar
  23. 23.
    Ciabattoni, A., N. Galatos, and K. Terui, MacNeille completions of FL-algebras, Algebra Universalis 66(4):405–420, 2011.CrossRefGoogle Scholar
  24. 24.
    Ciabattoni, A., N. Galatos, and K. Terui, Algebraic proof theory for substructural logics: Cut-elimination and completions, Annals of Pure and Applied Logic 163(3):266–290, 2012.CrossRefGoogle Scholar
  25. 25.
    Ciabattoni, A., N. Galatos, and K. Terui, Algebraic proof theory: Hypersequents and hypercompletions, Annals of Pure and Applied Logic 168(3):693–737, 2017.CrossRefGoogle Scholar
  26. 26.
    Ciabattoni, A., P. Maffezioli, and L. Spendier, Hypersequent and labelled calculi for intermediate logics, in D. Galmiche et al. [32], pp. 81–96.Google Scholar
  27. 27.
    Ciabattoni, A., and R. Ramanayake, Power and limits of structural display rules, ACM Transactions on Computational Logic 17(3):17, 2016.CrossRefGoogle Scholar
  28. 28.
    Conradie, W., V. Goranko, and D. Vakarelov, Algorithmic correspondence and completeness in modal logic I. The core algorithm SQEMA, Logical Methods in Computer Science 2(1), 2006.Google Scholar
  29. 29.
    Corsi, G., A cut-free calculus for Dummett’s LC quantified, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 35:289–301, 1989.CrossRefGoogle Scholar
  30. 30.
    Dyckhoff, R., and S. Negri, Proof analysis in intermediate logics, Archive for Mathematical Logic 51(1-2):71–92, 2012.CrossRefGoogle Scholar
  31. 31.
    Galatos, N., P. Jipsen, T. Kowalski, and H. Ono, Residuated Lattices: An Algebraic Glimpse at Substructural Logics, volume 151 of Studies in Logic and the Foundations of Mathematics, Elsevier, Amsterdam, 2007.Google Scholar
  32. 32.
    Galmiche, D. et al., (eds.), TABLEAUX 2013, Proceedings, volume 8123 of Lecture Notes in Computer Science, Springer, Berlin, 2013.Google Scholar
  33. 33.
    Gehrke, M., and J. Harding, Bounded lattice expansions, Journal of Algebra 238:345–371, 2001.CrossRefGoogle Scholar
  34. 34.
    Gehrke, M., J. Harding, and Y. Venema, MacNeille completions and canonical extensions, Transactions of the American Mathematical Society 358(2):573–590, 2006.CrossRefGoogle Scholar
  35. 35.
    Greco, G., M. Ma, A. Palmigiano, A. Tzimoulis, Z. Zhao, Unified correspondence as a proof-theoretic tool, Journal of Logic and Computation.
  36. 36.
    Hodges, W., Model Theory, volume 42 of Encyclopedia of Mathematics and Its Applications, Cambridge University Press, Cambridge, England, 1993.Google Scholar
  37. 37.
    Horn, A., and N. Kimura, The category of semilattices, Algebra Universalis 1(1):26–38, 1971.CrossRefGoogle Scholar
  38. 38.
    Hosoi, T., Gentzen-type formulation of the propositional logic LQ, Studia Logica 47(1):41–48, 1988.CrossRefGoogle Scholar
  39. 39.
    Iemhoff, R., Uniform interpolation and sequent calculi in modal logic. Submitted.
  40. 40.
    Iemhoff, R., Uniform interpolation and the existence of sequent calculi. Submitted.
  41. 41.
    Jeřábek, E., Canonical rules, Journal of Symbolic Logic 74(4):1171–1205, 2009.CrossRefGoogle Scholar
  42. 42.
    Lahav, O., From frame properties to hypersequent rules in modal logics, in Proceedings of 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, IEEE Computer Society, 2013, pp. 408–417.Google Scholar
  43. 43.
    Lellmann, B., Hypersequent rules with restricted contexts for propositional modal logics, Theoretical Computer Science 656:76–105, 2016.CrossRefGoogle Scholar
  44. 44.
    Lellmann, B., and D. Pattinson, Correspondence between modal Hilbert axioms and sequent rules with an application to S5, in D. Galmiche et al. [32], pp. 219–233.Google Scholar
  45. 45.
    Minc, G. E., On some calculi of modal logic, in V. P. Orevkov, (ed.), The Calculi of Symbolic Logic I, volume 98 of Proceedings of the Steklov Institute of Mathematics, AMS, 1971, pp. 97–124.Google Scholar
  46. 46.
    Negri, S., Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem, Archive for Mathematical Logic 42(4):389–401, 2003.CrossRefGoogle Scholar
  47. 47.
    Pottinger, G., Uniform, cut-free formulations of T, S4, S5, (abstract), Journal of Symbolic Logic 48:900, 1983.Google Scholar
  48. 48.
    Rothenberg, R., On the Relationship Between Hypersequent Calculi and Labelled Sequent Calculi for Intermediate Logics with Geometric Kripke Semantics, Ph.D. thesis, University of St Andrews, 2010.Google Scholar
  49. 49.
    Simpson, A. K., The Proof Theory and Semantics of Intuitionistic Modal Logic, Ph.D. thesis, University of Edinburgh, 1994.Google Scholar
  50. 50.
    Sonobe, O., A Gentzen-type formulation of some intermediate logics, Journal of Tsuda College 7:7–14, 1975.Google Scholar
  51. 51.
    Wronski, A., Intermediate logics and the disjunction property, Reports on Mathematical Logic 1:39–51, 1973.Google Scholar
  52. 52.
    Zakharyaschev, M., Syntax and semantics of superintuitionistic logics, Algebra and Logic 28(4):262–282, 1989.CrossRefGoogle Scholar
  53. 53.
    Zakharyaschev, M., Canonical formulas for K4, part II: cofinal subframe logics, Journal of Symbolic Logic 61(2):421–449, 1996.CrossRefGoogle Scholar

Copyright information

© The Author(s) 2018

Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (, which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.

Authors and Affiliations

  1. 1.Institute for Logic, Language and ComputationUniversity of AmsterdamAmsterdamThe Netherlands

Personalised recommendations