Proof-theoretic methods are developed for subsystems of Johansson’s logic obtained by extending the positive fragment of intuitionistic logic with weak negations. These methods are exploited to establish properties of the logical systems. In particular, cut-free complete sequent calculi are introduced and used to provide a proof of the fact that the systems satisfy the Craig interpolation property. Alternative versions of the calculi are later obtained by means of an appropriate loop-checking history mechanism. Termination of the new calculi is proved, and (...) used to conclude that the considered logical systems are PSPACE-complete. (shrink)

We investigate uniform interpolants in propositional modal logics from the proof-theoretical point of view. Our approach is adopted from Pitts’ proof of uniform interpolationin intuitionistic propositional logic [15]. The method is based on a simulation of certain quantifiers ranging over propositional variables and uses a terminating sequent calculus for which structural rules are admissible.

We introduce the logic LRC, designed to describe and reason about agents’ abilities and capabilities in using resources. The proposed framework bridges two—up to now—mutually independent strands of literature: the one on logics of abilities and capabilities, developed within the theory of agency, and the one on logics of resources, motivated by program semantics. The logic LRC is suitable to describe and reason about key aspects of social behaviour in organizations. We prove a number of properties enjoyed by LRC and (...) its associated analytic calculus. These results lay at the intersection of the algebraic theory of unified correspondence and the theory of multitype calculi in structural proof theory. Case studies are discussed which showcase several ways in which this framework can be extended and enriched while retaining its basic properties, so as to model an array of issues, both practically and theoretically relevant, spanning from planning problems to the logical foundations of the theory of organizations. (shrink)

In this paper, we study IL(), the interpretability logic of . As is neither an essentially reflexive theory nor finitely axiomatizable, the two known arithmetical completeness results do not apply to : IL() is not or . IL() does, of course, contain all the principles known to be part of IL, the interpretability logic of the principles common to all reasonable arithmetical theories. In this paper, we take two arithmetical properties of and see what their consequences in the modal logic (...) IL() are. These properties are reflected in the so-called Beklemishev Principle , and Zambella’s Principle , neither of which is a part of IL. Both principles and their interrelation are submitted to a modal study. In particular, we prove a frame condition for . Moreover, we prove that follows from a restricted form of . Finally, we give an overview of the known relationships of IL() to important other interpretability principles. (shrink)

Relevant propositional dynamic logics have been sporadically discussed in the broader context of modal relevant logics, but have not come up for sustained investigation until recently. In this paper, we develop a philosophical motivation for these systems, and present some new results suggested by the proposed motivation. Among these, we’ll show how to adapt some recent work to show that the extensions of relevant logics by the extensional truth constants \ are complete with respect to a natural class of ternary (...) relation models to show a similar result for the constant-free versions of the logic. In addition, we prove that the logics in question satisfy the variable sharing property, vindicating the claim that they really are relevant logics. (shrink)