Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ackermann, W., Untersuchung über das Eliminationsproblem der Mathematischen Logic, Mathematische Annalen 110(1):390–413, 1935.
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.
Avron, A., A constructive analysis of RM, Journal of Symbolic Logic 52(4):939–951, 1987.
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.
Balbes, R., and P. Dwinger, Distributive Lattices, University of Missouri Press, Columbia, 1974.
Balbes, R., and A. Horn, Projective distributive lattices, Pacific Journal of Mathematics 33:273–279, 1970.
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.
Bezhanishvili, G., N. Bezhanishvili, and R. Iemhoff, Stable canonical rules, Journal of Symbolic Logic 81(1):284–315, 2016.
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.
Bezhanishvili, G., N. Bezhanishvili, and J. Ilin, Cofinal stable logics, Studia Logica 104(6):1287–1317, 2016.
Bezhanishvili, G., and R. Jansana, Priestley style duality for distributive meet-semilattices, Studia Logica 98(1-2):83–122, 2011.
Bezhanishvili, N., Lattices of Intermediate and Cylindric Modal Logics, Ph.D. thesis, University of Amsterdam, 2006.
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.
Bezhanishvili, N., N. Galatos, and L. Spada, Canonical formulas for k-potent commutative, integral residuated lattices, Algebra Universalis 77(3):321–343, 2017.
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.
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.
Burris, S., and H. P. Sankappanavar, A Course in Universal Algebra. Graduate Texts in Mathematics, Springer, 1981.
Chagrov, A. V., and M. Zakharyaschev, Modal Logic, volume 35 of Oxford logic guides, Clarendon Press, 1997.
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.
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.
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.
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.
Ciabattoni, A., N. Galatos, and K. Terui, MacNeille completions of FL-algebras, Algebra Universalis 66(4):405–420, 2011.
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.
Ciabattoni, A., N. Galatos, and K. Terui, Algebraic proof theory: Hypersequents and hypercompletions, Annals of Pure and Applied Logic 168(3):693–737, 2017.
Ciabattoni, A., P. Maffezioli, and L. Spendier, Hypersequent and labelled calculi for intermediate logics, in D. Galmiche et al. [32], pp. 81–96.
Ciabattoni, A., and R. Ramanayake, Power and limits of structural display rules, ACM Transactions on Computational Logic 17(3):17, 2016.
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.
Corsi, G., A cut-free calculus for Dummett’s LC quantified, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 35:289–301, 1989.
Dyckhoff, R., and S. Negri, Proof analysis in intermediate logics, Archive for Mathematical Logic 51(1-2):71–92, 2012.
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.
Galmiche, D. et al., (eds.), TABLEAUX 2013, Proceedings, volume 8123 of Lecture Notes in Computer Science, Springer, Berlin, 2013.
Gehrke, M., and J. Harding, Bounded lattice expansions, Journal of Algebra 238:345–371, 2001.
Gehrke, M., J. Harding, and Y. Venema, MacNeille completions and canonical extensions, Transactions of the American Mathematical Society 358(2):573–590, 2006.
Greco, G., M. Ma, A. Palmigiano, A. Tzimoulis, Z. Zhao, Unified correspondence as a proof-theoretic tool, Journal of Logic and Computation. https://doi.org/10.1093/logcom/exw022.
Hodges, W., Model Theory, volume 42 of Encyclopedia of Mathematics and Its Applications, Cambridge University Press, Cambridge, England, 1993.
Horn, A., and N. Kimura, The category of semilattices, Algebra Universalis 1(1):26–38, 1971.
Hosoi, T., Gentzen-type formulation of the propositional logic LQ, Studia Logica 47(1):41–48, 1988.
Iemhoff, R., Uniform interpolation and sequent calculi in modal logic. Submitted. http://www.phil.uu.nl/~iemhoff/papers.html
Iemhoff, R., Uniform interpolation and the existence of sequent calculi. Submitted. http://www.phil.uu.nl/~iemhoff/papers.html
Jeřábek, E., Canonical rules, Journal of Symbolic Logic 74(4):1171–1205, 2009.
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.
Lellmann, B., Hypersequent rules with restricted contexts for propositional modal logics, Theoretical Computer Science 656:76–105, 2016.
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.
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.
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.
Pottinger, G., Uniform, cut-free formulations of T, S4, S5, (abstract), Journal of Symbolic Logic 48:900, 1983.
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.
Simpson, A. K., The Proof Theory and Semantics of Intuitionistic Modal Logic, Ph.D. thesis, University of Edinburgh, 1994.
Sonobe, O., A Gentzen-type formulation of some intermediate logics, Journal of Tsuda College 7:7–14, 1975.
Wronski, A., Intermediate logics and the disjunction property, Reports on Mathematical Logic 1:39–51, 1973.
Zakharyaschev, M., Syntax and semantics of superintuitionistic logics, Algebra and Logic 28(4):262–282, 1989.
Zakharyaschev, M., Canonical formulas for K4, part II: cofinal subframe logics, Journal of Symbolic Logic 61(2):421–449, 1996.
Author information
Authors and Affiliations
Corresponding author
Additional information
Presented by Heinrich Wansing
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), 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.
About this article
Cite this article
Lauridsen, F.M. Intermediate Logics Admitting a Structural Hypersequent Calculus. Stud Logica 107, 247–282 (2019). https://doi.org/10.1007/s11225-018-9791-y
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-018-9791-y