Abstract Intuitionistic conditional logic, studied by Weiss, Ciardelli and Liu, and Olkhovikov, aims at providing a constructive analysis of conditional reasoning. In this framework, the would and the might conditional operators are no longer interdefinable. The intuitionistic conditional logics considered in the literature are defined by setting Chellas’ conditional logic $$\textsf{CK}$$ CK , whose semantics is defined using selection functions, within the constructive and intuitionistic framework introduced for intuitionistic modal logics. This operation gives rise to a constructive variant of might-free- $$\textsf{CK}$$ CK , which we call "Image missing" , and an intuitionistic variant of $$\textsf{CK}$$ CK , called $$\textsf{IntCK}$$ IntCK . Building on the proof systems defined for $$\textsf{CK}$$ CK and for intuitionistic modal logics, in this paper we introduce a nested calculus for $$\textsf{IntCK}$$ IntCK and a sequent calculus for "Image missing" . Based on the sequent calculus, we define $$\textsf{ConstCK}$$ ConstCK , a conservative extension of Weiss’ logic "Image missing" with the might operator. We introduce a class of models and an axiomatisation for $$\textsf{ConstCK}$$ ConstCK , and extend these result to some extensions of $$\textsf{ConstCK}$$ ConstCK .

Abstract The logic of bringing-it-about (BIAT) aims to capture a notion of agency in which actions are analysed in terms of their results: ‘An agent does something’ means that the agent brings it about that something takes place. Our starting point is the basic BIAT logic as introduced by Elgesem in the ‘90s: this logic contains only a modal operator to express BIAT statements by single agents. Several extensions have been proposed by Elgesem himself and others, notably with the capability operator, coalitions of agents and means-end BIAT statements (i.e. of the form ‘the agent does B by doing A’). We first propose a variant of the neighbourhood semantics, called bi-neighbourhood semantics, for the basic BIAT logic and the mentioned extensions, in which a world is equipped by a set of pairs or neighbourhoods. Differently from the semantics defined in the literature, this reformulation is well suited for countermodel construction. We then introduce modular hypersequent calculi for all logics considered in this work. Our calculi enjoy the fundamental property of cut admissibility, from which it follows their completeness with respect to the axiomatization. Moreover, our calculi provide at the same time a decision procedure, as well as the first practical countermodel extraction procedure: from a single failed proof it is possible to build directly a finite countermodel of the formula under verification in the bi-neighbourhood semantics. By this last result, we obtain constructive proofs of the semantic completeness of the calculi and consequently of the finite model property for all logics.

Abstract We study the complexity of the validity/derivability problem for combinations of non-normal modal logics in the form of logic fusions, possibly extended with simple interaction axioms. We first present cut-free sequent calculi for these logic combinations. Then, we introduce hypersequent calculi with invertible rules, and show that they allow for a coNP proof search procedure. In the last part of the paper, we consider the case of combinations of logics sharing a universal modality. Using the hypersequent calculi, we show that these logics remain coNP-complete, and also provide an equivalent axiomatisation for them.

Abstract We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms ${T}$, ${P}$ and ${D}$ and for every $n \geq 1$, rule ${RD}_n^+$. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.