Bounded-analytic sequent calculi and embeddings for hypersequent logics

Revantha Ramanayake*, Timo Lang, Agata Ciabattoni

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

2 Citations (Scopus)
55 Downloads (Pure)


A sequent calculus with the subformula property has long been recognised as a highly favourable starting point for the proof theoretic investigation of a logic. However, most logics of interest cannot be presented using a sequent calculus with the subformula property. In response, many formalisms more intricate than the sequent calculus have been formulated. In this work we identify an alternative: retain the sequent calculus but generalise the subformula property to permit specific axiom substitutions and their subformulas. Our investigation leads to a classification of generalised subformula properties and is applied to infinitely many substructural, intermediate, and modal logics (specifically: those with a cut-free hypersequent calculus). We also develop a complementary perspective on the generalised subformula properties in terms of logical embeddings. This yields new complexity upper bounds for contractive-mingle substructural logics and situates isolated results on the so-called simple substitution property within a general theory.
Original languageEnglish
Pages (from-to)635-668
JournalJournal of Symbolic Logic
Issue number2
Publication statusPublished - Jun-2021

Cite this