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.

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)

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)

We discuss two-layered logics formalising reasoning with paraconsistent probabilities that combine the Łukasiewicz [0, 1]-valued logic with Baaz ▵\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\triangle $$\end{document} operator and the Belnap–Dunn logic. The first logic (introduced in [7]) formalises a ‘two-valued’ approach where each event ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi $$\end{document} has independent positive and negative measures that stand for, respectively, the likelihoods of ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi (...) $$\end{document} and ¬ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\lnot \phi $$\end{document}. The second logic that we introduce here corresponds to ‘four-valued’ probabilities. There, ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi $$\end{document} is equipped with four measures standing for pure belief, pure disbelief, conflict and uncertainty of an agent in ϕ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\phi $$\end{document}.We construct faithful embeddings of and into one another and axiomatise using a Hilbert-style calculus. We also establish the decidability of both logics and provide complexity evaluations for them using an expansion of the constraint tableaux calculus for. (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)

The notion of a critical successor [5] in relational semantics has been central to most classic modal completeness proofs in interpretability logics. In this paper we shall work with a more general notion, that of an assuring successor. This will enable more concisely formulated completeness proofs, both with respect to ordinary and generalised Veltman semantics. Due to their interesting theoretical properties, we will devote some space to the study of a particular kind of assuring labels, the so‐called full labels and (...) maximal labels. After a general treatment of assuringness, we shall apply it to obtain a completeness result for the modal logic w.r.t. generalised semantics for a restricted class of frames. (shrink)