-
Complexities of Well-Quasi-Ordered Substructural Logics
Authors:
Nikolaos Galatos,
Vitor Greati,
Revantha Ramanayake,
Gavin St. John
Abstract:
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 philosophic…
▽ More
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.
△ Less
Submitted 30 April, 2025;
originally announced April 2025.
-
Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
Authors:
Manfred Borzechowski,
Malvin Gattinger,
Helle Hvid Hansen,
Revantha Ramanayake,
Valentina Trucco Dalmas,
Yde Venema
Abstract:
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). We define a cyclic tableau system for PDL with a loading mechanism to recognize successful repeats. For this system, w…
▽ More
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). 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.
△ Less
Submitted 17 March, 2025;
originally announced March 2025.
-
Virtue Ethics For Ethically Tunable Robotic Assistants
Authors:
Rajitha Ramanayake,
Vivek Nallur
Abstract:
The common consensus is that robots designed to work alongside or serve humans must adhere to the ethical standards of their operational environment. To achieve this, several methods based on established ethical theories have been suggested. Nonetheless, numerous empirical studies show that the ethical requirements of the real world are very diverse and can change rapidly from region to region. Th…
▽ More
The common consensus is that robots designed to work alongside or serve humans must adhere to the ethical standards of their operational environment. To achieve this, several methods based on established ethical theories have been suggested. Nonetheless, numerous empirical studies show that the ethical requirements of the real world are very diverse and can change rapidly from region to region. This eliminates the idea of a universal robot that can fit into any ethical context. However, creating customised robots for each deployment, using existing techniques is challenging. This paper presents a way to overcome this challenge by introducing a virtue ethics inspired computational method that enables character-based tuning of robots to accommodate the specific ethical needs of an environment. Using a simulated elder-care environment, we illustrate how tuning can be used to change the behaviour of a robot that interacts with an elderly resident in an ambient-assisted environment. Further, we assess the robot's responses by consulting ethicists to identify potential shortcomings.
△ Less
Submitted 23 July, 2024;
originally announced July 2024.
-
Deducibility in the full Lambek calculus with weakening is HAck-complete
Authors:
Vitor Greati,
Revantha Ramanayake
Abstract:
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 bo…
▽ More
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).
△ Less
Submitted 21 June, 2024;
originally announced June 2024.
-
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
Authors:
Tim S. Lyon,
Agata Ciabattoni,
Didier Galmiche,
Marianna Girlando,
Dominique Larchey-Wendling,
Daniel Méry,
Nicola Olivetti,
Revantha Ramanayake
Abstract:
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…
▽ More
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.
△ Less
Submitted 7 May, 2025; v1 submitted 6 December, 2023;
originally announced December 2023.
-
Cut-restriction: from cuts to analytic cuts
Authors:
Agata Ciabattoni,
Timo Lang,
Revantha Ramanayake
Abstract:
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-know…
▽ More
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.
△ Less
Submitted 28 April, 2023; v1 submitted 26 April, 2023;
originally announced April 2023.
-
A theory of cut-restriction: first steps
Authors:
Agata Ciabattoni,
Timo Lang,
Revantha Ramanayake
Abstract:
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 re…
▽ More
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.
△ Less
Submitted 3 March, 2022;
originally announced March 2022.
-
Immune Moral Models? Pro-Social Rule Breaking as a Moral Enhancement Approach for Ethical AI
Authors:
Rajitha Ramanayake,
Philipp Wicke,
Vivek Nallur
Abstract:
We are moving towards a future where Artificial Intelligence (AI) based agents make many decisions on behalf of humans. From healthcare decision making to social media censoring, these agents face problems, and make decisions with ethical and societal implications. Ethical behaviour is a critical characteristic that we would like in a human-centric AI. A common observation in human-centric industr…
▽ More
We are moving towards a future where Artificial Intelligence (AI) based agents make many decisions on behalf of humans. From healthcare decision making to social media censoring, these agents face problems, and make decisions with ethical and societal implications. Ethical behaviour is a critical characteristic that we would like in a human-centric AI. A common observation in human-centric industries, like the service industry and healthcare, is that their professionals tend to break rules, if necessary, for pro-social reasons. This behaviour among humans is defined as pro-social rule breaking. To make AI agents more human centric, we argue that there is a need for a mechanism that helps AI agents identify when to break rules set by their designers. To understand when AI agents need to break rules, we examine the conditions under which humans break rules for pro-social reasons. In this paper, we present a study that introduces a 'vaccination strategy dilemma' to human participants and analyses their responses. In this dilemma, one needs to decide whether they would distribute Covid-19 vaccines only to members of a high-risk group (follow the enforced rule) or, in selected cases, administer the vaccine to a few social influencers (break the rule), which might yield an overall greater benefit to society. The results of the empirical study suggest a relationship between stakeholder utilities and pro-social rule breaking (PSRB), which neither deontological nor utilitarian ethics completely explain. Finally, the paper discusses the design characteristics of an ethical agent capable of PSRB and the future research directions on PSRB in the AI realm. We hope that this will inform the design of future AI agents, and their decision-making behaviour.
△ Less
Submitted 9 May, 2022; v1 submitted 17 June, 2021;
originally announced July 2021.
-
Decidability and Complexity in Weakening and Contraction Hypersequent Substructural Logics
Authors:
A. R. Balasubramanian,
Timo Lang,
Revantha Ramanayake
Abstract:
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…
▽ More
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.
△ Less
Submitted 19 April, 2021;
originally announced April 2021.
-
Display to Labeled Proofs and Back Again for Tense Logics
Authors:
Agata Ciabattoni,
Tim S. Lyon,
Revantha Ramanayake,
Alwen Tiu
Abstract:
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 wi…
▽ More
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.
△ Less
Submitted 6 May, 2021; v1 submitted 6 November, 2019;
originally announced November 2019.
-
Inducing syntactic cut-elimination for indexed nested sequents
Authors:
Revantha Ramanayake
Abstract:
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 sub…
▽ More
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.
△ Less
Submitted 23 November, 2018; v1 submitted 3 March, 2017;
originally announced March 2017.
-
A syntactic proof of decidability for the logic of bunched implication BI
Authors:
Revantha Ramanayake
Abstract:
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 calcu…
▽ More
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.
△ Less
Submitted 2 December, 2016; v1 submitted 19 September, 2016;
originally announced September 2016.
