Search

Previous works by Gor\'e, Postniece and Tiu have provided sound and cut-free complete proof systems for modal logics extended with path axioms using the formalism of nested sequent. Our aim is to provide (i) a constructive cut-elimination procedure and (ii) alternative modular formulations for these systems. We present our methodology to achieve these two goals on a subclass of path axioms, namely quasi-transitivity axioms.

We derive an intuitionistic version of G\"odel-L\"ob modal logic ($\sf{GL}$) in the style of Simpson, via proof theoretic techniques. We recover a labelled system, $\sf{\ell IGL}$, by restricting a non-wellfounded labelled system for $\sf{GL}$ to have only one formula on the right. The latter is obtained using techniques from cyclic proof theory, sidestepping the barrier that $\sf{GL}$'s usual frame condition (converse well-foundedness) is not first-order definable. While existing intuitionistic versions of $\sf{GL}$ are typically defined over only the box (and not the diamond), our presentation includes both modalities. Our main result is that $\sf{\ell IGL}$ coincides with a corresponding semantic condition in birelational semantics: the composition of the modal relation and the intuitionistic relation is conversely well-founded. We call the resulting logic $\sf{IGL}$. While the soundness direction is proved using standard ideas, the completeness direction is more complex and necessitates a detour through several intermediate characterisations of $\sf{IGL}$., Comment: 25 pages including 8 pages appendix, 4 figures

Session types are types for specifying the protocols that communicating processes must follow in a concurrent system. When composing two or more well-typed processes, a session typing system must check whether such processes are multiparty compatible, a property that guarantees that all sent messages are eventually received and no deadlock ever occurs. Previous work has shown that duality and the more general notion of coherence are sufficient syntactic conditions for guaranteeing the multiparty compatibility property. In this paper, following a propositions-as-types fashion which relates session types to linear logic, we generalise coherence to forwarders. Forwarders are processes that act as middleware by forwarding messages according to a given protocol. Our main result shows that forwarders not only generalise coherence, but fully capture all well-typed multiparty compatible processes., Comment: arXiv admin note: substantial text overlap with arXiv:2112.07636

In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area., Comment: 13 pages conference paper + 26 pages appendix with examples and proofs

The quest of smoothly combining logics so that connectives from classical and intuitionistic logics can co-exist in peace has been a fascinating topic of research for decades now. In 2015, Dag Prawitz proposed a natural deduction system for an ecumenical first-order logic. We start this work by proposing a {\em pure} sequent calculus version for it, in the sense that connectives are introduced without the use of other connectives. For doing this, we extend sequents with an extra context, the stoup, and define the ecumenical notion of polarities. Finally, we smoothly extend these ideas for handling modalities, presenting pure labeled and nested systems for ecumenical modal logics., Comment: 26 pages

Session types define protocols that processes must follow when communicating. The special case of binary session types, i.e. type annotations of protocols between two parties, is known to be in a propositions-as-types correspondence with linear logic. In previous work, we have shown that the generalization to multiparty session types can be expressed either by coherence proofs or by arbiters, processes that act as middleware by forwarding messages according to the given protocol. In this paper, following the propositions-as-types fashion, we generalize arbiters to a logic, which we call forwarder logic, a fragment of classical linear logic still satisfying cut-elimination. Our main result is summarized as follows: forwarders generalize coherence and give an elegant proof-theoretic characterization of multiparty compatibility, a property of concurrent systems guaranteeing that all sent messages are eventually received and no deadlock ever occurs.

Session types are types for specifying protocols that processes must follow when communicating with each other. Session types are in a propositions-as-types correspondence with linear logic. Previous work has shown that a multiparty session type, a generalisation of session types to protocols of two or more parties, can be modelled as a proof of coherence, a generalisation of linear logic duality. And, protocols expressed as coherence can be simulated by arbiters, processes that act as a middleware by forwarding messages according to the given protocol. In this paper, we generalise the concept of arbiter to that of synchronous forwarder, that is a processes that implements the behaviour of an arbiter in several different ways. In a propositions-as-types fashion, synchronous forwarders form a logic equipped with cut elimination which is a special restriction of classical linear logic. Our main result shows that synchronous forwarders are a characterisation of coherence, i.e., coherence proofs can be transformed into synchronous forwarders and, viceversa, every synchronous forwarder corresponds to a coherence proofs.

The logic of Bunched Implications (BI) freely combines additive and multiplicative connectives, including implications; however, despite its well-studied proof theory, proof-search in BI has always been a difficult problem. The focusing principle is a restriction of the proof-search space that can capture various goal-directed proof-search procedures. In this paper, we show that focused proof-search is complete for BI by first reformulating the traditional bunched sequent calculus using the simpler data-structure of nested sequents, following with a polarised and focused variant that we show is sound and complete via a cut-elimination argument. This establishes an operational semantics for focused proof-search in the logic of Bunched Implications., Comment: 18 pages content

The discussion about how to put together Gentzen's systems for classical and intuitionistic logic in a single unified system is back in fashion. Indeed, recently Prawitz and others have been discussing the so called Ecumenical Systems, where connectives from these logics can co-exist in peace. In Prawitz' system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation, and the constant for the absurd, but they would each have their own existential quantifier, disjunction, and implication, with different meanings. Prawitz' main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. In a recent work, Ecumenical sequent calculi and a nested system were presented, and some very interesting proof theoretical properties of the systems were established. In this work we extend Prawitz' Ecumenical idea to alethic K-modalities.