A sequent calculus methodology for systems of agency based on branching-time frames with agents and choices is proposed, starting with a complete and cut-free system for multi-agent deliberative STIT; the methodology allows a transparent justification of the rules, good structural properties, analyticity, direct completeness and decidability proofs.

The main object of this article is to give two novel proofs of the admissibility of Ackermann’s rule (γ) for the propositional relevant logic R. The results are established as corollaries of cut elimination for systems of tableaux for R. Cut elimination, in turn, is established both nonconstructively (as a corollary of completeness) and constructively (using Gentzen-like methods). The extensibility of the techniques is demonstrated by showing that (γ) is admissible for RQ* (R with constant domain quantifiers). The status of (...) the admissibility of (γ) for RQ* was, to the best of the author’s knowledge, an open problem. Further extensions of these results will be explored in the sequel(s). (shrink)

Conditional logics were originally developed for the purpose of modeling intuitively correct modes of reasoning involving conditional—especially counterfactual—expressions in natural language. While the debate over the logic of conditionals is as old as propositional logic, it was the development of worlds semantics for modal logic in the past century that catalyzed the rapid maturation of the field. Moreover, like modal logic, conditional logic has subsequently found a wide array of uses, from the traditional (e.g. counterfactuals) to the exotic (e.g. conditional (...) obligation). Despite the close connections between conditional and modal logic, both the technical development and philosophical exploitation of the latter has outstripped that of the former, with the result that noticeable lacunae exist in the literature on conditional logic. My dissertation addresses a number of these underdeveloped frontiers, producing new technical insights and philosophical applications. -/- I contribute to the solution of a problem posed by Priest of finding sound and complete labeled tableaux for systems of conditional logic from Lewis' V-family. To develop these tableaux, I draw on previous work on labeled tableaux for modal and conditional logic; errors and shortcomings in recent work on this problem are identified and corrected. While modal logic has by now been thoroughly studied in non-classical contexts, e.g. intuitionistic and relevant logic, the literature on conditional logic is still overwhelmingly classical. Another contribution of my dissertation is a thorough analysis of intuitionistic conditional logic, in which I utilize both algebraic and worlds semantics, and investigate how several novel embedding results might shed light on the philosophical interpretation of both intuitionistic logic and conditional logic extensions thereof. -/- My dissertation examines deontic and connexive conditional logic as well as the underappreciated history of connexive notions in the analysis of conditional obligation. The possibility of interpreting deontic modal logics in such systems (via embedding results) serves as an important theoretical guide. A philosophically motivated proscription on impossible obligations is shown to correspond to, and justify, certain (weak) connexive theses. Finally, I contribute to the intensifying debate over counterpossibles, counterfactuals with impossible antecedents, and take—in contrast to Lewis and Williamson—a non-vacuous line. Thus, in my view, a counterpossible like "If there had been a counterexample to the law of the excluded middle, Brouwer would not have been vindicated" is false, not (vacuously) true, although it has an impossible antecedent. I exploit impossible (non-normal) worlds—originally developed to model non-normal modal logics—to provide non-vacuous semantics for counterpossibles. I buttress the case for non-vacuous semantics by making recourse to both novel technical results and theoretical considerations. (shrink)

This paper develops sequent calculi for several classical modal logics. Utilizing a polymodal translation of the standard modal language, we are able to establish a base system for the minimal classical modal logic E from which we generate extensions in a modular manner. Our systems admit contraction and cut admissibility, and allow a systematic proof-search procedure of formal derivations.

Stone representation theorems are a central ingredient in the metatheory of philosophical logics and are used to establish modal embedding results in a general but indirect and non-constructive way. Their use in logical embeddings will be reviewed and it will be shown how they can be circumvented in favour of direct and constructive arguments through the methods of analytic proof theory, and how the intensional part of the representation results can be recovered from the syntactic proof of those embeddings. Analytic (...) methods will also be used to establish the embedding of subintuitionistic logics into the corresponding modal logics. Finally, proof-theoretic embeddings will be interpreted as a reduction of classes of word problems. (shrink)

That every first-order theory has a coherent conservative extension is regarded by some as obvious, even trivial, and by others as not at all obvious, but instead remarkable and valuable; the result is in any case neither sufficiently well-known nor easily found in the literature. Various approaches to the result are presented and discussed in detail, including one inspired by a problem in the proof theory of intermediate logics that led us to the proof of the present paper. It can (...) be seen as a modification of Skolem’s argument from 1920 for his “Normal Form” theorem. “Geometric” being the infinitary version of “coherent”, it is further shown that every infinitary first-order theory, suitably restricted, has a geometric conservative extension, hence the title. The results are applied to simplify methods used in reasoning in and about modal and intermediate logics. We include also a new algorithm to generate special coherent implications from an axiom, designed to preserve the structure of formulae with relatively little use of normal forms. (shrink)

In this article, I present a semantically natural conservative extension of Urquhart’s positive semilattice logic with a sort of constructive negation. A subscripted sequent calculus is given for this logic and proofs of its soundness and completeness are sketched. It is shown that the logic lacks the finite model property. I discuss certain questions Urquhart has raised concerning the decision problem for the positive semilattice logic in the context of this logic and pose some problems for further research.

This paper extends the investigations into logical properties of the quantified argument calculus (Quarc) by suggesting a series of proper subsystems which, although retaining the entire vocabulary of Quarc, restrict quantification in such a way as to make the result decidable. The proof of decidability is via a procedure that prunes the infinite branches of a derivation tree in what is a syntactic counterpart of semantic filtration. We demonstrate an application of one of these systems by showing that Aristotle’s assertoric (...) syllogistic is embeddable within, thus also providing another method of showing its decidability. (shrink)

We investigate a simple game paradigm for intuitionistic logic, inspired by Wajsberg’s implicit inhabitation algorithm and Beth tableaux. The principal idea is that one player, ∃ros, is trying to construct a proof in normal form while his opponent, ∀phrodite, attempts to build a counter-model. The determinacy of the game implies therefore both completeness and semantic cut-elimination.