Bounded-analytic sequent calculi and embeddings for hypersequent logics

Revantha Ramanayake*, Timo Lang, Agata Ciabattoni

*Bijbehorende auteur voor dit werk

OnderzoeksoutputAcademicpeer review

21 Downloads (Pure)

Samenvatting

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.
Originele taal-2English
Pagina's (van-tot)635-668
TijdschriftJournal of Symbolic Logic
Volume86
Nummer van het tijdschrift2
DOI's
StatusPublished - jun-2021

Citeer dit