arXiv subjects

Revantha Ramanayake

Publications and source records attributed to Revantha Ramanayake.

13 recordsLinked to original sources

arXiv2026

The logic of bunched implications is undecidable

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 {and, or, not, --*}-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.

math.LO↗

arXiv2026

Hypersequent Calculi Have Ackermannian Complexity

For substructural logics with contraction or weakening admitting cut-free sequent calculi, proof search was analyzed using well-quasi-orders on $\mathbb{N}^d$ (Dickson's lemma), yielding Ackermannian 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 Ackermannian to hyper-Ackermannian complexity in the fast-growing hierarchy, suggesting that cut-free hypersequent calculi for extensions of the commutative Full Lambek calculus with contraction or weakening ($\mathbf{FL_{ec}}$/$\mathbf{FL_{ew}}$) inherently entail hyper-Ackermannian upper bounds. We show that this intuition does not hold: every extension of $\mathbf{FL_{ec}}$ and $\mathbf{FL_{ew}}$ admitting a cut-free hypersequent calculus has an Ackermannian 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 $\mathbf{MTL}$. Our Ackermannian upper bound is optimal for the contraction case (realized by the logic $\mathbf{FL_{ec}}$).

cs.LO↗

arXiv2025

Predicative Ordinal Recursion on the Constructive Veblen Hierarchy

Inspired by Leivant's work on absolute predicativism, Bellantoni and Cook in 1992 introduced a structurally restricted form of recursion called predicative recursion. Using this recursion scheme on the inductive structures of natural numbers and binary strings, they provide a structural and machine-independent characterization of the classes of linear-space and polynomial-time computable functions, respectively. This recursion scheme can be applied to any well-founded or inductive structure, and its underlying principle, predicativization, extends naturally to other computational frameworks, such as higher-order functionals and nested recursion. In this paper, we initiate a systematic project to gauge the computational power of predicative recursion on arbitrary well-founded structures. As a natural measuring stick for well-foundedness, we use constructive ordinals. More precisely, for any downset $\mathsf{A}$ of constructive ordinals, we define a class $\mathrm{PredR}_{\mathsf{A}}$ of predicative ordinal recursive functions that are permitted to employ a suitable form of predicative recursion on the ordinals in $\mathsf{A}$. We focus on the case that $\mathsf{A}$ is a downset of constructive ordinals below ${\phi}_{{\omega}}({0}) = \bigcup_{k=0}^{\infty} {\phi}_k({0})$, where $\{{\phi}_k\}_{k=0}^{\infty}$ are the functions in the Veblen hierarchy with finite index. We give a complete classification of $\mathrm{PredR}_{\mathsf{A}}$ -- for those downsets that contain at least one infinite ordinal -- in terms of the Grzegorczyk hierarchy $\{\mathcal{E}_k\}_{k=2}^{\omega}$. In this way, we extend Bellantoni-Cook's characterization of $\mathcal{E}_2$ (the class of linear-space computable functions) to obtain a machine-independent and structural characterization of the entire Grzegorczyk hierarchy.

math.LO↗

arXiv2025

Complexities of Well-Quasi-Ordered Substructural Logics

Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity), and associativity. This leads to a resource-sensitive logical framework that has proven influential beyond mathematical logic and its algebraic semantics, across theoretical computer science, linguistics, and philosophical logic. The set of theorems of a substructural logic is recursively enumerable and, in many cases, recursive. These logics also possess an intricate mathematical structure that has been the subject of research for over six decades. We undertake a comprehensive study of substructural logics possessing an underlying well-quasi-order (wqo), using established ordinal-indexed fast-growing complexity classes to classify the complexity of their deducibility (quasiequational) and provability (equational) problems. This includes substructural logics with weak variants of contraction and weakening, and logics with weak or even no exchange. We further consider infinitely many axiomatic extensions over the base systems. We establish a host of decidability and complexity bounds, many of them tight, by developing new techniques in proof theory, well-quasi-order theory (contributing new length theorems), the algebraic semantics of substructural logics via residuated lattices, algebraic proof theory, and novel encodings of counter machines. Classifying the computational complexity of substructural logics (and the complexity of the word problem and of the equational theory of their algebraic semantics) reveals how subtle variations in their design influence their algorithmic behavior, with the decision problems often reaching Ackermannian or even hyper-Ackermannian complexity.

cs.LO↗

arXiv2025

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof

We show that Propositional Dynamic Logic (PDL) has the Craig Interpolation Property. This question has been open for many years. Three proof attempts were published, but later criticized in the literature or retracted. Our proof is based on the main ideas from Borzechowski (1988, master thesis). We define a cyclic tableau system for PDL with a loading mechanism to recognize successful repeats. For this system, we show soundness and completeness via a game. To show interpolation, we modify Maehara's method to work for tableaux with repeats: we first define pre-interpolants at each node, and then use a quasi-tableau to define interpolants for clusters (strongly connected components). In different terms, our method solves the fixpoint equations that characterize the desired interpolants, and the method ensures that the solutions to these equations can be expressed within PDL. The proof is constructive and we show how to compute interpolants. We also make available a Haskell implementation of the proof system that provides interpolants. Lastly, we mention ongoing work to formally verify this proof in the interactive theorem prover Lean, and several questions for future work.

cs.LO↗

arXiv2024

Deducibility in the full Lambek calculus with weakening is HAck-complete

We prove that the problem of deciding the consequence relation of the full Lambek calculus with weakening is complete for the class HAck of hyper-Ackermannian problems (i.e., level F_ω^ω of the ordinal-indexed hierarchy of fast-growing complexity classes). Provability was already known to be PSPACE-complete. We prove that deducibility is HAck-complete even for the multiplicative fragment. Lower bounds are proved via a novel reduction from reachability in lossy channel systems and the upper bounds are obtained by combining structural proof theory (forward proof search over sequent calculi) and well-quasi-order theory (length theorems for Higman's Lemma).

cs.LO↗

arXiv2023

Internal and External Calculi: Ordering the Jungle without Being Lost in Translations

This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively straightforward while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi.' We discuss the ambiguities involved in the informal definitions of these categories, and we critically assess the properties that (calculi from) these classes are purported to possess.

cs.LO↗

arXiv2023

Cut-restriction: from cuts to analytic cuts

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 including decidability, complexity, disjunction property, and interpolation. 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, and establishes novel analytic subformula properties.

cs.LO↗

arXiv2022

A theory of cut-restriction: first steps

Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-elimination applies to many logics irrespective of their semantics. Such is its influence that whenever cut-elimination is not provable in a sequent calculus the invariable response has been a move to a richer proof system to regain it. In this paper we investigate a radically different approach to the latter: adapting age-old cut-elimination to restrict the shape of the cut-formulas when elimination is not possible. We tackle the "first level" above cut-free: analytic cuts. Our methodology is applied to the sequent calculi for bi-intuitionistic logic and S5 where analytic cuts are already known to be required. This marks the first steps in a theory of cut-restriction.

cs.LO↗

arXiv2021

Display to Labeled Proofs and Back Again for Tense Logics

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.

cs.LO↗

arXiv2021

Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics

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). 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 long-standing open problem.

cs.LO↗

arXiv2018

Inducing syntactic cut-elimination for indexed nested sequents

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.

cs.LO↗

arXiv2016

A syntactic proof of decidability for the logic of bunched implication BI

The logic of bunched implication BI provides a framework for reasoning about resource composition and forms the basis for an assertion language of separation logic which is used to reason about software programs. Propositional BI is obtained by freely combining propositional intuitionistic logic and multiplicative intuitionistic linear logic. It possesses an elegant proof theory: its bunched calculus combines the sequent calculi for these logics. Several natural extensions of BI have been shown as undecidable, e.g. Boolean BI which replaces intuitionistic logic with classical logic. This makes the decidability of BI, proved recently via an intricate semantical argument, particularly noteworthy. However, a syntactic proof of decidability has thus far proved elusive. We obtain such a proof here using a proof-theoretic argument. The proof is technically interesting, accessible as it uses the usual bunched calculus (it does not require any knowledge of the semantics of BI), yields an implementable decision procedure and implies an upper bound on the complexity of the logic.

cs.LO↗