For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on ℕ^d (Dickson’s lemma), yielding Ackermann upper bounds via controlled bad-sequence arguments. For hypersequent calculi, that argument lifted the ordering to the powerset, since a hypersequent is a (multi)set of sequents. This induces a jump from Ackermann to hyper-Ackermann complexity in the fast-growing hierarchy, suggesting that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening (FL_ec/FL_ew) inherently entail hyper-Ackermann upper bounds. We show that this intuition does not hold: every extension of FL_ec and FL_ew admitting a cut-free hypersequent calculus has an Ackermann upper bound on provability. To avoid the powerset, we exploit novel dependencies between individual sequents within any hypersequent in backward proof search. The weakening case, in particular, introduces a Karp-Miller-style acceleration, and it improves the upper bound for the fundamental fuzzy logic MTL. Our Ackermann upper bound is optimal for the contraction case (realized by the logic FL_ec).

The logic of bunched implications (BI), introduced by O’Hearn and Pym (1999), has attracted significant attention due to its elegant proof calculus, varied semantics, and close connections to the propositional fragment of separation logic. We show here that provability in BI is undecidable by encoding Wang tilings into its ternary relational semantics. Equivalently, this yields the undecidability of the equational theory of BI-algebras. Our result is much more general, applying to the {∧, ∨, ¬, -*}-fragment of stronger and weaker logics: the negation simply needs to be disjointive, and the multiplicative conjunction need not be commutative (then -* splits into two divisions ⧵, ∕). Consequently, our result covers an interval that includes BI, the non-commutative logic GBI, and Boolean BI (BBI), the latter already known to be undecidable. This result contrasts with a long-standing expectation that BI might be decidable. We also identify the gaps in the publications claiming decidability.

Abstract The first algorithm to transform a proof in Nishimura’s sequent calculus $$\textbf{GKt}$$ GKt for tense logic $$\textbf{Kt}$$ Kt into an analytic proof of the same sequent is presented. In an analytic proof, every rule instance is analytic i.e., each formula in every premise is a subformula of some formula in its conclusion. We call this algorithm analytic restriction to convey that it extends analytic cut-restriction where just the cut-rule instances are made analytic. This distinction is essential in tense logic since cut and modal rules can both cause non-analyticity. Analytic cut-restriction is itself an extension of cut-elimination so our work contributes to a broader program of transforming arbitrary sequent proofs into ones constructed from a designated set of formulas—not necessarily subformulas. As with cut-elimination, the aim is to limit the proof search space and support proof-theoretic and meta-logical investigations.

A well-quasi-ordered (wqo) set generalizes the notion of well-foundedness andis a powerful tool for analyzing the complexity of computational problemsthrough upper bounds on the length of controlled bad sequences, known aslength theorems. The finitary multiset extension of a wqo-set induces anordering on finite multisets over elements of that set, where one multisetprecedes another if there exists an injective mapping between their elementsthat preserves the original ordering. In this work, we refine existing lengththeorems for the finitary multiset extension of Higman’s ordering over finitealphabets, and we establish a matching lower bound. As a corollary, weobtain tighter length bounds for the majoring extension of Higman’s orderingover finite alphabets. We demonstrate the application of our results in thecomplexity analysis of noncommutative hypersequent logics.

Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations into decidability, complexity, disjunction property, interpolation, and more. Unfortunately cut-elimination does not hold for the sequent calculi of most non-classical logics. It is well-known that the key to applications is the subformula property (a typical consequence of cut-elimination) rather than cut-elimination itself. With this in mind, we introduce cut-restriction, a procedure to restrict arbitrary cuts to analytic cuts (when elimination is not possible). The algorithm applies to all sequent calculi satisfying language-independent and simple-to-check conditions, and it is obtained by adapting age-old cut-elimination. Our work encompasses existing results in a uniform way, subsumes Gentzen’s cut-elimination, and establishes new analytic cut properties.

We establish decidability for the infinitely many axiomatic extensions of the commutative Full Lambek logic with weakening FLew (i.e. IMALLW) that have a cut-free hypersequent proof calculus. Specifically: every analytic structural rule extension of HFLew. Decidability for the corresponding extensions of its contraction counterpart FLec was established recently but their computational complexity was left unanswered. In the second part of this paper, we introduce just enough on length functions for well-quasi-orderings and the fast-growing complexity classes to obtain complexity upper bounds for both the weakening and contraction extensions. A specific instance of this result yields the first complexity bound for the prominent fuzzy logic MTL (monoidal t-norm based logic) providing an answer to a longstanding open problem.

Abstract 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.

We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to a derivation in the associated display calculus. A key insight in this converse translation is a canonical representation of display sequents as labeled polytrees. Labeled polytrees, which represent equivalence classes of display sequents modulo display postulates, also shed light on related correspondence results for tense logics.

We establish the decidability of every axiomatic extension of the commutative Full Lambek calculus with contraction FLec that has a cut-free hypersequent calculus. The axioms include familiar properties such as linearity (fuzzy logics) and the substructural versions of bounded width and weak excluded middle. Kripke famously proved the decidability of FLec by combining structural proof theory and combinatorics. This work significantly extends both ingredients: height-preserving admissibility of contraction by internalising a fixed amount of contraction (a Curry's lemma for hypersequent calculi) and an extended Kripke lemma for hypersequents that relies on the componentwise partial order on n-tuples being an ω2-well-quasi-order.

The key to the proof-theoretic study of a logic is a proof calculus with a subformula property. Many different proof formalisms have been introduced (e.g. sequent, nested sequent, labelled sequent formalisms) in order to provide such calculi for the many logics of interest. The nested sequent formalism was recently generalised to indexed nested sequents in order to yield proof calculi with the subformula property for extensions of the modal logic K by (Lemmon-Scott) Geach axioms. The proofs of completeness and cut-elimination therein were semantic and intricate. Here we show that derivations in the labelled sequent formalism whose sequents are `almost treelike' correspond exactly to indexed nested sequents. This correspondence is exploited to induce syntactic proofs for indexed nested sequent calculi making use of the elegant proofs that exist for the labelled sequent calculi. A larger goal of this work is to demonstrate how specialising existing proof-theoretic transformations alleviate the need for independent proofs in each formalism. Such coercion can also be used to induce new cutfree calculi. We employ this to present the first indexed nested sequent calculi for intermediate logics. Comment: This is an extended version of the conference paper [20]

We introduce a new proof-theoretic framework which enhances the expressive power of bunched sequents by extending them with a hypersequent structure. A general cut-elimination theorem that applies to bunched hypersequent calculi satisfying general rule conditions is then proved. We adapt the methods of transforming axioms into rules to provide cutfree bunched hypersequent calculi for a large class of logics extending the distributive commutative Full Lambek calculus DFLe and Bunched Implication logic BI. The methodology is then used to formulate new logics equipped with a cutfree calculus in the vicinity of Boolean BI.

What can (and cannot) be expressed by structural display rules? Given a display calculus, we present a systematic procedure for transforming axioms into structural rules. The conditions for the procedure are given in terms of (purely syntactic) abstract properties of the base calculus; thus, the method applies to large classes of calculi and logics. If the calculus satisfies certain additional properties, we prove the converse direction, thus characterising the class of axioms that can be captured by structural display rules. Determining if an axiom belongs to this class or not is shown to be decidable. Applied to the display calculus for tense logic, we obtain a new proof of Kracht’s Display Theorem I.

The difficulty in finding analytic Gentzen sequent calculi for non-classical logics has lead to the development of many new proof frameworks (proof systems) that have been used to give analytic calculi for these logics. The multitude and diversity of such frameworks has made it increasingly important to identify their interrelationships and relative expressive power. Hypersequent and Display calculi are two widely-used proof frameworks employed to present analytic calculi for large classes of logics. In this article, we show how any hypersequent calculus can be used to construct a display calculus for the same logic. The display calculus we obtain preserves proof-theoretic properties of the original calculus including cut-elimination and the subformula property. Since the construction applies to any hypersequent calculus, this result shows that in terms of presenting logics the display calculus formalism subsumes the hypersequent calculus formalism.