Relational Hypersequent S4 and B are Cut-Free Hypersequent Incomplete
Kai Tanter
TL;DR
This paper demonstrates that certain relational hypersequent logics, including K4, S4, KB, and RB, are incomplete when using cut-free hypersequent calculus, with K4 and S4 also incomplete in sequent and formula forms.
Contribution
It establishes the cut-free hypersequent incompleteness of K4, S4, KB, and RB, highlighting limitations in their proof systems compared to prior assumptions.
Findings
K4 and S4 are cut-free hypersequent incomplete.
K4 and S4 are also cut-free sequent and formula incomplete.
Relational hypersequent logics K4, S4, KB, RB are incomplete without cuts.
Abstract
We show that relational hypersequent K4, S4, KB and RB, investigated in Parisi (2020) and Burns and Zach (2020) are cut-free hypersequent incomplete. In addition, the former two are also cut-free sequent and formula incomplete.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Algebra and Logic · Logic, programming, and type systems